search

ocaml-multicore / saturn

Lock-free data structures for multicore OCaml
ISC License
184 stars 28 forks source link

Document that Saturn_lockfree.Queue.{snapshot + next} are not linearizable #132

Open edwintorok opened 2 months ago

edwintorok commented 2 months ago

The documentation doesn't say what the semantics of Saturn_lockfree.Queue.cursor is, but the word "snapshot" might mean that it doesn't change when the underlying queue changes.

But that is not true, if I implement a snapshot_as_list function based on snapshot and next the resulting list may observe a list of values that can never be produced by sequential interleaving:

 let snapshot_as_list t = t |> F.snapshot |> Seq.unfold F.next |> List.of_seq

  let api =
    [ val_ "is_empty" F.is_empty (t @-> returning bool)
    ; val_ "push" F.push (t @-> int @-> returning unit)
    ; val_ "pop_opt" F.pop_opt (t @-> returning @@ option int)
    ; val_ "snapshot_as_list" snapshot_as_list (t @-> returning @@ list int) ]
end

Found by qcheck-lin:

Messages for test Lin FIFO tests:

  Results incompatible with sequential execution

                                     |                     
                               push t 0 : ()               
                                     |                     
                  .------------------------------------.
                  |                                    |                     
     snapshot_as_list t : [0; 7]             pop_opt t : Some (0)            
                                                 push t 7 : ()

Here we should observe either:

The observed [0; 7] cannot be produced by this sequence of operations, because 0 is always removed before 7 is added.

I think this should at least be documented as a warning, snapshot can still be useful for debugging (the snapshot will not match the contents of the queue, but should match the order in which elements are pop-ed)

polytypic commented 2 months ago

Yeah... I didn't write original implementation, but I also think that the word "snapshot" is potentially misleading. I might call it "a tap", i.e. you can tap into the queue at a point in time and start pulling elements after that point. Personally I would actually suggest removing the "snapshot" mechanism. My optimized version (#122) drops it, because it cannot be implemented nicely (because to avoid space leaks you destructively clear elements at the front of the queue). There are also other queue designs that can implement a proper snapshot and can also be faster on modern CPUs like the 2-stack queue in #112. The PR doesn't implement it, but it is fairly easy to extend it with a linearizable snapshot operation, i.e. val to_seq : 'a t -> 'a Seq.t.