search

ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
38 stars 10 forks source link

[QCheck-STM] Make `Ortac/QCheck-STM` generate tests in parallel #274

Open n-osborne opened 1 day ago

n-osborne commented 1 day ago

The QCheck-STM test framework allows to test a library in parallel, using domains. This is simply done by instantiating another functor (STM_domain.Make instead of STM_sequential.Make).

The problem is that Ortac/QCheck-STM is directly using STM.Internal.Make. The reason why is that it needs to define its own check_disagree function to be able to build the failure message introduced in version 0.2.0

In order to make Ortac/QCheck-STM be able to generate parallel tests, we need to implement our custom Make_domain in ortac_runtime_qcheck_stm.ml. This should be done in two steps:

  1. Make it work, meaning we can generate parallel tests.
  2. Make is display a useful failure message, mostly meaning build the display of the parallel program as the other elements shouldn't change.
jmid commented 1 day ago

I fear that there can also be complications arising from uncoordinated access to the stack of suts from parallel domains, making this issue slightly more thorny... :grimacing:

n-osborne commented 19 hours ago

Thanks for pointing that out! That's very true!

This would be part of the first step. I believe that moving from a stack of SUTs to a list of SUTs (like it is done for the models) is a possible way to avoid this kind of problems. As we already have an implementation for the models, I'm inclined to keep the good-first-issue tag. It is a bit more work than I first thought.