Faster Lin check for pure operations

[art-w]

This is just a suggestion, feel free to discard! (... especially since it changes the public API)

I think the sequential consistency check can be a tiny bit faster if the user specifies which operations are side-effect free (because then it doesn't need to replay everything when these functions fail to produce the expected result) ... But then there's a risk that a user could misuse the pure annotation!

Some very arbitrary benchmarks (I didn't find an existing test that performs worse with the ~pure:true annotations, most are already very fast):

• Queue before/after:

  src/queue $ dune exec -- ./lin_tests.exe --seed 0 -v
  
  generated error fail pass / total     time test name
  [✓] 1000    0    0 1000 / 1000     4.1s Lin Queue test with Domain and mutex
  [✓] 1000    0    0 1000 / 1000     8.0s Lin Queue test with Thread and mutex
  [✓]    1    0    1    0 / 1000     2.1s Lin Queue test with Domain without mutex
  [✓] 1000    0    0 1000 / 1000     6.9s Lin Queue test with Thread without mutex
  
  [✓] 1000    0    0 1000 / 1000     3.6s Lin Queue test with Domain and mutex
  [✓] 1000    0    0 1000 / 1000     6.0s Lin Queue test with Thread and mutex
  [✓]    1    0    1    0 / 1000     2.1s Lin Queue test with Domain without mutex
  [✓] 1000    0    0 1000 / 1000     5.9s Lin Queue test with Thread without mutex
  

• I didn't expect Lazy to benefit as much, since only is_val is pure:

  src/lazy $ dune exec -- ./lin_tests_dsl.exe --seed 0 -v
  
  generated error fail pass / total     time test name
  [✓]   39    0    1   38 /  100   157.7s Lin DSL Lazy test with Domain
  [✓]  100    0    0  100 /  100     0.3s Lin DSL Lazy test with Domain from_val
  [✓]   39    0    1   38 /  100   136.6s Lin DSL Lazy test with Domain from_fun
  
  [✓]   39    0    1   38 /  100    95.6s Lin DSL Lazy test with Domain
  [✓]  100    0    0  100 /  100     0.3s Lin DSL Lazy test with Domain from_val
  [✓]   39    0    1   38 /  100    96.1s Lin DSL Lazy test with Domain from_fun
  

(The tests produce the same counter-examples as before)

[jmid]

Sorry for the slowness on this one! :pray: I realized you had some nice renaming and so ripped out the first commit and created #292 from it for a start.

I follow you completely on getting this to run faster! It reminds me of an optimization from the original QuickCheck race-condition paper:

This is a greedy algorithm: as soon as a postcondition fails, then we can discard all potential sequentializations with the failing command as the next one in the sequence. This happens often enough to make the search reasonably fast in practice. As a further optimization, we memoize the search function on the remaining parallel branches and the test case state. This is useful, for example, when searching for a sequentialization of [A, B] and [C, D], if both [A, C] and [C, A] are possible prefixes, and they lead to the same test state—for then we need only try to sequentialize [B] and [D] once. We memoize the non-interference test in a similar way, and these optimizations give an appreciable, though not dramatic, speed-up in our experiments—of about 20%. With these optimizations, generating and running parallel tests is acceptably fast.

This is for a model-based framework like STM, meaning we have an oracle to decide "lead to the same test state" for us instead of the ~pure:true annotation.

As much as I appreciate the contribution, I'm hesitant to include it ATM:

• It requires more user input and so goes a bit against the "provide minimal module signatures" philosophy of Lin (potentially a user could annotate wrong and mess further up)
• It makes changes to the central sequential-consistency search which is non-trivial (I confess that I messed up in it more than once myself)
• We are still exploring what works well and less well for these kinds of tests, so I'm concerned whether this is ... a premature optimization :grimacing:

[art-w]

Yes no worries, I understand that this goes against the grain now! But it was a lot of fun playing with the sequential consistency search ^^

[jmid]

I'll close this for now. A part of the PR was merged in the form of #292. Thanks again!