From 6541ddd37dc3066fe068c196cfc68bb16f73138b Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Wed, 6 Dec 2023 12:51:03 +0200 Subject: [PATCH] Demonstrate "linearizable chaining" of non-blocking data structures --- src/kcas_data/dllist.ml | 20 ++- src/kcas_data/dllist.mli | 6 +- test/kcas_data/dune | 1 + test/kcas_data/linearizable_chaining.ml | 193 ++++++++++++++++++++++++ 4 files changed, 214 insertions(+), 6 deletions(-) create mode 100644 test/kcas_data/linearizable_chaining.ml diff --git a/src/kcas_data/dllist.ml b/src/kcas_data/dllist.ml index 23003ae9..9be89070 100644 --- a/src/kcas_data/dllist.ml +++ b/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 } diff --git a/src/kcas_data/dllist.mli b/src/kcas_data/dllist.mli index eb43aef7..b109ed9e 100644 --- a/src/kcas_data/dllist.mli +++ b/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} *) diff --git a/test/kcas_data/dune b/test/kcas_data/dune index ad442943..9244af8b 100644 --- a/test/kcas_data/dune +++ b/test/kcas_data/dune @@ -11,6 +11,7 @@ (tests (names + linearizable_chaining accumulator_test dllist_test hashtbl_test diff --git a/test/kcas_data/linearizable_chaining.ml b/test/kcas_data/linearizable_chaining.ml new file mode 100644 index 00000000..ea3ffad5 --- /dev/null +++ b/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