Test of write skew with the Michael-Scott queue

[polytypic]

This PR adds a test of write skew with the Michael-Scott queue.

The test runs composed reagents in parallel:

1. One reagent tries to pop from q1 and push to q2 if q1 was empty.
2. One reagent tries to pop from q2 and push to q1 if q2 was empty.
3. One reagent tries to pop both q1 and q2. If both were non-empty it indicates write skew.

The reason for the write skew is that the try_pop operation of the Michael-Scott queue performs an "invisible" read when it determines the queue to be empty. An invisible read is performed immediately and is not part of the shared memory accesses that are performed atomically together in a composed reagent. This allows two reagents to simultaneusly find queues to be empty and to push to the other queues. This means that the composed reagents are not strictly serializable (i.e. both linearizable and serializable).

[bartoszmodelski]

Thank you for highlighting this and contributing a test.

Indeed, both of the writes should never succeed. I had a stab at fixing this and the diagnosis here is correct + another bug lurking in the implementation of ref. I'll fix the ref bug since the patch is trivial. Michael-Scott is going to take a bit more thought because I suspect that we may still be able (or even be required to) perform an invisible read. Just in the right way.

Futhermore, it seems, based on the bugs I found here before, that this implementation is a 1-1 mirror of a structure using ordinary atomic operations. We might want to give it a better look this time. I'll open an issue and post my code there.

In the meantime, we can just merge this test to ensure its maintained.

• I've changed the runner to one that does not mask deadlocks, since we don't expect any here.
• I've changed the test to expect the erroneous case.
• Bumped ocamlformat.

[polytypic]

I noticed that the CI was failing and created a quick PR #44 to upgrade Reagents to be kcas 0.4.0 compatible.

[polytypic]

I rebased this against main so that CI will be able to build it.