Write skew in Michael-Scott

[bartoszmodelski]

Michael-Scott Queue has a bug, which makes it perform unserialized accesses. See #41 for details. The current implementation is a fairly simple adaptation a structure using normal atomic accesses and it seems to assume stronger guarantees than Reagents provide. For example:

  let try_pop q =
    Ref.upd q.head (fun s () ->
        match s with
        | Nil -> failwith "MSQueue.try_pop: impossible"
        | Next (_, x) as n -> (
            match Ref.read_imm x with
            | Next (v, _) as n -> Some (n, Some v)
            | Nil -> Some (n, None)))

In the PR above, two reagents observe x of two different queues and insert items only if x is empty. Since the read on x is immediate and thus not part of a transaction, may observe empty queues and insert elements simultaneously.

Two fixes are required. The first one in #42, since the queue is a nested data structure. The second one may look as follows:

  let try_pop (q : 'a t) =
    let hd_val = Ref.read_imm q.head in
    match hd_val with
    | Nil -> assert false
    | Next (_, x) -> (
        Ref.read x >>= function
        | Nil -> constant None
        | Next (v, _) as next ->
            attempt (Ref.cas ~never_block:true q.head hd_val next >>> constant v)
        )

This ensures that the read on ‘x’ is part of the reagent.

But we should take a closer look at other functions as well, and perhaps what's best way to serialize above accesses from performance perspective.