From 86d00e48e6875d7fa3a7a1ac81ca6548e877a128 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Wed, 8 Feb 2023 01:52:10 +0200
Subject: [PATCH] Fix bug to handle non-linearizable cases with `cas r x x`
 correctly

It turns out @bartoszmodelski was absolutely right in questioning whether one of
the "optimizations" in my GKMZ adaptation might break linearization:

  https://github.com/ocaml-multicore/kcas/pull/20#discussion_r1066113300

My reasoning at the time was simply wrong.

Consider performing these two k-CAS operations in parallel:

    [ Kcas.mk_cas a 0 0; Kcas.mk_cas b 0 1 ]
    [ Kcas.mk_cas a 0 1; Kcas.mk_cas b 0 0 ]

The "optimization" I had implemented allows both of those to succeed resulting
in the invalid state `a=1 and b=1`.  The correct behaviour is that only one may
succeed and the other must fail.

The intention of the optimization was to check if the (current) `state` had
already been determined without reading the `casn` descriptor.  Unfortunately
that breaks when `state.before == state.after` initially and the `casn` is still
undetermined, because it then allows two conflicting k-CAS operations to succeed
simultaneously.

The proposed fix does a similar optimization, postponing the access of `casn`,
but correctly.  The crucial difference is that the correct optimization requires
that the previous k-CAS has actually completed.

A couple of other places in the code have similar optimizations.  However, in
those other cases this problem cannot occur: `cas` only updates a single
location (so it can always be considered to happen after any potentially
undetermined k-CAS with `state.before == state.after`) and `get` does not update
any locations.
---
 CHANGES.md   |  4 ++++
 src/kcas.ml  | 17 +++++++++--------
 test/test.ml | 34 ++++++++++++++++++++++++++++++++++
 3 files changed, 47 insertions(+), 8 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 89d1cdff..0a0ecb18 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,6 +2,10 @@
 
 All notable changes to this project will be documented in this file.
 
+## 0.1.8
+
+* Fix a bug in GKMZ implementation (@polytypic, review: @bartoszmodelski)
+
 ## 0.1.7
 
 * Change to use the new GKMZ algorithm (@polytypic, review: @bartoszmodelski)
diff --git a/src/kcas.ml b/src/kcas.ml
index 2137b4e1..d4a8a79d 100644
--- a/src/kcas.ml
+++ b/src/kcas.ml
@@ -70,21 +70,22 @@ let finish casn (`Undetermined cass as undetermined)
 
 let rec determine casn undetermined skip = function
   | NIL -> skip || finish casn undetermined `After
-  | CAS (atom, state, lt, gt) as eq ->
+  | CAS (atom, desired, lt, gt) as eq ->
       determine casn undetermined true lt
       &&
-      let state' = Atomic.get atom.state in
-      if state == state' then determine casn undetermined skip gt
+      let current = Atomic.get atom.state in
+      if desired == current then determine casn undetermined skip gt
       else
-        let before = state.before in
-        let before' = state'.before and after' = state'.after in
+        let expected = desired.before in
         if
-          (before == before' && before == after')
-          || before == if is_after state'.casn then after' else before'
+          expected == current.after
+          && (current.casn == casn_after || is_after current.casn)
+          || expected == current.before
+             && (current.casn == casn_before || not (is_after current.casn))
         then
           let status = Atomic.get casn in
           if status != (undetermined :> status) then status == `After
-          else if Atomic.compare_and_set atom.state state' state then
+          else if Atomic.compare_and_set atom.state current desired then
             determine casn undetermined skip gt
           else determine casn undetermined skip eq
         else finish casn undetermined `Before
diff --git a/test/test.ml b/test/test.ml
index 62a3cb77..64f07ca7 100644
--- a/test/test.ml
+++ b/test/test.ml
@@ -42,6 +42,39 @@ module Barrier = struct
     done
 end
 
+let test_non_linearizable () =
+  let barrier = Barrier.make 2
+  and n_iter = 1_000_000
+  and test_finished = ref false in
+
+  let a = Kcas.ref 0 and b = Kcas.ref 0 in
+
+  let cass1a = [ Kcas.mk_cas b 0 0; Kcas.mk_cas a 0 1 ]
+  and cass1b = [ Kcas.mk_cas b 0 0; Kcas.mk_cas a 1 0 ]
+  and cass2a = [ Kcas.mk_cas b 0 1; Kcas.mk_cas a 0 0 ]
+  and cass2b = [ Kcas.mk_cas b 1 0; Kcas.mk_cas a 0 0 ] in
+
+  let thread1 () =
+    Barrier.await barrier;
+    while not !test_finished do
+      if Kcas.kCAS cass1a then
+        while not (Kcas.kCAS cass1b) do
+          assert (Kcas.get a == 1 && Kcas.get b == 0)
+        done
+    done
+  and thread2 () =
+    Barrier.await barrier;
+    for _ = 1 to n_iter do
+      if Kcas.kCAS cass2a then
+        while not (Kcas.kCAS cass2b) do
+          assert (Kcas.get a == 0 && Kcas.get b == 1)
+        done
+    done;
+    test_finished := true
+  in
+
+  [ thread2; thread1 ] |> List.map Domain.spawn |> List.iter Domain.join
+
 (* test 1 *)
 let test_set () =
   let a = Kcas.ref 0 in
@@ -209,6 +242,7 @@ let test_presort () =
   refs |> Array.iter (fun r -> assert (Kcas.get r = n_incs * n_domains))
 
 let () =
+  test_non_linearizable ();
   test_set ();
   test_casn ();
   test_read_casn ();