From c584936c61a7d8db1e80b81652b137c0efcca408 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sun, 24 Nov 2024 12:43:09 +0100 Subject: [PATCH 1/4] Improve documentation, add of_list and drop_exn. --- bench/dune | 2 +- src/dune | 2 +- src/michael_scott_queue/dune | 8 + .../michael_scott_queue.ml | 34 ++- .../michael_scott_queue_intf.ml | 61 ----- .../michael_scott_queue_intf.mli | 160 ++++++++++++ .../michael_scott_queue_unsafe.ml | 44 +++- .../michael_scott_queue_unsafe_node.ml | 13 + test/michael_scott_queue/dune | 2 +- .../michael_scott_queue_dscheck.ml | 241 +++++++++++++----- .../michael_scott_queue_unsafe_node.ml | 14 + test/michael_scott_queue/ms_queues/dune | 2 +- .../stm_michael_scott_queue.ml | 12 +- 13 files changed, 447 insertions(+), 148 deletions(-) create mode 100644 src/michael_scott_queue/dune delete mode 100644 src/michael_scott_queue/michael_scott_queue_intf.ml create mode 100644 src/michael_scott_queue/michael_scott_queue_intf.mli diff --git a/bench/dune b/bench/dune index 81fd3e6d..8651fcb1 100644 --- a/bench/dune +++ b/bench/dune @@ -14,7 +14,7 @@ let () = (rule (action - (copy ../src/michael_scott_queue/michael_scott_queue_intf.ml michael_scott_queue_intf.ml)) + (copy ../src/michael_scott_queue/michael_scott_queue_intf.mli michael_scott_queue_intf.ml)) (package saturn)) (rule diff --git a/src/dune b/src/dune index c4d88b1c..62aade7c 100644 --- a/src/dune +++ b/src/dune @@ -12,7 +12,7 @@ let () = (library (name saturn) (public_name saturn) - (modules_without_implementation htbl_intf bounded_queue_intf spsc_queue_intf) + (modules_without_implementation htbl_intf bounded_queue_intf spsc_queue_intf michael_scott_queue_intf) (libraries backoff multicore-magic |} ^ maybe_threads ^ {| )) diff --git a/src/michael_scott_queue/dune b/src/michael_scott_queue/dune new file mode 100644 index 00000000..575256a7 --- /dev/null +++ b/src/michael_scott_queue/dune @@ -0,0 +1,8 @@ +(mdx + (package saturn) + (enabled_if + (and + (<> %{os_type} Win32) + (>= %{ocaml_version} 5.0.0))) + (libraries saturn) + (files michael_scott_queue_intf.mli)) diff --git a/src/michael_scott_queue/michael_scott_queue.ml b/src/michael_scott_queue/michael_scott_queue.ml index 42d5b13e..a89c6300 100644 --- a/src/michael_scott_queue/michael_scott_queue.ml +++ b/src/michael_scott_queue/michael_scott_queue.ml @@ -33,19 +33,36 @@ let create () = let is_empty { head; _ } = Atomic.get (Atomic.get head) == Nil +let of_list list = + let tail_ = Atomic.make Nil in + let tail = Atomic.make_contended tail_ in + let rec build_next = function + | [] -> tail_ + | hd :: tl -> Atomic.make @@ Next (hd, build_next tl) + in + let head = Atomic.make_contended @@ build_next list in + { head; tail } + +(* *) + exception Empty -type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly +type ('a, _) poly = + | Option : ('a, 'a option) poly + | Value : ('a, 'a) poly + | Unit : ('a, unit) poly let rec pop_as : type a r. a node Atomic.t Atomic.t -> Backoff.t -> (a, r) poly -> r = fun head backoff poly -> let old_head = Atomic.get head in match Atomic.get old_head with - | Nil -> begin match poly with Value -> raise Empty | Option -> None end + | Nil -> begin + match poly with Value | Unit -> raise Empty | Option -> None + end | Next (value, next) -> if Atomic.compare_and_set head old_head next then begin - match poly with Value -> value | Option -> Some value + match poly with Value -> value | Option -> Some value | Unit -> () end else let backoff = Backoff.once backoff in @@ -53,18 +70,25 @@ let rec pop_as : let pop_exn t = pop_as t.head Backoff.default Value let pop_opt t = pop_as t.head Backoff.default Option +let drop_exn t = pop_as t.head Backoff.default Unit + +(* *) let peek_as : type a r. a node Atomic.t Atomic.t -> (a, r) poly -> r = fun head poly -> let old_head = Atomic.get head in match Atomic.get old_head with - | Nil -> begin match poly with Value -> raise Empty | Option -> None end + | Nil -> begin + match poly with Value | Unit -> raise Empty | Option -> None + end | Next (value, _) -> ( - match poly with Value -> value | Option -> Some value) + match poly with Value -> value | Option -> Some value | Unit -> ()) let peek_opt t = peek_as t.head Option let peek_exn t = peek_as t.head Value +(* *) + let rec fix_tail tail new_tail = let old_tail = Atomic.get tail in if diff --git a/src/michael_scott_queue/michael_scott_queue_intf.ml b/src/michael_scott_queue/michael_scott_queue_intf.ml deleted file mode 100644 index 9b63e79a..00000000 --- a/src/michael_scott_queue/michael_scott_queue_intf.ml +++ /dev/null @@ -1,61 +0,0 @@ -(* - * Copyright (c) 2015, Théo Laurent - * Copyright (c) 2015, KC Sivaramakrishnan - * - * 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. - *) - -(** - Michael-Scott classic multi-producer multi-consumer queue. - - All functions are lockfree. It is the recommended starting point - when needing FIFO structure. It is inspired by {{: - https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} - Simple, Fast, and Practical Non-Blocking and Blocking Concurrent - Queue Algorithms}. -*) - -module type MS_QUEUE = sig - type 'a t - (** The type of lock-free queue. *) - - val create : unit -> 'a t - (** [create ()] returns a new queue, initially empty. *) - - val is_empty : 'a t -> bool - (** [is_empty q] returns empty if [q] is empty. *) - - val push : 'a t -> 'a -> unit - (** [push q v] adds the element [v] at the end of the queue [q]. *) - - exception Empty - (** Raised when {!pop_exn} or {!peek_exn} is applied to an empty queue. *) - - val pop_exn : 'a t -> 'a - (** [pop_exn q] removes and returns the first element in queue [q]. - - @raise Empty if [q] is empty. *) - - val pop_opt : 'a t -> 'a option - (** [pop_opt q] removes and returns the first element in queue [q], or - returns [None] if the queue is empty. *) - - val peek_exn : 'a t -> 'a - (** [peek_exn q] returns the first element in queue [q]. - - @raise Empty if [q] is empty. *) - - val peek_opt : 'a t -> 'a option - (** [peek_opt q] returns the first element in queue [q], or - returns [None] if the queue is empty. *) -end diff --git a/src/michael_scott_queue/michael_scott_queue_intf.mli b/src/michael_scott_queue/michael_scott_queue_intf.mli new file mode 100644 index 00000000..49c649be --- /dev/null +++ b/src/michael_scott_queue/michael_scott_queue_intf.mli @@ -0,0 +1,160 @@ +(* + * Copyright (c) 2015, Théo Laurent + * Copyright (c) 2015, KC Sivaramakrishnan + * + * 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 MS_QUEUE = sig + (** + Michael-Scott classic multi-producer multi-consumer queue. + + All functions are lockfree. It is the recommended starting point + when needing FIFO structure. It is inspired by {{: + https://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf} + Simple, Fast, and Practical Non-Blocking and Blocking Concurrent + Queue Algorithms}. + + If you need a [length] function, you can use the bounded queue + {!Saturn.Bounded_queue} instead with maximun capacity (default value). + However, this adds a general overhead to the operation. +*) + + (** {1 API} *) + + type 'a t + (** Represents a lock-free queue holding elements of type ['a]. *) + + val create : unit -> 'a t + (** [create ()] returns a new queue, initially empty. *) + + val of_list : 'a list -> 'a t + (** [of_list list] creates a new queue from a list. + + {[ + # open Saturn.Queue + # let t : int t = of_list [1;2;3;4] + val t : int t = + # pop_opt t + - : int option = Some 1 + # pop_opt t + - : int option = Some 2 + ]} + *) + + val is_empty : 'a t -> bool + (** [is_empty q] returns [true] if [q] is empty and [false otherwise]. *) + + (** {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 q] removes and returns the first element in queue [q], or + returns [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. *) + + (** {2 Producer functions} *) + + val push : 'a t -> 'a -> unit + (** [push q v] adds the element [v] at the end of the queue [q]. *) + + (** {1 Examples} *) + + (** {2 Sequential example} + + An example top-level session: + {[ + # open Saturn.Queue + # let t : int t = of_list [1;2;3] + val t : int t = + # push t 42 + - : unit = () + # 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 = Some 42 + # pop_exn t + Exception: Saturn__Michael_scott_queue.Empty.]} + *) + + (** {2 Parallel example} + **Note** that the use of a barrier is only necessary to make the result of + this example interesting by improving the likelihood of parallelism. + Spawning a domain is a costly operation compared to the work actually run on them + here. In practice, you should not use a barrier. + + {@ocaml non-deterministic[ + # open Saturn.Queue + # let t : string t = create () + val t : string t = + # Random.self_init () + - : unit = () + # let barrier = Atomic.make 2 + val barrier : int Atomic.t = + + # let work id = + Atomic.decr barrier; + while Atomic.get barrier <> 0 do + Domain.cpu_relax () + done; + for _ = 1 to 4 do + Domain.cpu_relax (); + if Random.bool () then push t id + else + match pop_opt t with + | None -> Format.printf "Domain %s sees an empty queue.\n%!" id + | Some v -> Format.printf "Domain %s pops values pushed by %s.\n%!" id v + done + val work : string -> unit = + + # let domainA = Domain.spawn (fun () -> work "A") + val domainA : unit Domain.t = + # let domainB = Domain.spawn (fun () -> work "B") + Domain B pops values pushed by B. + Domain A pops values pushed by A. + Domain B pops values pushed by A. + Domain B pops values pushed by A. + val domainB : unit Domain.t = + + # Domain.join domainA; Domain.join domainB + - : unit = () + ]} + *) +end diff --git a/src/michael_scott_queue/michael_scott_queue_unsafe.ml b/src/michael_scott_queue/michael_scott_queue_unsafe.ml index 5d15aa41..7ca00215 100644 --- a/src/michael_scott_queue/michael_scott_queue_unsafe.ml +++ b/src/michael_scott_queue/michael_scott_queue_unsafe.ml @@ -32,27 +32,38 @@ let create () = let is_empty t = Atomic.get (Node.as_atomic (Atomic.get t.head)) == Nil +let of_list list = + match list with + | [] -> create () + | _ -> + let tail, head = Node.node_of_list list in + let head = Node.Next { next = head; value = Obj.magic () } in + let head = Atomic.make head |> Multicore_magic.copy_as_padded in + let tail = Atomic.make tail |> Multicore_magic.copy_as_padded in + { head; tail } |> Multicore_magic.copy_as_padded + +(* *) + exception Empty -type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly +type ('a, _) poly = + | Option : ('a, 'a option) poly + | Value : ('a, 'a) poly + | Unit : ('a, unit) poly let rec pop_as : type a r. (a, [ `Next ]) Node.t Atomic.t -> Backoff.t -> (a, r) poly -> r = fun head backoff poly -> let old_head = Atomic.get head in match Atomic.get (Node.as_atomic old_head) with - | Nil -> begin match poly with Value -> raise Empty | Option -> None end + | Nil -> begin + match poly with Value | Unit -> raise Empty | Option -> None + end | Next r as new_head -> if Atomic.compare_and_set head old_head new_head then begin - match poly with - | Value -> - let value = r.value in - r.value <- Obj.magic (); - value - | Option -> - let value = r.value in - r.value <- Obj.magic (); - Some value + let value = r.value in + r.value <- Obj.magic (); + match poly with Value -> value | Option -> Some value | Unit -> () end else let backoff = Backoff.once backoff in @@ -60,21 +71,28 @@ let rec pop_as : let pop_opt t = pop_as t.head Backoff.default Option let pop_exn t = pop_as t.head Backoff.default Value +let drop_exn t = pop_as t.head Backoff.default Unit + +(* *) let rec peek_as : type a r. (a, [ `Next ]) Node.t Atomic.t -> (a, r) poly -> r = fun head poly -> let old_head = Atomic.get head in match Atomic.get (Node.as_atomic old_head) with - | Nil -> begin match poly with Value -> raise Empty | Option -> None end + | Nil -> begin + match poly with Value | Unit -> raise Empty | Option -> None + end | Next r -> let value = r.value in if Atomic.get head == old_head then - match poly with Value -> value | Option -> Some value + match poly with Value -> value | Option -> Some value | Unit -> () else peek_as head poly let peek_opt t = peek_as t.head Option let peek_exn t = peek_as t.head Value +(* *) + let rec fix_tail tail new_tail backoff = let old_tail = Atomic.get tail in if diff --git a/src/michael_scott_queue/michael_scott_queue_unsafe_node.ml b/src/michael_scott_queue/michael_scott_queue_unsafe_node.ml index 10405e18..386a1570 100644 --- a/src/michael_scott_queue/michael_scott_queue_unsafe_node.ml +++ b/src/michael_scott_queue/michael_scott_queue_unsafe_node.ml @@ -10,5 +10,18 @@ type ('a, _) t = let[@inline] make value = Next { next = Nil; value } +let node_of_list values = + let (Next tail_node as tail) : ('a, [ `Next ]) t = + Next { value = Obj.magic (); next = Nil } + in + let rec build_next = function + | [ x ] -> + tail_node.value <- x; + tail + | hd :: tl -> Next { next = build_next tl; value = hd } + | [] -> assert false + in + (tail, build_next values) + external as_atomic : ('a, [ `Next ]) t -> ('a, [ `Nil | `Next ]) t Atomic.t = "%identity" diff --git a/test/michael_scott_queue/dune b/test/michael_scott_queue/dune index aecb9e94..7be22cc0 100644 --- a/test/michael_scott_queue/dune +++ b/test/michael_scott_queue/dune @@ -15,7 +15,7 @@ (rule (action (copy - ../../src/michael_scott_queue/michael_scott_queue_intf.ml + ../../src/michael_scott_queue/michael_scott_queue_intf.mli michael_scott_queue_intf.ml)) (package saturn)) diff --git a/test/michael_scott_queue/michael_scott_queue_dscheck.ml b/test/michael_scott_queue/michael_scott_queue_dscheck.ml index fd3187fe..4e91ff6f 100644 --- a/test/michael_scott_queue/michael_scott_queue_dscheck.ml +++ b/test/michael_scott_queue/michael_scott_queue_dscheck.ml @@ -1,107 +1,175 @@ module Atomic = Dscheck.TracedAtomic -module Dscheck_ms_queue - (Michael_scott_queue : Michael_scott_queue_intf.MS_QUEUE) = -struct - let drain queue = - let remaining = ref 0 in - while not (Michael_scott_queue.is_empty queue) do - remaining := !remaining + 1; - assert (Option.is_some (Michael_scott_queue.pop_opt queue)) - done; - !remaining - - let producer_consumer () = +module Dscheck_ms_queue (Queue : Michael_scott_queue_intf.MS_QUEUE) = struct + let drain cue = + let rec pop_until_empty acc = + match Queue.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 queue = Michael_scott_queue.create () in + let queue = Queue.create () in let items_total = 4 in (* producer *) Atomic.spawn (fun () -> for i = 1 to items_total do - Michael_scott_queue.push queue i + Queue.push queue i done); (* consumer *) - let popped = ref 0 in + let popped = ref [] in Atomic.spawn (fun () -> for _ = 1 to items_total do - match Michael_scott_queue.pop_opt queue with - | None -> () - | Some v -> - assert (v == !popped + 1); - popped := !popped + 1 + begin + match Queue.pop_opt queue with + | None -> () + | Some v -> popped := v :: !popped + end; + (* Ensure is_empty does not interfere with other functions *) + Queue.is_empty queue |> ignore done); (* checks*) Atomic.final (fun () -> Atomic.check (fun () -> let remaining = drain queue in - !popped + remaining = items_total))) + 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 queue = Queue.create () in + + (* producer *) + Atomic.spawn (fun () -> Queue.push queue 1); + + (* consumer *) + let res = ref false in + Atomic.spawn (fun () -> + match Queue.pop_opt queue with + | None -> res := true + | Some _ -> res := Queue.is_empty queue); + + (* checks*) + Atomic.final (fun () -> Atomic.check (fun () -> !res))) - let producer_consumer_peek () = + let push_drop () = Atomic.trace (fun () -> - let queue = Michael_scott_queue.create () in - let items_total = 1 in - let pushed = List.init items_total (fun i -> i) in + let queue = Queue.create () in + let items_total = 4 in (* producer *) Atomic.spawn (fun () -> - List.iter (fun elt -> Michael_scott_queue.push queue elt) pushed); + for i = 1 to items_total do + Queue.push queue i + done); (* consumer *) - let popped = ref [] in - let peeked = ref [] in + let dropped = ref 0 in Atomic.spawn (fun () -> for _ = 1 to items_total do - peeked := Michael_scott_queue.peek_opt queue :: !peeked; - popped := Michael_scott_queue.pop_opt queue :: !popped + match Queue.drop_exn queue with + | () -> dropped := !dropped + 1 + | exception Queue.Empty -> () done); (* checks*) Atomic.final (fun () -> - Atomic.check (fun () -> - let rec check pushed peeked popped = - match (pushed, peeked, popped) with - | _, [], [] -> true - | _, 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)); Atomic.check (fun () -> let remaining = drain queue in - let popped = List.filter Option.is_some !popped in - List.length popped + remaining = items_total))) + remaining + = List.init (items_total - !dropped) (fun x -> x + !dropped + 1)))) - let two_producers () = + let push_push () = Atomic.trace (fun () -> - let queue = Michael_scott_queue.create () in - let items_total = 4 in + let queue = Queue.create () in + let items_total = 6 in - (* producers *) - for _ = 1 to 2 do + (* two producers *) + for i = 0 to 1 do Atomic.spawn (fun () -> - for _ = 1 to items_total / 2 do - Michael_scott_queue.push queue 0 + for j = 1 to items_total / 2 do + (* even nums belong to thr 1, odd nums to thr 2 *) + Queue.push queue (i + (j * 2)) done) done; + (* checks*) + Atomic.final (fun () -> + let items = drain queue 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_pop_of_list () = + Atomic.trace (fun () -> + let items_total = 4 in + let pushed = List.init items_total (fun x -> x + 1) in + let cue = Queue.of_list pushed in + + Atomic.spawn (fun () -> Queue.push cue 42); + + (* consumer *) + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + begin + match Queue.pop_opt cue with + | None -> () + | Some v -> popped := v :: !popped + end + done); + (* checks*) Atomic.final (fun () -> Atomic.check (fun () -> - let remaining = drain queue in - remaining = items_total))) + let remaining = drain cue in + let pushed = pushed @ [ 42 ] in + List.sort Int.compare (!popped @ remaining) = pushed))) + + let pop_pop () = + Atomic.trace (fun () -> + let items_total = 4 in + let queue = Queue.of_list (List.init items_total (fun x -> x + 1)) in + + (* 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 (Queue.pop_opt queue) :: !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 stack = Michael_scott_queue.create () in + let stack = Queue.create () in let n1, n2 = (2, 1) in (* two producers *) @@ -117,9 +185,8 @@ struct List.iter (fun elt -> (* even nums belong to thr 1, odd nums to thr 2 *) - Michael_scott_queue.push stack elt; - lpop := - Option.get (Michael_scott_queue.pop_opt stack) :: !lpop) + Queue.push stack elt; + lpop := Option.get (Queue.pop_opt stack) :: !lpop) lpush) |> ignore) lists; @@ -142,15 +209,63 @@ struct let is_sorted l = List.sort (fun a b -> -compare a b) l = l in is_sorted l1 && is_sorted l2 && is_sorted l3 && is_sorted l4))) + let two_domains_more_pop () = + Atomic.trace (fun () -> + let queue = Queue.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 -> + Queue.push queue elt; + lpop := Queue.pop_opt queue :: !lpop; + lpop := Queue.pop_opt queue :: !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 producer_consumer; - test_case "1-producer-1-consumer-peek" `Slow producer_consumer_peek; - test_case "2-producers" `Slow two_producers; + test_case "1-producer-1-consumer" `Slow push_pop; + test_case "2-domains-is_empty" `Slow is_empty; + test_case "1-push-1-drop" `Slow push_drop; + test_case "1-push-1-pop-of_list" `Slow push_pop_of_list; + test_case "2-producers" `Slow push_push; + 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 diff --git a/test/michael_scott_queue/michael_scott_queue_unsafe_node.ml b/test/michael_scott_queue/michael_scott_queue_unsafe_node.ml index cf7a5ed0..af1d3686 100644 --- a/test/michael_scott_queue/michael_scott_queue_unsafe_node.ml +++ b/test/michael_scott_queue/michael_scott_queue_unsafe_node.ml @@ -10,4 +10,18 @@ type ('a, _) t = -> ('a, [> `Next ]) t let[@inline] make value = Next { next = Atomic.make Nil; value } + +let node_of_list values = + let (Next tail_node as tail) : ('a, [ `Next ]) t = + Next { value = Obj.magic (); next = Atomic.make Nil } + in + let rec build_next = function + | [ x ] -> + tail_node.value <- x; + tail + | value :: tl -> Next { value; next = Atomic.make @@ build_next tl } + | [] -> assert false + in + (tail, Atomic.make @@ build_next values) + let[@inline] as_atomic (Next r : ('a, [ `Next ]) t) = r.next diff --git a/test/michael_scott_queue/ms_queues/dune b/test/michael_scott_queue/ms_queues/dune index 33ef2ad2..17b64c8b 100644 --- a/test/michael_scott_queue/ms_queues/dune +++ b/test/michael_scott_queue/ms_queues/dune @@ -1,7 +1,7 @@ (rule (action (copy - ../../../src/michael_scott_queue/michael_scott_queue_intf.ml + ../../../src/michael_scott_queue/michael_scott_queue_intf.mli michael_scott_queue_intf.ml)) (package saturn)) diff --git a/test/michael_scott_queue/stm_michael_scott_queue.ml b/test/michael_scott_queue/stm_michael_scott_queue.ml index 6ff26348..57cf712b 100644 --- a/test/michael_scott_queue/stm_michael_scott_queue.ml +++ b/test/michael_scott_queue/stm_michael_scott_queue.ml @@ -4,13 +4,14 @@ open STM (** Sequential and Parallel model-based tests of michael_scott_queue *) module STM_ms_queue (Queue : Ms_queues.MS_queue_tests) = struct module Spec = struct - type cmd = Push of int | Pop | Peek | Is_empty + type cmd = Push of int | Pop | Peek | Drop | Is_empty let show_cmd c = match c with | Push i -> "Push " ^ string_of_int i | Pop -> "Pop" | Peek -> "Peek" + | Drop -> "Drop" | Is_empty -> "Is_empty" type state = int list @@ -24,6 +25,7 @@ module STM_ms_queue (Queue : Ms_queues.MS_queue_tests) = struct Gen.map (fun i -> Push i) int_gen; Gen.return Pop; Gen.return Peek; + Gen.return Drop; Gen.return Is_empty; ]) @@ -34,7 +36,8 @@ module STM_ms_queue (Queue : Ms_queues.MS_queue_tests) = struct let next_state c s = match c with | Push i -> i :: s - | Pop -> ( match List.rev s with [] -> s | _ :: s' -> List.rev s') + | Pop | Drop -> ( + match List.rev s with [] -> s | _ :: s' -> List.rev s') | Peek | Is_empty -> s let precond _ _ = true @@ -44,6 +47,7 @@ module STM_ms_queue (Queue : Ms_queues.MS_queue_tests) = struct | Push i -> Res (unit, Queue.push d i) | Pop -> Res (result int exn, protect Queue.pop_exn d) | Peek -> Res (result int exn, protect Queue.peek_exn d) + | Drop -> Res (result unit exn, protect Queue.drop_exn d) | Is_empty -> Res (bool, Queue.is_empty d) let postcond c (s : state) res = @@ -53,6 +57,10 @@ module STM_ms_queue (Queue : Ms_queues.MS_queue_tests) = struct match List.rev s with | [] -> res = Error Queue.Empty | j :: _ -> res = Ok j) + | Drop, Res ((Result (Unit, Exn), _), res) -> ( + match List.rev s with + | [] -> res = Error Queue.Empty + | _ -> res = Ok ()) | Is_empty, Res ((Bool, _), res) -> res = (s = []) | _, _ -> false end From add0115bf25638e0016decc49fd878162e7f80f9 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 26 Nov 2024 19:38:57 +0100 Subject: [PATCH 2/4] Add useful warning --- src/michael_scott_queue/michael_scott_queue_intf.mli | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/michael_scott_queue/michael_scott_queue_intf.mli b/src/michael_scott_queue/michael_scott_queue_intf.mli index 49c649be..e2c3b7fc 100644 --- a/src/michael_scott_queue/michael_scott_queue_intf.mli +++ b/src/michael_scott_queue/michael_scott_queue_intf.mli @@ -41,6 +41,8 @@ module type MS_QUEUE = sig val of_list : 'a list -> 'a t (** [of_list list] creates a new queue from a list. + 🐌 This is a linear-time operation. + {[ # open Saturn.Queue # let t : int t = of_list [1;2;3;4] @@ -115,10 +117,11 @@ module type MS_QUEUE = sig *) (** {2 Parallel example} - **Note** that the use of a barrier is only necessary to make the result of - this example interesting by improving the likelihood of parallelism. - Spawning a domain is a costly operation compared to the work actually run on them - here. In practice, you should not use a barrier. + Note: The barrier is used in this example solely to make the results more + interesting by increasing the likelihood of parallelism. Spawning a domain is + a costly operation, especially compared to the relatively small amount of work + being performed here. In practice, using a barrier in this manner is unnecessary. + {@ocaml non-deterministic[ # open Saturn.Queue From 468e3a4f08ac0a6c348a04c2e119c0d7bf31e686 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 26 Nov 2024 20:34:08 +0100 Subject: [PATCH 3/4] debug mdx test. --- src/michael_scott_queue/michael_scott_queue_intf.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/michael_scott_queue/michael_scott_queue_intf.mli b/src/michael_scott_queue/michael_scott_queue_intf.mli index e2c3b7fc..3011b41e 100644 --- a/src/michael_scott_queue/michael_scott_queue_intf.mli +++ b/src/michael_scott_queue/michael_scott_queue_intf.mli @@ -123,7 +123,7 @@ module type MS_QUEUE = sig being performed here. In practice, using a barrier in this manner is unnecessary. - {@ocaml non-deterministic[ + {@ocaml non-deterministic=command[ # open Saturn.Queue # let t : string t = create () val t : string t = From a31f9716688efa53f6a1b3d2e4619f943419d6bc Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 28 Nov 2024 17:57:11 +0100 Subject: [PATCH 4/4] Apply reviews. --- src/michael_scott_queue/michael_scott_queue_intf.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/michael_scott_queue/michael_scott_queue_intf.mli b/src/michael_scott_queue/michael_scott_queue_intf.mli index 3011b41e..5c0acc8d 100644 --- a/src/michael_scott_queue/michael_scott_queue_intf.mli +++ b/src/michael_scott_queue/michael_scott_queue_intf.mli @@ -55,13 +55,13 @@ module type MS_QUEUE = sig *) val is_empty : 'a t -> bool - (** [is_empty q] returns [true] if [q] is empty and [false otherwise]. *) + (** [is_empty q] returns [true] if [q] is empty and [false] otherwise. *) (** {2 Consumer functions} *) exception Empty (** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty - stack. *) + queue. *) val peek_exn : 'a t -> 'a (** [peek_exn queue] returns the first element of the [queue] without removing it.