Closed jmid closed 1 year ago
I grew increasingly unhappy with the short-comings the initial version, and therefore set out to write an STM
test addressing some of them in ef4b42d.
The resulting STM
test
Domain
(to avoid Domain.DLS
polution across repetitions) andI also adjusted the Util.repeat
and retries
parameters as a lot repetition didn't seem necessary to trigger it, and since I needed to write out the properties anyway to run the test properties in a child Domain
.
This results in a negative test, that is quickly able to produce a counterexample where simultanious changes in two children are not seen in the sibling:
Results incompatible with linearized model
|
|
.------------------------------------.
| |
Set (2, 1) : () Set (0, 43) : ()
Get 0 : 0 Get 2 : 2
A round of focused tests confirmed that the STM Domain.DLS
test runs fast and works reasonable well.
I've therefore disabled the initial Lin
test.
I expect this full CI run to fail its trunk
workflows without #12545 merged into ocaml/ocaml.
CI summary
opam install qcheck-core
which has been reported and fixed upstreamthreadomain
#203 Out of 59 workflows and 19 failures, the 2 non-trunk
failures were thus genuine.
I'll merge.
This PR adds a quick Lin stress test of
Domain.DLS
.It uses only one
DLS.key
for a start - not impressive but it is a start. We might revisit it based onmultiple-ts
or consider replacing it by anSTM
test later.Without the optional
~split_from_parent
the child domain does not inherit the key, which makes for a fast negative test. I did notice that the test takes longer and longer as it progresses, which may be due to the inability to removeDSL.key
s again. For this reason, it seems faster to run the negative test first... We might consider (a) running the property/test in child domain or (b) splitting the two tests to run in separate processes.