search

GaloisInc / pate

Patches Assured up to Trace Equivalence
Other
15 stars 3 forks source link

Nondeterministic startup behavior #438

Closed danmatichuk closed 2 months ago

danmatichuk commented 2 months ago

The startup behavior of the verifier has been observed to be somewhat nondeterministic, occasionally breaking the expected interaction loop with the GUI front end. Likely the issue is related to the initial bootstrapping phase when the GHCI REPL is converted into the pate TTY interface.

The easiest solution would be to add an additional flag to the verifier that tells it to wait for an explicit request from the user before starting up the main thread. The GUI can then just make this request and show an error if the TTY doesn't respond to the startup request (or possibly retry after some delay).

jim-carciofini commented 2 months ago

Does this only happen from the GUI? I am pretty sure I have seen it with the command line as well. But it is intermittent enough that I cannot be sure. Maybe try the docker image from the common line?

danmatichuk commented 2 months ago

I think occasionally there is odd behavior on the command line, but it's less catastrophic. I've tried running this through docker directly and it's been 100% consistent so far.

danmatichuk commented 2 months ago

I made an attempt at a fix in #439, which is now merged into master. With this fix in place I haven't seen any inconsistent behavior in the startup of the verifier, either natively or via docker. I'll close the issue for now, but it would benefit from some testing on different hardware configurations.