From 5114f011994a0ee78790aa2fed4713a4ec667f6d Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Thu, 16 Nov 2023 10:28:07 +0200 Subject: [PATCH] Add skiplist with generalized size computation --- bench/bench_skiplist.ml | 6 +- src_lockfree/skiplist.ml | 522 ++++++++++++------ src_lockfree/skiplist.mli | 54 +- ...kiplist_dscheck.ml => dscheck_skiplist.ml} | 45 +- test/skiplist/dune | 30 +- test/skiplist/qcheck_skiplist.ml | 44 +- test/skiplist/stm_skiplist.ml | 30 +- 7 files changed, 471 insertions(+), 260 deletions(-) rename test/skiplist/{skiplist_dscheck.ml => dscheck_skiplist.ml} (62%) diff --git a/bench/bench_skiplist.ml b/bench/bench_skiplist.ml index 285dc450..2b420570 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,9 +9,9 @@ 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.try_add sl (Random.int 10000) () |> ignore else if prob >= add && prob < add +. remove then - Skiplist.remove sl (Random.int 10000) |> ignore + Skiplist.try_remove sl (Random.int 10000) |> ignore else Skiplist.mem sl elems.(i) |> ignore done; start_time) diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml index 936eb82b..bd4aabf3 100644 --- a/src_lockfree/skiplist.ml +++ b/src_lockfree/skiplist.ml @@ -1,193 +1,355 @@ -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 -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 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 - 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 + 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. *) + +module Atomic = Transparent_atomic + +(* 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; + 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, [< `Null | `Node | `Mark ]) 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 + +(* *) + +(** [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 rec find_path t key preds succs lowest = + let prev = t.root in + let level = Array.length prev - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_path_rec t key prev prev_at_level preds succs level lowest + (Atomic.get prev_at_level) + +and find_path_rec t key prev prev_at_level preds succs level lowest = function + | Link Null -> + if level < Array.length preds then begin + Array.unsafe_set preds level prev_at_level; + Array.unsafe_set succs level Null + end; + lowest < level + && + let level = level - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_path_rec t key prev prev_at_level preds succs level lowest + (Atomic.get prev_at_level) + | Link (Node r as curr) -> begin + let next_at_level = Array.unsafe_get r.next level in + match Atomic.get next_at_level with + | Link (Null | Node _) as next -> + let c = t.compare key r.key in + if 0 < c then + find_path_rec t key r.next next_at_level preds succs level lowest + next + else begin + if level < Array.length preds then begin + Array.unsafe_set preds level (Array.unsafe_get prev level); + Array.unsafe_set succs level curr + end; + if lowest < level then + let level = level - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_path_rec t key prev prev_at_level preds succs level lowest + (Atomic.get prev_at_level) + 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) -> + (* The [curr_node] is being removed from the skiplist and we help with + that. *) + if level = 0 then Size.update_once t.size r.decr; + find_path_rec t key prev prev_at_level preds succs level lowest + (let after = Link r.node in + if Atomic.compare_and_set prev_at_level (Link curr) after then + after + else Atomic.get prev_at_level) + end + | Link (Mark _) -> + (* The node corresponding to [prev] is being removed from the skiplist. + This means we might no longer have an up-to-date view of the skiplist + and so we must restart the search. *) + find_path t key preds succs lowest + +(* *) + +(** [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 rec find_node t key = + let prev = t.root in + let level = Array.length prev - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_node_rec t key prev prev_at_level level (Atomic.get prev_at_level) + +and find_node_rec t key prev prev_at_level level : + _ -> (_, _, [< `Null | `Node ]) node = function + | Link Null -> + if 0 < level then + let level = level - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_node_rec t key prev prev_at_level level (Atomic.get prev_at_level) + else Null + | Link (Node r as curr) -> begin + let next_at_level = Array.unsafe_get r.next level in + match Atomic.get next_at_level with + | Link (Null | Node _) as next -> + let c = t.compare key r.key in + if 0 < c then find_node_rec t key r.next next_at_level level next + 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; + curr + end + else if 0 < level then + let level = level - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_node_rec t key prev prev_at_level level + (Atomic.get prev_at_level) + else Null + | Link (Mark r) -> + if level = 0 then Size.update_once t.size r.decr; + find_node_rec t key prev prev_at_level level + (let after = Link r.node in + if Atomic.compare_and_set prev_at_level (Link curr) after then + after + else Atomic.get prev_at_level) + end + | Link (Mark _) -> find_node t key + +(* *) + +let create ?(max_height = 10) ~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 () in + { compare; root; size } + +let max_height_of t = Array.length t.root + +(* *) + +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 try_add t key value preds succs = + (not (find_path t key preds succs 0)) + && + let (Node r as node : (_, _, [ `Node ]) node) = + let next = Array.map (fun succ -> Atomic.make (Link succ)) succs in + let incr = Size.new_once t.size Size.incr in + 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 r.next = level then begin + if is_marked (Atomic.get (Array.unsafe_get r.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 r.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 + (* It is possible for a concurrent remove operation to have + marked the link. *) + 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 r.next - 1) in - let rec update_upper_levels level = - let { node = succ; marked = mark } = - Atomic.get nodeToRemove.next.(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_levels 1 + end + else try_add t key value preds succs + +let try_add t key value = + let height = get_random_height (Array.length t.root) in + let preds = + (* Init with [Obj.magic ()] is safe as the array is fully overwritten by + [find_path] called at the start of the recursive [try_add]. *) + Array.make height (Obj.magic ()) + in + let succs = Array.make height Null in + try_add t key value preds succs + +(* *) + +let rec try_remove t key next level link = function + | Link (Mark r) -> + if level = 0 then begin + Size.update_once t.size r.decr; + false + end + else + let level = level - 1 in + let link = Array.unsafe_get next level in + try_remove t key next level link (Atomic.get link) + | Link ((Null | Node _) as succ) -> + let decr = + if level = 0 then Size.new_once t.size Size.decr else Size.used_once 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 + let marked_succ = Mark { node = succ; decr } in + if Atomic.compare_and_set link (Link succ) (Link marked_succ) then + if level = 0 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 + let level = level - 1 in + let link = Array.unsafe_get next level in + try_remove t key next level link (Atomic.get link) + else try_remove t key next level link (Atomic.get link) + +let try_remove t key = + match find_node t key with + | Null -> false + | Node { next; _ } -> + let level = Array.length next - 1 in + let link = Array.unsafe_get next level in + try_remove t key next level link (Atomic.get link) + +(* *) + +let length t = Size.get t.size diff --git a/src_lockfree/skiplist.mli b/src_lockfree/skiplist.mli index bc18575e..e6dad1e1 100644 --- a/src_lockfree/skiplist.mli +++ b/src_lockfree/skiplist.mli @@ -1,24 +1,42 @@ -(** Skiplist TODO +(** A lock-free skiplist. *) - [key] values are compared with [=] and thus should not be functions or - objects. -*) +type (!'k, !'v) t +(** The type of a lock-free skiplist containing bindings of keys of type ['k] to + values of type ['v]. *) -type 'a t -(** The type of lock-free skiplist. *) +val create : ?max_height:int -> compare:('k -> 'k -> int) -> unit -> ('k, 'v) t +(** [create ~compare ()] creates a new empty skiplist where keys are ordered + based on the given [compare] function. -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. *) + Note that the polymorphic [Stdlib.compare] function has relatively high + overhead and it is usually better to use a type specific [compare] function + such as [Int.compare] or [String.compare]. -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. *) + The optional [max_height] argument determines the maximum height of nodes in + the skiplist and directly affects the performance of the skiplist. The + current implementation does not adjust height automically. *) -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 max_height_of : ('k, 'v) t -> int +(** [max_height_of s] returns the maximum height of nodes of the skiplist [s] as + specified to {!create}. *) -val mem : 'a t -> 'a -> bool -(** [mem s v] returns [true] if v is in s and [false] otherwise. *) +val find_opt : ('k, 'v) t -> 'k -> 'v option +(** [find_opt s k] tries to find a binding of [k] to [v] from the skiplist [s] + and returns [Some v] in case such a binding was found or return [None] in + case no such binding was found. *) + +val mem : ('k, 'v) t -> 'k -> bool +(** [mem s k] determines whether the skiplist [s] contained a binding of [k]. *) + +val try_add : ('k, 'v) t -> 'k -> 'v -> bool +(** [try_add s k v] tries to add a new binding of [k] to [v] into the skiplist + [s] and returns [true] on success. Otherwise the skiplist already contained + a binding of [k] and [false] is returned. *) + +val try_remove : ('k, 'v) t -> 'k -> bool +(** [try_remove s k] tries to remove a binding of [k] from the skiplist and + returns [true] on success. Otherwise the skiplist did not contain a binding + of [k] and [false] is returned. *) + +val length : ('k, 'v) t -> int +(** [length s] computes the number of bindings in the skiplist [s]. *) diff --git a/test/skiplist/skiplist_dscheck.ml b/test/skiplist/dscheck_skiplist.ml similarity index 62% rename from test/skiplist/skiplist_dscheck.ml rename to test/skiplist/dscheck_skiplist.ml index 283ced0e..3ae8d4a5 100644 --- a/test/skiplist/skiplist_dscheck.ml +++ b/test/skiplist/dscheck_skiplist.ml @@ -1,15 +1,25 @@ open Skiplist +let test_max_height_of () = + let s = create ~max_height:1 ~compare () in + assert (max_height_of s = 1); + let s = create ~max_height:10 ~compare () in + assert (max_height_of s = 10); + let s = create ~max_height:30 ~compare () in + assert (max_height_of s = 30) + +let try_add s k = try_add s k () + let _two_mem () = Atomic.trace (fun () -> Random.init 0; - let sl = create ~max_height:2 () in + let sl = create ~max_height:2 ~compare:Int.compare () in let added1 = ref false in let found1 = ref false in let found2 = ref false in Atomic.spawn (fun () -> - added1 := add sl 1; + added1 := try_add sl 1; found1 := mem sl 1); Atomic.spawn (fun () -> found2 := mem sl 2); @@ -20,12 +30,12 @@ let _two_mem () = let _two_add () = Atomic.trace (fun () -> Random.init 0; - let sl = create ~max_height:3 () in + let sl = create ~max_height:3 ~compare:Int.compare () in let added1 = ref false in let added2 = ref false in - Atomic.spawn (fun () -> added1 := add sl 1); - Atomic.spawn (fun () -> added2 := add sl 2); + Atomic.spawn (fun () -> added1 := try_add sl 1); + Atomic.spawn (fun () -> added2 := try_add sl 2); Atomic.final (fun () -> Atomic.check (fun () -> !added1 && !added2 && mem sl 1 && mem sl 2))) @@ -33,12 +43,12 @@ let _two_add () = let _two_add_same () = Atomic.trace (fun () -> Random.init 0; - let sl = create ~max_height:3 () in + let sl = create ~max_height:3 ~compare:Int.compare () in let added1 = ref false in let added2 = ref false in - Atomic.spawn (fun () -> added1 := add sl 1); - Atomic.spawn (fun () -> added2 := add sl 1); + Atomic.spawn (fun () -> added1 := try_add sl 1); + Atomic.spawn (fun () -> added2 := try_add sl 1); Atomic.final (fun () -> Atomic.check (fun () -> @@ -48,15 +58,15 @@ let _two_add_same () = let _two_remove_same () = Atomic.trace (fun () -> Random.init 0; - let sl = create ~max_height:2 () in + let sl = create ~max_height:2 ~compare:Int.compare () in let added1 = ref false in let removed1 = ref false in let removed2 = ref false in Atomic.spawn (fun () -> - added1 := add sl 1; - removed1 := remove sl 1); - Atomic.spawn (fun () -> removed2 := remove sl 1); + added1 := try_add sl 1; + removed1 := try_remove sl 1); + Atomic.spawn (fun () -> removed2 := try_remove sl 1); Atomic.final (fun () -> Atomic.check (fun () -> @@ -67,15 +77,15 @@ let _two_remove_same () = let _two_remove () = Atomic.trace (fun () -> Random.init 0; - let sl = create ~max_height:2 () in + let sl = create ~max_height:2 ~compare:Int.compare () in let added1 = ref false in let removed1 = ref false in let removed2 = ref false in Atomic.spawn (fun () -> - added1 := add sl 1; - removed1 := remove sl 1); - Atomic.spawn (fun () -> removed2 := remove sl 2); + added1 := try_add sl 1; + removed1 := try_remove sl 1); + Atomic.spawn (fun () -> removed2 := try_remove sl 2); Atomic.final (fun () -> Atomic.check (fun () -> @@ -84,10 +94,11 @@ let _two_remove () = let () = let open Alcotest in - run "skiplist_dscheck" + run "DSCheck Skiplist" [ ( "basic", [ + test_case "max_height_of" `Quick test_max_height_of; test_case "2-mem" `Slow _two_mem; test_case "2-add-same" `Slow _two_add_same; test_case "2-add" `Slow _two_add; diff --git a/test/skiplist/dune b/test/skiplist/dune index 3ffaa883..4fd90697 100644 --- a/test/skiplist/dune +++ b/test/skiplist/dune @@ -1,22 +1,32 @@ (rule - (copy ../../src_lockfree/backoff.ml backoff.ml)) - -(rule - (copy ../../src_lockfree/skiplist.ml skiplist.ml)) + (action + (progn + (copy ../../src_lockfree/skiplist.ml skiplist.ml) + (copy ../../src_lockfree/size.ml size.ml))) + (package saturn_lockfree)) (test - (name skiplist_dscheck) - (libraries atomic dscheck alcotest) - (modules skiplist skiplist_dscheck)) + (package saturn_lockfree) + (name dscheck_skiplist) + (modules skiplist size dscheck_skiplist) + (libraries atomic transparent_atomic dscheck alcotest multicore-magic)) (test + (package saturn_lockfree) (name qcheck_skiplist) - (libraries saturn qcheck qcheck-alcotest) - (modules qcheck_skiplist)) + (modules qcheck_skiplist) + (libraries saturn qcheck qcheck-core qcheck-alcotest alcotest)) (test + (package saturn_lockfree) (name stm_skiplist) (modules stm_skiplist) - (libraries saturn qcheck-stm.sequential qcheck-stm.domain) + (libraries + saturn + qcheck-core + qcheck-core.runner + qcheck-stm.stm + qcheck-stm.sequential + qcheck-stm.domain) (action (run %{test} --verbose))) diff --git a/test/skiplist/qcheck_skiplist.ml b/test/skiplist/qcheck_skiplist.ml index bb89f799..6cb3b0e6 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 try_add s k = try_add s k () +end module IntSet = Set.Make (Int) @@ -13,11 +17,11 @@ let tests_sequential = [ (* TEST 1: add*) Test.make ~name:"add" (list int) (fun lpush -> - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let rec add_all_elems seen l = match l with | h :: t -> - if Skiplist.add sl h <> IntSet.mem h seen then + if Skiplist.try_add sl h <> IntSet.mem h seen then add_all_elems (IntSet.add h seen) t else false | [] -> true @@ -26,12 +30,12 @@ let tests_sequential = (*TEST 2: add_remove*) Test.make ~name:"add_remove" (list int) (fun lpush -> let lpush = uniq lpush in - let sl = Skiplist.create () in - List.iter (fun key -> ignore (Skiplist.add sl key)) lpush; + let sl = Skiplist.create ~compare:Int.compare () in + List.iter (fun key -> ignore (Skiplist.try_add sl key)) lpush; let rec remove_all_elems l = match l with | h :: t -> - if Skiplist.remove sl h then remove_all_elems t else false + if Skiplist.try_remove sl h then remove_all_elems t else false | [] -> true in remove_all_elems lpush); @@ -39,11 +43,11 @@ let tests_sequential = Test.make ~name:"add_find" (list int) (fun lpush -> let lpush = uniq lpush in let lpush = Array.of_list lpush in - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let len = Array.length lpush in let pos = Array.sub lpush 0 (len / 2) in let neg = Array.sub lpush (len / 2) (len / 2) in - Array.iter (fun key -> ignore @@ Skiplist.add sl key) pos; + Array.iter (fun key -> ignore @@ Skiplist.try_add sl key) pos; let rec check_pos index = if index < len / 2 then if Skiplist.mem sl pos.(index) then check_pos (index + 1) @@ -60,9 +64,9 @@ let tests_sequential = (* TEST 4: add_remove_find *) Test.make ~name:"add_remove_find" (list int) (fun lpush -> let lpush = uniq lpush in - let sl = Skiplist.create () in - List.iter (fun key -> ignore @@ Skiplist.add sl key) lpush; - List.iter (fun key -> ignore @@ Skiplist.remove sl key) lpush; + let sl = Skiplist.create ~compare:Int.compare () in + List.iter (fun key -> ignore @@ Skiplist.try_add sl key) lpush; + List.iter (fun key -> ignore @@ Skiplist.try_remove sl key) lpush; let rec not_find_all_elems l = match l with | h :: t -> @@ -79,14 +83,14 @@ let tests_two_domains = (* TEST 1: Two domains doing multiple adds *) Test.make ~name:"parallel_add" (pair small_nat small_nat) (fun (npush1, npush2) -> - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let sema = Semaphore.Binary.make false in let lpush1 = List.init npush1 (fun i -> i) in let lpush2 = List.init npush2 (fun i -> i + npush1) in let work lpush = List.map (fun elt -> - let completed = Skiplist.add sl elt in + let completed = Skiplist.try_add sl elt in Domain.cpu_relax (); completed) lpush @@ -114,7 +118,7 @@ let tests_two_domains = (* TEST 2: Two domains doing multiple one push and one pop in parallel *) Test.make ~count:10000 ~name:"parallel_add_remove" (pair small_nat small_nat) (fun (npush1, npush2) -> - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let sema = Semaphore.Binary.make false in let lpush1 = List.init npush1 (fun i -> i) in @@ -123,9 +127,9 @@ let tests_two_domains = let work lpush = List.map (fun elt -> - ignore @@ Skiplist.add sl elt; + ignore @@ Skiplist.try_add sl elt; Domain.cpu_relax (); - Skiplist.remove sl elt) + Skiplist.try_remove sl elt) lpush in @@ -152,10 +156,10 @@ let tests_two_domains = (* TEST 3: Parallel push and pop using the same elements in two domains *) Test.make ~name:"parallel_add_remove_same_list" (list int) (fun lpush -> - let sl = Skiplist.create () in + let sl = Skiplist.create ~compare:Int.compare () in let sema = Semaphore.Binary.make false in - let add_all_elems l = List.map (Skiplist.add sl) l in - let remove_all_elems l = List.map (Skiplist.remove sl) l in + let add_all_elems l = List.map (Skiplist.try_add sl) l in + let remove_all_elems l = List.map (Skiplist.try_remove sl) l in let domain1 = Domain.spawn (fun () -> @@ -185,7 +189,7 @@ let tests_two_domains = let () = let to_alcotest = List.map QCheck_alcotest.to_alcotest in - Alcotest.run "Skip List" + Alcotest.run "QCheck Skiplist" [ ("test_sequential", to_alcotest tests_sequential); ("tests_two_domains", to_alcotest tests_two_domains); diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml index 0831c4c9..0aab1c47 100644 --- a/test/skiplist/stm_skiplist.ml +++ b/test/skiplist/stm_skiplist.ml @@ -1,23 +1,25 @@ -(** Sequential and Parallel model-based tests of ws_deque *) - open QCheck open STM -module Skiplist = Saturn.Skiplist + +module Skiplist = struct + include Saturn.Skiplist + + type nonrec 'a t = ('a, unit) t + + let try_add s k = try_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,10 +32,11 @@ 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 - let init_sut () = Skiplist.create () + let init_sut () = Skiplist.create ~compare:Int.compare () let cleanup _ = () let next_state c s = @@ -41,20 +44,23 @@ module WSDConf = struct | Add i -> Sint.add i s | Remove i -> Sint.remove i s | Mem _ -> s + | Length -> s let precond _ _ = true let run c d = match c with - | Add i -> Res (bool, Skiplist.add d i) - | Remove i -> Res (bool, Skiplist.remove d i) + | Add i -> Res (bool, Skiplist.try_add d i) + | Remove i -> Res (bool, Skiplist.try_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