From 6922c6dc13f23a8b8715fb5ed3820f6f5b05d6f1 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 14 Nov 2024 11:36:47 +0100 Subject: [PATCH 01/19] Bounded queue --- src/cue/cue.ml | 149 +++++++++++++++++++++++++++++++++++++++++ src/cue/cue.mli | 1 + src/cue/cue_intf.mli | 50 ++++++++++++++ src/cue/cue_unsafe.ml | 149 +++++++++++++++++++++++++++++++++++++++++ src/cue/cue_unsafe.mli | 1 + src/dune | 2 +- src/saturn.ml | 1 + src/saturn.mli | 4 ++ 8 files changed, 356 insertions(+), 1 deletion(-) create mode 100644 src/cue/cue.ml create mode 100644 src/cue/cue.mli create mode 100644 src/cue/cue_intf.mli create mode 100644 src/cue/cue_unsafe.ml create mode 100644 src/cue/cue_unsafe.mli diff --git a/src/cue/cue.ml b/src/cue/cue.ml new file mode 100644 index 00000000..06e5ae28 --- /dev/null +++ b/src/cue/cue.ml @@ -0,0 +1,149 @@ +(* Copyright (c) 2023-2024, Vesa Karvonen + 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. *) + +module Atomic = Multicore_magic.Transparent_atomic + +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + mutable _next : 'a link; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" + +external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t + = "%identity" + +let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity + +let[@inline] set_capacity (Node r : (_, [< `Node ]) node) value = + r.capacity <- value + +let[@inline] get_counter (Node r : (_, [< `Node ]) node) = r.counter + +let[@inline] set_counter (Node r : (_, [< `Node ]) node) value = + r.counter <- value + +let[@inline] get_next node = Atomic.get (next_as_atomic node) + +let[@inline] fenceless_get_next node = + Atomic.fenceless_get (next_as_atomic node) + +let[@inline] compare_and_set_next node before after = + Atomic.compare_and_set (next_as_atomic node) before after + +type 'a t = { + head : ('a, [ `Node ]) node Atomic.t; + capacity : int; + tail : ('a, [ `Node ]) node Atomic.t; +} + +let create ?(capacity = Int.max_int) () = + let value = Obj.magic () in + let node = Node { _next = Link Null; value; capacity; counter = 0 } in + let head = Atomic.make node |> Multicore_magic.copy_as_padded + and tail = Atomic.make node |> Multicore_magic.copy_as_padded in + { head; capacity; tail } |> Multicore_magic.copy_as_padded + +let capacity_of t = t.capacity + +let is_empty t = + let head = Atomic.get t.head in + fenceless_get_next head == Link Null + +let rec snapshot t = + let head = Atomic.get t.head in + let tail = Atomic.fenceless_get t.tail in + match fenceless_get_next tail with + | Link (Node _ as node) -> + Atomic.compare_and_set t.tail tail node |> ignore; + snapshot t + | Link Null -> if Atomic.get t.head != head then snapshot t else (head, tail) + +let length t = + let head, tail = snapshot t in + get_counter tail - get_counter head + +(* *) + +let rec peek_opt t = + let head = Atomic.get t.head in + match fenceless_get_next head with + | Link Null -> None + | Link (Node r) -> + let value = r.value in + if Atomic.get t.head != head then peek_opt t else Some value + +(* *) + +let rec pop_opt t backoff = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> None + | Link (Node node as new_head) -> + if Atomic.compare_and_set t.head old_head new_head then begin + let value = node.value in + node.value <- Obj.magic (); + Some value + end + else pop_opt t (Backoff.once backoff) + +(* *) + +let rec fix_tail tail new_tail = + let old_tail = Atomic.get tail in + if + get_next new_tail == Link Null + && not (Atomic.compare_and_set tail old_tail new_tail) + then fix_tail tail new_tail + +(* *) + +let rec try_push t new_node old_tail = + let capacity = get_capacity old_tail in + if capacity = 0 then + let old_head = Atomic.get t.head in + let length = get_counter old_tail - get_counter old_head in + let capacity = t.capacity - length in + 0 < capacity + && begin + set_capacity old_tail capacity; + try_push t new_node old_tail + end + else begin + set_capacity new_node (capacity - 1); + set_counter new_node (get_counter old_tail + 1); + if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then + try_push t new_node (link_as_node (get_next old_tail)) + else begin + if not (Atomic.compare_and_set t.tail old_tail new_node) then + fix_tail t.tail new_node; + true + end + end + +(* *) + +let[@inline] pop_opt t = pop_opt t Backoff.default + +let[@inline] try_push t value = + let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + try_push t new_node (Atomic.get t.tail) diff --git a/src/cue/cue.mli b/src/cue/cue.mli new file mode 100644 index 00000000..fadb8e1f --- /dev/null +++ b/src/cue/cue.mli @@ -0,0 +1 @@ +include Cue_intf.CUE diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli new file mode 100644 index 00000000..10895114 --- /dev/null +++ b/src/cue/cue_intf.mli @@ -0,0 +1,50 @@ +(* Copyright (c) 2023-2024, Vesa Karvonen + 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. *) + +module type CUE = sig + (** Lock-free bounded queue. *) + + type !'a t + (** *) + + val create : ?capacity:int -> unit -> 'a t + (** *) + + val capacity_of : 'a t -> int + (** *) + + val is_empty : 'a t -> bool + (** *) + + val length : 'a t -> int + (** *) + + val peek_opt : 'a t -> 'a option + (** *) + + val pop_opt : 'a t -> 'a option + (** *) + + val try_push : 'a t -> 'a -> bool + (** *) + + (* +val to_list : 'a t -> 'a list +(** *) + +val transfer : 'a t -> 'a t +(** *) +*) +end diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml new file mode 100644 index 00000000..06e5ae28 --- /dev/null +++ b/src/cue/cue_unsafe.ml @@ -0,0 +1,149 @@ +(* Copyright (c) 2023-2024, Vesa Karvonen + 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. *) + +module Atomic = Multicore_magic.Transparent_atomic + +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + mutable _next : 'a link; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" + +external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t + = "%identity" + +let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity + +let[@inline] set_capacity (Node r : (_, [< `Node ]) node) value = + r.capacity <- value + +let[@inline] get_counter (Node r : (_, [< `Node ]) node) = r.counter + +let[@inline] set_counter (Node r : (_, [< `Node ]) node) value = + r.counter <- value + +let[@inline] get_next node = Atomic.get (next_as_atomic node) + +let[@inline] fenceless_get_next node = + Atomic.fenceless_get (next_as_atomic node) + +let[@inline] compare_and_set_next node before after = + Atomic.compare_and_set (next_as_atomic node) before after + +type 'a t = { + head : ('a, [ `Node ]) node Atomic.t; + capacity : int; + tail : ('a, [ `Node ]) node Atomic.t; +} + +let create ?(capacity = Int.max_int) () = + let value = Obj.magic () in + let node = Node { _next = Link Null; value; capacity; counter = 0 } in + let head = Atomic.make node |> Multicore_magic.copy_as_padded + and tail = Atomic.make node |> Multicore_magic.copy_as_padded in + { head; capacity; tail } |> Multicore_magic.copy_as_padded + +let capacity_of t = t.capacity + +let is_empty t = + let head = Atomic.get t.head in + fenceless_get_next head == Link Null + +let rec snapshot t = + let head = Atomic.get t.head in + let tail = Atomic.fenceless_get t.tail in + match fenceless_get_next tail with + | Link (Node _ as node) -> + Atomic.compare_and_set t.tail tail node |> ignore; + snapshot t + | Link Null -> if Atomic.get t.head != head then snapshot t else (head, tail) + +let length t = + let head, tail = snapshot t in + get_counter tail - get_counter head + +(* *) + +let rec peek_opt t = + let head = Atomic.get t.head in + match fenceless_get_next head with + | Link Null -> None + | Link (Node r) -> + let value = r.value in + if Atomic.get t.head != head then peek_opt t else Some value + +(* *) + +let rec pop_opt t backoff = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> None + | Link (Node node as new_head) -> + if Atomic.compare_and_set t.head old_head new_head then begin + let value = node.value in + node.value <- Obj.magic (); + Some value + end + else pop_opt t (Backoff.once backoff) + +(* *) + +let rec fix_tail tail new_tail = + let old_tail = Atomic.get tail in + if + get_next new_tail == Link Null + && not (Atomic.compare_and_set tail old_tail new_tail) + then fix_tail tail new_tail + +(* *) + +let rec try_push t new_node old_tail = + let capacity = get_capacity old_tail in + if capacity = 0 then + let old_head = Atomic.get t.head in + let length = get_counter old_tail - get_counter old_head in + let capacity = t.capacity - length in + 0 < capacity + && begin + set_capacity old_tail capacity; + try_push t new_node old_tail + end + else begin + set_capacity new_node (capacity - 1); + set_counter new_node (get_counter old_tail + 1); + if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then + try_push t new_node (link_as_node (get_next old_tail)) + else begin + if not (Atomic.compare_and_set t.tail old_tail new_node) then + fix_tail t.tail new_node; + true + end + end + +(* *) + +let[@inline] pop_opt t = pop_opt t Backoff.default + +let[@inline] try_push t value = + let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + try_push t new_node (Atomic.get t.tail) diff --git a/src/cue/cue_unsafe.mli b/src/cue/cue_unsafe.mli new file mode 100644 index 00000000..fadb8e1f --- /dev/null +++ b/src/cue/cue_unsafe.mli @@ -0,0 +1 @@ +include Cue_intf.CUE diff --git a/src/dune b/src/dune index edec87ee..94830efa 100644 --- a/src/dune +++ b/src/dune @@ -12,7 +12,7 @@ let () = (library (name saturn) (public_name saturn) - (modules_without_implementation htbl_intf) + (modules_without_implementation htbl_intf cue_intf) (libraries backoff multicore-magic |} ^ maybe_threads ^ {| )) diff --git a/src/saturn.ml b/src/saturn.ml index 7da90e4d..168bf45e 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -28,6 +28,7 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe +module Cue = Cue module Stack = Treiber_stack module Bounded_stack = Bounded_stack module Work_stealing_deque = Ws_deque diff --git a/src/saturn.mli b/src/saturn.mli index 52f9f821..4b049907 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -33,7 +33,11 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe module Stack = Treiber_stack +<<<<<<< HEAD module Bounded_stack = Bounded_stack +======= +module Cue = Cue +>>>>>>> 57f7acb (Bounded queue) module Work_stealing_deque = Ws_deque module Single_prod_single_cons_queue = Spsc_queue module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe From a9f975f96ba7416265af0cb2164beb138e5c3cf7 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 14 Nov 2024 14:35:54 +0100 Subject: [PATCH 02/19] Stm tests. --- test/cue/cues/cues.ml | 17 +++++++++++ test/cue/cues/dune | 8 +++++ test/cue/dune | 7 +++++ test/cue/stm_cue.ml | 69 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 101 insertions(+) create mode 100644 test/cue/cues/cues.ml create mode 100644 test/cue/cues/dune create mode 100644 test/cue/dune create mode 100644 test/cue/stm_cue.ml diff --git a/test/cue/cues/cues.ml b/test/cue/cues/cues.ml new file mode 100644 index 00000000..50fdc185 --- /dev/null +++ b/test/cue/cues/cues.ml @@ -0,0 +1,17 @@ +module type Cue_tests = sig + include Cue_intf.CUE + + val name : string +end + +module Cue : Cue_tests = struct + include Saturn.Cue + + let name = "htbl_safe" +end + +(* module Cue_unsafe : Cue_tests = struct + include Saturn.Cue_unsafe + + let name = "htbl_unsafe" + end *) diff --git a/test/cue/cues/dune b/test/cue/cues/dune new file mode 100644 index 00000000..28c6066d --- /dev/null +++ b/test/cue/cues/dune @@ -0,0 +1,8 @@ +(rule + (action + (copy ../../../src/cue/cue_intf.mli cue_intf.ml)) + (package saturn)) + +(library + (name cues) + (libraries saturn)) diff --git a/test/cue/dune b/test/cue/dune new file mode 100644 index 00000000..39a416b2 --- /dev/null +++ b/test/cue/dune @@ -0,0 +1,7 @@ +(test + (package saturn) + (name stm_cue) + (modules stm_cue) + (libraries cues saturn qcheck-core qcheck-stm.stm stm_run) + (enabled_if + (= %{arch_sixtyfour} true))) diff --git a/test/cue/stm_cue.ml b/test/cue/stm_cue.ml new file mode 100644 index 00000000..1d65f186 --- /dev/null +++ b/test/cue/stm_cue.ml @@ -0,0 +1,69 @@ +(** Sequential and Parallel model-based tests of (bounded queue) cue. *) + +open QCheck +open STM +module Cue = Saturn.Cue + +module Spec = struct + type cmd = Try_push of int | Pop_opt | Peek_opt | Length | Is_empty + + let show_cmd c = + match c with + | Try_push i -> "Try_push " ^ string_of_int i + | Pop_opt -> "Pop_opt" + | Peek_opt -> "Peek_opt" + | Length -> "Length" + | Is_empty -> "Is_empty" + + type state = int * int * int list + type sut = int Cue.t + + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map (fun i -> Try_push i) int_gen; + Gen.return Pop_opt; + Gen.return Peek_opt; + Gen.return Length; + Gen.return Is_empty; + ]) + + let init_state = (100, 0, []) + let init_sut () = Cue.create ~capacity:100 () + let cleanup _ = () + + let next_state c ((capacity, size, content) as s) = + match c with + | Try_push i -> + if size = capacity then s else (capacity, size + 1, i :: content) + | Pop_opt -> ( + match List.rev content with + | [] -> s + | _ :: content' -> (capacity, size - 1, List.rev content')) + | Peek_opt -> s + | Is_empty -> s + | Length -> s + + let precond _ _ = true + + let run c d = + match c with + | Try_push i -> Res (bool, Cue.try_push d i) + | Pop_opt -> Res (option int, Cue.pop_opt d) + | Peek_opt -> Res (option int, Cue.peek_opt d) + | Is_empty -> Res (bool, Cue.is_empty d) + | Length -> Res (int, Cue.length d) + + let postcond c ((capacity, size, content) : state) res = + match (c, res) with + | Try_push _, Res ((Bool, _), res) -> res = (size < capacity) + | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( + match List.rev content with [] -> res = None | j :: _ -> res = Some j) + | Is_empty, Res ((Bool, _), res) -> res = (content = []) + | Length, Res ((Int, _), res) -> res = size + | _, _ -> false +end + +let () = Stm_run.run ~name:"Saturn_lockfree.Cue" (module Spec) |> exit From e7be87c98b59b37a604d28c7b56245257dc06829 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 15 Nov 2024 15:40:20 +0100 Subject: [PATCH 03/19] Add of_list function. --- src/cue/cue.ml | 133 ++++++++++++++++++++++++++----------- src/cue/cue_intf.mli | 148 +++++++++++++++++++++++++++++++++++++----- src/cue/cue_unsafe.ml | 78 +++++++++++++++++++--- src/saturn.ml | 1 + src/saturn.mli | 4 +- test/cue/cues/cues.ml | 10 +-- test/cue/stm_cue.ml | 119 ++++++++++++++++++--------------- 7 files changed, 368 insertions(+), 125 deletions(-) diff --git a/src/cue/cue.ml b/src/cue/cue.ml index 06e5ae28..f605174b 100644 --- a/src/cue/cue.ml +++ b/src/cue/cue.ml @@ -12,13 +12,10 @@ 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. *) - -module Atomic = Multicore_magic.Transparent_atomic - type ('a, _) node = | Null : ('a, [> `Null ]) node | Node : { - mutable _next : 'a link; + next : 'a link Atomic.t; mutable value : 'a; mutable capacity : int; mutable counter : int; @@ -27,10 +24,8 @@ type ('a, _) node = and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] -external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" - -external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t - = "%identity" +exception Full +exception Empty let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity @@ -42,13 +37,14 @@ let[@inline] get_counter (Node r : (_, [< `Node ]) node) = r.counter let[@inline] set_counter (Node r : (_, [< `Node ]) node) value = r.counter <- value -let[@inline] get_next node = Atomic.get (next_as_atomic node) +let[@inline] get_next (Node node : (_, [< `Node ]) node) = Atomic.get node.next -let[@inline] fenceless_get_next node = - Atomic.fenceless_get (next_as_atomic node) +let[@inline] compare_and_set_next (Node node : (_, [< `Node ]) node) before + after = + Atomic.compare_and_set node.next before after -let[@inline] compare_and_set_next node before after = - Atomic.compare_and_set (next_as_atomic node) before after +let[@inline] link_as_node (Link n) : (_, [< `Node ]) node = + match n with Null -> assert false | Node _ as node -> node type 'a t = { head : ('a, [ `Node ]) node Atomic.t; @@ -58,25 +54,66 @@ type 'a t = { let create ?(capacity = Int.max_int) () = let value = Obj.magic () in - let node = Node { _next = Link Null; value; capacity; counter = 0 } in - let head = Atomic.make node |> Multicore_magic.copy_as_padded - and tail = Atomic.make node |> Multicore_magic.copy_as_padded in - { head; capacity; tail } |> Multicore_magic.copy_as_padded + let node = + Node { next = Atomic.make (Link Null); value; capacity; counter = 0 } + in + let head = Atomic.make_contended node and tail = Atomic.make_contended node in + { head; capacity; tail } + +let of_list ?(capacity = Int.max_int) list : 'a t = + let len = List.length list in + if len > capacity then raise Full + else + match list |> List.rev with + | [] -> create ~capacity () + | hd :: tl -> + let tail = + Node + { + value = hd; + counter = len; + capacity = capacity - len - 1; + next = Atomic.make (Link Null); + } + in + let _, _, next = + List.fold_left + (fun (counter, capacity, next) value -> + ( counter - 1, + capacity + 1, + Node + { value; counter; capacity; next = Atomic.make (Link next) } + )) + (len - 1, capacity - len, tail) + tl + in + let head = + Atomic.make_contended + @@ Node + { + value = Obj.magic (); + capacity; + counter = 0; + next = Atomic.make (Link next); + } + in + { head; capacity; tail = Atomic.make tail } let capacity_of t = t.capacity let is_empty t = - let head = Atomic.get t.head in - fenceless_get_next head == Link Null + let (Node head) = Atomic.get t.head in + Atomic.get head.next == Link Null let rec snapshot t = - let head = Atomic.get t.head in - let tail = Atomic.fenceless_get t.tail in - match fenceless_get_next tail with + let old_head = Atomic.get t.head in + let (Node tail as old_tail) = Atomic.get t.tail in + match Atomic.get tail.next with | Link (Node _ as node) -> - Atomic.compare_and_set t.tail tail node |> ignore; + Atomic.compare_and_set t.tail old_tail node |> ignore; snapshot t - | Link Null -> if Atomic.get t.head != head then snapshot t else (head, tail) + | Link Null -> + if Atomic.get t.head != old_head then snapshot t else (old_head, old_tail) let length t = let head, tail = snapshot t in @@ -84,28 +121,44 @@ let length t = (* *) -let rec peek_opt t = - let head = Atomic.get t.head in - match fenceless_get_next head with - | Link Null -> None - | Link (Node r) -> +type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly + +let rec peek_as : type a r. a t -> (a, r) poly -> r = + fun t poly -> + let (Node head as old_head) = Atomic.get t.head in + match Atomic.get head.next with + | Link Null -> ( match poly with Value -> raise Empty | Option -> None) + | Link (Node r) -> ( let value = r.value in - if Atomic.get t.head != head then peek_opt t else Some value + if Atomic.get t.head != old_head then peek_as t poly + else match poly with Value -> value | Option -> Some value) +let[@inline] peek_opt t = peek_as t Option +let[@inline] peek_exn t = peek_as t Value (* *) -let rec pop_opt t backoff = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> None +type ('a, _) poly2 = + | Option : ('a, 'a option) poly2 + | Value : ('a, 'a) poly2 + | Unit : ('a, unit) poly2 + +let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = + fun t backoff poly -> + let (Node head as old_head) = Atomic.get t.head in + match Atomic.get head.next with + | Link Null -> ( + match poly with Option -> None | Value | Unit -> raise Empty) | Link (Node node as new_head) -> if Atomic.compare_and_set t.head old_head new_head then begin let value = node.value in node.value <- Obj.magic (); - Some value + match poly with Option -> Some value | Value -> value | Unit -> () end - else pop_opt t (Backoff.once backoff) + else pop_as t (Backoff.once backoff) poly +let[@inline] pop_opt t = pop_as t Backoff.default Option +let[@inline] pop_exn t = pop_as t Backoff.default Value +let[@inline] drop_exn t = pop_as t Backoff.default Unit (* *) let rec fix_tail tail new_tail = @@ -142,8 +195,10 @@ let rec try_push t new_node old_tail = (* *) -let[@inline] pop_opt t = pop_opt t Backoff.default - let[@inline] try_push t value = - let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + let new_node = + Node { next = Atomic.make (Link Null); value; capacity = 0; counter = 0 } + in try_push t new_node (Atomic.get t.tail) + +let[@inline] push_exn t value = if not (try_push t value) then raise Full diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli index 10895114..005db069 100644 --- a/src/cue/cue_intf.mli +++ b/src/cue/cue_intf.mli @@ -14,37 +14,155 @@ PERFORMANCE OF THIS SOFTWARE. *) module type CUE = sig - (** Lock-free bounded queue. *) + (** Lock-free bounded Queue. - type !'a t - (** *) + This module implements a lock-free bounded queue based on Michael-Scott's queue + algorithm. Adding a capacity to this algorithm adds a general overhead to the + operations, and thus, it is recommended to use the unbounded queue + {!Saturn.Queue} if you don't need it. +*) + + (** {1 API} *) + + type 'a t + (** Represents a lock-free bounded queue holding elements of type ['a]. *) val create : ?capacity:int -> unit -> 'a t - (** *) + (** [create ~capacity ()] creates a new empty bounded queue with a maximum +capacity of [capacity]. The default [capacity] value is [Int.max_int]. +*) + + val of_list : ?capacity:int -> 'a list -> 'a t + (** [of_list list] creates a new queue from a list. + + @raises Full is the lenght of [list] is greater tant [capacity]. *) + + val length : 'a t -> int + (** [length queue] returns the number of elements currently in the [queue]. *) val capacity_of : 'a t -> int - (** *) + (** [capacity_of queue] returns the maximum number of elements that the [queue] + can hold. *) val is_empty : 'a t -> bool - (** *) + (** [is_empty queue] returns [true] if the [queue] is empty, otherwise [false]. *) - val length : 'a t -> int - (** *) + (** {2 Consumer functions} *) + + exception Empty + (** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty + stack. *) + + val peek_exn : 'a t -> 'a + (** [peek_exn queue] returns the first element of the [queue] without removing it. + + @raises Empty if the [queue] is empty. *) val peek_opt : 'a t -> 'a option - (** *) + (** [peek_opt queue] returns [Some] of the first element of the [queue] without + removing it, or [None] if the [queue] is empty. *) + + val pop_exn : 'a t -> 'a + (** [pop_exn queue] removes and returns the first element of the [queue]. + + @raises Empty if the [queue] is empty. *) val pop_opt : 'a t -> 'a option - (** *) + (** [pop_opt queue] removes and returns [Some] of the first element of the [queue], + or [None] if the [queue] is empty. *) + + val drop_exn : 'a t -> unit + (** [drop_exn queue] removes the top element of the [queue]. + @raises Empty if the [queue] is empty. *) + + (* + val try_compare_and_pop : 'a t -> 'a -> bool + (** [try_compare_and_pop stack before] tries to remove the top element of the + [stack] if it is equal to [before]. Returns [true] on success and [false] in + case the stack is empty or if the top element is not equal to [before]. + ℹ️ The values are compared using physical equality, i.e., the [==] operator. *) +*) + + (** {2 Producer functions} *) + + exception Full + (** Raised when {!push_exn} or {!push_all_exn} is applied to a full queue. *) + + val push_exn : 'a t -> 'a -> unit + (** [push_exn queue element] adds [element] at the end of the [queue]. + + @raises Full if the [queue] is full. *) val try_push : 'a t -> 'a -> bool - (** *) + (** [try_push queue element] tries to add [element] at the end of the [queue]. + Returns [true] if the element was successfully added, or [false] if the + queue is full. *) + + (* + val push_all_exn : 'a t -> 'a list -> unit + (** [push_all_exn queue elements] adds all [elements] at the end of the [queue]. + + @raises Full if the [stack] is full. *) + + val try_push_all : 'a t -> 'a list -> bool + (** [try_push_all stack elements] tries to add all [elements] to the top of the + [stack]. Returns [true] if the elements were successfully added, or [false] if + the stack is full. + + {[ + # let t : int t = create () + val t : int t = + # try_push_all t [1; 2; 3; 4] + - : bool = true + # pop_opt t + - : int option = Some 4 + # pop_opt t + - : int option = Some 3 + # pop_all t + - : int list = [2; 1] + ]} + *) +*) (* -val to_list : 'a t -> 'a list -(** *) -val transfer : 'a t -> 'a t -(** *) + (** {3 Updating bindings} *) + + val try_set : 'a t -> 'a -> bool + (** [try_set stack value] tries to update the top element of the [stack] to + [value]. Returns [true] on success and [false] if the [stack] is empty. + *) + + val try_compare_and_set : 'a t -> 'a -> 'a -> bool + (** [try_compare_and_set stack before after] tries to update the top element of +the [stack] from the [before] value to the [after] value. Returns [true] on +success and [false] if the [stack] is empty or the top element is not equal +to [before]. + ℹ️ The values are compared using physical equality, i.e., the [==] + operator. *) + + val set_exn : 'a t -> 'a -> 'a + (** [set_exn stack after] tries to update the top element of [stack] from some +[before] value to the [after] value. Returns the [before] value on success. + @raises Empty if the [stack] is empty. *) + + (** {2 With Sequences }*) + val to_seq : 'a t -> 'a Seq.t + (** [to_seq stack] takes a snapshot of [stack] and returns its value from top to +bottom. + 🐌 This is a linear time operation. *) + + val of_seq : ?capacity:int -> 'a Seq.t -> 'a t + (** [of_seq seq] creates a stack from a [seq]. It must be finite. *) + + val add_seq_exn : 'a t -> 'a Seq.t -> unit + (** [add_seq_exn stack seq] adds all elements of [seq] to the top of the +[stack]. [seq] must be finite. +@raises Full if the [seq] is too long to fit in the stack. *) + + val try_add_seq : 'a t -> 'a Seq.t -> bool + (** [try_add_seq stack seq] tries to add all elements of [seq] to the top of the +[stack]. Returns [true] if the elements were successfully added, or [false] if +the [seq] is too long to fit in the stack. *) *) end diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml index 06e5ae28..2520b15c 100644 --- a/src/cue/cue_unsafe.ml +++ b/src/cue/cue_unsafe.ml @@ -56,6 +56,9 @@ type 'a t = { tail : ('a, [ `Node ]) node Atomic.t; } +exception Full +exception Empty + let create ?(capacity = Int.max_int) () = let value = Obj.magic () in let node = Node { _next = Link Null; value; capacity; counter = 0 } in @@ -63,6 +66,43 @@ let create ?(capacity = Int.max_int) () = and tail = Atomic.make node |> Multicore_magic.copy_as_padded in { head; capacity; tail } |> Multicore_magic.copy_as_padded +let of_list ?(capacity = Int.max_int) list : 'a t = + let len = List.length list in + if len > capacity then raise Full + else + match list |> List.rev with + | [] -> create ~capacity () + | hd :: tl -> + let tail = + Node + { + value = hd; + counter = len; + capacity = capacity - len - 1; + _next = Link Null; + } + in + let _, _, next = + List.fold_left + (fun (counter, capacity, next) value -> + ( counter - 1, + capacity + 1, + Node { value; counter; capacity; _next = Link next } )) + (len - 1, capacity - len, tail) + tl + in + let head = + Atomic.make_contended + @@ Node + { + value = Obj.magic (); + capacity; + counter = 0; + _next = Link next; + } + in + { head; capacity; tail = Atomic.make tail } + let capacity_of t = t.capacity let is_empty t = @@ -84,27 +124,45 @@ let length t = (* *) -let rec peek_opt t = +type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly + +let rec peek_as : type a r. a t -> (a, r) poly -> r = + fun t poly -> let head = Atomic.get t.head in match fenceless_get_next head with - | Link Null -> None - | Link (Node r) -> + | Link Null -> ( match poly with Value -> raise Empty | Option -> None) + | Link (Node r) -> ( let value = r.value in - if Atomic.get t.head != head then peek_opt t else Some value + if Atomic.get t.head != head then peek_as t poly + else match poly with Value -> value | Option -> Some value) + +let[@inline] peek_opt t = peek_as t Option +let[@inline] peek_exn t = peek_as t Value (* *) -let rec pop_opt t backoff = +type ('a, _) poly2 = + | Option : ('a, 'a option) poly2 + | Value : ('a, 'a) poly2 + | Unit : ('a, unit) poly2 + +let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = + fun t backoff poly -> let old_head = Atomic.get t.head in match fenceless_get_next old_head with - | Link Null -> None + | Link Null -> ( + match poly with Option -> None | Value | Unit -> raise Empty) | Link (Node node as new_head) -> if Atomic.compare_and_set t.head old_head new_head then begin let value = node.value in node.value <- Obj.magic (); - Some value + match poly with Option -> Some value | Value -> value | Unit -> () end - else pop_opt t (Backoff.once backoff) + else pop_as t (Backoff.once backoff) poly + +let[@inline] pop_opt t = pop_as t Backoff.default Option +let[@inline] pop_exn t = pop_as t Backoff.default Value +let[@inline] drop_exn t = pop_as t Backoff.default Unit (* *) @@ -142,8 +200,8 @@ let rec try_push t new_node old_tail = (* *) -let[@inline] pop_opt t = pop_opt t Backoff.default - let[@inline] try_push t value = let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in try_push t new_node (Atomic.get t.tail) + +let[@inline] push_exn t value = if not (try_push t value) then raise Full diff --git a/src/saturn.ml b/src/saturn.ml index 168bf45e..a924e0f4 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -29,6 +29,7 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe module Cue = Cue +module Cue_unsafe = Cue_unsafe module Stack = Treiber_stack module Bounded_stack = Bounded_stack module Work_stealing_deque = Ws_deque diff --git a/src/saturn.mli b/src/saturn.mli index 4b049907..50d33cd4 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -33,11 +33,9 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe module Stack = Treiber_stack -<<<<<<< HEAD module Bounded_stack = Bounded_stack -======= module Cue = Cue ->>>>>>> 57f7acb (Bounded queue) +module Cue_unsafe = Cue_unsafe module Work_stealing_deque = Ws_deque module Single_prod_single_cons_queue = Spsc_queue module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe diff --git a/test/cue/cues/cues.ml b/test/cue/cues/cues.ml index 50fdc185..ad780caf 100644 --- a/test/cue/cues/cues.ml +++ b/test/cue/cues/cues.ml @@ -7,11 +7,11 @@ end module Cue : Cue_tests = struct include Saturn.Cue - let name = "htbl_safe" + let name = "cue_safe" end -(* module Cue_unsafe : Cue_tests = struct - include Saturn.Cue_unsafe +module Cue_unsafe : Cue_tests = struct + include Saturn.Cue_unsafe - let name = "htbl_unsafe" - end *) + let name = "cue_unsafe" +end diff --git a/test/cue/stm_cue.ml b/test/cue/stm_cue.ml index 1d65f186..f3638636 100644 --- a/test/cue/stm_cue.ml +++ b/test/cue/stm_cue.ml @@ -4,66 +4,79 @@ open QCheck open STM module Cue = Saturn.Cue -module Spec = struct - type cmd = Try_push of int | Pop_opt | Peek_opt | Length | Is_empty +module STM_cue (Cue : Cues.Cue_tests) = struct + module Spec = struct + type cmd = Try_push of int | Pop_opt | Peek_opt | Length | Is_empty - let show_cmd c = - match c with - | Try_push i -> "Try_push " ^ string_of_int i - | Pop_opt -> "Pop_opt" - | Peek_opt -> "Peek_opt" - | Length -> "Length" - | Is_empty -> "Is_empty" + let show_cmd c = + match c with + | Try_push i -> "Try_push " ^ string_of_int i + | Pop_opt -> "Pop_opt" + | Peek_opt -> "Peek_opt" + | Length -> "Length" + | Is_empty -> "Is_empty" - type state = int * int * int list - type sut = int Cue.t + type state = int * int * int list + type sut = int Cue.t - let arb_cmd _s = - let int_gen = Gen.nat in - QCheck.make ~print:show_cmd - (Gen.oneof - [ - Gen.map (fun i -> Try_push i) int_gen; - Gen.return Pop_opt; - Gen.return Peek_opt; - Gen.return Length; - Gen.return Is_empty; - ]) + let arb_cmd _s = + let int_gen = Gen.nat in + QCheck.make ~print:show_cmd + (Gen.oneof + [ + Gen.map (fun i -> Try_push i) int_gen; + Gen.return Pop_opt; + Gen.return Peek_opt; + Gen.return Length; + Gen.return Is_empty; + ]) - let init_state = (100, 0, []) - let init_sut () = Cue.create ~capacity:100 () - let cleanup _ = () + let init_state = (100, 0, []) + let init_sut () = Cue.create ~capacity:100 () + let cleanup _ = () - let next_state c ((capacity, size, content) as s) = - match c with - | Try_push i -> - if size = capacity then s else (capacity, size + 1, i :: content) - | Pop_opt -> ( - match List.rev content with - | [] -> s - | _ :: content' -> (capacity, size - 1, List.rev content')) - | Peek_opt -> s - | Is_empty -> s - | Length -> s + let next_state c ((capacity, size, content) as s) = + match c with + | Try_push i -> + if size = capacity then s else (capacity, size + 1, i :: content) + | Pop_opt -> ( + match List.rev content with + | [] -> s + | _ :: content' -> (capacity, size - 1, List.rev content')) + | Peek_opt -> s + | Is_empty -> s + | Length -> s - let precond _ _ = true + let precond _ _ = true - let run c d = - match c with - | Try_push i -> Res (bool, Cue.try_push d i) - | Pop_opt -> Res (option int, Cue.pop_opt d) - | Peek_opt -> Res (option int, Cue.peek_opt d) - | Is_empty -> Res (bool, Cue.is_empty d) - | Length -> Res (int, Cue.length d) + let run c d = + match c with + | Try_push i -> Res (bool, Cue.try_push d i) + | Pop_opt -> Res (option int, Cue.pop_opt d) + | Peek_opt -> Res (option int, Cue.peek_opt d) + | Is_empty -> Res (bool, Cue.is_empty d) + | Length -> Res (int, Cue.length d) - let postcond c ((capacity, size, content) : state) res = - match (c, res) with - | Try_push _, Res ((Bool, _), res) -> res = (size < capacity) - | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( - match List.rev content with [] -> res = None | j :: _ -> res = Some j) - | Is_empty, Res ((Bool, _), res) -> res = (content = []) - | Length, Res ((Int, _), res) -> res = size - | _, _ -> false + let postcond c ((capacity, size, content) : state) res = + match (c, res) with + | Try_push _, Res ((Bool, _), res) -> res = (size < capacity) + | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( + match List.rev content with + | [] -> res = None + | j :: _ -> res = Some j) + | Is_empty, Res ((Bool, _), res) -> res = (content = []) + | Length, Res ((Int, _), res) -> res = size + | _, _ -> false + end + + let run () = Stm_run.run ~name:"Saturn_lockfree.Cue" (module Spec) |> exit end -let () = Stm_run.run ~name:"Saturn_lockfree.Cue" (module Spec) |> exit +let () = + Random.self_init (); + let module Safe = STM_cue (Cues.Cue) in + let exit_code = Safe.run () in + if exit_code <> 0 then exit exit_code + else + let module Unsafe = STM_cue (Cues.Cue_unsafe) in + Unsafe.run () |> exit From 4928e1d04ebc531eaac19b18ad571643332254cd Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 15 Nov 2024 16:01:59 +0100 Subject: [PATCH 04/19] Dscheck tests. --- src/cue/cue.ml | 2 +- src/cue/cue_intf.mli | 42 ++---- src/cue/cue_unsafe.ml | 2 +- test/cue/dscheck_cue.ml | 290 ++++++++++++++++++++++++++++++++++++++++ test/cue/dune | 30 +++++ 5 files changed, 336 insertions(+), 30 deletions(-) create mode 100644 test/cue/dscheck_cue.ml diff --git a/src/cue/cue.ml b/src/cue/cue.ml index f605174b..1e654b48 100644 --- a/src/cue/cue.ml +++ b/src/cue/cue.ml @@ -60,7 +60,7 @@ let create ?(capacity = Int.max_int) () = let head = Atomic.make_contended node and tail = Atomic.make_contended node in { head; capacity; tail } -let of_list ?(capacity = Int.max_int) list : 'a t = +let of_list_exn ?(capacity = Int.max_int) list : 'a t = let len = List.length list in if len > capacity then raise Full else diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli index 005db069..41c1af11 100644 --- a/src/cue/cue_intf.mli +++ b/src/cue/cue_intf.mli @@ -32,10 +32,22 @@ module type CUE = sig capacity of [capacity]. The default [capacity] value is [Int.max_int]. *) - val of_list : ?capacity:int -> 'a list -> 'a t + val of_list_exn : ?capacity:int -> 'a list -> 'a t (** [of_list list] creates a new queue from a list. - @raises Full is the lenght of [list] is greater tant [capacity]. *) + @raises Full is the lenght of [list] is greater tant [capacity]. + + {[ + # let t : int t = of_list_exn [1;2;3;4] + val t : int t = + # pop_opt t + - : int option = Some 1 + # pop_opt t + - : int option = Some 2 + # length t + - : int = 2 + ]} + *) val length : 'a t -> int (** [length queue] returns the number of elements currently in the [queue]. *) @@ -98,32 +110,6 @@ capacity of [capacity]. The default [capacity] value is [Int.max_int]. Returns [true] if the element was successfully added, or [false] if the queue is full. *) - (* - val push_all_exn : 'a t -> 'a list -> unit - (** [push_all_exn queue elements] adds all [elements] at the end of the [queue]. - - @raises Full if the [stack] is full. *) - - val try_push_all : 'a t -> 'a list -> bool - (** [try_push_all stack elements] tries to add all [elements] to the top of the - [stack]. Returns [true] if the elements were successfully added, or [false] if - the stack is full. - - {[ - # let t : int t = create () - val t : int t = - # try_push_all t [1; 2; 3; 4] - - : bool = true - # pop_opt t - - : int option = Some 4 - # pop_opt t - - : int option = Some 3 - # pop_all t - - : int list = [2; 1] - ]} - *) -*) - (* (** {3 Updating bindings} *) diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml index 2520b15c..feaeac0f 100644 --- a/src/cue/cue_unsafe.ml +++ b/src/cue/cue_unsafe.ml @@ -66,7 +66,7 @@ let create ?(capacity = Int.max_int) () = and tail = Atomic.make node |> Multicore_magic.copy_as_padded in { head; capacity; tail } |> Multicore_magic.copy_as_padded -let of_list ?(capacity = Int.max_int) list : 'a t = +let of_list_exn ?(capacity = Int.max_int) list : 'a t = let len = List.length list in if len > capacity then raise Full else diff --git a/test/cue/dscheck_cue.ml b/test/cue/dscheck_cue.ml new file mode 100644 index 00000000..e079d640 --- /dev/null +++ b/test/cue/dscheck_cue.ml @@ -0,0 +1,290 @@ +[@@@warning "-32"] + +module Atomic = Dscheck.TracedAtomic + +module Dscheck_cue (Cue : Cue_intf.CUE) = struct + let drain cue = + let rec pop_until_empty acc = + match Cue.pop_opt cue with + | None -> acc |> List.rev + | Some v -> pop_until_empty (v :: acc) + in + pop_until_empty [] + + let push_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Cue.pop_opt cue with + | None -> () + | Some v -> popped := v :: !popped + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain cue in + let pushed = List.init items_total (fun x -> x + 1) in + List.sort Int.compare (!popped @ remaining) = pushed))) + + let push_drop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let dropped = ref 0 in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Cue.drop_exn cue with + | () -> dropped := !dropped + 1 + | exception Cue.Empty -> () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain cue in + remaining + = List.init (items_total - !dropped) (fun x -> x + !dropped + 1)))) + + let push_pop_with_capacity () = + Atomic.trace (fun () -> + let cue = Cue.create ~capacity:2 () in + let items_total = 4 in + + (* producer *) + let pushed = Array.make items_total false in + Atomic.spawn (fun () -> + Array.iteri (fun i _ -> pushed.(i) <- Cue.try_push cue i) pushed); + + (* consumer *) + let popped = Array.make items_total None in + Atomic.spawn (fun () -> + Array.iteri (fun i _ -> popped.(i) <- Cue.pop_opt cue) popped); + (* checks*) + Atomic.final (fun () -> + let popped = Array.to_list popped |> List.filter_map Fun.id in + let remaining = drain cue in + Atomic.check (fun () -> + let xor a b = (a && not b) || ((not a) && b) in + try + Array.iteri + (fun i elt -> + if elt then begin + if not @@ xor (List.mem i remaining) (List.mem i popped) + then raise Exit + end + else if List.mem i remaining || List.mem i popped then + raise Exit) + pushed; + true + with _ -> false))) + + let push_push () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 6 in + + (* two producers *) + for i = 0 to 1 do + Atomic.spawn (fun () -> + for j = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + Cue.try_push cue (i + (j * 2)) |> ignore + done) + done; + + (* checks*) + Atomic.final (fun () -> + let items = drain cue in + + (* got the same number of items out as in *) + Atomic.check (fun () -> items_total = List.length items); + + (* they are in fifo order *) + let odd, even = List.partition (fun v -> v mod 2 == 0) items in + + Atomic.check (fun () -> List.sort Int.compare odd = odd); + Atomic.check (fun () -> List.sort Int.compare even = even))) + + let push_push_with_capacity () = + Atomic.trace (fun () -> + let capacity = 3 in + let cue = Cue.create ~capacity () in + let items_total = 6 in + + (* two producers *) + for i = 0 to 1 do + Atomic.spawn (fun () -> + for j = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + Cue.try_push cue (i + (j * 2)) |> ignore + done) + done; + + (* checks*) + Atomic.final (fun () -> + let items = drain cue in + + (* got the same number of items out as in *) + Atomic.check (fun () -> capacity = List.length items))) + + let pop_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done; + + (* two consumers *) + let lists = [ ref []; ref [] ] in + List.iter + (fun list -> + Atomic.spawn (fun () -> + for _ = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + list := Option.get (Cue.pop_opt cue) :: !list + done) + |> ignore) + lists; + + (* checks*) + Atomic.final (fun () -> + let l1 = !(List.nth lists 0) in + let l2 = !(List.nth lists 1) in + + (* got the same number of items out as in *) + Atomic.check (fun () -> + items_total = List.length l1 + List.length l2); + + (* they are in fifo order *) + Atomic.check (fun () -> List.sort Int.compare l1 = List.rev l1); + Atomic.check (fun () -> List.sort Int.compare l2 = List.rev l2))) + + let two_domains () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let n1, n2 = (1, 2) in + + (* two producers *) + let lists = + [ + (List.init n1 (fun i -> i), ref []); + (List.init n2 (fun i -> i + n1), ref []); + ] + in + List.iter + (fun (lpush, lpop) -> + Atomic.spawn (fun () -> + List.iter + (fun elt -> + (* even nums belong to thr 1, odd nums to thr 2 *) + Cue.try_push cue elt |> ignore; + lpop := Option.get (Cue.pop_opt cue) :: !lpop) + lpush) + |> ignore) + lists; + + (* checks*) + Atomic.final (fun () -> + let lpop1 = !(List.nth lists 0 |> snd) in + let lpop2 = !(List.nth lists 1 |> snd) in + + (* got the same number of items out as in *) + Atomic.check (fun () -> List.length lpop1 = 1); + Atomic.check (fun () -> List.length lpop2 = 2); + + (* no element are missing *) + Atomic.check (fun () -> + List.sort Int.compare (lpop1 @ lpop2) + = List.init (n1 + n2) (fun i -> i)))) + + let two_domains_more_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let n1, n2 = (2, 1) in + + (* two producers *) + let lists = + [ + (List.init n1 (fun i -> i), ref []); + (List.init n2 (fun i -> i + n1), ref []); + ] + in + List.iter + (fun (lpush, lpop) -> + Atomic.spawn (fun () -> + List.iter + (fun elt -> + Cue.try_push cue elt |> ignore; + lpop := Cue.pop_opt cue :: !lpop; + lpop := Cue.pop_opt cue :: !lpop) + lpush) + |> ignore) + lists; + + (* checks*) + Atomic.final (fun () -> + let lpop1 = + !(List.nth lists 0 |> snd) + |> List.filter Option.is_some |> List.map Option.get + in + let lpop2 = + !(List.nth lists 1 |> snd) + |> List.filter Option.is_some |> List.map Option.get + in + + (* got the same number of items out as in *) + Atomic.check (fun () -> + n1 + n2 = List.length lpop1 + List.length lpop2); + + (* no element are missing *) + Atomic.check (fun () -> + List.sort Int.compare (lpop1 @ lpop2) + = List.init (n1 + n2) (fun i -> i)))) + + let tests name = + let open Alcotest in + [ + ( "basic " ^ name, + [ + test_case "1-producer-1-consumer" `Slow push_pop; + test_case "1-producer-1-consumer-capacity" `Slow + push_pop_with_capacity; + test_case "1-push-1-drop" `Slow push_drop; + test_case "2-producers" `Slow push_push; + test_case "2-producers-capacity" `Slow push_push_with_capacity; + test_case "2-consumers" `Slow pop_pop; + test_case "2-domains" `Slow two_domains; + test_case "2-domains-more-pops" `Slow two_domains_more_pop; + ] ); + ] +end + +let () = + let module Safe = Dscheck_cue (Cue) in + let safe_test = Safe.tests "safe" in + (* let module Unsafe = Dscheck_cue (Cue_unsafe) in + let unsafe_test = Unsafe.tests "unsafe" in *) + let open Alcotest in + run "dscheck_cue" safe_test diff --git a/test/cue/dune b/test/cue/dune index 39a416b2..608eb75d 100644 --- a/test/cue/dune +++ b/test/cue/dune @@ -1,3 +1,33 @@ +(rule + (action + (copy ../../src/cue/cue.ml cue.ml)) + (package saturn)) + +(rule + (action + (copy ../../src/cue/cue_unsafe.ml cue_unsafe.ml)) + (package saturn)) + +(rule + (action + (copy ../../src/cue/cue_intf.mli cue_intf.ml)) + (package saturn)) + +(test + (package saturn) + (name dscheck_cue) + (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) + (build_if + (and + (>= %{ocaml_version} 5) + (not + (and + (= %{arch_sixtyfour} false) + (= %{architecture} arm))))) + (modules cue cue_unsafe cue_intf dscheck_cue) + (flags + (:standard -open Multicore_magic_dscheck))) + (test (package saturn) (name stm_cue) From fa157c1ea97cdb61ab1df6a19eb64c32d6522d5e Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 15 Nov 2024 16:57:46 +0100 Subject: [PATCH 05/19] Back to a version of cue_unsafe that is closer from the original implementaiton. Still seg fault. --- src/cue/cue_intf.mli | 53 +-------------------- src/cue/cue_unsafe.ml | 102 +++++++++++++++++++++++++++++----------- test/cue/dscheck_cue.ml | 6 +-- 3 files changed, 78 insertions(+), 83 deletions(-) diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli index 41c1af11..6035967c 100644 --- a/src/cue/cue_intf.mli +++ b/src/cue/cue_intf.mli @@ -29,8 +29,7 @@ module type CUE = sig val create : ?capacity:int -> unit -> 'a t (** [create ~capacity ()] creates a new empty bounded queue with a maximum -capacity of [capacity]. The default [capacity] value is [Int.max_int]. -*) + capacity of [capacity]. The default [capacity] value is [Int.max_int].*) val of_list_exn : ?capacity:int -> 'a list -> 'a t (** [of_list list] creates a new queue from a list. @@ -87,14 +86,6 @@ capacity of [capacity]. The default [capacity] value is [Int.max_int]. (** [drop_exn queue] removes the top element of the [queue]. @raises Empty if the [queue] is empty. *) - (* - val try_compare_and_pop : 'a t -> 'a -> bool - (** [try_compare_and_pop stack before] tries to remove the top element of the - [stack] if it is equal to [before]. Returns [true] on success and [false] in - case the stack is empty or if the top element is not equal to [before]. - ℹ️ The values are compared using physical equality, i.e., the [==] operator. *) -*) - (** {2 Producer functions} *) exception Full @@ -109,46 +100,4 @@ capacity of [capacity]. The default [capacity] value is [Int.max_int]. (** [try_push queue element] tries to add [element] at the end of the [queue]. Returns [true] if the element was successfully added, or [false] if the queue is full. *) - - (* - - (** {3 Updating bindings} *) - - val try_set : 'a t -> 'a -> bool - (** [try_set stack value] tries to update the top element of the [stack] to - [value]. Returns [true] on success and [false] if the [stack] is empty. - *) - - val try_compare_and_set : 'a t -> 'a -> 'a -> bool - (** [try_compare_and_set stack before after] tries to update the top element of -the [stack] from the [before] value to the [after] value. Returns [true] on -success and [false] if the [stack] is empty or the top element is not equal -to [before]. - ℹ️ The values are compared using physical equality, i.e., the [==] - operator. *) - - val set_exn : 'a t -> 'a -> 'a - (** [set_exn stack after] tries to update the top element of [stack] from some -[before] value to the [after] value. Returns the [before] value on success. - @raises Empty if the [stack] is empty. *) - - (** {2 With Sequences }*) - val to_seq : 'a t -> 'a Seq.t - (** [to_seq stack] takes a snapshot of [stack] and returns its value from top to -bottom. - 🐌 This is a linear time operation. *) - - val of_seq : ?capacity:int -> 'a Seq.t -> 'a t - (** [of_seq seq] creates a stack from a [seq]. It must be finite. *) - - val add_seq_exn : 'a t -> 'a Seq.t -> unit - (** [add_seq_exn stack seq] adds all elements of [seq] to the top of the -[stack]. [seq] must be finite. -@raises Full if the [seq] is too long to fit in the stack. *) - - val try_add_seq : 'a t -> 'a Seq.t -> bool - (** [try_add_seq stack seq] tries to add all elements of [seq] to the top of the -[stack]. Returns [true] if the elements were successfully added, or [false] if -the [seq] is too long to fit in the stack. *) -*) end diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml index feaeac0f..4031413a 100644 --- a/src/cue/cue_unsafe.ml +++ b/src/cue/cue_unsafe.ml @@ -1,5 +1,4 @@ (* Copyright (c) 2023-2024, Vesa Karvonen - 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 @@ -124,45 +123,62 @@ let length t = (* *) -type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly - -let rec peek_as : type a r. a t -> (a, r) poly -> r = - fun t poly -> - let head = Atomic.get t.head in - match fenceless_get_next head with - | Link Null -> ( match poly with Value -> raise Empty | Option -> None) - | Link (Node r) -> ( +let rec peek_exn t = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> raise Empty + | Link (Node r) -> let value = r.value in - if Atomic.get t.head != head then peek_as t poly - else match poly with Value -> value | Option -> Some value) + if Atomic.get t.head != old_head then peek_exn t else value -let[@inline] peek_opt t = peek_as t Option -let[@inline] peek_exn t = peek_as t Value +(* *) + +let rec peek_opt t = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> None + | Link (Node r) -> + let value = r.value in + if Atomic.get t.head != old_head then peek_opt t else Some value (* *) -type ('a, _) poly2 = - | Option : ('a, 'a option) poly2 - | Value : ('a, 'a) poly2 - | Unit : ('a, unit) poly2 +let rec pop_exn t backoff = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> raise Empty + | Link (Node node as new_head) -> + if Atomic.compare_and_set t.head old_head new_head then begin + let value = node.value in + node.value <- Obj.magic (); + value + end + else pop_exn t (Backoff.once backoff) + +(* *) -let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = - fun t backoff poly -> +let rec pop_opt t backoff = let old_head = Atomic.get t.head in match fenceless_get_next old_head with - | Link Null -> ( - match poly with Option -> None | Value | Unit -> raise Empty) + | Link Null -> None | Link (Node node as new_head) -> if Atomic.compare_and_set t.head old_head new_head then begin let value = node.value in node.value <- Obj.magic (); - match poly with Option -> Some value | Value -> value | Unit -> () + Some value end - else pop_as t (Backoff.once backoff) poly + else pop_opt t (Backoff.once backoff) +(* *) -let[@inline] pop_opt t = pop_as t Backoff.default Option -let[@inline] pop_exn t = pop_as t Backoff.default Value -let[@inline] drop_exn t = pop_as t Backoff.default Unit +let rec drop_exn t backoff = + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with + | Link Null -> raise Empty + | Link (Node node as new_head) -> + if Atomic.compare_and_set t.head old_head new_head then begin + node.value <- Obj.magic () + end + else drop_exn t (Backoff.once backoff) (* *) @@ -175,6 +191,31 @@ let rec fix_tail tail new_tail = (* *) +let rec push_exn t new_node old_tail = + let capacity = get_capacity old_tail in + if capacity = 0 then begin + let old_head = Atomic.get t.head in + let length = get_counter old_tail - get_counter old_head in + let capacity = t.capacity - length in + if 0 < capacity then begin + set_capacity old_tail capacity; + push_exn t new_node old_tail + end + else raise Full + end + else begin + set_capacity new_node (capacity - 1); + set_counter new_node (get_counter old_tail + 1); + if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then + push_exn t new_node (link_as_node (get_next old_tail)) + else begin + if not (Atomic.compare_and_set t.tail old_tail new_node) then + fix_tail t.tail new_node + end + end + +(* *) + let rec try_push t new_node old_tail = let capacity = get_capacity old_tail in if capacity = 0 then @@ -199,9 +240,14 @@ let rec try_push t new_node old_tail = end (* *) +let[@inline] drop_exn t = drop_exn t Backoff.default +let[@inline] pop_exn t = pop_exn t Backoff.default +let[@inline] pop_opt t = pop_opt t Backoff.default + +let[@inline] push_exn t value = + let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + push_exn t new_node (Atomic.get t.tail) let[@inline] try_push t value = let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in try_push t new_node (Atomic.get t.tail) - -let[@inline] push_exn t value = if not (try_push t value) then raise Full diff --git a/test/cue/dscheck_cue.ml b/test/cue/dscheck_cue.ml index e079d640..d7f41541 100644 --- a/test/cue/dscheck_cue.ml +++ b/test/cue/dscheck_cue.ml @@ -284,7 +284,7 @@ end let () = let module Safe = Dscheck_cue (Cue) in let safe_test = Safe.tests "safe" in - (* let module Unsafe = Dscheck_cue (Cue_unsafe) in - let unsafe_test = Unsafe.tests "unsafe" in *) + let module Unsafe = Dscheck_cue (Cue_unsafe) in + let unsafe_test = Unsafe.tests "unsafe" in let open Alcotest in - run "dscheck_cue" safe_test + run "dscheck_cue" (safe_test @ unsafe_test) From 3b1e168668007e7ebe04d3ac9f4ca883c5bc166f Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Fri, 15 Nov 2024 18:37:12 +0100 Subject: [PATCH 06/19] Correct dscheck issue with the unsafe cue. --- src/cue/cue_unsafe.ml | 44 ++++++++----------------------------- src/cue/cue_unsafe_node.ml | 21 ++++++++++++++++++ test/cue/cue_unsafe_node.ml | 22 +++++++++++++++++++ test/cue/dune | 2 +- 4 files changed, 53 insertions(+), 36 deletions(-) create mode 100644 src/cue/cue_unsafe_node.ml create mode 100644 test/cue/cue_unsafe_node.ml diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml index 4031413a..9195dd8c 100644 --- a/src/cue/cue_unsafe.ml +++ b/src/cue/cue_unsafe.ml @@ -13,23 +13,8 @@ PERFORMANCE OF THIS SOFTWARE. *) module Atomic = Multicore_magic.Transparent_atomic - -type ('a, _) node = - | Null : ('a, [> `Null ]) node - | Node : { - mutable _next : 'a link; - mutable value : 'a; - mutable capacity : int; - mutable counter : int; - } - -> ('a, [> `Node ]) node - -and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] - -external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" - -external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t - = "%identity" +module Node = Cue_unsafe_node +open Node let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity @@ -60,7 +45,7 @@ exception Empty let create ?(capacity = Int.max_int) () = let value = Obj.magic () in - let node = Node { _next = Link Null; value; capacity; counter = 0 } in + let node = make_node ~value ~capacity ~counter:0 Null in let head = Atomic.make node |> Multicore_magic.copy_as_padded and tail = Atomic.make node |> Multicore_magic.copy_as_padded in { head; capacity; tail } |> Multicore_magic.copy_as_padded @@ -73,33 +58,22 @@ let of_list_exn ?(capacity = Int.max_int) list : 'a t = | [] -> create ~capacity () | hd :: tl -> let tail = - Node - { - value = hd; - counter = len; - capacity = capacity - len - 1; - _next = Link Null; - } + make_node ~value:hd ~capacity:(capacity - len - 1) ~counter:len Null in let _, _, next = List.fold_left (fun (counter, capacity, next) value -> ( counter - 1, capacity + 1, - Node { value; counter; capacity; _next = Link next } )) + make_node ~value ~capacity ~counter next )) (len - 1, capacity - len, tail) tl in let head = Atomic.make_contended - @@ Node - { - value = Obj.magic (); - capacity; - counter = 0; - _next = Link next; - } + (make_node ~value:(Obj.magic ()) ~capacity ~counter:0 next) in + { head; capacity; tail = Atomic.make tail } let capacity_of t = t.capacity @@ -245,9 +219,9 @@ let[@inline] pop_exn t = pop_exn t Backoff.default let[@inline] pop_opt t = pop_opt t Backoff.default let[@inline] push_exn t value = - let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + let new_node = make_node ~value ~capacity:0 ~counter:0 Null in push_exn t new_node (Atomic.get t.tail) let[@inline] try_push t value = - let new_node = Node { _next = Link Null; value; capacity = 0; counter = 0 } in + let new_node = make_node ~value ~capacity:0 ~counter:0 Null in try_push t new_node (Atomic.get t.tail) diff --git a/src/cue/cue_unsafe_node.ml b/src/cue/cue_unsafe_node.ml new file mode 100644 index 00000000..292ff99f --- /dev/null +++ b/src/cue/cue_unsafe_node.ml @@ -0,0 +1,21 @@ +module Atomic = Multicore_magic.Transparent_atomic + +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + mutable _next : 'a link; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" + +external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t + = "%identity" + +let[@inline] make_node ~value ~capacity ~counter next = + Node { _next = Link next; value; capacity; counter } diff --git a/test/cue/cue_unsafe_node.ml b/test/cue/cue_unsafe_node.ml new file mode 100644 index 00000000..4b15256d --- /dev/null +++ b/test/cue/cue_unsafe_node.ml @@ -0,0 +1,22 @@ +open Multicore_magic_dscheck +module Atomic = Multicore_magic.Transparent_atomic + +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + _next : 'a link Atomic.t; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" + +let[@inline] next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t = + fun (Node r : ('a, [< `Node ]) node) -> r._next + +let[@inline] make_node ~value ~capacity ~counter next = + Node { _next = Atomic.make (Link next); value; capacity; counter } diff --git a/test/cue/dune b/test/cue/dune index 608eb75d..e7b74fa4 100644 --- a/test/cue/dune +++ b/test/cue/dune @@ -24,7 +24,7 @@ (and (= %{arch_sixtyfour} false) (= %{architecture} arm))))) - (modules cue cue_unsafe cue_intf dscheck_cue) + (modules cue cue_unsafe cue_intf cue_unsafe_node dscheck_cue) (flags (:standard -open Multicore_magic_dscheck))) From 67ad70ff73198e9d014ec89ff0b609a13005ea01 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 09:59:25 +0100 Subject: [PATCH 07/19] Improve doc. --- src/cue/cue_intf.mli | 66 ++++++++++++++++++++++---------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli index 6035967c..f58fee40 100644 --- a/src/cue/cue_intf.mli +++ b/src/cue/cue_intf.mli @@ -16,11 +16,11 @@ module type CUE = sig (** Lock-free bounded Queue. - This module implements a lock-free bounded queue based on Michael-Scott's queue - algorithm. Adding a capacity to this algorithm adds a general overhead to the - operations, and thus, it is recommended to use the unbounded queue - {!Saturn.Queue} if you don't need it. -*) + This module implements a lock-free bounded queue based on Michael-Scott's queue + algorithm. Adding a capacity to this algorithm adds a general overhead to the + operations, and thus, it is recommended to use the unbounded queue + {!Saturn.Queue} if you don't need it. + *) (** {1 API} *) @@ -29,31 +29,31 @@ module type CUE = sig val create : ?capacity:int -> unit -> 'a t (** [create ~capacity ()] creates a new empty bounded queue with a maximum - capacity of [capacity]. The default [capacity] value is [Int.max_int].*) + capacity of [capacity]. The default [capacity] value is [Int.max_int].*) val of_list_exn : ?capacity:int -> 'a list -> 'a t - (** [of_list list] creates a new queue from a list. - - @raises Full is the lenght of [list] is greater tant [capacity]. + (** [of_list_exn ~capacity list] creates a new queue from a list. - {[ - # let t : int t = of_list_exn [1;2;3;4] - val t : int t = - # pop_opt t - - : int option = Some 1 - # pop_opt t - - : int option = Some 2 - # length t - - : int = 2 - ]} - *) + @raises Full if the length of [list] is greater than [capacity]. + + {[ + # let t : int t = of_list_exn [1;2;3;4] + val t : int t = + # pop_opt t + - : int option = Some 1 + # pop_opt t + - : int option = Some 2 + # length t + - : int = 2 + ]} + *) val length : 'a t -> int (** [length queue] returns the number of elements currently in the [queue]. *) val capacity_of : 'a t -> int (** [capacity_of queue] returns the maximum number of elements that the [queue] - can hold. *) + can hold. *) val is_empty : 'a t -> bool (** [is_empty queue] returns [true] if the [queue] is empty, otherwise [false]. *) @@ -62,29 +62,29 @@ module type CUE = sig exception Empty (** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty - stack. *) + stack. *) val peek_exn : 'a t -> 'a (** [peek_exn queue] returns the first element of the [queue] without removing it. - - @raises Empty if the [queue] is empty. *) + + @raises Empty if the [queue] is empty. *) val peek_opt : 'a t -> 'a option (** [peek_opt queue] returns [Some] of the first element of the [queue] without - removing it, or [None] if the [queue] is empty. *) + removing it, or [None] if the [queue] is empty. *) val pop_exn : 'a t -> 'a (** [pop_exn queue] removes and returns the first element of the [queue]. - - @raises Empty if the [queue] is empty. *) + + @raises Empty if the [queue] is empty. *) val pop_opt : 'a t -> 'a option (** [pop_opt queue] removes and returns [Some] of the first element of the [queue], - or [None] if the [queue] is empty. *) + or [None] if the [queue] is empty. *) val drop_exn : 'a t -> unit (** [drop_exn queue] removes the top element of the [queue]. - @raises Empty if the [queue] is empty. *) + @raises Empty if the [queue] is empty. *) (** {2 Producer functions} *) @@ -93,11 +93,11 @@ module type CUE = sig val push_exn : 'a t -> 'a -> unit (** [push_exn queue element] adds [element] at the end of the [queue]. - - @raises Full if the [queue] is full. *) + + @raises Full if the [queue] is full. *) val try_push : 'a t -> 'a -> bool (** [try_push queue element] tries to add [element] at the end of the [queue]. - Returns [true] if the element was successfully added, or [false] if the - queue is full. *) + Returns [true] if the element was successfully added, or [false] if the + queue is full. *) end From f3a4a8da7b1f12fbf875b171d12a8fefd7368ff5 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 11:01:11 +0100 Subject: [PATCH 08/19] Factorize code between the safe and unsafe implementation. --- src/cue/{cue.ml => cue.body.ml} | 117 ++-- src/cue/cue.head_safe.ml | 28 + ...{cue_unsafe_node.ml => cue.head_unsafe.ml} | 14 +- src/cue/cue_unsafe.ml | 227 -------- src/cue/dune | 19 + test/cue/cue_unsafe_node.ml | 32 ++ test/cue/dscheck_cue.ml | 528 +++++++++--------- test/cue/stm_cue.ml | 15 +- 8 files changed, 409 insertions(+), 571 deletions(-) rename src/cue/{cue.ml => cue.body.ml} (68%) create mode 100644 src/cue/cue.head_safe.ml rename src/cue/{cue_unsafe_node.ml => cue.head_unsafe.ml} (66%) delete mode 100644 src/cue/cue_unsafe.ml create mode 100644 src/cue/dune diff --git a/src/cue/cue.ml b/src/cue/cue.body.ml similarity index 68% rename from src/cue/cue.ml rename to src/cue/cue.body.ml index 1e654b48..2300fe6d 100644 --- a/src/cue/cue.ml +++ b/src/cue/cue.body.ml @@ -12,20 +12,6 @@ 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, _) node = - | Null : ('a, [> `Null ]) node - | Node : { - next : 'a link Atomic.t; - mutable value : 'a; - mutable capacity : int; - mutable counter : int; - } - -> ('a, [> `Node ]) node - -and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] - -exception Full -exception Empty let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity @@ -37,26 +23,18 @@ let[@inline] get_counter (Node r : (_, [< `Node ]) node) = r.counter let[@inline] set_counter (Node r : (_, [< `Node ]) node) value = r.counter <- value -let[@inline] get_next (Node node : (_, [< `Node ]) node) = Atomic.get node.next - -let[@inline] compare_and_set_next (Node node : (_, [< `Node ]) node) before - after = - Atomic.compare_and_set node.next before after - -let[@inline] link_as_node (Link n) : (_, [< `Node ]) node = - match n with Null -> assert false | Node _ as node -> node - type 'a t = { head : ('a, [ `Node ]) node Atomic.t; capacity : int; tail : ('a, [ `Node ]) node Atomic.t; } +exception Full +exception Empty + let create ?(capacity = Int.max_int) () = let value = Obj.magic () in - let node = - Node { next = Atomic.make (Link Null); value; capacity; counter = 0 } - in + let node = make_node ~value ~capacity ~counter:0 Null in let head = Atomic.make_contended node and tail = Atomic.make_contended node in { head; capacity; tail } @@ -68,52 +46,38 @@ let of_list_exn ?(capacity = Int.max_int) list : 'a t = | [] -> create ~capacity () | hd :: tl -> let tail = - Node - { - value = hd; - counter = len; - capacity = capacity - len - 1; - next = Atomic.make (Link Null); - } + make_node ~value:hd ~capacity:(capacity - len - 1) ~counter:len Null in let _, _, next = List.fold_left (fun (counter, capacity, next) value -> ( counter - 1, capacity + 1, - Node - { value; counter; capacity; next = Atomic.make (Link next) } - )) + make_node ~value ~capacity ~counter next )) (len - 1, capacity - len, tail) tl in let head = Atomic.make_contended - @@ Node - { - value = Obj.magic (); - capacity; - counter = 0; - next = Atomic.make (Link next); - } + (make_node ~value:(Obj.magic ()) ~capacity ~counter:0 next) in + { head; capacity; tail = Atomic.make tail } let capacity_of t = t.capacity let is_empty t = - let (Node head) = Atomic.get t.head in - Atomic.get head.next == Link Null + let head = Atomic.get t.head in + fenceless_get_next head == Link Null let rec snapshot t = - let old_head = Atomic.get t.head in - let (Node tail as old_tail) = Atomic.get t.tail in - match Atomic.get tail.next with + let head = Atomic.get t.head in + let tail = fenceless_get t.tail in + match fenceless_get_next tail with | Link (Node _ as node) -> - Atomic.compare_and_set t.tail old_tail node |> ignore; + Atomic.compare_and_set t.tail tail node |> ignore; snapshot t - | Link Null -> - if Atomic.get t.head != old_head then snapshot t else (old_head, old_tail) + | Link Null -> if Atomic.get t.head != head then snapshot t else (head, tail) let length t = let head, tail = snapshot t in @@ -125,16 +89,14 @@ type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly let rec peek_as : type a r. a t -> (a, r) poly -> r = fun t poly -> - let (Node head as old_head) = Atomic.get t.head in - match Atomic.get head.next with + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with | Link Null -> ( match poly with Value -> raise Empty | Option -> None) | Link (Node r) -> ( let value = r.value in if Atomic.get t.head != old_head then peek_as t poly else match poly with Value -> value | Option -> Some value) -let[@inline] peek_opt t = peek_as t Option -let[@inline] peek_exn t = peek_as t Value (* *) type ('a, _) poly2 = @@ -144,8 +106,8 @@ type ('a, _) poly2 = let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = fun t backoff poly -> - let (Node head as old_head) = Atomic.get t.head in - match Atomic.get head.next with + let old_head = Atomic.get t.head in + match fenceless_get_next old_head with | Link Null -> ( match poly with Option -> None | Value | Unit -> raise Empty) | Link (Node node as new_head) -> @@ -156,9 +118,6 @@ let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = end else pop_as t (Backoff.once backoff) poly -let[@inline] pop_opt t = pop_as t Backoff.default Option -let[@inline] pop_exn t = pop_as t Backoff.default Value -let[@inline] drop_exn t = pop_as t Backoff.default Unit (* *) let rec fix_tail tail new_tail = @@ -170,35 +129,51 @@ let rec fix_tail tail new_tail = (* *) -let rec try_push t new_node old_tail = +type _ mono = Bool : bool mono | Unit : unit mono + +let rec push_as : + type r. 'a t -> ('a, [ `Node ]) node -> ('a, [ `Node ]) node -> r mono -> r + = + fun t new_node old_tail mono -> let capacity = get_capacity old_tail in - if capacity = 0 then + if capacity = 0 then begin let old_head = Atomic.get t.head in let length = get_counter old_tail - get_counter old_head in let capacity = t.capacity - length in - 0 < capacity - && begin - set_capacity old_tail capacity; - try_push t new_node old_tail - end + if 0 < capacity then begin + set_capacity old_tail capacity; + push_as t new_node old_tail mono + end + else match mono with Unit -> raise Full | Bool -> false + end else begin set_capacity new_node (capacity - 1); set_counter new_node (get_counter old_tail + 1); if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then - try_push t new_node (link_as_node (get_next old_tail)) + push_as t new_node (link_as_node (get_next old_tail)) mono else begin if not (Atomic.compare_and_set t.tail old_tail new_node) then fix_tail t.tail new_node; - true + match mono with Unit -> () | Bool -> true end end (* *) +let[@inline] peek_opt t = peek_as t Option +let[@inline] peek_exn t = peek_as t Value +let[@inline] pop_opt t = pop_as t Backoff.default Option +let[@inline] pop_exn t = pop_as t Backoff.default Value +let[@inline] drop_exn t = pop_as t Backoff.default Unit + let[@inline] try_push t value = let new_node = Node { next = Atomic.make (Link Null); value; capacity = 0; counter = 0 } in - try_push t new_node (Atomic.get t.tail) + push_as t new_node (Atomic.get t.tail) Bool -let[@inline] push_exn t value = if not (try_push t value) then raise Full +let[@inline] push_exn t value = + let new_node = + Node { next = Atomic.make (Link Null); value; capacity = 0; counter = 0 } + in + push_as t new_node (Atomic.get t.tail) Unit diff --git a/src/cue/cue.head_safe.ml b/src/cue/cue.head_safe.ml new file mode 100644 index 00000000..e30f3338 --- /dev/null +++ b/src/cue/cue.head_safe.ml @@ -0,0 +1,28 @@ +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + next : 'a link Atomic.t; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +let[@inline] make_node ~value ~capacity ~counter next = + Node { next = Atomic.make (Link next); value; capacity; counter } + +let[@inline] link_as_node (Link n) : (_, [< `Node ]) node = + match n with Null -> assert false | Node _ as node -> node + +let[@inline] get_next (Node node : (_, [< `Node ]) node) = Atomic.get node.next + +let[@inline] fenceless_get_next (Node node : (_, [< `Node ]) node) = + Atomic.get node.next + +let[@inline] compare_and_set_next (Node node : (_, [< `Node ]) node) before + after = + Atomic.compare_and_set node.next before after + +let fenceless_get = Atomic.get diff --git a/src/cue/cue_unsafe_node.ml b/src/cue/cue.head_unsafe.ml similarity index 66% rename from src/cue/cue_unsafe_node.ml rename to src/cue/cue.head_unsafe.ml index 292ff99f..1c397046 100644 --- a/src/cue/cue_unsafe_node.ml +++ b/src/cue/cue.head_unsafe.ml @@ -12,10 +12,20 @@ type ('a, _) node = and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] +let[@inline] make_node ~value ~capacity ~counter next = + Node { _next = Link next; value; capacity; counter } + external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t = "%identity" -let[@inline] make_node ~value ~capacity ~counter next = - Node { _next = Link next; value; capacity; counter } +let[@inline] get_next node = Atomic.get (next_as_atomic node) + +let[@inline] fenceless_get_next node = + Atomic.fenceless_get (next_as_atomic node) + +let[@inline] compare_and_set_next node before after = + Atomic.compare_and_set (next_as_atomic node) before after + +let fenceless_get = Atomic.fenceless_get diff --git a/src/cue/cue_unsafe.ml b/src/cue/cue_unsafe.ml deleted file mode 100644 index 9195dd8c..00000000 --- a/src/cue/cue_unsafe.ml +++ /dev/null @@ -1,227 +0,0 @@ -(* Copyright (c) 2023-2024, Vesa Karvonen - - 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. *) - -module Atomic = Multicore_magic.Transparent_atomic -module Node = Cue_unsafe_node -open Node - -let[@inline] get_capacity (Node r : (_, [< `Node ]) node) = r.capacity - -let[@inline] set_capacity (Node r : (_, [< `Node ]) node) value = - r.capacity <- value - -let[@inline] get_counter (Node r : (_, [< `Node ]) node) = r.counter - -let[@inline] set_counter (Node r : (_, [< `Node ]) node) value = - r.counter <- value - -let[@inline] get_next node = Atomic.get (next_as_atomic node) - -let[@inline] fenceless_get_next node = - Atomic.fenceless_get (next_as_atomic node) - -let[@inline] compare_and_set_next node before after = - Atomic.compare_and_set (next_as_atomic node) before after - -type 'a t = { - head : ('a, [ `Node ]) node Atomic.t; - capacity : int; - tail : ('a, [ `Node ]) node Atomic.t; -} - -exception Full -exception Empty - -let create ?(capacity = Int.max_int) () = - let value = Obj.magic () in - let node = make_node ~value ~capacity ~counter:0 Null in - let head = Atomic.make node |> Multicore_magic.copy_as_padded - and tail = Atomic.make node |> Multicore_magic.copy_as_padded in - { head; capacity; tail } |> Multicore_magic.copy_as_padded - -let of_list_exn ?(capacity = Int.max_int) list : 'a t = - let len = List.length list in - if len > capacity then raise Full - else - match list |> List.rev with - | [] -> create ~capacity () - | hd :: tl -> - let tail = - make_node ~value:hd ~capacity:(capacity - len - 1) ~counter:len Null - in - let _, _, next = - List.fold_left - (fun (counter, capacity, next) value -> - ( counter - 1, - capacity + 1, - make_node ~value ~capacity ~counter next )) - (len - 1, capacity - len, tail) - tl - in - let head = - Atomic.make_contended - (make_node ~value:(Obj.magic ()) ~capacity ~counter:0 next) - in - - { head; capacity; tail = Atomic.make tail } - -let capacity_of t = t.capacity - -let is_empty t = - let head = Atomic.get t.head in - fenceless_get_next head == Link Null - -let rec snapshot t = - let head = Atomic.get t.head in - let tail = Atomic.fenceless_get t.tail in - match fenceless_get_next tail with - | Link (Node _ as node) -> - Atomic.compare_and_set t.tail tail node |> ignore; - snapshot t - | Link Null -> if Atomic.get t.head != head then snapshot t else (head, tail) - -let length t = - let head, tail = snapshot t in - get_counter tail - get_counter head - -(* *) - -let rec peek_exn t = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> raise Empty - | Link (Node r) -> - let value = r.value in - if Atomic.get t.head != old_head then peek_exn t else value - -(* *) - -let rec peek_opt t = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> None - | Link (Node r) -> - let value = r.value in - if Atomic.get t.head != old_head then peek_opt t else Some value - -(* *) - -let rec pop_exn t backoff = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> raise Empty - | Link (Node node as new_head) -> - if Atomic.compare_and_set t.head old_head new_head then begin - let value = node.value in - node.value <- Obj.magic (); - value - end - else pop_exn t (Backoff.once backoff) - -(* *) - -let rec pop_opt t backoff = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> None - | Link (Node node as new_head) -> - if Atomic.compare_and_set t.head old_head new_head then begin - let value = node.value in - node.value <- Obj.magic (); - Some value - end - else pop_opt t (Backoff.once backoff) -(* *) - -let rec drop_exn t backoff = - let old_head = Atomic.get t.head in - match fenceless_get_next old_head with - | Link Null -> raise Empty - | Link (Node node as new_head) -> - if Atomic.compare_and_set t.head old_head new_head then begin - node.value <- Obj.magic () - end - else drop_exn t (Backoff.once backoff) - -(* *) - -let rec fix_tail tail new_tail = - let old_tail = Atomic.get tail in - if - get_next new_tail == Link Null - && not (Atomic.compare_and_set tail old_tail new_tail) - then fix_tail tail new_tail - -(* *) - -let rec push_exn t new_node old_tail = - let capacity = get_capacity old_tail in - if capacity = 0 then begin - let old_head = Atomic.get t.head in - let length = get_counter old_tail - get_counter old_head in - let capacity = t.capacity - length in - if 0 < capacity then begin - set_capacity old_tail capacity; - push_exn t new_node old_tail - end - else raise Full - end - else begin - set_capacity new_node (capacity - 1); - set_counter new_node (get_counter old_tail + 1); - if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then - push_exn t new_node (link_as_node (get_next old_tail)) - else begin - if not (Atomic.compare_and_set t.tail old_tail new_node) then - fix_tail t.tail new_node - end - end - -(* *) - -let rec try_push t new_node old_tail = - let capacity = get_capacity old_tail in - if capacity = 0 then - let old_head = Atomic.get t.head in - let length = get_counter old_tail - get_counter old_head in - let capacity = t.capacity - length in - 0 < capacity - && begin - set_capacity old_tail capacity; - try_push t new_node old_tail - end - else begin - set_capacity new_node (capacity - 1); - set_counter new_node (get_counter old_tail + 1); - if not (compare_and_set_next old_tail (Link Null) (Link new_node)) then - try_push t new_node (link_as_node (get_next old_tail)) - else begin - if not (Atomic.compare_and_set t.tail old_tail new_node) then - fix_tail t.tail new_node; - true - end - end - -(* *) -let[@inline] drop_exn t = drop_exn t Backoff.default -let[@inline] pop_exn t = pop_exn t Backoff.default -let[@inline] pop_opt t = pop_opt t Backoff.default - -let[@inline] push_exn t value = - let new_node = make_node ~value ~capacity:0 ~counter:0 Null in - push_exn t new_node (Atomic.get t.tail) - -let[@inline] try_push t value = - let new_node = make_node ~value ~capacity:0 ~counter:0 Null in - try_push t new_node (Atomic.get t.tail) diff --git a/src/cue/dune b/src/cue/dune new file mode 100644 index 00000000..5be89ff9 --- /dev/null +++ b/src/cue/dune @@ -0,0 +1,19 @@ +(rule + (action + (with-stdout-to + cue.ml + (progn + (echo "# 1 \"cue.head_safe.ml\"\n") + (cat cue.head_safe.ml) + (echo "# 1 \"cue.body.ml\"\n") + (cat cue.body.ml))))) + +(rule + (action + (with-stdout-to + cue_unsafe.ml + (progn + (echo "# 1 \"cue.head_unsafe.ml\"\n") + (cat cue.head_safe.ml) + (echo "# 1 \"cue.body.ml\"\n") + (cat cue.body.ml))))) \ No newline at end of file diff --git a/test/cue/cue_unsafe_node.ml b/test/cue/cue_unsafe_node.ml index 4b15256d..9f0b9280 100644 --- a/test/cue/cue_unsafe_node.ml +++ b/test/cue/cue_unsafe_node.ml @@ -20,3 +20,35 @@ let[@inline] next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t = let[@inline] make_node ~value ~capacity ~counter next = Node { _next = Atomic.make (Link next); value; capacity; counter } + +module Atomic = Multicore_magic.Transparent_atomic + +type ('a, _) node = + | Null : ('a, [> `Null ]) node + | Node : { + mutable _next : 'a link; + mutable value : 'a; + mutable capacity : int; + mutable counter : int; + } + -> ('a, [> `Node ]) node + +and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] + +let[@inline] make_node ~value ~capacity ~counter next = + Node { _next = Link next; value; capacity; counter } + +external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" + +external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t + = "%identity" + +let[@inline] get_next node = Atomic.get (next_as_atomic node) + +let[@inline] fenceless_get_next node = + Atomic.fenceless_get (next_as_atomic node) + +let[@inline] compare_and_set_next node before after = + Atomic.compare_and_set (next_as_atomic node) before after + +let fenceless_get = Atomic.fenceless_get diff --git a/test/cue/dscheck_cue.ml b/test/cue/dscheck_cue.ml index d7f41541..648d82e1 100644 --- a/test/cue/dscheck_cue.ml +++ b/test/cue/dscheck_cue.ml @@ -2,289 +2,283 @@ module Atomic = Dscheck.TracedAtomic -module Dscheck_cue (Cue : Cue_intf.CUE) = struct - let drain cue = - let rec pop_until_empty acc = - match Cue.pop_opt cue with - | None -> acc |> List.rev - | Some v -> pop_until_empty (v :: acc) - in - pop_until_empty [] - - let push_pop () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let items_total = 4 in - - (* producer *) +(* Dscheck only tests the safe implementation of Cue. To make Cue_unsafe compatible with Dscheck, it needs to be modified to essentially become the safe version. *) + +let drain cue = + let rec pop_until_empty acc = + match Cue.pop_opt cue with + | None -> acc |> List.rev + | Some v -> pop_until_empty (v :: acc) + in + pop_until_empty [] + +let push_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Cue.pop_opt cue with + | None -> () + | Some v -> popped := v :: !popped + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain cue in + let pushed = List.init items_total (fun x -> x + 1) in + List.sort Int.compare (!popped @ remaining) = pushed))) + +let push_drop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let dropped = ref 0 in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Cue.drop_exn cue with + | () -> dropped := !dropped + 1 + | exception Cue.Empty -> () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain cue in + remaining + = List.init (items_total - !dropped) (fun x -> x + !dropped + 1)))) + +let push_pop_with_capacity () = + Atomic.trace (fun () -> + let cue = Cue.create ~capacity:2 () in + let items_total = 4 in + + (* producer *) + let pushed = Array.make items_total false in + Atomic.spawn (fun () -> + Array.iteri (fun i _ -> pushed.(i) <- Cue.try_push cue i) pushed); + + (* consumer *) + let popped = Array.make items_total None in + Atomic.spawn (fun () -> + Array.iteri (fun i _ -> popped.(i) <- Cue.pop_opt cue) popped); + (* checks*) + Atomic.final (fun () -> + let popped = Array.to_list popped |> List.filter_map Fun.id in + let remaining = drain cue in + Atomic.check (fun () -> + let xor a b = (a && not b) || ((not a) && b) in + try + Array.iteri + (fun i elt -> + if elt then begin + if not @@ xor (List.mem i remaining) (List.mem i popped) + then raise Exit + end + else if List.mem i remaining || List.mem i popped then + raise Exit) + pushed; + true + with _ -> false))) + +let push_push () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 6 in + + (* two producers *) + for i = 0 to 1 do Atomic.spawn (fun () -> - for i = 1 to items_total do - Cue.try_push cue i |> ignore - done); + for j = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + Cue.try_push cue (i + (j * 2)) |> ignore + done) + done; - (* consumer *) - let popped = ref [] in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - match Cue.pop_opt cue with - | None -> () - | Some v -> popped := v :: !popped - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = drain cue in - let pushed = List.init items_total (fun x -> x + 1) in - List.sort Int.compare (!popped @ remaining) = pushed))) - - let push_drop () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let items_total = 4 in - - (* producer *) - Atomic.spawn (fun () -> - for i = 1 to items_total do - Cue.try_push cue i |> ignore - done); + (* checks*) + Atomic.final (fun () -> + let items = drain cue in - (* consumer *) - let dropped = ref 0 in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - match Cue.drop_exn cue with - | () -> dropped := !dropped + 1 - | exception Cue.Empty -> () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = drain cue in - remaining - = List.init (items_total - !dropped) (fun x -> x + !dropped + 1)))) - - let push_pop_with_capacity () = - Atomic.trace (fun () -> - let cue = Cue.create ~capacity:2 () in - let items_total = 4 in - - (* producer *) - let pushed = Array.make items_total false in - Atomic.spawn (fun () -> - Array.iteri (fun i _ -> pushed.(i) <- Cue.try_push cue i) pushed); + (* got the same number of items out as in *) + Atomic.check (fun () -> items_total = List.length items); + + (* they are in fifo order *) + let odd, even = List.partition (fun v -> v mod 2 == 0) items in + + Atomic.check (fun () -> List.sort Int.compare odd = odd); + Atomic.check (fun () -> List.sort Int.compare even = even))) + +let push_push_with_capacity () = + Atomic.trace (fun () -> + let capacity = 3 in + let cue = Cue.create ~capacity () in + let items_total = 6 in - (* consumer *) - let popped = Array.make items_total None in + (* two producers *) + for i = 0 to 1 do Atomic.spawn (fun () -> - Array.iteri (fun i _ -> popped.(i) <- Cue.pop_opt cue) popped); - (* checks*) - Atomic.final (fun () -> - let popped = Array.to_list popped |> List.filter_map Fun.id in - let remaining = drain cue in - Atomic.check (fun () -> - let xor a b = (a && not b) || ((not a) && b) in - try - Array.iteri - (fun i elt -> - if elt then begin - if not @@ xor (List.mem i remaining) (List.mem i popped) - then raise Exit - end - else if List.mem i remaining || List.mem i popped then - raise Exit) - pushed; - true - with _ -> false))) - - let push_push () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let items_total = 6 in - - (* two producers *) - for i = 0 to 1 do + for j = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + Cue.try_push cue (i + (j * 2)) |> ignore + done) + done; + + (* checks*) + Atomic.final (fun () -> + let items = drain cue in + + (* got the same number of items out as in *) + Atomic.check (fun () -> capacity = List.length items))) + +let pop_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done; + + (* two consumers *) + let lists = [ ref []; ref [] ] in + List.iter + (fun list -> Atomic.spawn (fun () -> - for j = 1 to items_total / 2 do + for _ = 1 to items_total / 2 do (* even nums belong to thr 1, odd nums to thr 2 *) - Cue.try_push cue (i + (j * 2)) |> ignore + list := Option.get (Cue.pop_opt cue) :: !list done) - done; + |> ignore) + lists; - (* checks*) - Atomic.final (fun () -> - let items = drain cue in + (* checks*) + Atomic.final (fun () -> + let l1 = !(List.nth lists 0) in + let l2 = !(List.nth lists 1) in - (* got the same number of items out as in *) - Atomic.check (fun () -> items_total = List.length items); + (* got the same number of items out as in *) + Atomic.check (fun () -> items_total = List.length l1 + List.length l2); - (* they are in fifo order *) - let odd, even = List.partition (fun v -> v mod 2 == 0) items in + (* they are in fifo order *) + Atomic.check (fun () -> List.sort Int.compare l1 = List.rev l1); + Atomic.check (fun () -> List.sort Int.compare l2 = List.rev l2))) - Atomic.check (fun () -> List.sort Int.compare odd = odd); - Atomic.check (fun () -> List.sort Int.compare even = even))) +let two_domains () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let n1, n2 = (1, 2) in - let push_push_with_capacity () = - Atomic.trace (fun () -> - let capacity = 3 in - let cue = Cue.create ~capacity () in - let items_total = 6 in - - (* two producers *) - for i = 0 to 1 do + (* two producers *) + let lists = + [ + (List.init n1 (fun i -> i), ref []); + (List.init n2 (fun i -> i + n1), ref []); + ] + in + List.iter + (fun (lpush, lpop) -> Atomic.spawn (fun () -> - for j = 1 to items_total / 2 do - (* even nums belong to thr 1, odd nums to thr 2 *) - Cue.try_push cue (i + (j * 2)) |> ignore - done) - done; - - (* checks*) - Atomic.final (fun () -> - let items = drain cue in - - (* got the same number of items out as in *) - Atomic.check (fun () -> capacity = List.length items))) - - let pop_pop () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let items_total = 4 in - - for i = 1 to items_total do - Cue.try_push cue i |> ignore - done; - - (* two consumers *) - let lists = [ ref []; ref [] ] in - List.iter - (fun list -> - Atomic.spawn (fun () -> - for _ = 1 to items_total / 2 do + List.iter + (fun elt -> (* even nums belong to thr 1, odd nums to thr 2 *) - list := Option.get (Cue.pop_opt cue) :: !list - done) - |> ignore) - lists; - - (* checks*) - Atomic.final (fun () -> - let l1 = !(List.nth lists 0) in - let l2 = !(List.nth lists 1) in - - (* got the same number of items out as in *) - Atomic.check (fun () -> - items_total = List.length l1 + List.length l2); - - (* they are in fifo order *) - Atomic.check (fun () -> List.sort Int.compare l1 = List.rev l1); - Atomic.check (fun () -> List.sort Int.compare l2 = List.rev l2))) - - let two_domains () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let n1, n2 = (1, 2) in - - (* two producers *) - let lists = - [ - (List.init n1 (fun i -> i), ref []); - (List.init n2 (fun i -> i + n1), ref []); - ] - in - List.iter - (fun (lpush, lpop) -> - Atomic.spawn (fun () -> - List.iter - (fun elt -> - (* even nums belong to thr 1, odd nums to thr 2 *) - Cue.try_push cue elt |> ignore; - lpop := Option.get (Cue.pop_opt cue) :: !lpop) - lpush) - |> ignore) - lists; - - (* checks*) - Atomic.final (fun () -> - let lpop1 = !(List.nth lists 0 |> snd) in - let lpop2 = !(List.nth lists 1 |> snd) in - - (* got the same number of items out as in *) - Atomic.check (fun () -> List.length lpop1 = 1); - Atomic.check (fun () -> List.length lpop2 = 2); - - (* no element are missing *) - Atomic.check (fun () -> - List.sort Int.compare (lpop1 @ lpop2) - = List.init (n1 + n2) (fun i -> i)))) - - let two_domains_more_pop () = - Atomic.trace (fun () -> - let cue = Cue.create () in - let n1, n2 = (2, 1) in - - (* two producers *) - let lists = - [ - (List.init n1 (fun i -> i), ref []); - (List.init n2 (fun i -> i + n1), ref []); - ] - in - List.iter - (fun (lpush, lpop) -> - Atomic.spawn (fun () -> - List.iter - (fun elt -> - Cue.try_push cue elt |> ignore; - lpop := Cue.pop_opt cue :: !lpop; - lpop := Cue.pop_opt cue :: !lpop) - lpush) - |> ignore) - lists; - - (* checks*) - Atomic.final (fun () -> - let lpop1 = - !(List.nth lists 0 |> snd) - |> List.filter Option.is_some |> List.map Option.get - in - let lpop2 = - !(List.nth lists 1 |> snd) - |> List.filter Option.is_some |> List.map Option.get - in - - (* got the same number of items out as in *) - Atomic.check (fun () -> - n1 + n2 = List.length lpop1 + List.length lpop2); - - (* no element are missing *) - Atomic.check (fun () -> - List.sort Int.compare (lpop1 @ lpop2) - = List.init (n1 + n2) (fun i -> i)))) - - let tests name = - let open Alcotest in - [ - ( "basic " ^ name, + Cue.try_push cue elt |> ignore; + lpop := Option.get (Cue.pop_opt cue) :: !lpop) + lpush) + |> ignore) + lists; + + (* checks*) + Atomic.final (fun () -> + let lpop1 = !(List.nth lists 0 |> snd) in + let lpop2 = !(List.nth lists 1 |> snd) in + + (* got the same number of items out as in *) + Atomic.check (fun () -> List.length lpop1 = 1); + Atomic.check (fun () -> List.length lpop2 = 2); + + (* no element are missing *) + Atomic.check (fun () -> + List.sort Int.compare (lpop1 @ lpop2) + = List.init (n1 + n2) (fun i -> i)))) + +let two_domains_more_pop () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let n1, n2 = (2, 1) in + + (* two producers *) + let lists = [ - test_case "1-producer-1-consumer" `Slow push_pop; - test_case "1-producer-1-consumer-capacity" `Slow - push_pop_with_capacity; - test_case "1-push-1-drop" `Slow push_drop; - test_case "2-producers" `Slow push_push; - test_case "2-producers-capacity" `Slow push_push_with_capacity; - test_case "2-consumers" `Slow pop_pop; - test_case "2-domains" `Slow two_domains; - test_case "2-domains-more-pops" `Slow two_domains_more_pop; - ] ); - ] -end + (List.init n1 (fun i -> i), ref []); + (List.init n2 (fun i -> i + n1), ref []); + ] + in + List.iter + (fun (lpush, lpop) -> + Atomic.spawn (fun () -> + List.iter + (fun elt -> + Cue.try_push cue elt |> ignore; + lpop := Cue.pop_opt cue :: !lpop; + lpop := Cue.pop_opt cue :: !lpop) + lpush) + |> ignore) + lists; + + (* checks*) + Atomic.final (fun () -> + let lpop1 = + !(List.nth lists 0 |> snd) + |> List.filter Option.is_some |> List.map Option.get + in + let lpop2 = + !(List.nth lists 1 |> snd) + |> List.filter Option.is_some |> List.map Option.get + in + + (* got the same number of items out as in *) + Atomic.check (fun () -> + n1 + n2 = List.length lpop1 + List.length lpop2); + + (* no element are missing *) + Atomic.check (fun () -> + List.sort Int.compare (lpop1 @ lpop2) + = List.init (n1 + n2) (fun i -> i)))) + +let tests = + let open Alcotest in + [ + ( "basic", + [ + test_case "1-producer-1-consumer" `Slow push_pop; + test_case "1-producer-1-consumer-capacity" `Slow push_pop_with_capacity; + test_case "1-push-1-drop" `Slow push_drop; + test_case "2-producers" `Slow push_push; + test_case "2-producers-capacity" `Slow push_push_with_capacity; + test_case "2-consumers" `Slow pop_pop; + test_case "2-domains" `Slow two_domains; + test_case "2-domains-more-pops" `Slow two_domains_more_pop; + ] ); + ] let () = - let module Safe = Dscheck_cue (Cue) in - let safe_test = Safe.tests "safe" in - let module Unsafe = Dscheck_cue (Cue_unsafe) in - let unsafe_test = Unsafe.tests "unsafe" in let open Alcotest in - run "dscheck_cue" (safe_test @ unsafe_test) + run "dscheck_cue" tests diff --git a/test/cue/stm_cue.ml b/test/cue/stm_cue.ml index f3638636..da6a9c11 100644 --- a/test/cue/stm_cue.ml +++ b/test/cue/stm_cue.ml @@ -51,7 +51,12 @@ module STM_cue (Cue : Cues.Cue_tests) = struct let run c d = match c with - | Try_push i -> Res (bool, Cue.try_push d i) + | Try_push i -> + Res + ( bool, + match Cue.push_exn d i with + | () -> true + | exception Cue.Full -> true (*Cue.try_push d i*) ) | Pop_opt -> Res (option int, Cue.pop_opt d) | Peek_opt -> Res (option int, Cue.peek_opt d) | Is_empty -> Res (bool, Cue.is_empty d) @@ -73,10 +78,12 @@ module STM_cue (Cue : Cues.Cue_tests) = struct end let () = + (* Since Cue and Cue_unsafe share the same implementation, it is not necessary + to test both of them. *) Random.self_init (); - let module Safe = STM_cue (Cues.Cue) in - let exit_code = Safe.run () in - if exit_code <> 0 then exit exit_code + if Random.bool () then + let module Safe = STM_cue (Cues.Cue) in + Safe.run () |> exit else let module Unsafe = STM_cue (Cues.Cue_unsafe) in Unsafe.run () |> exit From 8d5003bab99010862033b8ccacf635b5b65253fa Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 11:04:57 +0100 Subject: [PATCH 09/19] Add tests for drop_exn. --- test/cue/stm_cue.ml | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/test/cue/stm_cue.ml b/test/cue/stm_cue.ml index da6a9c11..71116d13 100644 --- a/test/cue/stm_cue.ml +++ b/test/cue/stm_cue.ml @@ -6,13 +6,20 @@ module Cue = Saturn.Cue module STM_cue (Cue : Cues.Cue_tests) = struct module Spec = struct - type cmd = Try_push of int | Pop_opt | Peek_opt | Length | Is_empty + type cmd = + | Try_push of int + | Pop_opt + | Peek_opt + | Drop_exn + | Length + | Is_empty let show_cmd c = match c with | Try_push i -> "Try_push " ^ string_of_int i | Pop_opt -> "Pop_opt" | Peek_opt -> "Peek_opt" + | Drop_exn -> "Drop_exn" | Length -> "Length" | Is_empty -> "Is_empty" @@ -27,6 +34,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct Gen.map (fun i -> Try_push i) int_gen; Gen.return Pop_opt; Gen.return Peek_opt; + Gen.return Drop_exn; Gen.return Length; Gen.return Is_empty; ]) @@ -39,7 +47,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct match c with | Try_push i -> if size = capacity then s else (capacity, size + 1, i :: content) - | Pop_opt -> ( + | Pop_opt | Drop_exn -> ( match List.rev content with | [] -> s | _ :: content' -> (capacity, size - 1, List.rev content')) @@ -59,6 +67,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | exception Cue.Full -> true (*Cue.try_push d i*) ) | Pop_opt -> Res (option int, Cue.pop_opt d) | Peek_opt -> Res (option int, Cue.peek_opt d) + | Drop_exn -> Res (result unit exn, protect Cue.drop_exn d) | Is_empty -> Res (bool, Cue.is_empty d) | Length -> Res (int, Cue.length d) @@ -69,6 +78,10 @@ module STM_cue (Cue : Cues.Cue_tests) = struct match List.rev content with | [] -> res = None | j :: _ -> res = Some j) + | Drop_exn, Res ((Result (Unit, Exn), _), res) -> ( + match List.rev content with + | [] -> res = Error Cue.Empty + | _ -> res = Ok ()) | Is_empty, Res ((Bool, _), res) -> res = (content = []) | Length, Res ((Int, _), res) -> res = size | _, _ -> false From eb31573a7f954b4b0337b97600222b638ca4eed0 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 12:12:02 +0100 Subject: [PATCH 10/19] Fix last commit. --- src/cue/cue.body.ml | 8 ++---- src/cue/dune | 4 +-- test/cue/cue_unsafe_node.ml | 54 ------------------------------------- test/cue/dune | 2 +- 4 files changed, 5 insertions(+), 63 deletions(-) delete mode 100644 test/cue/cue_unsafe_node.ml diff --git a/src/cue/cue.body.ml b/src/cue/cue.body.ml index 2300fe6d..acd36c45 100644 --- a/src/cue/cue.body.ml +++ b/src/cue/cue.body.ml @@ -167,13 +167,9 @@ let[@inline] pop_exn t = pop_as t Backoff.default Value let[@inline] drop_exn t = pop_as t Backoff.default Unit let[@inline] try_push t value = - let new_node = - Node { next = Atomic.make (Link Null); value; capacity = 0; counter = 0 } - in + let new_node = make_node ~value ~capacity:0 ~counter:0 Null in push_as t new_node (Atomic.get t.tail) Bool let[@inline] push_exn t value = - let new_node = - Node { next = Atomic.make (Link Null); value; capacity = 0; counter = 0 } - in + let new_node = make_node ~value ~capacity:0 ~counter:0 Null in push_as t new_node (Atomic.get t.tail) Unit diff --git a/src/cue/dune b/src/cue/dune index 5be89ff9..0dceb0e9 100644 --- a/src/cue/dune +++ b/src/cue/dune @@ -14,6 +14,6 @@ cue_unsafe.ml (progn (echo "# 1 \"cue.head_unsafe.ml\"\n") - (cat cue.head_safe.ml) + (cat cue.head_unsafe.ml) (echo "# 1 \"cue.body.ml\"\n") - (cat cue.body.ml))))) \ No newline at end of file + (cat cue.body.ml))))) diff --git a/test/cue/cue_unsafe_node.ml b/test/cue/cue_unsafe_node.ml deleted file mode 100644 index 9f0b9280..00000000 --- a/test/cue/cue_unsafe_node.ml +++ /dev/null @@ -1,54 +0,0 @@ -open Multicore_magic_dscheck -module Atomic = Multicore_magic.Transparent_atomic - -type ('a, _) node = - | Null : ('a, [> `Null ]) node - | Node : { - _next : 'a link Atomic.t; - mutable value : 'a; - mutable capacity : int; - mutable counter : int; - } - -> ('a, [> `Node ]) node - -and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] - -external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" - -let[@inline] next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t = - fun (Node r : ('a, [< `Node ]) node) -> r._next - -let[@inline] make_node ~value ~capacity ~counter next = - Node { _next = Atomic.make (Link next); value; capacity; counter } - -module Atomic = Multicore_magic.Transparent_atomic - -type ('a, _) node = - | Null : ('a, [> `Null ]) node - | Node : { - mutable _next : 'a link; - mutable value : 'a; - mutable capacity : int; - mutable counter : int; - } - -> ('a, [> `Node ]) node - -and 'a link = Link : ('a, [< `Null | `Node ]) node -> 'a link [@@unboxed] - -let[@inline] make_node ~value ~capacity ~counter next = - Node { _next = Link next; value; capacity; counter } - -external link_as_node : 'a link -> ('a, [ `Node ]) node = "%identity" - -external next_as_atomic : ('a, [< `Node ]) node -> 'a link Atomic.t - = "%identity" - -let[@inline] get_next node = Atomic.get (next_as_atomic node) - -let[@inline] fenceless_get_next node = - Atomic.fenceless_get (next_as_atomic node) - -let[@inline] compare_and_set_next node before after = - Atomic.compare_and_set (next_as_atomic node) before after - -let fenceless_get = Atomic.fenceless_get diff --git a/test/cue/dune b/test/cue/dune index e7b74fa4..608eb75d 100644 --- a/test/cue/dune +++ b/test/cue/dune @@ -24,7 +24,7 @@ (and (= %{arch_sixtyfour} false) (= %{architecture} arm))))) - (modules cue cue_unsafe cue_intf cue_unsafe_node dscheck_cue) + (modules cue cue_unsafe cue_intf dscheck_cue) (flags (:standard -open Multicore_magic_dscheck))) From 997ab2d5aa7c015107fa3b18e3e308c4e6b6cdce Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 12:17:35 +0100 Subject: [PATCH 11/19] Add is_full function, with tests. --- src/cue/cue.body.ml | 15 ++++++ src/cue/cue_intf.mli | 3 ++ test/cue/dscheck_cue.ml | 103 ++++++++++++++++++++++++++++++++++++++-- test/cue/stm_cue.ml | 6 +++ 4 files changed, 124 insertions(+), 3 deletions(-) diff --git a/src/cue/cue.body.ml b/src/cue/cue.body.ml index acd36c45..6e44356e 100644 --- a/src/cue/cue.body.ml +++ b/src/cue/cue.body.ml @@ -70,6 +70,21 @@ let is_empty t = let head = Atomic.get t.head in fenceless_get_next head == Link Null +let is_full t = + let tail = Atomic.get t.tail in + let capacity = get_capacity tail in + if capacity = 0 then begin + let old_head = Atomic.get t.head in + let length = get_counter tail - get_counter old_head in + let capacity = t.capacity - length in + if 0 < capacity then begin + set_capacity tail capacity; + false + end + else true + end + else false + let rec snapshot t = let head = Atomic.get t.head in let tail = fenceless_get t.tail in diff --git a/src/cue/cue_intf.mli b/src/cue/cue_intf.mli index f58fee40..a770b5b2 100644 --- a/src/cue/cue_intf.mli +++ b/src/cue/cue_intf.mli @@ -58,6 +58,9 @@ module type CUE = sig val is_empty : 'a t -> bool (** [is_empty queue] returns [true] if the [queue] is empty, otherwise [false]. *) + val is_full : 'a t -> bool + (** [is_full queue] returns [true] if the [queue] is full, otherwise [false]. *) + (** {2 Consumer functions} *) exception Empty diff --git a/test/cue/dscheck_cue.ml b/test/cue/dscheck_cue.ml index 648d82e1..56bdcf12 100644 --- a/test/cue/dscheck_cue.ml +++ b/test/cue/dscheck_cue.ml @@ -27,9 +27,13 @@ let push_pop () = let popped = ref [] in Atomic.spawn (fun () -> for _ = 1 to items_total do - match Cue.pop_opt cue with - | None -> () - | Some v -> popped := v :: !popped + begin + match Cue.pop_opt cue with + | None -> () + | Some v -> popped := v :: !popped + end; + (* Ensure is_empty does not interfere with other functions *) + Cue.is_empty cue |> ignore done); (* checks*) @@ -39,6 +43,95 @@ let push_pop () = let pushed = List.init items_total (fun x -> x + 1) in List.sort Int.compare (!popped @ remaining) = pushed))) +let is_empty () = + Atomic.trace (fun () -> + let cue = Cue.create () in + + (* producer *) + Atomic.spawn (fun () -> Cue.try_push cue 1 |> ignore); + + (* consumer *) + let res = ref false in + Atomic.spawn (fun () -> + match Cue.pop_opt cue with + | None -> res := true + | Some _ -> res := Cue.is_empty cue); + + (* checks*) + Atomic.final (fun () -> Atomic.check (fun () -> !res))) + +let push_length_is_full () = + Atomic.trace (fun () -> + let cue = Cue.create () in + let items_total = 4 in + + Cue.try_push cue 0 |> ignore; + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let length_res = ref [] in + let is_full_res = ref false in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + length_res := Cue.length cue :: !length_res; + is_full_res := Cue.is_full cue || !is_full_res + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> not !is_full_res); + + Atomic.check (fun () -> + let pushed = drain cue in + pushed = List.init (items_total + 1) Fun.id); + + Atomic.check (fun () -> + !length_res |> List.rev = List.sort compare !length_res + && List.for_all + (fun x -> x >= 1 && x <= items_total + 1) + !length_res))) + +let push_length_is_full_with_capacity () = + Atomic.trace (fun () -> + let capacity = 3 in + let cue = Cue.create ~capacity () in + let items_total = 5 in + + Cue.try_push cue 0 |> ignore; + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total - 1 do + Cue.try_push cue i |> ignore + done); + + (* consumer *) + let length_res = ref [] in + let test = ref true in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + let len = Cue.length cue in + length_res := len :: !length_res; + test := if len < capacity then !test else !test && Cue.is_full cue + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> !test); + + Atomic.check (fun () -> + let pushed = drain cue in + pushed = List.init capacity Fun.id); + + Atomic.check (fun () -> + !length_res |> List.rev = List.sort compare !length_res + && List.for_all (fun x -> x >= 1 && x <= capacity) !length_res))) + let push_drop () = Atomic.trace (fun () -> let cue = Cue.create () in @@ -269,6 +362,10 @@ let tests = ( "basic", [ test_case "1-producer-1-consumer" `Slow push_pop; + test_case "push-length-is_full" `Slow push_length_is_full; + test_case "push-length-is_full-capacity" `Slow + push_length_is_full_with_capacity; + test_case "2-domains-is_empty" `Slow is_empty; test_case "1-producer-1-consumer-capacity" `Slow push_pop_with_capacity; test_case "1-push-1-drop" `Slow push_drop; test_case "2-producers" `Slow push_push; diff --git a/test/cue/stm_cue.ml b/test/cue/stm_cue.ml index 71116d13..674eeef7 100644 --- a/test/cue/stm_cue.ml +++ b/test/cue/stm_cue.ml @@ -13,6 +13,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | Drop_exn | Length | Is_empty + | Is_full let show_cmd c = match c with @@ -22,6 +23,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | Drop_exn -> "Drop_exn" | Length -> "Length" | Is_empty -> "Is_empty" + | Is_full -> "Is_full" type state = int * int * int list type sut = int Cue.t @@ -37,6 +39,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct Gen.return Drop_exn; Gen.return Length; Gen.return Is_empty; + Gen.return Is_full; ]) let init_state = (100, 0, []) @@ -53,6 +56,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | _ :: content' -> (capacity, size - 1, List.rev content')) | Peek_opt -> s | Is_empty -> s + | Is_full -> s | Length -> s let precond _ _ = true @@ -69,6 +73,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | Peek_opt -> Res (option int, Cue.peek_opt d) | Drop_exn -> Res (result unit exn, protect Cue.drop_exn d) | Is_empty -> Res (bool, Cue.is_empty d) + | Is_full -> Res (bool, Cue.is_full d) | Length -> Res (int, Cue.length d) let postcond c ((capacity, size, content) : state) res = @@ -83,6 +88,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | [] -> res = Error Cue.Empty | _ -> res = Ok ()) | Is_empty, Res ((Bool, _), res) -> res = (content = []) + | Is_full, Res ((Bool, _), res) -> res = (size = capacity) | Length, Res ((Int, _), res) -> res = size | _, _ -> false end From fc5b494b7ff5b832b2e1effd4dda5ce0028ce2c9 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 16:42:13 +0100 Subject: [PATCH 12/19] Bench for the cue. --- bench/bench_cue.body.ml | 78 ++++++++++++++++++++++++++++++++++ bench/bench_cue.head.ml | 2 + bench/bench_cue_unsafe.head.ml | 2 + bench/dune | 20 +++++++++ bench/main.ml | 2 + 5 files changed, 104 insertions(+) create mode 100644 bench/bench_cue.body.ml create mode 100644 bench/bench_cue.head.ml create mode 100644 bench/bench_cue_unsafe.head.ml diff --git a/bench/bench_cue.body.ml b/bench/bench_cue.body.ml new file mode 100644 index 00000000..4821142f --- /dev/null +++ b/bench/bench_cue.body.ml @@ -0,0 +1,78 @@ +let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = + let t = Cue.create () in + + let op push = + if push then Cue.try_push t 101 |> ignore else Cue.pop_opt t |> ignore + in + + let init _ = + assert (Cue.is_empty t); + Util.generate_push_and_pop_sequence n_msgs + in + let work _ bits = Util.Bits.iter op bits in + + Times.record ~budgetf ~n_domains:1 ~init ~work () + |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config:"one domain" + +let run_one ~budgetf ?(n_adders = 2) ?(n_takers = 2) + ?(n_msgs = 50 * Util.iter_factor) () = + let n_domains = n_adders + n_takers in + + let t = Cue.create () in + + let n_msgs_to_take = Atomic.make 0 |> Multicore_magic.copy_as_padded in + let n_msgs_to_add = Atomic.make 0 |> Multicore_magic.copy_as_padded in + + let init _ = + assert (Cue.is_empty t); + Atomic.set n_msgs_to_take n_msgs; + Atomic.set n_msgs_to_add n_msgs + in + let work i () = + if i < n_adders then + let rec work () = + let n = Util.alloc n_msgs_to_add in + if 0 < n then begin + for i = 1 to n do + Cue.try_push t i |> ignore + done; + work () + end + in + work () + else + let rec work () = + let n = Util.alloc n_msgs_to_take in + if n <> 0 then + let rec loop n = + if 0 < n then begin + match Cue.pop_opt t with + | None -> + Domain.cpu_relax (); + loop n + | Some _ -> loop (n - 1) + end + else work () + in + loop n + in + work () + in + + let config = + let format role n = + Printf.sprintf "%d %s%s" n role (if n = 1 then "" else "s") + in + Printf.sprintf "%s, %s" + (format "nb adder" n_adders) + (format "nb taker" n_takers) + in + + Times.record ~budgetf ~n_domains ~init ~work () + |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config + +let run_suite ~budgetf = + run_one_domain ~budgetf () + @ (Util.cross [ 1; 2 ] [ 1; 2 ] + |> List.concat_map @@ fun (n_adders, n_takers) -> + run_one ~budgetf ~n_adders ~n_takers ()) diff --git a/bench/bench_cue.head.ml b/bench/bench_cue.head.ml new file mode 100644 index 00000000..a487d1c6 --- /dev/null +++ b/bench/bench_cue.head.ml @@ -0,0 +1,2 @@ +open Multicore_bench +module Cue = Saturn.Cue diff --git a/bench/bench_cue_unsafe.head.ml b/bench/bench_cue_unsafe.head.ml new file mode 100644 index 00000000..31c61f28 --- /dev/null +++ b/bench/bench_cue_unsafe.head.ml @@ -0,0 +1,2 @@ +open Multicore_bench +module Cue = Saturn.Cue_unsafe diff --git a/bench/dune b/bench/dune index 671a62c5..e020f53a 100644 --- a/bench/dune +++ b/bench/dune @@ -17,6 +17,26 @@ let () = (copy ../src/michael_scott_queue/michael_scott_queue_intf.ml michael_scott_queue_intf.ml)) (package saturn)) + (rule + (action + (with-stdout-to + bench_cue.ml + (progn + (echo "# 1 \"bench_cue.head.ml\"\n") + (cat bench_cue.head.ml) + (echo "# 1 \"bench_cue.body.ml\"\n") + (cat bench_cue.body.ml))))) + +(rule + (action + (with-stdout-to + bench_cue_unsafe.ml + (progn + (echo "# 1 \"bench_cue_unsafe.head.ml\"\n") + (cat bench_cue_unsafe.head.ml) + (echo "# 1 \"bench_cue.body.ml\"\n") + (cat bench_cue.body.ml))))) + (test (package saturn) (name main) diff --git a/bench/main.ml b/bench/main.ml index c072d174..5a9390ec 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -2,6 +2,8 @@ let benchmarks = [ ("Saturn Queue", Bench_queue.Safe.run_suite); ("Saturn Queue_unsafe", Bench_queue.Unsafe.run_suite); + ("Saturn Cue", Bench_cue.run_suite); + ("Saturn Cue_unsafe", Bench_cue_unsafe.run_suite); ("Saturn Single_prod_single_cons_queue", Bench_spsc_queue.run_suite); ("Saturn Size", Bench_size.run_suite); ("Saturn Skiplist", Bench_skiplist.run_suite); From a289fd2b588e429bbe887efa8edf7e9075ae33c1 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 16 Nov 2024 17:12:50 +0100 Subject: [PATCH 13/19] Change benches to use a function instead of dune shenigans. --- bench/bench_cue.body.ml | 78 ----------------------------- bench/bench_cue.head.ml | 2 - bench/bench_cue.ml | 90 ++++++++++++++++++++++++++++++++++ bench/bench_cue_unsafe.head.ml | 2 - bench/dune | 19 +------ bench/main.ml | 4 +- 6 files changed, 94 insertions(+), 101 deletions(-) delete mode 100644 bench/bench_cue.body.ml delete mode 100644 bench/bench_cue.head.ml create mode 100644 bench/bench_cue.ml delete mode 100644 bench/bench_cue_unsafe.head.ml diff --git a/bench/bench_cue.body.ml b/bench/bench_cue.body.ml deleted file mode 100644 index 4821142f..00000000 --- a/bench/bench_cue.body.ml +++ /dev/null @@ -1,78 +0,0 @@ -let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = - let t = Cue.create () in - - let op push = - if push then Cue.try_push t 101 |> ignore else Cue.pop_opt t |> ignore - in - - let init _ = - assert (Cue.is_empty t); - Util.generate_push_and_pop_sequence n_msgs - in - let work _ bits = Util.Bits.iter op bits in - - Times.record ~budgetf ~n_domains:1 ~init ~work () - |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config:"one domain" - -let run_one ~budgetf ?(n_adders = 2) ?(n_takers = 2) - ?(n_msgs = 50 * Util.iter_factor) () = - let n_domains = n_adders + n_takers in - - let t = Cue.create () in - - let n_msgs_to_take = Atomic.make 0 |> Multicore_magic.copy_as_padded in - let n_msgs_to_add = Atomic.make 0 |> Multicore_magic.copy_as_padded in - - let init _ = - assert (Cue.is_empty t); - Atomic.set n_msgs_to_take n_msgs; - Atomic.set n_msgs_to_add n_msgs - in - let work i () = - if i < n_adders then - let rec work () = - let n = Util.alloc n_msgs_to_add in - if 0 < n then begin - for i = 1 to n do - Cue.try_push t i |> ignore - done; - work () - end - in - work () - else - let rec work () = - let n = Util.alloc n_msgs_to_take in - if n <> 0 then - let rec loop n = - if 0 < n then begin - match Cue.pop_opt t with - | None -> - Domain.cpu_relax (); - loop n - | Some _ -> loop (n - 1) - end - else work () - in - loop n - in - work () - in - - let config = - let format role n = - Printf.sprintf "%d %s%s" n role (if n = 1 then "" else "s") - in - Printf.sprintf "%s, %s" - (format "nb adder" n_adders) - (format "nb taker" n_takers) - in - - Times.record ~budgetf ~n_domains ~init ~work () - |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config - -let run_suite ~budgetf = - run_one_domain ~budgetf () - @ (Util.cross [ 1; 2 ] [ 1; 2 ] - |> List.concat_map @@ fun (n_adders, n_takers) -> - run_one ~budgetf ~n_adders ~n_takers ()) diff --git a/bench/bench_cue.head.ml b/bench/bench_cue.head.ml deleted file mode 100644 index a487d1c6..00000000 --- a/bench/bench_cue.head.ml +++ /dev/null @@ -1,2 +0,0 @@ -open Multicore_bench -module Cue = Saturn.Cue diff --git a/bench/bench_cue.ml b/bench/bench_cue.ml new file mode 100644 index 00000000..9fa2e9cf --- /dev/null +++ b/bench/bench_cue.ml @@ -0,0 +1,90 @@ +open Multicore_bench + +module type BENCH = sig + val run_suite : budgetf:float -> Metric.t list +end + +module Make (Cue : Cue_intf.CUE) : BENCH = struct + let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = + let t = Cue.create () in + + let op push = + if push then Cue.try_push t 101 |> ignore else Cue.pop_opt t |> ignore + in + + let init _ = + assert (Cue.is_empty t); + Util.generate_push_and_pop_sequence n_msgs + in + let work _ bits = Util.Bits.iter op bits in + + Times.record ~budgetf ~n_domains:1 ~init ~work () + |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" + ~config:"one domain" + + let run_one ~budgetf ?(n_adders = 2) ?(n_takers = 2) + ?(n_msgs = 50 * Util.iter_factor) () = + let n_domains = n_adders + n_takers in + + let t = Cue.create () in + + let n_msgs_to_take = Atomic.make 0 |> Multicore_magic.copy_as_padded in + let n_msgs_to_add = Atomic.make 0 |> Multicore_magic.copy_as_padded in + + let init _ = + assert (Cue.is_empty t); + Atomic.set n_msgs_to_take n_msgs; + Atomic.set n_msgs_to_add n_msgs + in + let work i () = + if i < n_adders then + let rec work () = + let n = Util.alloc n_msgs_to_add in + if 0 < n then begin + for i = 1 to n do + Cue.try_push t i |> ignore + done; + work () + end + in + work () + else + let rec work () = + let n = Util.alloc n_msgs_to_take in + if n <> 0 then + let rec loop n = + if 0 < n then begin + match Cue.pop_opt t with + | None -> + Domain.cpu_relax (); + loop n + | Some _ -> loop (n - 1) + end + else work () + in + loop n + in + work () + in + + let config = + let format role n = + Printf.sprintf "%d %s%s" n role (if n = 1 then "" else "s") + in + Printf.sprintf "%s, %s" + (format "nb adder" n_adders) + (format "nb taker" n_takers) + in + + Times.record ~budgetf ~n_domains ~init ~work () + |> Times.to_thruput_metrics ~n:n_msgs ~singular:"message" ~config + + let run_suite ~budgetf = + run_one_domain ~budgetf () + @ (Util.cross [ 1; 2 ] [ 1; 2 ] + |> List.concat_map @@ fun (n_adders, n_takers) -> + run_one ~budgetf ~n_adders ~n_takers ()) +end + +module Safe = Make (Saturn.Cue) +module Unsafe = Make (Saturn.Cue_unsafe) diff --git a/bench/bench_cue_unsafe.head.ml b/bench/bench_cue_unsafe.head.ml deleted file mode 100644 index 31c61f28..00000000 --- a/bench/bench_cue_unsafe.head.ml +++ /dev/null @@ -1,2 +0,0 @@ -open Multicore_bench -module Cue = Saturn.Cue_unsafe diff --git a/bench/dune b/bench/dune index e020f53a..3f13b4fc 100644 --- a/bench/dune +++ b/bench/dune @@ -17,25 +17,10 @@ let () = (copy ../src/michael_scott_queue/michael_scott_queue_intf.ml michael_scott_queue_intf.ml)) (package saturn)) - (rule - (action - (with-stdout-to - bench_cue.ml - (progn - (echo "# 1 \"bench_cue.head.ml\"\n") - (cat bench_cue.head.ml) - (echo "# 1 \"bench_cue.body.ml\"\n") - (cat bench_cue.body.ml))))) - (rule (action - (with-stdout-to - bench_cue_unsafe.ml - (progn - (echo "# 1 \"bench_cue_unsafe.head.ml\"\n") - (cat bench_cue_unsafe.head.ml) - (echo "# 1 \"bench_cue.body.ml\"\n") - (cat bench_cue.body.ml))))) + (copy ../src/cue/cue_intf.mli cue_intf.ml)) + (package saturn)) (test (package saturn) diff --git a/bench/main.ml b/bench/main.ml index 5a9390ec..5150ec14 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -2,8 +2,8 @@ let benchmarks = [ ("Saturn Queue", Bench_queue.Safe.run_suite); ("Saturn Queue_unsafe", Bench_queue.Unsafe.run_suite); - ("Saturn Cue", Bench_cue.run_suite); - ("Saturn Cue_unsafe", Bench_cue_unsafe.run_suite); + ("Saturn Cue", Bench_cue.Safe.run_suite); + ("Saturn Cue_unsafe", Bench_cue.Unsafe.run_suite); ("Saturn Single_prod_single_cons_queue", Bench_spsc_queue.run_suite); ("Saturn Size", Bench_size.run_suite); ("Saturn Skiplist", Bench_skiplist.run_suite); From c135b518d416e442be41ef9daa2d4856af3bdcae Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sun, 17 Nov 2024 19:28:35 +0100 Subject: [PATCH 14/19] Cue qcheck tests. --- test/cue/dune | 14 ++ test/cue/qcheck_cue.ml | 336 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 350 insertions(+) create mode 100644 test/cue/qcheck_cue.ml diff --git a/test/cue/dune b/test/cue/dune index 608eb75d..56d3cb5b 100644 --- a/test/cue/dune +++ b/test/cue/dune @@ -35,3 +35,17 @@ (libraries cues saturn qcheck-core qcheck-stm.stm stm_run) (enabled_if (= %{arch_sixtyfour} true))) + +(test + (package saturn) + (name qcheck_cue) + (libraries + cues + saturn + barrier + qcheck + qcheck-core + qcheck-alcotest + domain_shims + alcotest) + (modules qcheck_cue)) \ No newline at end of file diff --git a/test/cue/qcheck_cue.ml b/test/cue/qcheck_cue.ml new file mode 100644 index 00000000..0d164cf5 --- /dev/null +++ b/test/cue/qcheck_cue.ml @@ -0,0 +1,336 @@ +module Qcheck_cue (Cue : Cues.Cue_tests) = struct + let tests_sequential = + QCheck. + [ + (* TEST 1: push *) + Test.make ~name:"push" (list int) (fun lpush -> + assume (lpush <> []); + (* Building a random Cue *) + let cue = Cue.create () in + List.iter (Cue.push_exn cue) lpush; + + (* Testing property *) + (not (Cue.is_empty cue)) && Cue.length cue = List.length lpush); + (* TEST 1: of_list *) + Test.make ~name:"of_list_exn" (list int) (fun lpush -> + assume (lpush <> []); + (* Building a random Cue *) + let cue = Cue.of_list_exn lpush in + + (* Testing property *) + (not (Cue.is_empty cue)) && Cue.length cue = List.length lpush); + (* TEST 1bis: push *) + Test.make ~name:"of_list_exn_raise_full" + (pair (list int) small_nat) + (fun (lpush, capacity) -> + assume (lpush <> []); + (* Building a random Cue *) + match Cue.of_list_exn ~capacity lpush with + | cue -> + capacity >= List.length lpush + && (not (Cue.is_empty cue)) + && Cue.length cue = List.length lpush + | exception Cue.Full -> capacity <= List.length lpush); + (* TEST 1: push and full *) + Test.make ~name:"push_capacity" (list int) (fun lpush -> + assume (lpush <> []); + (* Building a random Cue *) + let capacity = 10 in + let cue = Cue.create ~capacity () in + List.map + (fun elt -> + try + Cue.push_exn cue elt; + true + with Cue.Full -> false) + lpush + |> List.filteri (fun i elt -> if i < capacity then not elt else elt) + |> List.is_empty); + (* TEST 2 - push, pop until empty *) + Test.make ~name:"push_pop_opt_until_empty" (list int) (fun lpush -> + (* Building a random Cue *) + let cue = Cue.create () in + List.iter (Cue.push_exn cue) lpush; + + (* Popping until [is_empty q] is true *) + let count = ref 0 in + while not (Cue.is_empty cue) do + incr count; + ignore (Cue.pop_opt cue) + done; + + (* Testing property *) + Cue.pop_opt cue = None && !count = List.length lpush); + (* TEST 3 - push, pop_opt, check FIFO *) + Test.make ~name:"fifo" (list int) (fun lpush -> + (* Building a random Cue *) + let cue = Cue.create () in + List.iter (Cue.push_exn cue) lpush; + + let out = ref [] in + let insert v = out := v :: !out in + + for _ = 1 to List.length lpush do + match Cue.pop_opt cue with + | None -> assert false + | Some v -> insert v + done; + + (* Testing property *) + lpush = List.rev !out); + (* TEST 3 - push, pop_opt, peek_opt check FIFO *) + Test.make ~name:"fifo_peek_opt" (list int) (fun lpush -> + (* Building a random Cue *) + let cue = Cue.create () in + List.iter (Cue.push_exn cue) lpush; + + let pop = ref [] in + let peek = ref [] in + let insert out v = out := v :: !out in + + for _ = 1 to List.length lpush do + match Cue.peek_opt cue with + | None -> assert false + | Some v -> ( + insert peek v; + match Cue.pop_opt cue with + | None -> assert false + | Some v -> insert pop v) + done; + + (* Testing property *) + lpush = List.rev !pop && lpush = List.rev !peek); + ] + + let tests_one_consumer_one_producer = + QCheck. + [ + (* TEST 1 - one consumer one producer: + Parallel [push] and [pop_opt]. *) + Test.make ~name:"parallel_fifo" (list int) (fun lpush -> + (* Initialization *) + let cue = Cue.create () in + let barrier = Barrier.create 2 in + + (* Producer pushes. *) + let producer = + Domain.spawn (fun () -> + Barrier.await barrier; + List.iter (Cue.push_exn cue) lpush) + in + + Barrier.await barrier; + let fifo = + List.fold_left + (fun acc item -> + let rec pop_one () = + match Cue.pop_opt cue with + | None -> + Domain.cpu_relax (); + pop_one () + | Some item' -> acc && item = item' + in + pop_one ()) + true lpush + in + let empty = Cue.is_empty cue in + + (* Ensure nothing is left behind. *) + Domain.join producer; + fifo && empty); + (* TEST 2 - one consumer one producer: + Parallel [push] and [peek_opt] and [pop_opt]. *) + Test.make ~name:"parallel_peek" (list int) (fun pushed -> + (* Initialization *) + let npush = List.length pushed in + let cue = Cue.create () in + let barrier = Barrier.create 2 in + + (* Producer pushes. *) + let producer = + Domain.spawn (fun () -> + Barrier.await barrier; + List.iter (Cue.push_exn cue) pushed) + in + + let peeked = ref [] in + let popped = ref [] in + Barrier.await barrier; + for _ = 1 to npush do + peeked := Cue.peek_opt cue :: !peeked; + popped := Cue.pop_opt cue :: !popped + done; + + Domain.join producer; + let rec check = function + | _, [], [] -> true + | pushed, None :: peeked, None :: popped -> + check (pushed, peeked, popped) + | push :: pushed, None :: peeked, Some pop :: popped + when push = pop -> + check (pushed, peeked, popped) + | push :: pushed, Some peek :: peeked, Some pop :: popped + when push = peek && push = pop -> + check (pushed, peeked, popped) + | _, _, _ -> false + in + check (pushed, List.rev @@ !peeked, List.rev @@ !popped)); + ] + + let tests_two_domains = + QCheck. + [ + (* TEST 1 - two domains doing multiple times one push then one pop_opt. + Parallel [push] and [pop_opt]. + *) + Test.make ~name:"parallel_pop_opt_push" (pair small_nat small_nat) + (fun (npush1, npush2) -> + (* Initialization *) + let cue = Cue.create () in + let barrier = Barrier.create 2 in + + (* Using these lists instead of a random one enables to + check for more properties. *) + 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 -> + Cue.push_exn cue elt; + Domain.cpu_relax (); + Cue.pop_opt cue) + lpush + in + + let domain1 = + Domain.spawn (fun () -> + Barrier.await barrier; + work lpush1) + in + let popped2 = + Barrier.await barrier; + work lpush2 + in + + (* As a domain always pushs before popping, all pops + succeeds. *) + let popped1 = Domain.join domain1 |> List.map Option.get in + let popped2 = popped2 |> List.map Option.get in + + (* Check 1 : no elements are missing (everyting is popped). *) + let all_elt_in = + List.sort compare (popped1 @ popped2) = lpush1 @ lpush2 + in + (* filter the elements pushed and popped by domain 1 *) + let push1_pop1 = List.filter (fun elt -> elt < npush1) popped1 in + (* filter the elements pushed by domain 2 and popped by domain 1 *) + let push2_pop1 = List.filter (fun elt -> elt >= npush1) popped1 in + (* filter the elements pushed by domain 1 and popped by domain 2 *) + let push1_pop2 = List.filter (fun elt -> elt < npush1) popped2 in + (* filter the elements pushed and popped by domain 2 *) + let push2_pop2 = List.filter (fun elt -> elt >= npush1) popped2 in + + (* all these lists must be sorted *) + let is_sorted list = List.sort compare list = list in + all_elt_in && is_sorted push1_pop1 && is_sorted push1_pop2 + && is_sorted push2_pop1 && is_sorted push2_pop2); + (* TEST 2 - + Parallel [push] and [pop_opt] with two domains + + Two domains randomly pushs and pops in parallel. They stop as + soon as they have finished pushing a list of element to + push. *) + Test.make ~name:"parallel_pop_opt_push_random" + (pair small_nat small_nat) (fun (npush1, npush2) -> + (* Initialization *) + let cue = Cue.create () in + let barrier = Barrier.create 2 in + + let lpush1 = List.init npush1 (fun i -> i) in + let lpush2 = List.init npush2 (fun i -> i + npush1) in + + let work lpush = + let consecutive_pop = ref 0 in + let rec loop lpush popped = + let what_to_do = Random.int 2 in + if what_to_do = 0 || !consecutive_pop > 10 then ( + (* randomly choosing between pushing and popping except + if too many consecutive pops have already occurred *) + consecutive_pop := 0; + match lpush with + | [] -> popped + | elt :: xs -> + Cue.push_exn cue elt; + loop xs popped) + else ( + incr consecutive_pop; + let p = Cue.pop_opt cue in + loop lpush (p :: popped)) + in + loop lpush [] + in + + let domain1 = + Domain.spawn (fun () -> + Barrier.await barrier; + work lpush1) + in + let popped2 = + Barrier.await barrier; + work lpush2 + in + + let popped1 = + Domain.join domain1 + |> List.filter (function None -> false | _ -> true) + |> List.map Option.get + in + let popped2 = + popped2 + |> List.filter (function None -> false | _ -> true) + |> List.map Option.get + in + + (* Pop everything that is still on the Cue *) + let popped3 = + let rec loop popped = + match Cue.pop_opt cue with + | None -> popped + | Some v -> loop (v :: popped) + in + loop [] + in + (* Check that no element is missing. *) + let all_n_elt_in = + List.sort compare (popped1 @ popped2 @ popped3) = lpush1 @ lpush2 + in + + all_n_elt_in); + ] +end + +let () = + let to_alcotest = List.map QCheck_alcotest.to_alcotest in + + let module Safe = Qcheck_cue (Cues.Cue) in + let name = "safe" in + let safe_tests = + [ + ("test_sequential_" ^ name, to_alcotest Safe.tests_sequential); + ( "one_cons_one_prod_" ^ name, + to_alcotest Safe.tests_one_consumer_one_producer ); + ("two_domains_" ^ name, to_alcotest Safe.tests_two_domains); + ] + in + let module Unsafe = Qcheck_cue (Cues.Cue_unsafe) in + let name = "unsafe" in + let unsafe_tests = + [ + ("test_sequential_" ^ name, to_alcotest Unsafe.tests_sequential); + ( "one_cons_one_prod_" ^ name, + to_alcotest Unsafe.tests_one_consumer_one_producer ); + ("two_domains_" ^ name, to_alcotest Unsafe.tests_two_domains); + ] + in + Alcotest.run "Michael_scott_Cue" (safe_tests @ unsafe_tests) From 944c2c5a733ae6a62b5f1454ec5e3f506f680c67 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sun, 17 Nov 2024 21:32:58 +0100 Subject: [PATCH 15/19] Fmt --- test/cue/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cue/dune b/test/cue/dune index 56d3cb5b..7f0b6063 100644 --- a/test/cue/dune +++ b/test/cue/dune @@ -48,4 +48,4 @@ qcheck-alcotest domain_shims alcotest) - (modules qcheck_cue)) \ No newline at end of file + (modules qcheck_cue)) From 565f3e47c3f6032d2dba2c7bdccaf6555a7acc4e Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sun, 17 Nov 2024 21:55:34 +0100 Subject: [PATCH 16/19] Remove List.is_empty for backward compatibility. --- test/cue/qcheck_cue.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cue/qcheck_cue.ml b/test/cue/qcheck_cue.ml index 0d164cf5..16af9d20 100644 --- a/test/cue/qcheck_cue.ml +++ b/test/cue/qcheck_cue.ml @@ -45,7 +45,7 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct with Cue.Full -> false) lpush |> List.filteri (fun i elt -> if i < capacity then not elt else elt) - |> List.is_empty); + |> ( = ) []); (* TEST 2 - push, pop until empty *) Test.make ~name:"push_pop_opt_until_empty" (list int) (fun lpush -> (* Building a random Cue *) From 2d06a9f84adceb4958b0390f3a669cae0e894dbf Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 23 Nov 2024 11:38:56 +0100 Subject: [PATCH 17/19] Rename cue -> bounded_queue --- .../{bench_cue.ml => bench_bounded_queue.ml} | 21 ++-- bench/dune | 2 +- bench/main.ml | 4 +- .../bounded_queue.body.ml} | 0 .../bounded_queue.head_safe.ml} | 0 .../bounded_queue.head_unsafe.ml} | 0 src/bounded_queue/bounded_queue.mli | 1 + .../bounded_queue_intf.mli} | 2 +- src/bounded_queue/bounded_queue_unsafe.mli | 1 + src/bounded_queue/dune | 19 ++++ src/cue/cue.mli | 1 - src/cue/cue_unsafe.mli | 1 - src/cue/dune | 19 ---- src/dune | 2 +- src/saturn.ml | 4 +- src/saturn.mli | 4 +- .../bounded_queues/bounded_queues.ml | 17 +++ test/bounded_queue/bounded_queues/dune | 10 ++ .../dscheck_bounded_queue.ml} | 5 +- test/{cue => bounded_queue}/dune | 28 +++-- .../qcheck_bounded_queue.ml} | 107 +++++++++--------- .../stm_bounded_queue.ml} | 38 ++++--- test/cue/cues/cues.ml | 17 --- test/cue/cues/dune | 8 -- 24 files changed, 163 insertions(+), 148 deletions(-) rename bench/{bench_cue.ml => bench_bounded_queue.ml} (79%) rename src/{cue/cue.body.ml => bounded_queue/bounded_queue.body.ml} (100%) rename src/{cue/cue.head_safe.ml => bounded_queue/bounded_queue.head_safe.ml} (100%) rename src/{cue/cue.head_unsafe.ml => bounded_queue/bounded_queue.head_unsafe.ml} (100%) create mode 100644 src/bounded_queue/bounded_queue.mli rename src/{cue/cue_intf.mli => bounded_queue/bounded_queue_intf.mli} (99%) create mode 100644 src/bounded_queue/bounded_queue_unsafe.mli create mode 100644 src/bounded_queue/dune delete mode 100644 src/cue/cue.mli delete mode 100644 src/cue/cue_unsafe.mli delete mode 100644 src/cue/dune create mode 100644 test/bounded_queue/bounded_queues/bounded_queues.ml create mode 100644 test/bounded_queue/bounded_queues/dune rename test/{cue/dscheck_cue.ml => bounded_queue/dscheck_bounded_queue.ml} (97%) rename test/{cue => bounded_queue}/dune (50%) rename test/{cue/qcheck_cue.ml => bounded_queue/qcheck_bounded_queue.ml} (75%) rename test/{cue/stm_cue.ml => bounded_queue/stm_bounded_queue.ml} (67%) delete mode 100644 test/cue/cues/cues.ml delete mode 100644 test/cue/cues/dune diff --git a/bench/bench_cue.ml b/bench/bench_bounded_queue.ml similarity index 79% rename from bench/bench_cue.ml rename to bench/bench_bounded_queue.ml index 9fa2e9cf..aae68491 100644 --- a/bench/bench_cue.ml +++ b/bench/bench_bounded_queue.ml @@ -4,16 +4,17 @@ module type BENCH = sig val run_suite : budgetf:float -> Metric.t list end -module Make (Cue : Cue_intf.CUE) : BENCH = struct +module Make (Bounded_queue : Bounded_queue_intf.BOUNDED_QUEUE) : BENCH = struct let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = - let t = Cue.create () in + let t = Bounded_queue.create () in let op push = - if push then Cue.try_push t 101 |> ignore else Cue.pop_opt t |> ignore + if push then Bounded_queue.try_push t 101 |> ignore + else Bounded_queue.pop_opt t |> ignore in let init _ = - assert (Cue.is_empty t); + assert (Bounded_queue.is_empty t); Util.generate_push_and_pop_sequence n_msgs in let work _ bits = Util.Bits.iter op bits in @@ -26,13 +27,13 @@ module Make (Cue : Cue_intf.CUE) : BENCH = struct ?(n_msgs = 50 * Util.iter_factor) () = let n_domains = n_adders + n_takers in - let t = Cue.create () in + let t = Bounded_queue.create () in let n_msgs_to_take = Atomic.make 0 |> Multicore_magic.copy_as_padded in let n_msgs_to_add = Atomic.make 0 |> Multicore_magic.copy_as_padded in let init _ = - assert (Cue.is_empty t); + assert (Bounded_queue.is_empty t); Atomic.set n_msgs_to_take n_msgs; Atomic.set n_msgs_to_add n_msgs in @@ -42,7 +43,7 @@ module Make (Cue : Cue_intf.CUE) : BENCH = struct let n = Util.alloc n_msgs_to_add in if 0 < n then begin for i = 1 to n do - Cue.try_push t i |> ignore + Bounded_queue.try_push t i |> ignore done; work () end @@ -54,7 +55,7 @@ module Make (Cue : Cue_intf.CUE) : BENCH = struct if n <> 0 then let rec loop n = if 0 < n then begin - match Cue.pop_opt t with + match Bounded_queue.pop_opt t with | None -> Domain.cpu_relax (); loop n @@ -86,5 +87,5 @@ module Make (Cue : Cue_intf.CUE) : BENCH = struct run_one ~budgetf ~n_adders ~n_takers ()) end -module Safe = Make (Saturn.Cue) -module Unsafe = Make (Saturn.Cue_unsafe) +module Safe = Make (Saturn.Bounded_queue) +module Unsafe = Make (Saturn.Bounded_queue_unsafe) diff --git a/bench/dune b/bench/dune index 3f13b4fc..cf68fa33 100644 --- a/bench/dune +++ b/bench/dune @@ -19,7 +19,7 @@ let () = (rule (action - (copy ../src/cue/cue_intf.mli cue_intf.ml)) + (copy ../src/bounded_queue/bounded_queue_intf.mli bounded_queue_intf.ml)) (package saturn)) (test diff --git a/bench/main.ml b/bench/main.ml index 5150ec14..4cf7f0dd 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -2,8 +2,8 @@ let benchmarks = [ ("Saturn Queue", Bench_queue.Safe.run_suite); ("Saturn Queue_unsafe", Bench_queue.Unsafe.run_suite); - ("Saturn Cue", Bench_cue.Safe.run_suite); - ("Saturn Cue_unsafe", Bench_cue.Unsafe.run_suite); + ("Saturn Bounded_Queue", Bench_bounded_queue.Safe.run_suite); + ("Saturn Bounded_Queue_unsafe", Bench_bounded_queue.Unsafe.run_suite); ("Saturn Single_prod_single_cons_queue", Bench_spsc_queue.run_suite); ("Saturn Size", Bench_size.run_suite); ("Saturn Skiplist", Bench_skiplist.run_suite); diff --git a/src/cue/cue.body.ml b/src/bounded_queue/bounded_queue.body.ml similarity index 100% rename from src/cue/cue.body.ml rename to src/bounded_queue/bounded_queue.body.ml diff --git a/src/cue/cue.head_safe.ml b/src/bounded_queue/bounded_queue.head_safe.ml similarity index 100% rename from src/cue/cue.head_safe.ml rename to src/bounded_queue/bounded_queue.head_safe.ml diff --git a/src/cue/cue.head_unsafe.ml b/src/bounded_queue/bounded_queue.head_unsafe.ml similarity index 100% rename from src/cue/cue.head_unsafe.ml rename to src/bounded_queue/bounded_queue.head_unsafe.ml diff --git a/src/bounded_queue/bounded_queue.mli b/src/bounded_queue/bounded_queue.mli new file mode 100644 index 00000000..d64f6612 --- /dev/null +++ b/src/bounded_queue/bounded_queue.mli @@ -0,0 +1 @@ +include Bounded_queue_intf.BOUNDED_QUEUE diff --git a/src/cue/cue_intf.mli b/src/bounded_queue/bounded_queue_intf.mli similarity index 99% rename from src/cue/cue_intf.mli rename to src/bounded_queue/bounded_queue_intf.mli index a770b5b2..b982bd0d 100644 --- a/src/cue/cue_intf.mli +++ b/src/bounded_queue/bounded_queue_intf.mli @@ -13,7 +13,7 @@ OTHER TORTIOUS ACTION, ARISING OUT OF OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. *) -module type CUE = sig +module type BOUNDED_QUEUE = sig (** Lock-free bounded Queue. This module implements a lock-free bounded queue based on Michael-Scott's queue diff --git a/src/bounded_queue/bounded_queue_unsafe.mli b/src/bounded_queue/bounded_queue_unsafe.mli new file mode 100644 index 00000000..d64f6612 --- /dev/null +++ b/src/bounded_queue/bounded_queue_unsafe.mli @@ -0,0 +1 @@ +include Bounded_queue_intf.BOUNDED_QUEUE diff --git a/src/bounded_queue/dune b/src/bounded_queue/dune new file mode 100644 index 00000000..55d9e3b1 --- /dev/null +++ b/src/bounded_queue/dune @@ -0,0 +1,19 @@ +(rule + (action + (with-stdout-to + bounded_queue.ml + (progn + (echo "# 1 \"bounded_queue.head_safe.ml\"\n") + (cat bounded_queue.head_safe.ml) + (echo "# 1 \"bounded_queue.body.ml\"\n") + (cat bounded_queue.body.ml))))) + +(rule + (action + (with-stdout-to + bounded_queue_unsafe.ml + (progn + (echo "# 1 \"bounded_queue.head_unsafe.ml\"\n") + (cat bounded_queue.head_unsafe.ml) + (echo "# 1 \"bounded_queue.body.ml\"\n") + (cat bounded_queue.body.ml))))) diff --git a/src/cue/cue.mli b/src/cue/cue.mli deleted file mode 100644 index fadb8e1f..00000000 --- a/src/cue/cue.mli +++ /dev/null @@ -1 +0,0 @@ -include Cue_intf.CUE diff --git a/src/cue/cue_unsafe.mli b/src/cue/cue_unsafe.mli deleted file mode 100644 index fadb8e1f..00000000 --- a/src/cue/cue_unsafe.mli +++ /dev/null @@ -1 +0,0 @@ -include Cue_intf.CUE diff --git a/src/cue/dune b/src/cue/dune deleted file mode 100644 index 0dceb0e9..00000000 --- a/src/cue/dune +++ /dev/null @@ -1,19 +0,0 @@ -(rule - (action - (with-stdout-to - cue.ml - (progn - (echo "# 1 \"cue.head_safe.ml\"\n") - (cat cue.head_safe.ml) - (echo "# 1 \"cue.body.ml\"\n") - (cat cue.body.ml))))) - -(rule - (action - (with-stdout-to - cue_unsafe.ml - (progn - (echo "# 1 \"cue.head_unsafe.ml\"\n") - (cat cue.head_unsafe.ml) - (echo "# 1 \"cue.body.ml\"\n") - (cat cue.body.ml))))) diff --git a/src/dune b/src/dune index 94830efa..fa8a6d27 100644 --- a/src/dune +++ b/src/dune @@ -12,7 +12,7 @@ let () = (library (name saturn) (public_name saturn) - (modules_without_implementation htbl_intf cue_intf) + (modules_without_implementation htbl_intf bounded_queue_intf) (libraries backoff multicore-magic |} ^ maybe_threads ^ {| )) diff --git a/src/saturn.ml b/src/saturn.ml index a924e0f4..5441421f 100644 --- a/src/saturn.ml +++ b/src/saturn.ml @@ -28,8 +28,8 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe -module Cue = Cue -module Cue_unsafe = Cue_unsafe +module Bounded_queue = Bounded_queue +module Bounded_queue_unsafe = Bounded_queue_unsafe module Stack = Treiber_stack module Bounded_stack = Bounded_stack module Work_stealing_deque = Ws_deque diff --git a/src/saturn.mli b/src/saturn.mli index 50d33cd4..21b5c526 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -34,8 +34,8 @@ module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe module Stack = Treiber_stack module Bounded_stack = Bounded_stack -module Cue = Cue -module Cue_unsafe = Cue_unsafe +module Bounded_queue = Bounded_queue +module Bounded_queue_unsafe = Bounded_queue_unsafe module Work_stealing_deque = Ws_deque module Single_prod_single_cons_queue = Spsc_queue module Single_prod_single_cons_queue_unsafe = Spsc_queue_unsafe diff --git a/test/bounded_queue/bounded_queues/bounded_queues.ml b/test/bounded_queue/bounded_queues/bounded_queues.ml new file mode 100644 index 00000000..13853976 --- /dev/null +++ b/test/bounded_queue/bounded_queues/bounded_queues.ml @@ -0,0 +1,17 @@ +module type Bounded_queue_tests = sig + include Bounded_queue_intf.BOUNDED_QUEUE + + val name : string +end + +module Bounded_queue : Bounded_queue_tests = struct + include Saturn.Bounded_queue + + let name = "Bounded_queue_safe" +end + +module Bounded_queue_unsafe : Bounded_queue_tests = struct + include Saturn.Bounded_queue_unsafe + + let name = "Bounded_queue_unsafe" +end diff --git a/test/bounded_queue/bounded_queues/dune b/test/bounded_queue/bounded_queues/dune new file mode 100644 index 00000000..6e281fc5 --- /dev/null +++ b/test/bounded_queue/bounded_queues/dune @@ -0,0 +1,10 @@ +(rule + (action + (copy + ../../../src/bounded_queue/bounded_queue_intf.mli + bounded_queue_intf.ml)) + (package saturn)) + +(library + (name bounded_queues) + (libraries saturn)) diff --git a/test/cue/dscheck_cue.ml b/test/bounded_queue/dscheck_bounded_queue.ml similarity index 97% rename from test/cue/dscheck_cue.ml rename to test/bounded_queue/dscheck_bounded_queue.ml index 56bdcf12..239498ca 100644 --- a/test/cue/dscheck_cue.ml +++ b/test/bounded_queue/dscheck_bounded_queue.ml @@ -1,8 +1,9 @@ [@@@warning "-32"] module Atomic = Dscheck.TracedAtomic +module Cue = Bounded_queue -(* Dscheck only tests the safe implementation of Cue. To make Cue_unsafe compatible with Dscheck, it needs to be modified to essentially become the safe version. *) +(* Dscheck only tests the safe implementation of Bounded_queue. To make Bounded_queue_unsafe compatible with Dscheck, it needs to be modified to essentially become the safe version. *) let drain cue = let rec pop_until_empty acc = @@ -378,4 +379,4 @@ let tests = let () = let open Alcotest in - run "dscheck_cue" tests + run "dscheck_bounded_queue" tests diff --git a/test/cue/dune b/test/bounded_queue/dune similarity index 50% rename from test/cue/dune rename to test/bounded_queue/dune index 7f0b6063..3e1b23b7 100644 --- a/test/cue/dune +++ b/test/bounded_queue/dune @@ -1,21 +1,23 @@ (rule (action - (copy ../../src/cue/cue.ml cue.ml)) + (copy ../../src/bounded_queue/bounded_queue.ml bounded_queue.ml)) (package saturn)) (rule (action - (copy ../../src/cue/cue_unsafe.ml cue_unsafe.ml)) + (copy + ../../src/bounded_queue/bounded_queue_unsafe.ml + bounded_queue_unsafe.ml)) (package saturn)) (rule (action - (copy ../../src/cue/cue_intf.mli cue_intf.ml)) + (copy ../../src/bounded_queue/bounded_queue_intf.mli bounded_queue_intf.ml)) (package saturn)) (test (package saturn) - (name dscheck_cue) + (name dscheck_bounded_queue) (libraries alcotest atomic backoff dscheck multicore-magic-dscheck) (build_if (and @@ -24,23 +26,27 @@ (and (= %{arch_sixtyfour} false) (= %{architecture} arm))))) - (modules cue cue_unsafe cue_intf dscheck_cue) + (modules + bounded_queue + bounded_queue_unsafe + bounded_queue_intf + dscheck_bounded_queue) (flags (:standard -open Multicore_magic_dscheck))) (test (package saturn) - (name stm_cue) - (modules stm_cue) - (libraries cues saturn qcheck-core qcheck-stm.stm stm_run) + (name stm_bounded_queue) + (modules stm_bounded_queue) + (libraries bounded_queues saturn qcheck-core qcheck-stm.stm stm_run) (enabled_if (= %{arch_sixtyfour} true))) (test (package saturn) - (name qcheck_cue) + (name qcheck_bounded_queue) (libraries - cues + bounded_queues saturn barrier qcheck @@ -48,4 +54,4 @@ qcheck-alcotest domain_shims alcotest) - (modules qcheck_cue)) + (modules qcheck_bounded_queue)) diff --git a/test/cue/qcheck_cue.ml b/test/bounded_queue/qcheck_bounded_queue.ml similarity index 75% rename from test/cue/qcheck_cue.ml rename to test/bounded_queue/qcheck_bounded_queue.ml index 16af9d20..b2b847fd 100644 --- a/test/cue/qcheck_cue.ml +++ b/test/bounded_queue/qcheck_bounded_queue.ml @@ -1,77 +1,80 @@ -module Qcheck_cue (Cue : Cues.Cue_tests) = struct +module Qcheck_bounded_queue (Bounded_queue : Bounded_queues.Bounded_queue_tests) = +struct let tests_sequential = QCheck. [ (* TEST 1: push *) Test.make ~name:"push" (list int) (fun lpush -> assume (lpush <> []); - (* Building a random Cue *) - let cue = Cue.create () in - List.iter (Cue.push_exn cue) lpush; + (* Building a random Bounded_queue *) + let queue = Bounded_queue.create () in + List.iter (Bounded_queue.push_exn queue) lpush; (* Testing property *) - (not (Cue.is_empty cue)) && Cue.length cue = List.length lpush); + (not (Bounded_queue.is_empty queue)) + && Bounded_queue.length queue = List.length lpush); (* TEST 1: of_list *) Test.make ~name:"of_list_exn" (list int) (fun lpush -> assume (lpush <> []); - (* Building a random Cue *) - let cue = Cue.of_list_exn lpush in + (* Building a random Bounded_queue *) + let queue = Bounded_queue.of_list_exn lpush in (* Testing property *) - (not (Cue.is_empty cue)) && Cue.length cue = List.length lpush); + (not (Bounded_queue.is_empty queue)) + && Bounded_queue.length queue = List.length lpush); (* TEST 1bis: push *) Test.make ~name:"of_list_exn_raise_full" (pair (list int) small_nat) (fun (lpush, capacity) -> assume (lpush <> []); - (* Building a random Cue *) - match Cue.of_list_exn ~capacity lpush with - | cue -> + (* Building a random Bounded_queue *) + match Bounded_queue.of_list_exn ~capacity lpush with + | queue -> capacity >= List.length lpush - && (not (Cue.is_empty cue)) - && Cue.length cue = List.length lpush - | exception Cue.Full -> capacity <= List.length lpush); + && (not (Bounded_queue.is_empty queue)) + && Bounded_queue.length queue = List.length lpush + | exception Bounded_queue.Full -> capacity <= List.length lpush); (* TEST 1: push and full *) Test.make ~name:"push_capacity" (list int) (fun lpush -> assume (lpush <> []); - (* Building a random Cue *) + (* Building a random Bounded_queue *) let capacity = 10 in - let cue = Cue.create ~capacity () in + let queue = Bounded_queue.create ~capacity () in List.map (fun elt -> try - Cue.push_exn cue elt; + Bounded_queue.push_exn queue elt; true - with Cue.Full -> false) + with Bounded_queue.Full -> false) lpush |> List.filteri (fun i elt -> if i < capacity then not elt else elt) |> ( = ) []); (* TEST 2 - push, pop until empty *) Test.make ~name:"push_pop_opt_until_empty" (list int) (fun lpush -> - (* Building a random Cue *) - let cue = Cue.create () in - List.iter (Cue.push_exn cue) lpush; + (* Building a random Bounded_queue *) + let queue = Bounded_queue.create () in + List.iter (Bounded_queue.push_exn queue) lpush; (* Popping until [is_empty q] is true *) let count = ref 0 in - while not (Cue.is_empty cue) do + while not (Bounded_queue.is_empty queue) do incr count; - ignore (Cue.pop_opt cue) + ignore (Bounded_queue.pop_opt queue) done; (* Testing property *) - Cue.pop_opt cue = None && !count = List.length lpush); + Bounded_queue.pop_opt queue = None && !count = List.length lpush); (* TEST 3 - push, pop_opt, check FIFO *) Test.make ~name:"fifo" (list int) (fun lpush -> - (* Building a random Cue *) - let cue = Cue.create () in - List.iter (Cue.push_exn cue) lpush; + (* Building a random Bounded_queue *) + let queue = Bounded_queue.create () in + List.iter (Bounded_queue.push_exn queue) lpush; let out = ref [] in let insert v = out := v :: !out in for _ = 1 to List.length lpush do - match Cue.pop_opt cue with + match Bounded_queue.pop_opt queue with | None -> assert false | Some v -> insert v done; @@ -80,20 +83,20 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct lpush = List.rev !out); (* TEST 3 - push, pop_opt, peek_opt check FIFO *) Test.make ~name:"fifo_peek_opt" (list int) (fun lpush -> - (* Building a random Cue *) - let cue = Cue.create () in - List.iter (Cue.push_exn cue) lpush; + (* Building a random Bounded_queue *) + let queue = Bounded_queue.create () in + List.iter (Bounded_queue.push_exn queue) lpush; let pop = ref [] in let peek = ref [] in let insert out v = out := v :: !out in for _ = 1 to List.length lpush do - match Cue.peek_opt cue with + match Bounded_queue.peek_opt queue with | None -> assert false | Some v -> ( insert peek v; - match Cue.pop_opt cue with + match Bounded_queue.pop_opt queue with | None -> assert false | Some v -> insert pop v) done; @@ -109,14 +112,14 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct Parallel [push] and [pop_opt]. *) Test.make ~name:"parallel_fifo" (list int) (fun lpush -> (* Initialization *) - let cue = Cue.create () in + let queue = Bounded_queue.create () in let barrier = Barrier.create 2 in (* Producer pushes. *) let producer = Domain.spawn (fun () -> Barrier.await barrier; - List.iter (Cue.push_exn cue) lpush) + List.iter (Bounded_queue.push_exn queue) lpush) in Barrier.await barrier; @@ -124,7 +127,7 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct List.fold_left (fun acc item -> let rec pop_one () = - match Cue.pop_opt cue with + match Bounded_queue.pop_opt queue with | None -> Domain.cpu_relax (); pop_one () @@ -133,7 +136,7 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct pop_one ()) true lpush in - let empty = Cue.is_empty cue in + let empty = Bounded_queue.is_empty queue in (* Ensure nothing is left behind. *) Domain.join producer; @@ -143,22 +146,22 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct Test.make ~name:"parallel_peek" (list int) (fun pushed -> (* Initialization *) let npush = List.length pushed in - let cue = Cue.create () in + let queue = Bounded_queue.create () in let barrier = Barrier.create 2 in (* Producer pushes. *) let producer = Domain.spawn (fun () -> Barrier.await barrier; - List.iter (Cue.push_exn cue) pushed) + List.iter (Bounded_queue.push_exn queue) pushed) in let peeked = ref [] in let popped = ref [] in Barrier.await barrier; for _ = 1 to npush do - peeked := Cue.peek_opt cue :: !peeked; - popped := Cue.pop_opt cue :: !popped + peeked := Bounded_queue.peek_opt queue :: !peeked; + popped := Bounded_queue.pop_opt queue :: !popped done; Domain.join producer; @@ -186,7 +189,7 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct Test.make ~name:"parallel_pop_opt_push" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let cue = Cue.create () in + let queue = Bounded_queue.create () in let barrier = Barrier.create 2 in (* Using these lists instead of a random one enables to @@ -197,9 +200,9 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct let work lpush = List.map (fun elt -> - Cue.push_exn cue elt; + Bounded_queue.push_exn queue elt; Domain.cpu_relax (); - Cue.pop_opt cue) + Bounded_queue.pop_opt queue) lpush in @@ -244,7 +247,7 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct Test.make ~name:"parallel_pop_opt_push_random" (pair small_nat small_nat) (fun (npush1, npush2) -> (* Initialization *) - let cue = Cue.create () in + let queue = Bounded_queue.create () in let barrier = Barrier.create 2 in let lpush1 = List.init npush1 (fun i -> i) in @@ -261,11 +264,11 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct match lpush with | [] -> popped | elt :: xs -> - Cue.push_exn cue elt; + Bounded_queue.push_exn queue elt; loop xs popped) else ( incr consecutive_pop; - let p = Cue.pop_opt cue in + let p = Bounded_queue.pop_opt queue in loop lpush (p :: popped)) in loop lpush [] @@ -292,10 +295,10 @@ module Qcheck_cue (Cue : Cues.Cue_tests) = struct |> List.map Option.get in - (* Pop everything that is still on the Cue *) + (* Pop everything that is still on the Bounded_queue *) let popped3 = let rec loop popped = - match Cue.pop_opt cue with + match Bounded_queue.pop_opt queue with | None -> popped | Some v -> loop (v :: popped) in @@ -313,7 +316,7 @@ end let () = let to_alcotest = List.map QCheck_alcotest.to_alcotest in - let module Safe = Qcheck_cue (Cues.Cue) in + let module Safe = Qcheck_bounded_queue (Bounded_queues.Bounded_queue) in let name = "safe" in let safe_tests = [ @@ -323,7 +326,7 @@ let () = ("two_domains_" ^ name, to_alcotest Safe.tests_two_domains); ] in - let module Unsafe = Qcheck_cue (Cues.Cue_unsafe) in + let module Unsafe = Qcheck_bounded_queue (Bounded_queues.Bounded_queue_unsafe) in let name = "unsafe" in let unsafe_tests = [ @@ -333,4 +336,4 @@ let () = ("two_domains_" ^ name, to_alcotest Unsafe.tests_two_domains); ] in - Alcotest.run "Michael_scott_Cue" (safe_tests @ unsafe_tests) + Alcotest.run "Bounded_queue" (safe_tests @ unsafe_tests) diff --git a/test/cue/stm_cue.ml b/test/bounded_queue/stm_bounded_queue.ml similarity index 67% rename from test/cue/stm_cue.ml rename to test/bounded_queue/stm_bounded_queue.ml index 674eeef7..f9163016 100644 --- a/test/cue/stm_cue.ml +++ b/test/bounded_queue/stm_bounded_queue.ml @@ -1,10 +1,11 @@ -(** Sequential and Parallel model-based tests of (bounded queue) cue. *) +(** Sequential and Parallel model-based tests of (bounded queue) Bounded_queue. *) open QCheck open STM -module Cue = Saturn.Cue +module Bounded_queue = Saturn.Bounded_queue -module STM_cue (Cue : Cues.Cue_tests) = struct +module STM_Bounded_queue (Bounded_queue : Bounded_queues.Bounded_queue_tests) = +struct module Spec = struct type cmd = | Try_push of int @@ -26,7 +27,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | Is_full -> "Is_full" type state = int * int * int list - type sut = int Cue.t + type sut = int Bounded_queue.t let arb_cmd _s = let int_gen = Gen.nat in @@ -43,7 +44,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct ]) let init_state = (100, 0, []) - let init_sut () = Cue.create ~capacity:100 () + let init_sut () = Bounded_queue.create ~capacity:100 () let cleanup _ = () let next_state c ((capacity, size, content) as s) = @@ -66,15 +67,16 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | Try_push i -> Res ( bool, - match Cue.push_exn d i with + match Bounded_queue.push_exn d i with | () -> true - | exception Cue.Full -> true (*Cue.try_push d i*) ) - | Pop_opt -> Res (option int, Cue.pop_opt d) - | Peek_opt -> Res (option int, Cue.peek_opt d) - | Drop_exn -> Res (result unit exn, protect Cue.drop_exn d) - | Is_empty -> Res (bool, Cue.is_empty d) - | Is_full -> Res (bool, Cue.is_full d) - | Length -> Res (int, Cue.length d) + | exception Bounded_queue.Full -> + true (*Bounded_queue.try_push d i*) ) + | Pop_opt -> Res (option int, Bounded_queue.pop_opt d) + | Peek_opt -> Res (option int, Bounded_queue.peek_opt d) + | Drop_exn -> Res (result unit exn, protect Bounded_queue.drop_exn d) + | Is_empty -> Res (bool, Bounded_queue.is_empty d) + | Is_full -> Res (bool, Bounded_queue.is_full d) + | Length -> Res (int, Bounded_queue.length d) let postcond c ((capacity, size, content) : state) res = match (c, res) with @@ -85,7 +87,7 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | j :: _ -> res = Some j) | Drop_exn, Res ((Result (Unit, Exn), _), res) -> ( match List.rev content with - | [] -> res = Error Cue.Empty + | [] -> res = Error Bounded_queue.Empty | _ -> res = Ok ()) | Is_empty, Res ((Bool, _), res) -> res = (content = []) | Is_full, Res ((Bool, _), res) -> res = (size = capacity) @@ -93,16 +95,16 @@ module STM_cue (Cue : Cues.Cue_tests) = struct | _, _ -> false end - let run () = Stm_run.run ~name:"Saturn_lockfree.Cue" (module Spec) |> exit + let run () = Stm_run.run ~name:"Saturn.Bounded_queue" (module Spec) |> exit end let () = - (* Since Cue and Cue_unsafe share the same implementation, it is not necessary + (* Since Bounded_queue and Bounded_queue_unsafe share the same implementation, it is not necessary to test both of them. *) Random.self_init (); if Random.bool () then - let module Safe = STM_cue (Cues.Cue) in + let module Safe = STM_Bounded_queue (Bounded_queues.Bounded_queue) in Safe.run () |> exit else - let module Unsafe = STM_cue (Cues.Cue_unsafe) in + let module Unsafe = STM_Bounded_queue (Bounded_queues.Bounded_queue_unsafe) in Unsafe.run () |> exit diff --git a/test/cue/cues/cues.ml b/test/cue/cues/cues.ml deleted file mode 100644 index ad780caf..00000000 --- a/test/cue/cues/cues.ml +++ /dev/null @@ -1,17 +0,0 @@ -module type Cue_tests = sig - include Cue_intf.CUE - - val name : string -end - -module Cue : Cue_tests = struct - include Saturn.Cue - - let name = "cue_safe" -end - -module Cue_unsafe : Cue_tests = struct - include Saturn.Cue_unsafe - - let name = "cue_unsafe" -end diff --git a/test/cue/cues/dune b/test/cue/cues/dune deleted file mode 100644 index 28c6066d..00000000 --- a/test/cue/cues/dune +++ /dev/null @@ -1,8 +0,0 @@ -(rule - (action - (copy ../../../src/cue/cue_intf.mli cue_intf.ml)) - (package saturn)) - -(library - (name cues) - (libraries saturn)) From c3cbae83490800efb4d63f4a26d5b9f0e688567c Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 23 Nov 2024 15:26:15 +0100 Subject: [PATCH 18/19] Add examples in doc. --- src/bounded_queue/bounded_queue_intf.mli | 66 ++++++++++++++++++++++++ src/bounded_queue/dune | 9 ++++ 2 files changed, 75 insertions(+) diff --git a/src/bounded_queue/bounded_queue_intf.mli b/src/bounded_queue/bounded_queue_intf.mli index b982bd0d..509f822c 100644 --- a/src/bounded_queue/bounded_queue_intf.mli +++ b/src/bounded_queue/bounded_queue_intf.mli @@ -37,6 +37,7 @@ module type BOUNDED_QUEUE = sig @raises Full if the length of [list] is greater than [capacity]. {[ + # open Saturn.Bounded_queue # let t : int t = of_list_exn [1;2;3;4] val t : int t = # pop_opt t @@ -104,3 +105,68 @@ module type BOUNDED_QUEUE = sig Returns [true] if the element was successfully added, or [false] if the queue is full. *) end + +(** {1 Examples} + An example top-level session: + {[ + # open Saturn.Bounded_queue + # let t : int t = create ~capacity:3 () + val t : int t = + # try_push t 1 + - : bool = true + # try_push t 2 + - : bool = true + # push_exn t 3 + - : unit = () + # push_exn t 4 + Exception: Saturn__Bounded_queue.Full. + # try_push t 4 + - : bool = false + # pop_exn t + - : int = 1 + # peek_opt t + - : int option = Some 2 + # drop_exn t + - : unit = () + # pop_opt t + - : int option = Some 3 + # pop_opt t + - : int option = None + # pop_exn t + Exception: Saturn__Bounded_queue.Empty.]} + + A multicore example: + {@ocaml non-deterministic[ + # open Saturn.Bounded_queue + # let t :int t = create ~capacity:4 () + val t : int t = + + # let barrier = Atomic.make 2 + val barrier : int Atomic.t = + + # let pusher () = + Atomic.decr barrier; + while Atomic.get barrier != 0 do Domain.cpu_relax () done; + List.init 8 (fun i -> i) + |> List.map (fun i -> Domain.cpu_relax (); try_push t i) + val pusher : unit -> bool list = + + # let popper () = + Atomic.decr barrier; + while Atomic.get barrier != 0 do Domain.cpu_relax () done; + List.init 8 (fun i -> Domain.cpu_relax (); pop_opt t) + val popper : unit -> int option list = + + # let domain_pusher = Domain.spawn pusher + val domain_pusher : bool list Domain.t = + + # let domain_popper = Domain.spawn popper + val domain_popper : int option list Domain.t = + + # Domain.join domain_pusher + - : bool list = [true; true; true; true; true; false; true; true] + # Domain.join domain_popper + - : int option list = [None; None; Some 0; None; Some 1; Some 2; Some 3; Some 4] + ]} + + *) diff --git a/src/bounded_queue/dune b/src/bounded_queue/dune index 55d9e3b1..3c804b5c 100644 --- a/src/bounded_queue/dune +++ b/src/bounded_queue/dune @@ -17,3 +17,12 @@ (cat bounded_queue.head_unsafe.ml) (echo "# 1 \"bounded_queue.body.ml\"\n") (cat bounded_queue.body.ml))))) + +(mdx + (package saturn) + (enabled_if + (and + (<> %{os_type} Win32) + (>= %{ocaml_version} 5.0.0))) + (libraries saturn) + (files bounded_queue_intf.mli)) \ No newline at end of file From a5da17e61588b1f14bd2dba419e1eb50c88fd207 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 23 Nov 2024 16:08:51 +0100 Subject: [PATCH 19/19] fmt --- src/bounded_queue/dune | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bounded_queue/dune b/src/bounded_queue/dune index 3c804b5c..843ccd9a 100644 --- a/src/bounded_queue/dune +++ b/src/bounded_queue/dune @@ -25,4 +25,4 @@ (<> %{os_type} Win32) (>= %{ocaml_version} 5.0.0))) (libraries saturn) - (files bounded_queue_intf.mli)) \ No newline at end of file + (files bounded_queue_intf.mli))