From 3a0f0fb359a8a21bdff25c610b8cec4252a3cbe5 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 2 Dec 2024 09:48:42 +0100 Subject: [PATCH 1/2] Priority queue. --- src/priority_queue.ml | 350 ++++++++++++++++++ src/priority_queue.mli | 49 +++ src/saturn.ml | 1 + src/saturn.mli | 1 + test/htbl/stm_htbl.ml | 33 -- test/priority_queue/dscheck_priority_queue.ml | 240 ++++++++++++ test/priority_queue/dune | 22 ++ test/priority_queue/stm_priority_queue.ml | 95 +++++ 8 files changed, 758 insertions(+), 33 deletions(-) create mode 100644 src/priority_queue.ml create mode 100644 src/priority_queue.mli create mode 100644 test/priority_queue/dscheck_priority_queue.ml create mode 100644 test/priority_queue/dune create mode 100644 test/priority_queue/stm_priority_queue.ml diff --git a/src/priority_queue.ml b/src/priority_queue.ml new file mode 100644 index 00000000..51e81f97 --- /dev/null +++ b/src/priority_queue.ml @@ -0,0 +1,350 @@ +(* Copyright (c) 2024 Carine Morel + + 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. + + 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. *) + +(* Based on the skiplist implementation written by Vesa Karvonen. *) + +module Atomic = Multicore_magic.Transparent_atomic + +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 + +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] search fo the position after all the + nodes with key [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; + 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) + | 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 + (* key >= r.key *) + 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 then begin + if r.incr != Size.used_once then begin + Size.update_once t.size r.incr; + r.incr <- Size.used_once + end; + () (* Return *) + end + 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 first 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 ?timestamp 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 ~timestamp key prev prev_at_level level + (Atomic.get prev_at_level) + +and find_node_rec t ~timestamp 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 ~timestamp 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 ~timestamp key r.next next_at_level level next + else if 0 < level then + let level = level - 1 in + let prev_at_level = Array.unsafe_get prev level in + find_node_rec t ~timestamp key prev prev_at_level level + (Atomic.get prev_at_level) + else if c = 0 then begin + if r.incr != Size.used_once then begin + Size.update_once t.size r.incr; + r.incr <- Size.used_once + end; + curr + end + else Null + | Link (Mark r) -> + if level = 0 then Size.update_once t.size r.decr; + find_node_rec t ~timestamp 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 rec add t key value preds succs = + 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 + 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 : unit = + 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 + 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 _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_path t key preds succs level + in + update_nexts (Array.length r.next - 1) + in + update_levels 1 + end + else add t key value preds succs + +let add t key value : unit = + 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 + add t key value preds succs + +(* *) + +let length t = Size.get t.size + +(* *) + +let rec find_min t : (_, _, [< `Node | `Null ]) node = + let root = t.root in + let root_at_level0 = Array.unsafe_get root 0 in + match Atomic.get root_at_level0 with + | Link (Mark _) -> assert false + | Link Null -> Null + | Link (Node r) as curr_link -> ( + let next_at_level_0 = Array.unsafe_get r.next 0 in + match Atomic.get next_at_level_0 with + | Link (Null | Node _) -> Node r + | Link (Mark next_marked) -> + Size.update_once t.size next_marked.decr; + if + Atomic.compare_and_set root_at_level0 curr_link + (Link next_marked.node) + then find_min t + else find_min t) + +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 marked_succ = Mark { node = succ; decr } in + if Atomic.compare_and_set link (Link succ) (Link marked_succ) then + if level = 0 then + 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 remove_min_opt t = + let rec loop t = + match find_min t with + | Null -> None + | Node { next; key; value; _ } -> + let level = Array.length next - 1 in + let link = Array.unsafe_get next level in + if try_remove t key next level link (Atomic.get link) then + Some (key, value) + else loop t + in + loop t diff --git a/src/priority_queue.mli b/src/priority_queue.mli new file mode 100644 index 00000000..165d8719 --- /dev/null +++ b/src/priority_queue.mli @@ -0,0 +1,49 @@ +(** A lock-free priority queue. + + This is based on a fixed-sized skiplist implementation: + - add operations have an average logarithmic complexity as long as the + number of elements in it is less than `2^max_height`. Passed that, + performance will decrease. + + - remove operations (with `remove_min_opt`) have a o(1) complexity. *) + +type (!'p, !'v) t +(** The type of a lock-free priority queue containing elements of type [`v] + bound to priority of type ['p]. *) + +val create : ?max_height:int -> compare:('p -> 'p -> int) -> unit -> ('p, 'v) t +(** [create ~compare ()] creates a new empty priority queue where prioriries are + ordered based on the given [compare] function. + + 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]. + + The implementation is based on a skiplist. The optional [max_height] + argument determines the maximum height of nodes in the skiplist and directly + affects the performance of the data structure. The current implementation + does not adjust height automatically. *) + +val max_height_of : ('p, 'v) t -> int +(** [max_height_of pq] returns the maximum height of nodes of the priority queue + [pq] as specified to {!create}. + + The maximum number of elements that the prioriry queue can contain before, + statistically, the performance decreases is `2^(max_height)`. *) + +val add : ('p, 'v) t -> 'p -> 'v -> unit +(** [add pq p v] adds a new element [v] with priority [p] into the priority + queue [pq] skiplist [s] and returns [true] on success. *) + +val remove_min_opt : ('p, 'v) t -> ('p * 'v) option +(** [remove_min_opt s] removes and returns [Some] of the element with the + smallest priority from the priority queue [pq]. If the priority queue [pq] + was empty [None] is returned. The elements with the same priority are + removed in fifo order. *) + +val length : ('k, 'v) t -> int +(** [length pq] computes and returns the number of elements in the priority + queue [pq]. + + This function is not linearizable and should only be used to get an + indication of the size of [pq]. *) diff --git a/src/saturn.ml b/src/saturn.ml index ab250c6b..a9bed7d2 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -41,3 +41,4 @@ module Skiplist = Skiplist module Htbl = Htbl module Htbl_unsafe = Htbl_unsafe module Bag = Bag +module Priority_queue = Priority_queue diff --git a/src/saturn.mli b/src/saturn.mli index 93850d43..cfaba66b 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -83,6 +83,7 @@ module Bounded_queue_unsafe = Bounded_queue_unsafe module Single_consumer_queue = Mpsc_queue module Single_prod_single_cons_queue = Spsc_queue module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe +module Priority_queue = Priority_queue (** {2 Stacks} *) diff --git a/test/htbl/stm_htbl.ml b/test/htbl/stm_htbl.ml index 0ec646a0..e313407b 100644 --- a/test/htbl/stm_htbl.ml +++ b/test/htbl/stm_htbl.ml @@ -161,39 +161,6 @@ module STM_htbl (Htbl : Htbls.Htbl_tests) = struct end let run () = Stm_run.run ~name:"Htbl" (module Spec) |> exit - - (* let test () = - let open Htbl in - let h = create ~hashed_type:(module Int) () in - let t1 = try_add h 1 1 in - let t2 = try Some (set_exn h 1 2) with Not_found -> None in - let t3 = try_add h 1 1 in - let t4 = try Some (set_exn h 1 3) with Not_found -> None in - (t1, t2, t3, t4) - - let test_m () = - let module State = Map.Make (Int) in - let m = State.empty in - let t1 = State.mem 1 m in - let m = State.add 1 1 m in - let t2 = State.find_opt 1 m in - let m = State.add 1 2 m in - let t3 = State.mem 1 m in - let m = if t3 then m else State.add 1 1 m in - let t4 = State.find_opt 1 m in - (t1, t2, t3, t4) - - let run test n = - let count = ref 0 in - let res = ref [] in - let expected = (true, Some 1, false, Some 2) in - for _ = 1 to n do - let r = test () in - if r <> expected then ( - res := r :: !res; - incr count) - done; - (!count, !res) *) end let () = diff --git a/test/priority_queue/dscheck_priority_queue.ml b/test/priority_queue/dscheck_priority_queue.ml new file mode 100644 index 00000000..3502d2b4 --- /dev/null +++ b/test/priority_queue/dscheck_priority_queue.ml @@ -0,0 +1,240 @@ +open Priority_queue + +module Atomic = Dscheck.TracedAtomic +(** This is needed in this order as the priority_queue.ml file contains + {[ + module Atomic = Multicore_magic.Transparent_atomic + ]} + which is in multicore-magic-dscheck library only a subset of + [Dscheck.TracedAtomic] function. *) + +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 _two_add () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:3 ~compare:Int.compare () in + + Atomic.spawn (fun () -> add pq 1 1); + Atomic.spawn (fun () -> add pq 2 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + let r1 = remove_min_opt pq in + let r2 = remove_min_opt pq in + r1 = Some (1, 1) && r2 = Some (2, 2)))) + +let _two_add_same () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:3 ~compare:Int.compare () in + + Atomic.spawn (fun () -> add pq 1 1); + Atomic.spawn (fun () -> add pq 1 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + let r1 = remove_min_opt pq in + let r2 = remove_min_opt pq in + (r1 = Some (1, 1) && r2 = Some (1, 2)) + || (r2 = Some (1, 1) && r1 = Some (1, 2))))) + +let _two_remove () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:2 ~compare:Int.compare () in + let removed1 = ref None in + let removed2 = ref None in + + Atomic.spawn (fun () -> + add pq 1 1; + removed1 := remove_min_opt pq); + + Atomic.spawn (fun () -> removed2 := remove_min_opt pq); + + Atomic.final (fun () -> + Atomic.check (fun () -> + match (!removed1, !removed2) with + | None, Some (1, 1) | Some (1, 1), None -> true + | _ -> false); + Atomic.check (fun () -> remove_min_opt pq = None))) + +let _two_remove2 () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:2 ~compare:Int.compare () in + let removed1 = ref None in + let removed2 = ref None in + let removed3 = ref None in + add pq 1 1; + + Atomic.spawn (fun () -> removed1 := remove_min_opt pq); + + Atomic.spawn (fun () -> + removed2 := remove_min_opt pq; + removed3 := remove_min_opt pq); + + Atomic.final (fun () -> + Atomic.check (fun () -> !removed3 = None); + Atomic.check (fun () -> + match (!removed1, !removed2) with + | None, Some (1, 1) | Some (1, 1), None -> true + | _ -> false); + Atomic.check (fun () -> remove_min_opt pq = None))) + +let _two_remove_fifo () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:2 ~compare:Int.compare () in + let removed1 = ref None in + let removed2 = ref None in + + Atomic.spawn (fun () -> + removed1 := remove_min_opt pq; + removed2 := remove_min_opt pq); + Atomic.spawn (fun () -> + add pq 1 1; + add pq 2 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + let r1 = remove_min_opt pq in + let r2 = remove_min_opt pq in + match (!removed1, !removed2) with + | None, None -> r1 = Some (1, 1) && r2 = Some (2, 2) + | Some (1, 1), None | None, Some (1, 1) -> + r1 = Some (2, 2) && r2 = None + | Some (1, 1), Some (2, 2) -> r1 = None && r2 = None + | _ -> false))) + +let _two_remove_add () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:2 ~compare:Int.compare () in + let removed1 = ref None in + + Atomic.spawn (fun () -> + add pq 1 1; + removed1 := remove_min_opt pq); + Atomic.spawn (fun () -> add pq 1 2); + + Atomic.final (fun () -> + Atomic.check (fun () -> + (!removed1 = Some (1, 1) && remove_min_opt pq = Some (1, 2)) + || (!removed1 = Some (1, 2) && remove_min_opt pq = Some (1, 1))))) + +let _two_remove_add2 () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:2 ~compare:Int.compare () in + let removed1 = ref None in + + Atomic.spawn (fun () -> + add pq 2 2; + removed1 := remove_min_opt pq); + + Atomic.spawn (fun () -> add pq 1 1); + + Atomic.final (fun () -> + Atomic.check (fun () -> length pq = 1); + Atomic.check (fun () -> + (!removed1 = Some (1, 1) && remove_min_opt pq = Some (2, 2)) + || (!removed1 = Some (2, 2) && remove_min_opt pq = Some (1, 1))))) + +let _two_remove_add3 () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:1 ~compare:Int.compare () in + let removed1 = ref None in + let removed2 = ref None in + let removed3 = ref None in + + add pq 2 2; + add pq 2 10; + + Atomic.spawn (fun () -> removed1 := remove_min_opt pq); + Atomic.spawn (fun () -> + add pq 4 10; + removed2 := remove_min_opt pq; + removed3 := remove_min_opt pq); + + Atomic.final (fun () -> + Atomic.check (fun () -> !removed2 != None && !removed3 != None); + Atomic.check (fun () -> + (!removed1 != None && length pq = 0) + || !removed1 = None + && length pq = 1 + && remove_min_opt pq = Some (4, 10)))) + +let _two_remove_add4 () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:1 ~compare:Int.compare () in + let removed1 = ref None in + let removed2 = ref None in + add pq 2 2; + + Atomic.spawn (fun () -> + add pq 1 1; + removed1 := remove_min_opt pq); + + Atomic.spawn (fun () -> + add pq 0 0; + removed2 := remove_min_opt pq); + + Atomic.final (fun () -> + Atomic.check (fun () -> + length pq = 1 + && + match (!removed1, !removed2) with + | Some (1, 1), Some (0, 0) -> remove_min_opt pq = Some (2, 2) + | Some (0, 0), Some (1, 1) -> remove_min_opt pq = Some (2, 2) + | _ -> false))) + +(* length is not linearisable, this test is not working. *) +(* let _two_add_remove_length () = + Atomic.trace (fun () -> + Random.init 0; + let pq = create ~max_height:1 ~compare:Int.compare () in + let removed1 = ref None in + let len = ref 0 in + add pq 2 2; + + Atomic.spawn (fun () -> + add pq 1 1; + len := length pq); + + Atomic.spawn (fun () -> removed1 := remove_min_opt pq); + + Atomic.final (fun () -> + Atomic.check (fun () -> + match (!removed1, remove_min_opt pq) with + | Some (2, 2), Some (1, 1) -> !len = 1 + | Some (1, 1), Some (2, 2) -> !len = 2 || !len = 1 + | _ -> false))) *) + +let () = + let open Alcotest in + run "DSCheck_Skiplist" + [ + ( "basic", + [ + test_case "max_height_of" `Quick _test_max_height_of; + test_case "2-add-same" `Slow _two_add_same; + test_case "2-add" `Slow _two_add; + test_case "2-remove" `Slow _two_remove; + test_case "2-remove2" `Slow _two_remove2; + test_case "2-remove-fifo" `Slow _two_remove_fifo; + test_case "2-remove-add" `Slow _two_remove_add; + test_case "2-remove-add2" `Slow _two_remove_add2; + test_case "2-remove-add3" `Slow _two_remove_add3; + test_case "2-remove-add4" `Slow _two_remove_add4; + (* test_case "2-length" `Slow _two_add_remove_length; *) + ] ); + ] diff --git a/test/priority_queue/dune b/test/priority_queue/dune new file mode 100644 index 00000000..7a758610 --- /dev/null +++ b/test/priority_queue/dune @@ -0,0 +1,22 @@ +(rule + (action + (progn + (copy ../../src/priority_queue.ml priority_queue.ml) + (copy ../../src/size.ml size.ml))) + (package saturn)) + +(test + (package saturn) + (name dscheck_priority_queue) + (modules priority_queue size dscheck_priority_queue) + (build_if + (>= %{ocaml_version} 5)) + (libraries alcotest dscheck multicore-magic-dscheck) + (flags + (:standard -open Multicore_magic_dscheck))) + +(test + (package saturn) + (name stm_priority_queue) + (modules stm_priority_queue) + (libraries saturn qcheck-core qcheck-stm.stm stm_run)) diff --git a/test/priority_queue/stm_priority_queue.ml b/test/priority_queue/stm_priority_queue.ml new file mode 100644 index 00000000..9ccc4b54 --- /dev/null +++ b/test/priority_queue/stm_priority_queue.ml @@ -0,0 +1,95 @@ +open QCheck +open STM +module Priority_queue = Saturn.Priority_queue + +module Spec = struct + type cmd = Add of int * int | Remove_min + (* | Find of int *) + (* | Length *) + + let show_cmd c = + match c with + | Add (i, k) -> "Add (" ^ string_of_int i ^ ", " ^ string_of_int k ^ ")" + | Remove_min -> "Remove_min" + (* | Length -> "Length" *) + (* | Find i -> "Find " ^ string_of_int i *) + + module Mint = Map.Make (Int) + + type state = int * int list Mint.t + type sut = (int, int) Priority_queue.t + + let arb_cmd _s = + let priority_gen = Gen.int_bound 5 in + let val_gen = Gen.int_bound 20 in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map2 (fun p i -> Add (p, i)) priority_gen val_gen; + (* Gen.map (fun p -> Find p) priority_gen; *) + Gen.return Remove_min; + (* Gen.return Length; *) + ]) + + let init_state = (0, Mint.empty) + let init_sut () = Priority_queue.create ~compare:Int.compare () + let cleanup _ = () + + let next_state c ((len, s) : state) = + match c with + | Add (p, i) -> + ( len + 1, + begin + match Mint.find_opt p s with + | None -> Mint.add p [ i ] s + | Some l -> Mint.add p (i :: List.rev l |> List.rev) s + end ) + | Remove_min -> ( + let bindings = Mint.bindings s in + match bindings with + | [] -> (len, s) + | (p, values) :: _ -> + ( len - 1, + let s = Mint.remove p s in + match values with + | [] -> assert false + | [ _x ] -> s + | _ :: values -> Mint.add p values s ) + (* | Find _ -> s *)) + (* | Length -> (len, s) *) + + let precond _ _ = true + + let run c d = + match c with + | Add (p, i) -> Res (unit, Priority_queue.add d p i) + | Remove_min -> + Res + ( list int, + match Priority_queue.remove_min_opt d with + | None -> [] + | Some (p, v) -> [ p; v ] ) + (* | Find i -> Res (option int, Priority_queue.find_opt d i) *) + (* | Length -> Res (int, Priority_queue.length d) *) + + let postcond c ((_, s) : state) res = + match (c, res) with + | Add (_, _), Res ((Unit, _), ()) -> true + | Remove_min, Res ((List Int, _), res) -> begin + match Mint.bindings s with + | [] -> res = [] + | (p, values) :: _ -> begin + match values with [] -> assert false | v :: _ -> res = [ p; v ] + end + end + (* | Length, Res ((Int, _), res) -> len = res *) + (* | Find p, Res ((Option Int, _), res) -> begin + match Mint.find_opt p s with + | None -> res = None + | Some (x :: _) -> res = Some x + | _ -> false + end *) + | _, _ -> false +end + +let () = Stm_run.run ~name:"Saturn.Priority_queue" (module Spec) |> exit From 78c36ab38bae52955c3d5aa16464b63627f0961f Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Mon, 6 Jan 2025 15:26:55 +0100 Subject: [PATCH 2/2] Add remove_min_exn function. --- src/priority_queue.ml | 28 ++++++++++++++++------------ src/priority_queue.mli | 11 ++++++++++- 2 files changed, 26 insertions(+), 13 deletions(-) diff --git a/src/priority_queue.ml b/src/priority_queue.ml index 51e81f97..f4c899c3 100644 --- a/src/priority_queue.ml +++ b/src/priority_queue.ml @@ -44,6 +44,7 @@ type 'k compare = 'k -> 'k -> int type ('k, 'v) t = { compare : 'k compare; root : ('k, 'v) links; size : Size.t } +exception Empty (* *) (** [get_random_height max_height] gives a random value [n] in the range from @@ -293,6 +294,8 @@ let length t = Size.get t.size (* *) +type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly + let rec find_min t : (_, _, [< `Node | `Null ]) node = let root = t.root in let root_at_level0 = Array.unsafe_get root 0 in @@ -336,15 +339,16 @@ let rec try_remove t key next level link = function try_remove t key next level link (Atomic.get link) else try_remove t key next level link (Atomic.get link) -let remove_min_opt t = - let rec loop t = - match find_min t with - | Null -> None - | Node { next; key; value; _ } -> - let level = Array.length next - 1 in - let link = Array.unsafe_get next level in - if try_remove t key next level link (Atomic.get link) then - Some (key, value) - else loop t - in - loop t +let rec remove_min_as : type p v r. (p, v) t -> (p * v, r) poly -> r = + fun t poly -> + match find_min t with + | Null -> ( match poly with Value -> raise Empty | Option -> None) + | Node { next; key; value; _ } -> + let level = Array.length next - 1 in + let link = Array.unsafe_get next level in + if try_remove t key next level link (Atomic.get link) then + match poly with Value -> (key, value) | Option -> Some (key, value) + else remove_min_as t poly + +let remove_min_opt t = remove_min_as t Option +let remove_min_exn t = remove_min_as t Value diff --git a/src/priority_queue.mli b/src/priority_queue.mli index 165d8719..2c66fe79 100644 --- a/src/priority_queue.mli +++ b/src/priority_queue.mli @@ -38,9 +38,18 @@ val add : ('p, 'v) t -> 'p -> 'v -> unit val remove_min_opt : ('p, 'v) t -> ('p * 'v) option (** [remove_min_opt s] removes and returns [Some] of the element with the smallest priority from the priority queue [pq]. If the priority queue [pq] - was empty [None] is returned. The elements with the same priority are + was empty, [None] is returned. The elements with the same priority are removed in fifo order. *) +exception Empty + +val remove_min_exn : ('p, 'v) t -> 'p * 'v +(** [remove_min_exn s] removes and returns the element with the smallest + priority from the priority queue [pq]. The elements with the same priority + are removed in fifo order. + + @raise Empty if the priority queue [pq] is empty.*) + val length : ('k, 'v) t -> int (** [length pq] computes and returns the number of elements in the priority queue [pq].