diff --git a/.ocamlformat b/.ocamlformat index 29a9cf72..905a6b22 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,2 +1,4 @@ profile = default -version = 0.26.0 +version = 0.26.1 + +exp-grouping=preserve diff --git a/Makefile b/Makefile index ef3b81b1..2dcd1134 100644 --- a/Makefile +++ b/Makefile @@ -10,4 +10,4 @@ clean: dune clean bench: - @dune exec -- ./bench/main.exe + @dune exec --release -- ./bench/main.exe diff --git a/bench/bench_skiplist.ml b/bench/bench_skiplist.ml index 285dc450..2f82144a 100644 --- a/bench/bench_skiplist.ml +++ b/bench/bench_skiplist.ml @@ -1,7 +1,7 @@ open Saturn let workload num_elems num_threads add remove = - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let elems = Array.init num_elems (fun _ -> Random.int 10000) in let push () = Domain.spawn (fun () -> @@ -9,7 +9,7 @@ let workload num_elems num_threads add remove = for i = 0 to (num_elems - 1) / num_threads do Domain.cpu_relax (); let prob = Random.float 1.0 in - if prob < add then Skiplist.add sl (Random.int 10000) |> ignore + if prob < add then Skiplist.add sl (Random.int 10000) () |> ignore else if prob >= add && prob < add +. remove then Skiplist.remove sl (Random.int 10000) |> ignore else Skiplist.mem sl elems.(i) |> ignore diff --git a/dune-project b/dune-project index 4805fbb8..352352f2 100644 --- a/dune-project +++ b/dune-project @@ -13,6 +13,8 @@ (ocaml (>= 4.12)) (domain_shims (>= 0.1.0)) (saturn_lockfree (= :version)) + (multicore-magic (and (>= 2.0.0) :with-test)) + (alcotest (and (>= 1.7.0) :with-test)) (qcheck (and (>= 0.18.1) :with-test)) (qcheck-stm (and (>= 0.2) :with-test)) (qcheck-alcotest (and (>= 0.18.1) :with-test)) @@ -24,6 +26,8 @@ (depends (ocaml (>= 4.12)) (domain_shims (>= 0.1.0)) + (multicore-magic (>= 2.0.0)) + (alcotest (and (>= 1.7.0) :with-test)) (qcheck (and (>= 0.18.1) :with-test)) (qcheck-stm (and (>= 0.2) :with-test)) (qcheck-alcotest (and (>= 0.18.1) :with-test)) diff --git a/saturn.opam b/saturn.opam index 20dbb25b..b97e313a 100644 --- a/saturn.opam +++ b/saturn.opam @@ -13,6 +13,8 @@ depends: [ "ocaml" {>= "4.12"} "domain_shims" {>= "0.1.0"} "saturn_lockfree" {= version} + "multicore-magic" {>= "2.0.0" & with-test} + "alcotest" {>= "1.7.0" & with-test} "qcheck" {>= "0.18.1" & with-test} "qcheck-stm" {>= "0.2" & with-test} "qcheck-alcotest" {>= "0.18.1" & with-test} diff --git a/saturn_lockfree.opam b/saturn_lockfree.opam index b5c2d30f..afd6a3fd 100644 --- a/saturn_lockfree.opam +++ b/saturn_lockfree.opam @@ -11,6 +11,8 @@ depends: [ "dune" {>= "3.2"} "ocaml" {>= "4.12"} "domain_shims" {>= "0.1.0"} + "multicore-magic" {>= "2.0.0"} + "alcotest" {>= "1.7.0" & with-test} "qcheck" {>= "0.18.1" & with-test} "qcheck-stm" {>= "0.2" & with-test} "qcheck-alcotest" {>= "0.18.1" & with-test} diff --git a/src_lockfree/bits.ml b/src_lockfree/bits.ml new file mode 100644 index 00000000..483a914f --- /dev/null +++ b/src_lockfree/bits.ml @@ -0,0 +1,14 @@ +let ceil_pow_2_minus_1 n = + let n = n lor (n lsr 1) in + let n = n lor (n lsr 2) in + let n = n lor (n lsr 4) in + let n = n lor (n lsr 8) in + let n = n lor (n lsr 16) in + if Sys.int_size > 32 then n lor (n lsr 32) else n + +let ceil_pow_2 n = + if n <= 1 then 1 + else + let n = n - 1 in + let n = ceil_pow_2_minus_1 n in + n + 1 diff --git a/src_lockfree/bits.mli b/src_lockfree/bits.mli new file mode 100644 index 00000000..40c46f0b --- /dev/null +++ b/src_lockfree/bits.mli @@ -0,0 +1,7 @@ +(** *) + +val ceil_pow_2_minus_1 : int -> int +(** *) + +val ceil_pow_2 : int -> int +(** *) diff --git a/src_lockfree/dune b/src_lockfree/dune index 7a76425e..c62b76e3 100644 --- a/src_lockfree/dune +++ b/src_lockfree/dune @@ -1,4 +1,4 @@ (library (name saturn_lockfree) (public_name saturn_lockfree) - (libraries domain_shims)) + (libraries domain_shims multicore-magic)) diff --git a/src_lockfree/size.ml b/src_lockfree/size.ml new file mode 100644 index 00000000..4e270c4f --- /dev/null +++ b/src_lockfree/size.ml @@ -0,0 +1,158 @@ +module Snapshot = struct + type t = int Atomic.t array + + let zero = [| Atomic.make 0 |] + let collecting = Int.min_int + let computing = -1 + + let[@inline] is_collecting (s : t) = + Atomic.get (Array.unsafe_get s 0) = collecting + + let create n = Array.init n @@ fun _ -> Atomic.make collecting + + let add s i after = + let snap = Array.unsafe_get s i in + while + let before = Atomic.get snap in + before < after && not (Atomic.compare_and_set snap before after) + do + () + done + + let rec compute s decrs incrs i = + if i < Array.length s then + compute s + (decrs + Atomic.get (Array.unsafe_get s i)) + (incrs + Atomic.get (Array.unsafe_get s (i + 1))) + (i + 2) + else incrs - decrs + + let get s = + let status = Array.unsafe_get s 0 in + if Atomic.get status = collecting then + Atomic.compare_and_set status collecting computing |> ignore; + if Atomic.get status = computing then begin + let computed = compute s 0 0 1 in + if Atomic.get status = computing then + Atomic.compare_and_set status computing computed |> ignore + end; + Atomic.get status +end + +type t = Obj.t Atomic.t array + +let[@inline] get_current_snapshot (t : t) : Snapshot.t = + Obj.magic (Atomic.get (Array.unsafe_get t 0)) + +let[@inline] cas_current_snapshot (t : t) (before : Snapshot.t) + (after : Snapshot.t) = + Atomic.compare_and_set (Array.unsafe_get t 0) (Obj.repr before) + (Obj.repr after) + +(* *) + +let n_way_max = Domain.recommended_domain_count () |> Bits.ceil_pow_2 +let n_way_default = n_way_max |> Int.min 8 + +let create ?n_way () = + let n_way = + match n_way with + | None -> n_way_default + | Some n_way -> n_way |> Int.min n_way_max |> Bits.ceil_pow_2 + in + Array.init ((n_way * 2) + 1) @@ fun i -> + Atomic.make (if i = 0 then Obj.repr Snapshot.zero else Obj.repr 0) + |> Multicore_magic.copy_as_padded + +(* *) + +type _ state = + | Open : { mutable index : int } -> [ `Open ] state + | Used : [ `Used ] state + +type once = Once : _ state -> once [@@unboxed] + +let used_index = 0 +let get_index (Open r) = r.index +let use_index (Open r) = r.index <- used_index + +(* *) + +let used_once = Once Used + +(* *) + +let new_once t ~incr = + let mask = Array.length t - 2 in + (* TODO: Consider hashing the domain id. *) + let index = ((Domain.self () :> int) * 2 land mask) + 1 + Bool.to_int incr in + Once (Open { index }) + +(* *) + +type tx = { counter : Obj.t Atomic.t; value : int; once : [ `Open ] state } + +let finish (t : t) tx = + (* At this point the [tx.counter] already has the [tx]. Before updating the + [tx.counter] we need to make make sure the [tx.once] will not be used + again. *) + let index = get_index tx.once in + if index != used_index then use_index tx.once; + (* At this point the [add_once] is essentially done. To free memory, we do + one more [compare_and_set]. *) + Atomic.compare_and_set tx.counter (Obj.repr tx) (Obj.repr tx.value) |> ignore; + if index != used_index then + let snapshot = get_current_snapshot t in + if Snapshot.is_collecting snapshot then + (* A size computation is running concurrently. We need to forward the + update. *) + Snapshot.add snapshot index tx.value + +let rec update_once (t : t) once = + let index = get_index once in + if index != used_index then + let counter = Array.unsafe_get t index in + let counter_state = Atomic.get counter in + if index = get_index once then + if Obj.is_int counter_state then begin + let value = Obj.magic counter_state + 1 in + let tx = { counter; value; once } in + if Atomic.compare_and_set counter counter_state (Obj.repr tx) then + finish t tx + else update_once t once + end + else begin + finish t (Obj.magic counter_state); + update_once t once + end + +let update_once t once = + match once with + | Once Used -> () + | Once (Open _ as once) -> update_once t once + +(* *) + +let get_collecting_snapshot t = + let before = get_current_snapshot t in + if Snapshot.is_collecting before then before + else + let after = Snapshot.create (Array.length t) in + if cas_current_snapshot t before after then after + else get_current_snapshot t + +let rec collect t snapshot i = + if i < Array.length t then begin + let after = + let counter_state = Atomic.get (Array.unsafe_get t i) in + if Obj.is_int counter_state then Obj.magic counter_state + else (Obj.magic counter_state).value + in + Snapshot.add snapshot i after; + collect t snapshot (i + 1) + end + +let get t = + let snapshot = get_collecting_snapshot t in + collect t snapshot 1; + Snapshot.get snapshot diff --git a/src_lockfree/size.mli b/src_lockfree/size.mli new file mode 100644 index 00000000..09265ac5 --- /dev/null +++ b/src_lockfree/size.mli @@ -0,0 +1,22 @@ +(** *) + +type t +(** *) + +val create : ?n_way:int -> unit -> t +(** *) + +type once +(** *) + +val used_once : once +(** *) + +val new_once : t -> incr:bool -> once +(** *) + +val update_once : t -> once -> unit +(** *) + +val get : t -> int +(** *) diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml index 936eb82b..ef806e43 100644 --- a/src_lockfree/skiplist.ml +++ b/src_lockfree/skiplist.ml @@ -1,193 +1,313 @@ -type 'a markable_reference = { node : 'a node; marked : bool } +(* Copyright (c) 2023 Vesa Karvonen -and 'a node = { - key : 'a; - height : int; - next : 'a markable_reference Atomic.t array; -} + Permission to use, copy, modify, and/or distribute this software for any + purpose with or without fee is hereby granted, provided that the above + copyright notice and this permission notice appear in all copies. -exception Failed_snip + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH + REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY + AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY SPECIAL, DIRECT, + INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES WHATSOEVER RESULTING FROM + LOSS OF USE, DATA OR PROFITS, WHETHER IN AN ACTION OF CONTRACT, NEGLIGENCE OR + OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR + PERFORMANCE OF THIS SOFTWARE. *) -type 'a t = { head : 'a node; max_height : int } +(* This implementation has been written from scratch with inspiration from a + lock-free skiplist implementation in PR -let min = Obj.new_block 5 5 |> Obj.obj -let max = Obj.new_block 5 5 |> Obj.obj -let null_node = { key = max; height = 0; next = [||] } + https://github.com/ocaml-multicore/saturn/pull/65 -let[@inline] create_dummy_node_array sl = - Array.make (sl.max_height + 1) null_node + by -let[@inline] create_new_node value height = - let next = - Array.init (height + 1) (fun _ -> - Atomic.make { node = null_node; marked = false }) - in - { key = value; height; next } + Sooraj Srinivasan ( https://github.com/sooraj-srini ) -let[@inline] get_random_level sl = - let rec count_level cur_level = - if Random.bool () then cur_level - else if cur_level == sl.max_height then count_level 0 - else count_level (cur_level + 1) - in - if sl.max_height = 0 then 0 else count_level 0 + including tests and changes by + + Carine Morel ( https://github.com/lyrm ). *) + +(* TODO: Grow and possibly shrink the skiplist or e.g. adjust search and node + generation based on the dynamic number of bindings. *) + +(* OCaml doesn't allow us to use one of the unused (always 0) bits in pointers + for the marks and an indirection is needed. This representation avoids the + indirection except for marked references in nodes to be removed. A GADT with + polymorphic variants is used to disallow nested [Mark]s. *) +type ('k, 'v, _) node = + | Null : ('k, 'v, [> `Null ]) node + | Node : { + key : 'k; + value : 'v; + next : ('k, 'v) links; + mutable incr : Size.once; + } + -> ('k, 'v, [> `Node ]) node + | Mark : { + node : ('k, 'v, [< `Null | `Node ]) node; + mutable decr : Size.once; + } + -> ('k, 'v, [ `Mark ]) node + +(* The implementation relies on this existential being unboxed. More + specifically, it is assumed that [Link node == Link node] meaning that the + [Link] constructor does not allocate. *) +and ('k, 'v) link = Link : ('k, 'v, _) node -> ('k, 'v) link [@@unboxed] +and ('k, 'v) links = ('k, 'v) link Atomic.t array + +type 'k compare = 'k -> 'k -> int +(* Encoding the [compare] function using an algebraic type would allow the + overhead of calling a closure to be avoided for selected primitive types like + [int]. *) + +type ('k, 'v) t = { compare : 'k compare; root : ('k, 'v) links; size : Size.t } + +(* *) + +(** [get_random_height max_height] gives a random value [n] in the range from + [1] to [max_height] with the desired distribution such that [n] is twice as + likely as [n + 1]. *) +let rec get_random_height max_height = + let m = (1 lsl max_height) - 1 in + let x = Random.bits () land m in + if x = 1 then + (* We reject [1] to get the desired distribution. *) + get_random_height max_height + else + (* We do a binary search for the highest 1 bit. Techniques in + + Using de Bruijn Sequences to Index a 1 in a Computer Word + by Leiserson, Prokop, and Randall + + could perhaps speed this up a bit, but this is likely not performance + critical. *) + let n = 0 in + let n, x = if 0xFFFF < x then (n + 0x10, x lsr 0x10) else (n, x) in + let n, x = if 0x00FF < x then (n + 0x08, x lsr 0x08) else (n, x) in + let n, x = if 0x000F < x then (n + 0x04, x lsr 0x04) else (n, x) in + let n, x = if 0x0003 < x then (n + 0x02, x lsr 0x02) else (n, x) in + let n, _ = if 0x0001 < x then (n + 0x01, x lsr 0x01) else (n, x) in + max_height - n + +(* *) + +let[@inline] is_marked = function + | Link (Mark _) -> true + | Link (Null | Node _) -> false + +(* *) + +let rec find_path t key prev preds succs level lowest = + (* Breaking the sequence of dependent loads could improve performance. *) + let prev_at_level = Array.unsafe_get prev level in + match Atomic.get prev_at_level with + | Link Null -> + Array.unsafe_set preds level prev_at_level; + Array.unsafe_set succs level Null; + lowest < level && find_path t key prev preds succs (level - 1) lowest + | Link (Node r as curr_node) as before -> begin + match Atomic.get (Array.unsafe_get r.next level) with + | Link (Null | Node _) -> + let c = t.compare key r.key in + if 0 < c then find_path t key r.next preds succs level lowest + else begin + Array.unsafe_set preds level prev_at_level; + Array.unsafe_set succs level curr_node; + if lowest < level then + find_path t key prev preds succs (level - 1) lowest + else begin + if level = 0 && r.incr != Size.used_once then begin + Size.update_once t.size r.incr; + r.incr <- Size.used_once + end; + 0 = c + end + end + | Link (Mark r) -> + if level = 0 && r.decr != Size.used_once then begin + Size.update_once t.size r.decr; + r.decr <- Size.used_once + end; + Atomic.compare_and_set prev_at_level before (Link r.node) |> ignore; + find_path t key prev preds succs level lowest + end + | Link (Mark _) -> + find_path t key t.root preds succs (Array.length t.root - 1) lowest + +(** [find_path t key preds succs lowest] tries to find the node with the specified + [key], updating [preds] and [succs] and removing nodes with marked + references along the way, and always descending down to [lowest] level. The + boolean return value is only meaningful when [lowest] is given as [0]. *) +let[@inline] find_path t key preds succs lowest = + find_path t key t.root preds succs (Array.length t.root - 1) lowest + +(* *) + +let rec find_node t key prev level = + (* Breaking the sequence of dependent loads could improve performance. *) + let prev_at_level = Array.unsafe_get prev level in + match Atomic.get prev_at_level with + | Link Null -> if 0 < level then find_node t key prev (level - 1) else Null + | Link (Node r as node) as before -> begin + match Atomic.get (Array.unsafe_get r.next level) with + | Link (Null | Node _) -> + let c = t.compare key r.key in + if 0 < c then find_node t key r.next level + else if 0 = c then begin + (* At this point we know the node was not removed, because removal + is done in order of descending levels. *) + if r.incr != Size.used_once then begin + Size.update_once t.size r.incr; + r.incr <- Size.used_once + end; + node + end + else if 0 < level then find_node t key prev (level - 1) + else Null + | Link (Mark r) -> + if level = 0 && r.decr != Size.used_once then begin + Size.update_once t.size r.decr; + r.decr <- Size.used_once + end; + Atomic.compare_and_set prev_at_level before (Link r.node) |> ignore; + find_node t key prev level + end + | Link (Mark _) -> find_node t key t.root (Array.length t.root - 1) + +(** [find_node t key] tries to find the node with the specified [key], removing + nodes with marked references along the way, and stopping as soon as the node + is found. *) +let[@inline] find_node t key = find_node t key t.root (Array.length t.root - 1) + +(* *) + +let create ?n_way ?(max_height = 10) ?(compare = Stdlib.compare) () = + (* The upper limit of [30] comes from [Random.bits ()] as well as from + limitations with 32-bit implementations. It should not be a problem in + practice. *) + if max_height < 1 || 30 < max_height then + invalid_arg "Skiplist: max_height must be in the range [1, 30]"; + let root = Array.init max_height @@ fun _ -> Atomic.make (Link Null) in + let size = Size.create ?n_way () in + { compare; root; size } -let create ?(max_height = 10) () = - let max_height = Int.max max_height 1 in - let tail = create_new_node max (max_height - 1) in +(* *) + +let find_opt t key = + match find_node t key with Null -> None | Node r -> Some r.value + +(* *) + +let mem t key = match find_node t key with Null -> false | Node _ -> true + +(* *) + +let rec add t key value preds succs = + (not (find_path t key preds succs 0)) + && let next = - Array.init max_height (fun _ -> Atomic.make { node = tail; marked = false }) - in - let head = { key = min; height = max_height - 1; next } in - { head; max_height = max_height - 1 } - -(** Compares old_node and old_mark with the atomic reference and if they are the same then - Replaces the value in the atomic with node and mark *) -let compare_and_set_mark_ref (atomic, old_node, old_mark, node, mark) = - let ({ node = current_node; marked = current_marked } as current) = - Atomic.get atomic + let height = get_random_height (Array.length t.root) in + Array.init height @@ fun i -> Atomic.make (Link (Array.unsafe_get succs i)) in - current_node == old_node && current_marked = old_mark - && ((current_node == node && current_marked = mark) - || Atomic.compare_and_set atomic current { node; marked = mark }) - -(** Returns true if key is found within the skiplist else false; - Irrespective of return value, fills the preds and succs array with - the predecessors nodes with smaller key and successors nodes with greater than - or equal to key - *) -let find_in (key, preds, succs, sl) = - let head = sl.head in - let rec iterate (prev, curr, succ, mark, level) = - if mark then - let snip = - compare_and_set_mark_ref (prev.next.(level), curr, false, succ, false) - in - if not snip then raise Failed_snip - else - let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in - iterate (prev, succ, new_succ, mark, level) - else if curr.key != max && curr.key < key then - let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in - iterate (curr, succ, new_succ, mark, level) - else (prev, curr) - in - let rec update_arrays prev level = - let { node = curr; marked = _ } = Atomic.get prev.next.(level) in - let { node = succ; marked = mark } = Atomic.get curr.next.(level) in - try - let prev, curr = iterate (prev, curr, succ, mark, level) in - preds.(level) <- prev; - succs.(level) <- curr; - if level > 0 then update_arrays prev (level - 1) - else if curr.key == max then false - else curr.key = key - with Failed_snip -> update_arrays head sl.max_height + let incr = Size.new_once t.size ~incr:true in + let (Node r as node : (_, _, [ `Node ]) node) = + Node { key; value; incr; next } in - update_arrays head sl.max_height - -(** Adds a new key to the skiplist sl. *) -let add sl key = - let top_level = get_random_level sl in - let preds = create_dummy_node_array sl in - let succs = create_dummy_node_array sl in - let rec repeat () = - let found = find_in (key, preds, succs, sl) in - if found then false - else - let new_node_next = - Array.map - (fun element -> - let mark_ref = { node = element; marked = false } in - Atomic.make mark_ref) - succs - in - let new_node = { key; height = top_level; next = new_node_next } in - let pred = preds.(0) in - let succ = succs.(0) in - if - not - (compare_and_set_mark_ref - (pred.next.(0), succ, false, new_node, false)) - then repeat () + if + let succ = Link (Array.unsafe_get succs 0) in + Atomic.compare_and_set (Array.unsafe_get preds 0) succ (Link node) + then begin + if r.incr != Size.used_once then begin + Size.update_once t.size r.incr; + r.incr <- Size.used_once + end; + (* The node is now considered as added to the skiplist. *) + let rec update_levels level = + if Array.length next = level then begin + if is_marked (Atomic.get (Array.unsafe_get next (level - 1))) then begin + (* The node we finished adding has been removed concurrently. To + ensure that no references we added to the node remain, we call + [find_node] which will remove nodes with marked references along + the way. *) + find_node t key |> ignore + end; + true + end + else if + let succ = Link (Array.unsafe_get succs level) in + Atomic.compare_and_set (Array.unsafe_get preds level) succ (Link node) + then update_levels (level + 1) else - let rec update_levels level = - let rec set_next () = - let pred = preds.(level) in - let succ = succs.(level) in - if - compare_and_set_mark_ref - (pred.next.(level), succ, false, new_node, false) - then () - else ( - find_in (key, preds, succs, sl) |> ignore; - set_next ()) - in - set_next (); - if level < top_level then update_levels (level + 1) + let _found = find_path t key preds succs level in + let rec update_nexts level' = + if level' < level then update_levels level + else + let next = Array.unsafe_get next level' in + match Atomic.get next with + | Link (Null | Node _) as before -> + let succ = Link (Array.unsafe_get succs level') in + if before != succ then + if Atomic.compare_and_set next before succ then + update_nexts (level' - 1) + else update_levels level + else update_nexts (level' - 1) + | Link (Mark _) -> + (* The node we were trying to add has been removed concurrently. + To ensure that no references we added to the node remain, we + call [find_node] which will remove nodes with marked + references along the way. *) + find_node t key |> ignore; + true in - if top_level > 0 then update_levels 1; - true - in - repeat () - -let mem sl key = - let rec search (pred, curr, succ, mark, level) = - if mark then - let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in - search (pred, succ, new_succ, mark, level) - else if curr.key != max && curr.key < key then - let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in - search (curr, succ, new_succ, mark, level) - else if level > 0 then - let level = level - 1 in - let { node = curr; marked = _ } = Atomic.get pred.next.(level) in - let { node = succ; marked = mark } = Atomic.get curr.next.(level) in - search (pred, curr, succ, mark, level) - else if curr.key == max then false - else curr.key = key - in - let pred = sl.head in - let { node = curr; marked = _ } = Atomic.get pred.next.(sl.max_height) in - let { node = succ; marked = mark } = Atomic.get curr.next.(sl.max_height) in - search (pred, curr, succ, mark, sl.max_height) - -let remove sl key = - let preds = create_dummy_node_array sl in - let succs = create_dummy_node_array sl in - let found = find_in (key, preds, succs, sl) in - if not found then false - else - let nodeToRemove = succs.(0) in - let nodeHeight = nodeToRemove.height in - let rec mark_levels succ level = - let _ = - compare_and_set_mark_ref - (nodeToRemove.next.(level), succ, false, succ, true) - in - let { node = succ; marked = mark } = - Atomic.get nodeToRemove.next.(level) - in - if not mark then mark_levels succ level + update_nexts (Array.length next - 1) in - let rec update_upper_levels level = - let { node = succ; marked = mark } = - Atomic.get nodeToRemove.next.(level) + update_levels 1 + end + else add t key value preds succs + +let add t key value = + let preds = Array.make (Array.length t.root) (Obj.magic ()) in + let succs = Array.make (Array.length t.root) Null in + add t key value preds succs + +(* *) + +let remove t key = + match find_node t key with + | Null -> false + | Node { next; _ } -> + let rec update_upper_levels level = + if 0 < level then + let link = Array.unsafe_get next level in + match Atomic.get link with + | Link (Mark _) -> update_upper_levels (level - 1) + | Link ((Null | Node _) as succ) -> + let marked_succ = Mark { node = succ; decr = Size.used_once } in + if Atomic.compare_and_set link (Link succ) (Link marked_succ) then + update_upper_levels (level - 1) + else update_upper_levels level in - if not mark then mark_levels succ level; - if level > 1 then update_upper_levels (level - 1) - in - let rec update_bottom_level succ = - let iMarkedIt = - compare_and_set_mark_ref (nodeToRemove.next.(0), succ, false, succ, true) + update_upper_levels (Array.length next - 1); + let rec try_update_bottom_level link = + match Atomic.get link with + | Link (Mark r) -> + if r.decr != Size.used_once then begin + Size.update_once t.size r.decr; + r.decr <- Size.used_once + end; + false + | Link ((Null | Node _) as succ) -> + let decr = Size.new_once t.size ~incr:false in + let marked_succ = Mark { node = succ; decr } in + if Atomic.compare_and_set link (Link succ) (Link marked_succ) then + (* We have finished marking references on the node. To ensure + that no references to the node remain, we call [find_node] + which will remove nodes with marked references along the + way. *) + let _node = find_node t key in + true + else try_update_bottom_level link in - let { node = succ; marked = mark } = Atomic.get succs.(0).next.(0) in - if iMarkedIt then ( - find_in (key, preds, succs, sl) |> ignore; - true) - else if mark then false - else update_bottom_level succ - in - if nodeHeight > 0 then update_upper_levels nodeHeight; - let { node = succ; marked = _ } = Atomic.get nodeToRemove.next.(0) in - update_bottom_level succ + try_update_bottom_level (Array.unsafe_get next 0) + +(* *) + +let length t = Size.get t.size diff --git a/src_lockfree/skiplist.mli b/src_lockfree/skiplist.mli index bc18575e..dae3a7fe 100644 --- a/src_lockfree/skiplist.mli +++ b/src_lockfree/skiplist.mli @@ -1,24 +1,27 @@ -(** Skiplist TODO +(** A lock-free skiplist. *) - [key] values are compared with [=] and thus should not be functions or - objects. -*) +type (!'k, !'v) t +(** *) -type 'a t -(** The type of lock-free skiplist. *) +val create : + ?n_way:int -> + ?max_height:int -> + ?compare:('k -> 'k -> int) -> + unit -> + ('k, 'v) t +(** *) -val create : ?max_height:int -> unit -> 'a t -(** [create ~max_height ()] returns a new empty skiplist. [~max_height] is the - number of level used to distribute nodes. Its default value is 10 by default - and can not be less than 1. *) +val find_opt : ('k, 'v) t -> 'k -> 'v option +(** *) -val add : 'a t -> 'a -> bool -(** [add s v] adds [v] to [s] if [v] is not already in [s] and returns - [true]. If [v] is already in [s], it returns [false] and [v] is unchanged. *) +val mem : ('k, 'v) t -> 'k -> bool +(** *) -val remove : 'a t -> 'a -> bool -(** [remove s v] removes [v] of [s] if [v] is in [s] and returns [true]. If [v] - is not in [s], it returns [false] and [v] is unchanged. *) +val add : ('k, 'v) t -> 'k -> 'v -> bool +(** *) -val mem : 'a t -> 'a -> bool -(** [mem s v] returns [true] if v is in s and [false] otherwise. *) +val remove : ('k, 'v) t -> 'k -> bool +(** *) + +val length : ('k, 'v) t -> int +(** *) diff --git a/test/skiplist/dune b/test/skiplist/dune index 3ffaa883..a9bad777 100644 --- a/test/skiplist/dune +++ b/test/skiplist/dune @@ -1,13 +1,13 @@ (rule - (copy ../../src_lockfree/backoff.ml backoff.ml)) - -(rule - (copy ../../src_lockfree/skiplist.ml skiplist.ml)) + (progn + (copy ../../src_lockfree/skiplist.ml skiplist.ml) + (copy ../../src_lockfree/bits.ml bits.ml) + (copy ../../src_lockfree/size.ml size.ml))) (test (name skiplist_dscheck) - (libraries atomic dscheck alcotest) - (modules skiplist skiplist_dscheck)) + (libraries atomic dscheck alcotest multicore-magic) + (modules skiplist size bits skiplist_dscheck)) (test (name qcheck_skiplist) diff --git a/test/skiplist/qcheck_skiplist.ml b/test/skiplist/qcheck_skiplist.ml index 94b65f81..2855b157 100644 --- a/test/skiplist/qcheck_skiplist.ml +++ b/test/skiplist/qcheck_skiplist.ml @@ -1,4 +1,8 @@ -module Skiplist = Saturn.Skiplist +module Skiplist = struct + include Saturn.Skiplist + + let add s k = add s k () +end let tests_sequential = QCheck. diff --git a/test/skiplist/skiplist_dscheck.ml b/test/skiplist/skiplist_dscheck.ml index 283ced0e..97f4f783 100644 --- a/test/skiplist/skiplist_dscheck.ml +++ b/test/skiplist/skiplist_dscheck.ml @@ -1,5 +1,7 @@ open Skiplist +let add s k = add s k () + let _two_mem () = Atomic.trace (fun () -> Random.init 0; diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml index 0831c4c9..87b7c4a4 100644 --- a/test/skiplist/stm_skiplist.ml +++ b/test/skiplist/stm_skiplist.ml @@ -2,22 +2,26 @@ open QCheck open STM -module Skiplist = Saturn.Skiplist + +module Skiplist = struct + include Saturn.Skiplist + + type nonrec 'a t = ('a, unit) t + + let add s k = add s k () +end module WSDConf = struct - type cmd = Mem of int | Add of int | Remove of int + type cmd = Mem of int | Add of int | Remove of int | Length let show_cmd c = match c with | Mem i -> "Mem " ^ string_of_int i | Add i -> "Add " ^ string_of_int i | Remove i -> "Remove " ^ string_of_int i + | Length -> "Length" - module Sint = Set.Make (struct - type t = int - - let compare = compare - end) + module Sint = Set.Make (Int) type state = Sint.t type sut = int Skiplist.t @@ -30,6 +34,7 @@ module WSDConf = struct Gen.map (fun i -> Add i) int_gen; Gen.map (fun i -> Mem i) int_gen; Gen.map (fun i -> Remove i) int_gen; + Gen.return Length; ]) let init_state = Sint.empty @@ -41,6 +46,7 @@ module WSDConf = struct | Add i -> Sint.add i s | Remove i -> Sint.remove i s | Mem _ -> s + | Length -> s let precond _ _ = true @@ -49,12 +55,14 @@ module WSDConf = struct | Add i -> Res (bool, Skiplist.add d i) | Remove i -> Res (bool, Skiplist.remove d i) | Mem i -> Res (bool, Skiplist.mem d i) + | Length -> Res (int, Skiplist.length d) let postcond c (s : state) res = match (c, res) with | Add i, Res ((Bool, _), res) -> Sint.mem i s = not res | Remove i, Res ((Bool, _), res) -> Sint.mem i s = res | Mem i, Res ((Bool, _), res) -> Sint.mem i s = res + | Length, Res ((Int, _), res) -> Sint.cardinal s = res | _, _ -> false end