Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extra-job invariant user job fails on first run after PV reboot. #212

Closed
cortlandstarrett opened this issue May 20, 2024 · 1 comment
Closed

Extra-job invariant user job fails on first run after PV reboot. #212

cortlandstarrett opened this issue May 20, 2024 · 1 comment

Comments

@cortlandstarrett
Copy link
Member

5.4 Timing Window?
I found a potential bug that is revealed with the development build. The scenario is as follows:

Use plus2json to produce job definitions for

AAExtraJobInvariantSourceJob.puml

ExtraJobInvariantUserJob1.puml

Launch Protocol Verifier.

Use plus2json to play AAExtraJobInvariantSourceJob.puml.

This will cause an extra-job invariant to be persisted.

Bring down the Protocol Verifier.

Re-launch the Protocol Verifier.

Use plus2json to play ExtraJobInvariantUserJob1.puml.

I observe that this job fails. If I play the same job again, it succeeds.

In the relaunch of Protocol Verifier, I observe that IStore loads the persisted invariants immediately and sends them (it) to Sequence Verification. However, Sequence Verification has not (even) loaded job definitions, yet. So it does not recognise the invariants, because it has no invariants defined in the instance population (yet).

This scenario is run with eji_reboot.sh.

I have not attempted to reproduce this in the multi-process (Kafka) space, yet.
cortlandstarrett added a commit that referenced this issue May 20, 2024
@cortlandstarrett
job: #212 fix race condition
447297e 
SVDC requests restoration of an invariant from IStore.  IStore responds
immediately and gets an event queued to SVDC ahead of the event that is
to put SVDC into the wait state (waiting on Persistence).
The solution initially proposed here it to use an accelerated event to self
in place of the polymorphic event.
An alternative is to add a transition between Assessing and Reassessing.
cortlandstarrett added a commit that referenced this issue May 20, 2024
@cortlandstarrett
job: #212 stop adding all invariants
5606e52 
IStore was proactively reporting all invariants to SVDC.  This is
not necessary and turns out to sometimes fail (SVDC not ready for them).
With multiple workers working on different jobs, with different invariants,
it will be better to report on the invariants requested (one by one) by SVDC.
cortlandstarrett added a commit that referenced this issue May 21, 2024
@cortlandstarrett
job: #212 performance statistics
1b141a4
@cortlandstarrett
Copy link
Member Author

#216

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@cortlandstarrett