Demonstrate "linearizable chaining" of non-blocking data structures

src/kcas_data/dllist.ml

@@ -16,7 +16,17 @@ let create () =
   Loc.set next list;
   list
 
-let create_node ~prev ~next value =
+let create_node value =
+  let node =
+    let node_prev = Loc.make (Obj.magic ())
+    and node_next = Loc.make (Obj.magic ()) in
+    { node_prev; node_next; value }
+  in
+  Loc.set node.node_prev (as_list node);
+  Loc.set node.node_next (as_list node);
+  node
+
+let create_node_with ~prev ~next value =
   { node_prev = Loc.make prev; node_next = Loc.make next; value }
 
 module Xt = struct
@@ -41,7 +51,7 @@ module Xt = struct
 
   let add_l ~xt value list =
     let next = Xt.get ~xt list.next in
-    let node = create_node ~prev:list ~next value in
+    let node = create_node_with ~prev:list ~next value in
     Xt.set ~xt list.next (as_list node);
     Xt.set ~xt next.prev (as_list node);
     node
@@ -56,7 +66,7 @@ module Xt = struct
 
   let add_r ~xt value list =
     let prev = Xt.get ~xt list.prev in
-    let node = create_node ~prev ~next:list value in
+    let node = create_node_with ~prev ~next:list value in
     Xt.set ~xt list.prev (as_list node);
     Xt.set ~xt prev.next (as_list node);
     node
@@ -163,11 +173,11 @@ let remove node = Kcas.Xt.commit { tx = Xt.remove node }
 let is_empty list = Loc.get list.prev == list
 
 let add_l value list =
-  let node = create_node ~prev:list ~next:list value in
+  let node = create_node_with ~prev:list ~next:list value in
   Kcas.Xt.commit { tx = Xt.add_node_l node list }
 
 let add_r value list =
-  let node = create_node ~prev:list ~next:list value in
+  let node = create_node_with ~prev:list ~next:list value in
   Kcas.Xt.commit { tx = Xt.add_node_r node list }
 
 let move_l node list = Kcas.Xt.commit { tx = Xt.move_l node list }

src/kcas_data/dllist.mli

@@ -43,7 +43,11 @@ val get : 'a node -> 'a
 (** [get node] returns the value stored in the {!node}. *)
 
 val create : unit -> 'a t
-(** [create ()] return a new doubly-linked list. *)
+(** [create ()] creates a new doubly-linked list. *)
+
+val create_node : 'a -> 'a node
+(** [create_node value] creates a new doubly-linked list node that is not in any
+    list. *)
 
 (** {1 Compositional interface} *)
 

test/kcas_data/dune

@@ -11,6 +11,7 @@
 
 (tests
  (names
+  linearizable_chaining
   accumulator_test
   dllist_test
   hashtbl_test

test/kcas_data/linearizable_chaining.ml

@@ -0,0 +1,193 @@
+open Kcas
+open Kcas_data
+
+module type Hashtbl_base = sig
+  type (!'k, !'v) t
+
+  val find_opt : ('k, 'v) t -> 'k -> 'v option
+  val add : ('k, 'v) t -> 'k -> 'v -> bool
+  val remove : ('k, 'v) t -> 'k -> bool
+end
+
+module Hashtbl : sig
+  include Hashtbl_base
+
+  val create :
+    ?idempotent_add:('k -> 'v -> ('k, 'v) t -> unit) ->
+    ?idempotent_remove:('k -> 'v -> ('k, 'v) t -> unit) ->
+    unit ->
+    ('k, 'v) t
+end = struct
+  type ('k, 'v) t = {
+    idempotent_add : 'k -> 'v -> ('k, 'v) t -> unit;
+    idempotent_remove : 'k -> 'v -> ('k, 'v) t -> unit;
+    hashtbl : ('k, ('k, 'v) value) Hashtbl.t;
+  }
+
+  and ('k, 'v) value =
+    | Add of { event : ('k, 'v) t -> unit; value : 'v }
+    | Remove of { event : ('k, 'v) t -> unit }
+
+  let create ?(idempotent_add = fun _ _ _ -> ())
+      ?(idempotent_remove = fun _ _ _ -> ()) () =
+    let hashtbl = Hashtbl.create () in
+    { idempotent_add; idempotent_remove; hashtbl }
+
+  let find_opt t key =
+    match Hashtbl.find_opt t.hashtbl key with
+    | None -> None
+    | Some (Add r) ->
+        r.event t;
+        Some r.value
+    | Some (Remove r) ->
+        r.event t;
+        None
+
+  let add t key value =
+    let event = t.idempotent_add key value in
+    let value = Add { event; value } in
+    let tx ~xt =
+      begin
+        match Hashtbl.Xt.find_opt ~xt t.hashtbl key with
+        | None -> true
+        | Some (Add r) ->
+            r.event t;
+            false
+        | Some (Remove r) ->
+            r.event t;
+            true
+      end
+      && begin
+           Hashtbl.Xt.replace ~xt t.hashtbl key value;
+           true
+         end
+    in
+    Xt.commit { tx }
+    && begin
+         event t;
+         true
+       end
+
+  let remove t key =
+    let tx ~xt =
+      begin
+        match Hashtbl.Xt.find_opt ~xt t.hashtbl key with
+        | None -> false
+        | Some (Add r) ->
+            r.event t;
+            let event = t.idempotent_remove key r.value in
+            let value = Remove { event } in
+            Hashtbl.Xt.replace ~xt t.hashtbl key value;
+            true
+        | Some (Remove r) ->
+            r.event t;
+            false
+      end
+    in
+    Xt.commit { tx }
+    &&
+    let tx ~xt =
+      match Hashtbl.Xt.find_opt ~xt t.hashtbl key with
+      | None -> ()
+      | Some (Add _) -> ()
+      | Some (Remove r) ->
+          r.event t;
+          Hashtbl.Xt.remove ~xt t.hashtbl key
+    in
+    Xt.commit { tx };
+    true
+end
+
+module Hashtbl_with_order : sig
+  include Hashtbl_base
+
+  val create : unit -> ('k, 'v) t
+  val order : ('k, 'v) t -> 'k list
+end = struct
+  type ('k, 'v) t = {
+    table : ('k, 'k Dllist.node * 'v) Hashtbl.t;
+    order : 'k Dllist.t;
+  }
+
+  let create () =
+    let order = Dllist.create () in
+    let idempotent_add _key (node, _value) =
+      let node = Loc.make (Some node) in
+      let tx ~xt =
+        match Xt.exchange ~xt node None with
+        | None -> ()
+        | Some node -> Dllist.Xt.move_l ~xt node order
+      in
+      fun _table -> Xt.commit { tx }
+    in
+    let idempotent_remove _key (node, _value) =
+      let node = Loc.make (Some node) in
+      let tx ~xt =
+        match Xt.exchange ~xt node None with
+        | None -> ()
+        | Some node -> Dllist.Xt.remove ~xt node
+      in
+      fun _table -> Xt.commit { tx }
+    in
+    let table = Hashtbl.create ~idempotent_add ~idempotent_remove () in
+    { table; order }
+
+  let find_opt t key =
+    Hashtbl.find_opt t.table key |> Option.map (fun (_, v) -> v)
+
+  let add t key value = Hashtbl.add t.table key (Dllist.create_node key, value)
+  let remove t key = Hashtbl.remove t.table key
+  let order t = Dllist.to_list_l t.order
+end
+
+module Spec = struct
+  type cmd = Add of int | Remove of int | Order
+
+  let show_cmd = function
+    | Add key -> "Add " ^ string_of_int key
+    | Remove key -> "Remove " ^ string_of_int key
+    | Order -> "Order"
+
+  type state = int list
+  type sut = (int, unit) Hashtbl_with_order.t
+
+  let arb_cmd _s =
+    QCheck.(
+      [
+        Gen.int_range 1 5 |> Gen.map (fun key -> Add key);
+        Gen.int_range 1 5 |> Gen.map (fun key -> Remove key);
+        Gen.return Order;
+      ]
+      |> Gen.oneof |> make ~print:show_cmd)
+
+  let init_state = []
+  let init_sut () = Hashtbl_with_order.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Add key -> if List.for_all (( != ) key) s then key :: s else s
+    | Remove key -> List.filter (( != ) key) s
+    | Order -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    let open STM in
+    match c with
+    | Add key -> Res (bool, Hashtbl_with_order.add d key ())
+    | Remove key -> Res (bool, Hashtbl_with_order.remove d key)
+    | Order -> Res (list int, Hashtbl_with_order.order d)
+
+  let postcond c (s : state) res =
+    let open STM in
+    match (c, res) with
+    | Add key, Res ((Bool, _), res) -> res = List.for_all (( != ) key) s
+    | Remove key, Res ((Bool, _), res) -> res = List.exists (( == ) key) s
+    | Order, Res ((List Int, _), res) -> res = s
+    | _, _ -> false
+end
+
+let () =
+  Stm_run.run ~count:1000 ~verbose:true ~name:"Hashtbl_with_order" (module Spec)
+  |> exit