Acquire-Release Experiment Checking

[Baltoli]

This issue tracks the status of the model checking algorithm with respect to the examples developed to demonstrate the acq_rel automaton.

• [x] basic : correctly identified as safe
• [x] basic_indirect : correctly identified as safe
• [x] more_usage : correctly identified as unsafe
• [x] mult_acq : correctly identified as unsafe
• [x] mult_rel : correctly identified as unsafe
• [x] no_acq_rel : correctly identified as unsafe
• [x] no_acq : correctly identified as unsafe
• [x] no_rel : correctly identified as unsafe
• [x] one_acq : correctly identified as unsafe
• [x] other : correctly identified as unsafe
• [x] rel_before_indirect: correctly identified as unsafe
• [x] rel_before : correctly identified as unsafe
• [ ] address: incorrectly identified as safe, but this is down to mem2reg being cleverer than me and removing the store / load.
• [x] wrong: correctly identified as unsafe

[Baltoli]

When all of these examples are properly checked by the model checking tool, it will be at least as powerful as the specialised checking developed in the initial phase.

It will also be important to track regressions in these examples, as they serve as useful litmus tests for the correctness of the algorithm.

[Baltoli]

Currently I think all the failing examples are caused by incorrect analysis of the branching from lock_acquire, and should be fixed by introducing some kind of constraint system.

[Baltoli]

Updating to the generative model checking algorithm fixes rel_before_indirect. The extension to return constraints remains the fix for mult_acq and one_acq.

[Baltoli]

Updating to include the return value constraint mechanism. This no longer exhibits such catastrophic exponential behaviour, and allows every test case to be checked correctly.

[Baltoli]

These are still passing after introducing parallelism and early exit to the checker.