From ae22a2cb4e03288b4ef9258bc3bd83e0f2af0931 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 8 Oct 2024 19:27:43 +0200 Subject: [PATCH 01/11] Add bounded_queue. --- bench/bench_bounded_stack.ml | 72 ++++++ bench/main.ml | 1 + dune-project | 1 + src/bounded_stack.ml | 156 ++++++++++++ src/bounded_stack.mli | 113 ++++++++ src/saturn.ml | 1 + src/saturn.mli | 1 + test/bounded_stack/bounded_stack_dscheck.ml | 269 ++++++++++++++++++++ test/bounded_stack/dune | 23 ++ test/bounded_stack/stm_bounded_stack.ml | 80 ++++++ 10 files changed, 717 insertions(+) create mode 100644 bench/bench_bounded_stack.ml create mode 100644 src/bounded_stack.ml create mode 100644 src/bounded_stack.mli create mode 100644 test/bounded_stack/bounded_stack_dscheck.ml create mode 100644 test/bounded_stack/dune create mode 100644 test/bounded_stack/stm_bounded_stack.ml diff --git a/bench/bench_bounded_stack.ml b/bench/bench_bounded_stack.ml new file mode 100644 index 00000000..3acacb0b --- /dev/null +++ b/bench/bench_bounded_stack.ml @@ -0,0 +1,72 @@ +open Multicore_bench +module Stack = Saturn_lockfree.Bounded_stack + +let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = + let t = Stack.create () in + + let op push = if push then Stack.push t 101 else Stack.pop_opt t |> ignore in + + let init _ = + assert (Stack.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 = Stack.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 (Stack.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 + Stack.push t i + done; + work () + end + in + work () + else + let rec work () = + let n = Util.alloc n_msgs_to_take in + if n <> 0 then begin + for _ = 1 to n do + while Option.is_none (Stack.pop_opt t) do + Domain.cpu_relax () + done + done; + work () + end + 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 "adder" n_adders) (format "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/main.ml b/bench/main.ml index 24870c77..43e6df78 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -7,6 +7,7 @@ let benchmarks = ("Saturn Htbl", Bench_htbl.run_suite); ("Saturn Stack", Bench_stack.run_suite); ("Saturn Work_stealing_deque", Bench_ws_deque.run_suite); + ("Saturn_lockfree Bounded_Stack", Bench_bounded_stack.run_suite); ] let () = Multicore_bench.Cmd.run ~benchmarks () diff --git a/dune-project b/dune-project index 2eceb755..645b1c75 100644 --- a/dune-project +++ b/dune-project @@ -16,6 +16,7 @@ (depends (ocaml (>= 4.14)) (backoff (>= 0.1.0)) + (picos (>= 0.5.0)) (multicore-magic (>= 2.3.0)) (alcotest (and (>= 1.7.0) :with-test)) (domain_shims (and (>= 0.1.0) :with-test)) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml new file mode 100644 index 00000000..0b70f8f7 --- /dev/null +++ b/src/bounded_stack.ml @@ -0,0 +1,156 @@ +open Picos + +type 'a node = Nil | Cons of { value : 'a; tail : 'a node; capacity : int } + +type 'a t = { + head : 'a node Atomic.t; + cons_waiters : Trigger.t list Atomic.t; + prod_waiters : Trigger.t list Atomic.t; + capacity : int; +} + +let create ?(capacity = Int.max_int) () = + let head = Atomic.make_contended Nil in + let cons_waiters = Atomic.make_contended [] in + let prod_waiters = Atomic.make_contended [] in + { head; cons_waiters; prod_waiters; capacity = max capacity 1 } + |> Multicore_magic.copy_as_padded + +let is_empty t = Atomic.get t.head == Nil + +let rec signal_all waiters = + let triggers = Atomic.get waiters in + if triggers != [] then + if Atomic.compare_and_set waiters triggers [] then + List.iter Trigger.signal triggers + else signal_all waiters + +let rec peek t = + let old_head = Atomic.get t.head in + match old_head with + | Nil -> + let trigger = Trigger.create () in + let triggers = Atomic.get t.cons_waiters in + if Atomic.compare_and_set t.cons_waiters triggers (trigger :: triggers) + then begin + if Atomic.get t.head != Nil then signal_all t.cons_waiters + else + match Trigger.await trigger with + | None -> () + | Some (exn, bt) -> + signal_all t.cons_waiters; + Printexc.raise_with_backtrace exn bt + end; + peek t + | Cons cons -> cons.value + +let peek_opt t = + let head = Atomic.get t.head in + match head with Nil -> None | Cons cons -> Some cons.value + +let rec pop t backoff = + match Atomic.get t.head with + | Nil -> + let trigger = Trigger.create () in + let triggers = Atomic.get t.cons_waiters in + if Atomic.compare_and_set t.cons_waiters triggers (trigger :: triggers) + then begin + if Atomic.get t.head != Nil then signal_all t.cons_waiters + else + match Trigger.await trigger with + | None -> () + | Some (exn, bt) -> + signal_all t.cons_waiters; + Printexc.raise_with_backtrace exn bt + end; + pop t backoff + | Cons cons_r as old_head -> + if Atomic.compare_and_set t.head old_head cons_r.tail then ( + signal_all t.prod_waiters; + cons_r.value) + else pop t (Backoff.once backoff) + +let pop t = pop t Backoff.default + +let rec pop_opt t backoff = + match Atomic.get t.head with + | Nil -> None + | Cons cons_r as old_head -> + if Atomic.compare_and_set t.head old_head cons_r.tail then ( + signal_all t.prod_waiters; + Some cons_r.value) + else pop_opt t (Backoff.once backoff) + +let pop_opt t = pop_opt t Backoff.default + +let rec push t backoff value = + match Atomic.get t.head with + | Nil -> + let new_head = Cons { value; tail = Nil; capacity = 1 } in + if Atomic.compare_and_set t.head Nil new_head then + signal_all t.cons_waiters + else push t (Backoff.once backoff) value + | Cons cons_r as old_head -> + if cons_r.capacity >= t.capacity then begin + let trigger = Trigger.create () in + let triggers = Atomic.get t.prod_waiters in + if Atomic.compare_and_set t.prod_waiters triggers (trigger :: triggers) + then begin + if Atomic.get t.head != old_head then signal_all t.prod_waiters + else + match Trigger.await trigger with + | None -> () + | Some (exn, bt) -> + signal_all t.prod_waiters; + Printexc.raise_with_backtrace exn bt + end; + push t backoff value + end + else + let new_head = + Cons { value; tail = old_head; capacity = cons_r.capacity + 1 } + in + if Atomic.compare_and_set t.head old_head new_head then + signal_all t.cons_waiters + else push t (Backoff.once backoff) value + +let push t value = push t Backoff.default value + +let rec try_push t backoff value = + match Atomic.get t.head with + | Nil -> + let new_head = Cons { value; tail = Nil; capacity = 1 } in + if Atomic.compare_and_set t.head Nil new_head then ( + signal_all t.cons_waiters; + true) + else try_push t (Backoff.once backoff) value + | Cons cons_r as old_head -> + if cons_r.capacity >= t.capacity then false + else + let new_head = + Cons { value; tail = old_head; capacity = cons_r.capacity + 1 } + in + if Atomic.compare_and_set t.head old_head new_head then ( + signal_all t.cons_waiters; + true) + else try_push t (Backoff.once backoff) value + +let try_push t value = try_push t Backoff.default value + +let length t = + match Atomic.get t.head with Nil -> 0 | Cons cons -> cons.capacity + +let rec pop_all t backoff = + match Atomic.get t.head with + | Nil -> [] + | old_head -> + if Atomic.compare_and_set t.head old_head Nil then ( + signal_all t.prod_waiters; + let rec aux acc = function + | Nil -> List.rev acc + | Cons cons -> aux (cons.value :: acc) cons.tail + in + aux [] old_head) + else pop_all t (Backoff.once backoff) + +let pop_all t = pop_all t Backoff.default diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli new file mode 100644 index 00000000..5b1f3178 --- /dev/null +++ b/src/bounded_stack.mli @@ -0,0 +1,113 @@ +(** Lock-free bounded stack. *) + +(** {1 API} *) + +type 'a t +(** Represents a lock-free bounded stack holding elements of type ['a]. *) + +val create : ?capacity:int -> unit -> 'a t +(** [create ~capacity ()] creates a new empty bounded stack with a maximum +capacity of [capacity]. Default [capacity] value is [Int.max_int]. +*) + +val length : 'a t -> int +(** [length stack] returns the number of elements currently in the [stack]. *) + +val is_empty : 'a t -> bool +(** [is_empty stack] returns [true] if the [stack] is empty, otherwise [false]. *) + +(** {2 Consumer functions} *) +val peek : 'a t -> 'a +(** [peek stack] returns the top element of the [stack] without removing it. If +the stack is empty, the domain will be suspended until another domain successfully +push another element in the stack with [push] or [push_opt] . *) + +val peek_opt : 'a t -> 'a option +(** [peek_opt stack] returns [Some] of the top element of the [stack] without + removing it, or [None] if the stack is empty. *) + +val pop : 'a t -> 'a +(** [pop stack] removes and returns the top element of the [stack]. + Raises an exception if the stack is empty. *) + +val pop_opt : 'a t -> 'a option +(** [pop_opt stack] removes and returns [Some] of the top element of the [stack], + or [None] if the stack is empty. *) + +val pop_all : 'a t -> 'a list +(** [pop_all stack] removes and returns all elements of the [stack] in the reverse +order they were pushed. *) + +(** {2 Producer functions} *) + +val push : 'a t -> 'a -> unit +(** [push stack element] adds [element] to the top of the [stack]. + Raises an exception if the stack is full. *) + +val try_push : 'a t -> 'a -> bool +(** [try_push stack element] tries to add [element] to the top of the [stack]. + Returns [true] if the element was successfully added, or [false] if the + stack is full. *) + +(** {1 Examples} + An example top-level session: + {[ + # let t : int Saturn.Bounded_stack.t = + Saturn.Bounded_stack.create () + val t : int Saturn.Bounded_stack.t = + # Saturn.Bounded_stack.try_push t 42 + - : bool = true + # Saturn.Bounded_stack.push t 1 + - : unit = () + # Saturn.Bounded_stack.pop t + - : int = 1 + # Saturn.Bounded_stack.peek_opt t + - : int option = Some 42 + # Saturn.Bounded_stack.pop_opt t + - : int option = Some 42 + # Saturn.Bounded_stack.pop_opt t + - : int option = None ]} + + A multicore example: + {[ + open Saturn_lockfree + open Picos_std_structured + + let main () = + let st = Bounded_stack.create ~capacity:2 () in + let popped = Bounded_stack.create ~capacity:Int.max_int () in + Flock.join_after + begin + fun () -> + for i = 0 to 2 lsl 5 - 1 do + Flock.fork @@ fun () -> + begin + if i/4 mod 2 = 0 then (* 4 pushes followed by 4 pops *) + let id = (Domain.self () :> int) in + Bounded_stack.push st id + else Bounded_stack.pop st |> Bounded_stack.push popped + (* stores the result of pop in popped *) + end; + Unix.sleepf (Random.float 0.1) + done + end; + assert (Bounded_stack.pop_all st = []); + Bounded_stack.pop_all popped |> List.rev + + let run () = + Picos_mux_multififo.run_on ~n_domains:4 main + ]} + This example uses Picos' prefined {{:https://ocaml-multicore.github.io/picos/doc/picos_mux/Picos_mux_multififo/index.html}multi-threaded scheduler} + to run four domains that are alternatively pushing their ids and popping in + a shared stack with a capacity of 2 elements. The returned list is the + pusher's ids in order. Note that with this scheduler, a maximum of 4 domains + can be used in parallel and each domain can spawn multiple fibers, meaning + even if run in a single domain, this example will not block indefinitely. + + {[ + # run ();; + - : int list = + [5; 4; 6; 6; 4; 5; 4; 0; 6; 5; 6; 4; 0; 5; 4; 5; 0; 5; 6; 5; 5; 0; 5; 4; + 4; 0; 0; 0; 0; 0; 0; 0] + ]} + *) diff --git a/src/saturn.ml b/src/saturn.ml index eff05f9d..7da90e4d 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 Stack = Treiber_stack +module Bounded_stack = Bounded_stack 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/src/saturn.mli b/src/saturn.mli index eac1789b..52f9f821 100644 --- a/src/saturn.mli +++ b/src/saturn.mli @@ -33,6 +33,7 @@ Copyright (c) 2017, Nicolas ASSOUAD module Queue = Michael_scott_queue module Queue_unsafe = Michael_scott_queue_unsafe module Stack = Treiber_stack +module Bounded_stack = Bounded_stack 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_stack/bounded_stack_dscheck.ml b/test/bounded_stack/bounded_stack_dscheck.ml new file mode 100644 index 00000000..fe86ff81 --- /dev/null +++ b/test/bounded_stack/bounded_stack_dscheck.ml @@ -0,0 +1,269 @@ +module Stack = Bounded_stack + +let drain stack = + let remaining = ref 0 in + while not (Stack.is_empty stack) do + remaining := !remaining + 1; + assert (Option.is_some (Stack.pop_opt stack)) + done; + !remaining + +let producer_consumer () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Stack.try_push stack i |> ignore + done); + + (* consumer *) + let popped = ref 0 in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Stack.pop_opt stack with + | None -> () + | Some _ -> popped := !popped + 1 + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = drain stack in + !popped + remaining = items_total))) + +let producer_consumer_with_capacity () = + Atomic.trace (fun () -> + let stack = Stack.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) <- Stack.try_push stack i) pushed); + + (* consumer *) + let popped = Array.make items_total None in + Atomic.spawn (fun () -> + Array.iteri (fun i _ -> popped.(i) <- Stack.pop_opt stack) popped); + (* checks*) + Atomic.final (fun () -> + let popped = Array.to_list popped |> List.filter_map Fun.id in + let remaining = Stack.pop_all stack 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 two_producers () = + Atomic.trace (fun () -> + let stack = Stack.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 *) + Stack.try_push stack (i + (j * 2)) |> ignore + done) + done; + + (* checks*) + Atomic.final (fun () -> + let items = Stack.pop_all stack in + + (* got the same number of items out as in *) + Atomic.check (fun () -> items_total = List.length items); + + (* they are in lifo order *) + let odd, even = List.partition (fun v -> v mod 2 == 0) items in + + Atomic.check (fun () -> List.sort Int.compare odd = List.rev odd); + Atomic.check (fun () -> List.sort Int.compare even = List.rev even))) + +let two_producers_with_capacity () = + Atomic.trace (fun () -> + let capacity = 3 in + let stack = Stack.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 *) + Stack.try_push stack (i + (j * 2)) |> ignore + done) + done; + + (* checks*) + Atomic.final (fun () -> + let items = Stack.pop_all stack in + + (* got the same number of items out as in *) + Atomic.check (fun () -> capacity = List.length items))) + +let two_consumers () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + + for i = 1 to items_total do + Stack.try_push stack 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 (Stack.pop_opt stack) :: !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 lifo order *) + Atomic.check (fun () -> List.sort Int.compare l1 = l1); + Atomic.check (fun () -> List.sort Int.compare l2 = l2))) + +let two_domains () = + Atomic.trace (fun () -> + let stack = Stack.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 *) + Stack.try_push stack elt |> ignore; + lpop := Option.get (Stack.pop_opt stack) :: !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 stack = Stack.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 -> + Stack.push stack elt; + lpop := Stack.pop_opt stack :: !lpop; + lpop := Stack.pop_opt stack :: !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 two_domains_pop_all () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let n_items = 6 in + Atomic.spawn (fun () -> + for i = 0 to n_items - 1 do + Stack.try_push stack i |> ignore + done); + + let popped = ref [] in + Atomic.spawn (fun () -> popped := Stack.pop_all stack); + + Atomic.final (fun () -> + let remaining = Stack.pop_all stack in + + (* got the same number of items out as in *) + Atomic.check (fun () -> + remaining @ !popped = List.rev @@ List.init n_items Fun.id))) + +let () = + let open Alcotest in + run "Stack_dscheck" + [ + ( "basic", + [ + test_case "1-producer-1-consumer" `Slow producer_consumer; + test_case "1-producer-1-consumer-capacity" `Slow + producer_consumer_with_capacity; + test_case "2-producers" `Slow two_producers; + test_case "2-producers-capacity" `Slow two_producers_with_capacity; + test_case "2-consumers" `Slow two_consumers; + test_case "2-domains" `Slow two_domains; + test_case "2-domains-more-pops" `Slow two_domains_more_pop; + test_case "2-domains-pops_all" `Slow two_domains_pop_all; + ] ); + ] diff --git a/test/bounded_stack/dune b/test/bounded_stack/dune new file mode 100644 index 00000000..4906625e --- /dev/null +++ b/test/bounded_stack/dune @@ -0,0 +1,23 @@ +(rule + (action + (copy ../../src_lockfree/bounded_stack.ml bounded_stack.ml)) + (package saturn_lockfree)) + +(test + (package saturn_lockfree) + (name bounded_stack_dscheck) + (libraries picos atomic dscheck alcotest backoff multicore-magic) + (build_if + (and + (>= %{ocaml_version} 5) + (not + (and + (= %{arch_sixtyfour} false) + (= %{architecture} arm))))) + (modules bounded_stack bounded_stack_dscheck)) + +(test + (package saturn_lockfree) + (name stm_bounded_stack) + (modules stm_bounded_stack) + (libraries saturn_lockfree qcheck-core qcheck-stm.stm stm_run)) diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml new file mode 100644 index 00000000..f1d03e69 --- /dev/null +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -0,0 +1,80 @@ +(** Sequential and Parallel model-based tests of bounded_queue *) + +open QCheck +open STM +module Stack = Saturn_lockfree.Bounded_stack + +module Spec = struct + type cmd = + | Try_push of int + | Pop_opt + | Pop_all + | Peek_opt + | Is_empty + | Length + + let show_cmd c = + match c with + | Try_push i -> "Try_push " ^ string_of_int i + | Pop_opt -> "Pop_opt" + | Pop_all -> "Pop_all" + | Peek_opt -> "Peek_opt" + | Is_empty -> "Is_empty" + | Length -> "Length" + + type state = int list + type sut = int Stack.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 Pop_all; + Gen.return Is_empty; + Gen.return Length; + Gen.return Peek_opt; + Gen.return Is_empty; + ]) + + let init_state = [] + let capacity = 8 + let init_sut () = Stack.create ~capacity () + let cleanup _ = () + + let next_state c s = + match c with + | Try_push i -> if List.length s >= capacity then s else i :: s + | Pop_opt -> ( match s with [] -> s | _ :: s' -> s') + | Pop_all -> [] + | Peek_opt -> s + | Is_empty -> s + | Length -> s + + let precond _ _ = true + + let run c d = + match c with + | Try_push i -> Res (bool, Stack.try_push d i) + | Pop_opt -> Res (option int, Stack.pop_opt d) + | Pop_all -> Res (list int, Stack.pop_all d) + | Peek_opt -> Res (option int, Stack.peek_opt d) + | Is_empty -> Res (bool, Stack.is_empty d) + | Length -> Res (int, Stack.length d) + + let postcond c (s : state) res = + match (c, res) with + | Try_push _, Res ((Bool, _), res) -> List.length s < capacity = res + | Pop_opt, Res ((Option Int, _), res) -> ( + match s with [] -> res = None | j :: _ -> res = Some j) + | Pop_all, Res ((List Int, _), res) -> res = s + | Peek_opt, Res ((Option Int, _), res) -> ( + match s with [] -> res = None | j :: _ -> res = Some j) + | Is_empty, Res ((Bool, _), res) -> res = (s = []) + | Length, Res ((Int, _), res) -> res = List.length s + | _, _ -> false +end + +let () = Stm_run.run ~name:"Saturn_lockfree.Bounded_stack" (module Spec) |> exit From c618a2e16cc8e8808cab3379a0c8847875b15f1b Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Sat, 26 Oct 2024 20:40:40 +0200 Subject: [PATCH 02/11] From bounded and blocking queue to bounded queue. Additional functions and tests --- bench/bench_bounded_stack.ml | 6 +- dune-project | 2 - src/bounded_stack.ml | 314 ++++++++++++-------- src/bounded_stack.mli | 250 +++++++++++----- src/dune | 8 +- src/seq.ocaml4.13.ml | 6 + test/bounded_stack/bounded_stack_dscheck.ml | 249 ++++++++++++++-- test/bounded_stack/dune | 2 +- test/bounded_stack/stm_bounded_stack.ml | 57 +++- 9 files changed, 660 insertions(+), 234 deletions(-) create mode 100644 src/seq.ocaml4.13.ml diff --git a/bench/bench_bounded_stack.ml b/bench/bench_bounded_stack.ml index 3acacb0b..8e8ee045 100644 --- a/bench/bench_bounded_stack.ml +++ b/bench/bench_bounded_stack.ml @@ -4,7 +4,9 @@ module Stack = Saturn_lockfree.Bounded_stack let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = let t = Stack.create () in - let op push = if push then Stack.push t 101 else Stack.pop_opt t |> ignore in + let op push = + if push then Stack.try_push t 101 |> ignore else Stack.pop_opt t |> ignore + in let init _ = assert (Stack.is_empty t); @@ -35,7 +37,7 @@ let run_one ~budgetf ?(n_adders = 2) ?(n_takers = 2) let n = Util.alloc n_msgs_to_add in if 0 < n then begin for i = 1 to n do - Stack.push t i + Stack.try_push t i |> ignore done; work () end diff --git a/dune-project b/dune-project index 645b1c75..9fe76bba 100644 --- a/dune-project +++ b/dune-project @@ -9,14 +9,12 @@ (documentation "https://ocaml-multicore.github.io/saturn/") (using mdx 0.4) - (package (name saturn) (synopsis "Collection of concurent-safe data structures for Multicore OCaml") (depends (ocaml (>= 4.14)) (backoff (>= 0.1.0)) - (picos (>= 0.5.0)) (multicore-magic (>= 2.3.0)) (alcotest (and (>= 1.7.0) :with-test)) (domain_shims (and (>= 0.1.0) :with-test)) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 0b70f8f7..3b932a09 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -1,156 +1,208 @@ -open Picos - type 'a node = Nil | Cons of { value : 'a; tail : 'a node; capacity : int } +type 'a t = { head : 'a node Atomic.t; capacity : int } -type 'a t = { - head : 'a node Atomic.t; - cons_waiters : Trigger.t list Atomic.t; - prod_waiters : Trigger.t list Atomic.t; - capacity : int; -} - +(* *) let create ?(capacity = Int.max_int) () = let head = Atomic.make_contended Nil in - let cons_waiters = Atomic.make_contended [] in - let prod_waiters = Atomic.make_contended [] in - { head; cons_waiters; prod_waiters; capacity = max capacity 1 } - |> Multicore_magic.copy_as_padded - -let is_empty t = Atomic.get t.head == Nil - -let rec signal_all waiters = - let triggers = Atomic.get waiters in - if triggers != [] then - if Atomic.compare_and_set waiters triggers [] then - List.iter Trigger.signal triggers - else signal_all waiters - -let rec peek t = - let old_head = Atomic.get t.head in - match old_head with - | Nil -> - let trigger = Trigger.create () in - let triggers = Atomic.get t.cons_waiters in - if Atomic.compare_and_set t.cons_waiters triggers (trigger :: triggers) - then begin - if Atomic.get t.head != Nil then signal_all t.cons_waiters - else - match Trigger.await trigger with - | None -> () - | Some (exn, bt) -> - signal_all t.cons_waiters; - Printexc.raise_with_backtrace exn bt - end; - peek t - | Cons cons -> cons.value - -let peek_opt t = - let head = Atomic.get t.head in - match head with Nil -> None | Cons cons -> Some cons.value - -let rec pop t backoff = - match Atomic.get t.head with - | Nil -> - let trigger = Trigger.create () in - let triggers = Atomic.get t.cons_waiters in - if Atomic.compare_and_set t.cons_waiters triggers (trigger :: triggers) - then begin - if Atomic.get t.head != Nil then signal_all t.cons_waiters - else - match Trigger.await trigger with - | None -> () - | Some (exn, bt) -> - signal_all t.cons_waiters; - Printexc.raise_with_backtrace exn bt - end; - pop t backoff - | Cons cons_r as old_head -> - if Atomic.compare_and_set t.head old_head cons_r.tail then ( - signal_all t.prod_waiters; - cons_r.value) - else pop t (Backoff.once backoff) + { head; capacity = max capacity 1 } |> Multicore_magic.copy_as_padded -let pop t = pop t Backoff.default +let length t = + match Atomic.get t.head with Nil -> 0 | Cons cons -> cons.capacity -let rec pop_opt t backoff = +let is_empty t = Atomic.get t.head = Nil + +exception Empty +exception Full + +let of_list ?(capacity = Int.max_int) list = + if capacity < List.length list then raise Full + else + let head = + List.fold_left + (fun (len, acc) elt -> + (len + 1, Cons { value = elt; tail = acc; capacity = len })) + (1, Nil) list + |> snd |> Atomic.make_contended + in + { head; capacity } |> Multicore_magic.copy_as_padded + +let of_seq ?(capacity = Int.max_int) seq = + if capacity < Seq.length seq then raise Full + else + let head = + Seq.fold_left + (fun (len, acc) elt -> + (len + 1, Cons { value = elt; tail = acc; capacity = len })) + (1, Nil) seq + |> snd |> Atomic.make_contended + in + { head; capacity } |> Multicore_magic.copy_as_padded + +(* *) + +type ('a, _) poly1 = Option : ('a, 'a option) poly1 | Value : ('a, 'a) poly1 + +let peek_as : type a r. a t -> (a, r) poly1 -> r = + fun t poly -> + match Atomic.get t.head with + | Nil -> begin + match poly with Option -> None | Value -> raise_notrace Empty + end + | Cons cons_r -> ( + match poly with Option -> Some cons_r.value | Value -> cons_r.value) + +let peek_exn t = peek_as t Value +let peek_opt t = peek_as t Option + +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 -> match Atomic.get t.head with - | Nil -> None + | Nil -> begin + match poly with + | Option -> None + | Value -> raise_notrace Empty + | Unit -> raise_notrace Empty + end | Cons cons_r as old_head -> - if Atomic.compare_and_set t.head old_head cons_r.tail then ( - signal_all t.prod_waiters; - Some cons_r.value) - else pop_opt t (Backoff.once backoff) + if Atomic.compare_and_set t.head old_head cons_r.tail then + match poly with + | Option -> Some cons_r.value + | Value -> cons_r.value + | Unit -> () + else pop_as t (Backoff.once backoff) poly -let pop_opt t = pop_opt t Backoff.default +let pop_exn t = pop_as t Backoff.default Value +let pop_opt t = pop_as t Backoff.default Option +let drop_exn t = pop_as t Backoff.default Unit -let rec push t backoff value = +let rec pop_all t backoff = match Atomic.get t.head with - | Nil -> - let new_head = Cons { value; tail = Nil; capacity = 1 } in - if Atomic.compare_and_set t.head Nil new_head then - signal_all t.cons_waiters - else push t (Backoff.once backoff) value - | Cons cons_r as old_head -> - if cons_r.capacity >= t.capacity then begin - let trigger = Trigger.create () in - let triggers = Atomic.get t.prod_waiters in - if Atomic.compare_and_set t.prod_waiters triggers (trigger :: triggers) - then begin - if Atomic.get t.head != old_head then signal_all t.prod_waiters - else - match Trigger.await trigger with - | None -> () - | Some (exn, bt) -> - signal_all t.prod_waiters; - Printexc.raise_with_backtrace exn bt - end; - push t backoff value - end - else - let new_head = - Cons { value; tail = old_head; capacity = cons_r.capacity + 1 } + | Nil -> [] + | old_head -> + if Atomic.compare_and_set t.head old_head Nil then + let[@tail_mod_cons] rec aux = function + | Nil -> [] + | Cons cons -> cons.value :: aux cons.tail in - if Atomic.compare_and_set t.head old_head new_head then - signal_all t.cons_waiters - else push t (Backoff.once backoff) value + aux old_head + else pop_all t (Backoff.once backoff) -let push t value = push t Backoff.default value +let pop_all t = pop_all t Backoff.default -let rec try_push t backoff value = +let to_seq t = + match Atomic.get t.head with + | Nil -> Seq.empty + | old_head -> + let rec aux s () = + match s with + | Nil -> Seq.Nil + | Cons cons -> Seq.Cons (cons.value, aux cons.tail) + in + aux old_head + +(* *) + +type _ mono = Unit : unit mono | Bool : bool mono + +let rec push_as : type r. 'a t -> Backoff.t -> 'a -> r mono -> r = + fun t backoff value mono -> match Atomic.get t.head with | Nil -> - let new_head = Cons { value; tail = Nil; capacity = 1 } in - if Atomic.compare_and_set t.head Nil new_head then ( - signal_all t.cons_waiters; - true) - else try_push t (Backoff.once backoff) value + if + Atomic.compare_and_set t.head Nil + @@ Cons { value; tail = Nil; capacity = 1 } + then match mono with Bool -> true | Unit -> () + else push_as t (Backoff.once backoff) value mono | Cons cons_r as old_head -> - if cons_r.capacity >= t.capacity then false + if cons_r.capacity >= t.capacity then + match mono with Bool -> false | Unit -> raise Full else let new_head = Cons { value; tail = old_head; capacity = cons_r.capacity + 1 } in - if Atomic.compare_and_set t.head old_head new_head then ( - signal_all t.cons_waiters; - true) - else try_push t (Backoff.once backoff) value + if Atomic.compare_and_set t.head old_head new_head then + match mono with Bool -> true | Unit -> () + else push_as t (Backoff.once backoff) value mono -let try_push t value = try_push t Backoff.default value +let push_exn t value = push_as t Backoff.default value Unit +let try_push t value = push_as t Backoff.default value Bool -let length t = - match Atomic.get t.head with Nil -> 0 | Cons cons -> cons.capacity +type ('a, _) poly3 = Value : ('a, 'a) poly3 | Bool : ('a, bool) poly3 -let rec pop_all t backoff = +let rec set_as : type v r. v t -> v -> Backoff.t -> (v, r) poly3 -> r = + fun t value backoff poly -> match Atomic.get t.head with - | Nil -> [] - | old_head -> - if Atomic.compare_and_set t.head old_head Nil then ( - signal_all t.prod_waiters; - let rec aux acc = function - | Nil -> List.rev acc - | Cons cons -> aux (cons.value :: acc) cons.tail - in - aux [] old_head) - else pop_all t (Backoff.once backoff) - -let pop_all t = pop_all t Backoff.default + | Nil -> ( match poly with Value -> raise_notrace Empty | Bool -> false) + | Cons cons_r as old_head -> + if Atomic.compare_and_set t.head old_head @@ Cons { cons_r with value } + then match poly with Value -> cons_r.value | Bool -> true + else set_as t value (Backoff.once backoff) poly + +let set_exn t value = set_as t value Backoff.default Value +let try_set t value = set_as t value Backoff.default Bool + +let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r = + fun t backoff values mono -> + let len = List.length values in + if len = 0 then match mono with Unit -> () | Bool -> true + else if len > t.capacity then + match mono with Unit -> raise Full | Bool -> false + else + let rec build_node len acc = function + | [] -> acc + | x :: xs -> + build_node (len + 1) + (Cons { capacity = len + 1; tail = acc; value = x }) + xs + in + match Atomic.get t.head with + | Nil -> + if Atomic.compare_and_set t.head Nil (build_node 0 Nil values) then + match mono with Bool -> true | Unit -> () + else push_all_as t (Backoff.once backoff) values mono + | Cons cons_r as old_head -> + if cons_r.capacity + len > t.capacity then + match mono with Bool -> false | Unit -> raise Full + else if + Atomic.compare_and_set t.head old_head + @@ build_node cons_r.capacity old_head values + then match mono with Bool -> true | Unit -> () + else push_all_as t (Backoff.once backoff) values mono + +let try_push_all t values = push_all_as t Backoff.default values Bool +let push_all_exn t values = push_all_as t Backoff.default values Unit +let add_seq_exn t seq = push_all_as t Backoff.default (List.of_seq seq) Unit +let try_add_seq t seq = push_all_as t Backoff.default (List.of_seq seq) Bool + +(* *) + +type op = Set | Pop + +let try_compare_and_ t old_value new_value op = + let rec aux backoff = + match Atomic.get t.head with + | Nil -> false + | Cons cons_r as old_head -> + if cons_r.value == old_value then + if + Atomic.compare_and_set t.head old_head + @@ + match op with + | Set -> Cons { cons_r with value = new_value } + | Pop -> cons_r.tail + then true + else aux (Backoff.once backoff) + else false + in + aux Backoff.default + +let try_compare_and_pop t value = try_compare_and_ t value value Pop + +let try_compare_and_set t old_value new_value = + try_compare_and_ t old_value new_value Set diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index 5b1f3178..a6b3823e 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -1,4 +1,11 @@ -(** Lock-free bounded stack. *) +(** Lock-free bounded stack. + + This module implements a lock-free bounded stack based on Treiber's stack + algorithm. Adding a capacity to this algorithm adds a general overhead to the + operations, and thus, it is recommended to use the unbounded stack + {!Saturn_lockfree.Stack} if neither the capacity nor the {!length} function + is needed. +*) (** {1 API} *) @@ -7,9 +14,12 @@ type 'a t val create : ?capacity:int -> unit -> 'a t (** [create ~capacity ()] creates a new empty bounded stack with a maximum -capacity of [capacity]. Default [capacity] value is [Int.max_int]. +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 Treiber stack from a list. *) + val length : 'a t -> int (** [length stack] returns the number of elements currently in the [stack]. *) @@ -17,97 +27,201 @@ val is_empty : 'a t -> bool (** [is_empty stack] returns [true] if the [stack] is empty, otherwise [false]. *) (** {2 Consumer functions} *) -val peek : 'a t -> 'a -(** [peek stack] returns the top element of the [stack] without removing it. If -the stack is empty, the domain will be suspended until another domain successfully -push another element in the stack with [push] or [push_opt] . *) + +exception Empty +(** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty + stack. + + This exception is meant to avoid allocations required by an option type. + As such, it does not register backtrace information, and it is recommended to + use the following pattern to catch it. + + {@ocaml skip[ + match pop_exn s with + | value -> () (* ... *) + | exception Empty -> () (* ... *) + ]} *) + +val peek_exn : 'a t -> 'a +(** [peek_exn stack] returns the top element of the [stack] without removing it. + + @raises Empty if the [stack] is empty. *) val peek_opt : 'a t -> 'a option (** [peek_opt stack] returns [Some] of the top element of the [stack] without - removing it, or [None] if the stack is empty. *) + removing it, or [None] if the [stack] is empty. *) -val pop : 'a t -> 'a -(** [pop stack] removes and returns the top element of the [stack]. - Raises an exception if the stack is empty. *) +val pop_exn : 'a t -> 'a +(** [pop_exn stack] removes and returns the top element of the [stack]. + + @raises Empty if the [stack] is empty. *) val pop_opt : 'a t -> 'a option (** [pop_opt stack] removes and returns [Some] of the top element of the [stack], - or [None] if the stack is empty. *) + or [None] if the [stack] is empty. *) + +val drop_exn : 'a t -> unit +(** [drop_exn stack] removes the top element of the [stack]. + + @raises Empty if the [stack] 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. *) val pop_all : 'a t -> 'a list -(** [pop_all stack] removes and returns all elements of the [stack] in the reverse -order they were pushed. *) +(** [pop_all stack] removes and returns all elements of the [stack] in LIFO +order. + + {[ + # open Saturn_lockfree.Bounded_stack + # let t : int t = create () + val t : int t = + # try_push t 1 + - : bool = true + # try_push t 2 + - : bool = true + # try_push t 3 + - : bool = true + # pop_all t + - : int list = [3; 2; 1] + ]} +*) (** {2 Producer functions} *) -val push : 'a t -> 'a -> unit -(** [push stack element] adds [element] to the top of the [stack]. - Raises an exception if the stack is full. *) +exception Full +(** Raised when {!push_exn} or {!push_all_exn} is applied to a full stack. *) + +val push_exn : 'a t -> 'a -> unit +(** [push_exn stack element] adds [element] to the top of the [stack]. + + @raises Full if the [stack] is full. *) val try_push : 'a t -> 'a -> bool (** [try_push stack element] tries to add [element] to the top of the [stack]. Returns [true] if the element was successfully added, or [false] if the stack is full. *) +val push_all_exn : 'a t -> 'a list -> unit +(** [push_all_exn stack elements] adds all [elements] to the top of the [stack]. + + @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} *) + +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. *) + (** {1 Examples} An example top-level session: {[ - # let t : int Saturn.Bounded_stack.t = - Saturn.Bounded_stack.create () - val t : int Saturn.Bounded_stack.t = - # Saturn.Bounded_stack.try_push t 42 + # open Saturn_lockfree.Bounded_stack + # let t : int t = create () + val t : int t = + # try_push t 42 - : bool = true - # Saturn.Bounded_stack.push t 1 + # push_exn t 1 - : unit = () - # Saturn.Bounded_stack.pop t + # pop_exn t - : int = 1 - # Saturn.Bounded_stack.peek_opt t + # peek_opt t - : int option = Some 42 - # Saturn.Bounded_stack.pop_opt t - - : int option = Some 42 - # Saturn.Bounded_stack.pop_opt t - - : int option = None ]} + # pop_opt t + - : int option = Some 42 + # pop_opt t + - : int option = None + # pop_exn t + Exception: Saturn_lockfree__Bounded_stack.Empty.]} A multicore example: - {[ - open Saturn_lockfree - open Picos_std_structured - - let main () = - let st = Bounded_stack.create ~capacity:2 () in - let popped = Bounded_stack.create ~capacity:Int.max_int () in - Flock.join_after - begin - fun () -> - for i = 0 to 2 lsl 5 - 1 do - Flock.fork @@ fun () -> - begin - if i/4 mod 2 = 0 then (* 4 pushes followed by 4 pops *) - let id = (Domain.self () :> int) in - Bounded_stack.push st id - else Bounded_stack.pop st |> Bounded_stack.push popped - (* stores the result of pop in popped *) - end; - Unix.sleepf (Random.float 0.1) - done - end; - assert (Bounded_stack.pop_all st = []); - Bounded_stack.pop_all popped |> List.rev - - let run () = - Picos_mux_multififo.run_on ~n_domains:4 main - ]} - This example uses Picos' prefined {{:https://ocaml-multicore.github.io/picos/doc/picos_mux/Picos_mux_multififo/index.html}multi-threaded scheduler} - to run four domains that are alternatively pushing their ids and popping in - a shared stack with a capacity of 2 elements. The returned list is the - pusher's ids in order. Note that with this scheduler, a maximum of 4 domains - can be used in parallel and each domain can spawn multiple fibers, meaning - even if run in a single domain, this example will not block indefinitely. - - {[ - # run ();; - - : int list = - [5; 4; 6; 6; 4; 5; 4; 0; 6; 5; 6; 4; 0; 5; 4; 5; 0; 5; 6; 5; 5; 0; 5; 4; - 4; 0; 0; 0; 0; 0; 0; 0] - ]} + {@ocaml non-deterministic[ + # open Saturn_lockfree.Bounded_stack + # let t :int t = create () + 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; + + try_push_all t [1;2;3] |> ignore; + push_exn t 42; + push_exn t 12 + val pusher : unit -> unit = + # let popper () = + Atomic.decr barrier; + while Atomic.get barrier != 0 do Domain.cpu_relax () done; + List.init 6 (fun i -> Domain.cpu_relax (); pop_opt t) + val popper : unit -> int option list = + # let domain_pusher = Domain.spawn pusher + val domain_pusher : unit Domain.t = + # let domain_popper = Domain.spawn popper + val domain_popper : int option list Domain.t = + # Domain.join domain_pusher + - : unit = () + # Domain.join domain_popper + - : int option list = [Some 42; Some 3; Some 2; Some 1; None; Some 12] + ]} + *) diff --git a/src/dune b/src/dune index 739869ca..edec87ee 100644 --- a/src/dune +++ b/src/dune @@ -23,6 +23,12 @@ let () = (action (copy domain.ocaml4.ml domain.ml))) +(rule + (enabled_if + (< %{ocaml_version} 4.14.0)) + (action + (copy seq.ocaml4.13.ml seq.ml))) + (rule (enabled_if (< %{ocaml_version} 5.2.0)) @@ -36,5 +42,5 @@ let () = (<> %{os_type} Win32) (>= %{ocaml_version} 5.0.0))) (libraries saturn) - (files treiber_stack.mli)) + (files treiber_stack.mli bounded_stack.mli)) |} diff --git a/src/seq.ocaml4.13.ml b/src/seq.ocaml4.13.ml new file mode 100644 index 00000000..1d29d539 --- /dev/null +++ b/src/seq.ocaml4.13.ml @@ -0,0 +1,6 @@ +include Stdlib.Seq + +let rec length_aux accu xs = + match xs () with Nil -> accu | Cons (_, xs) -> length_aux (accu + 1) xs + +let[@inline] length xs = length_aux 0 xs diff --git a/test/bounded_stack/bounded_stack_dscheck.ml b/test/bounded_stack/bounded_stack_dscheck.ml index fe86ff81..fb16bedd 100644 --- a/test/bounded_stack/bounded_stack_dscheck.ml +++ b/test/bounded_stack/bounded_stack_dscheck.ml @@ -1,14 +1,8 @@ module Stack = Bounded_stack -let drain stack = - let remaining = ref 0 in - while not (Stack.is_empty stack) do - remaining := !remaining + 1; - assert (Option.is_some (Stack.pop_opt stack)) - done; - !remaining - -let producer_consumer () = +let drain stack = Stack.pop_all stack |> List.length + +let push_pop () = Atomic.trace (fun () -> let stack = Stack.create () in let items_total = 4 in @@ -20,21 +14,48 @@ let producer_consumer () = done); (* consumer *) - let popped = ref 0 in + let popped = ref [] in Atomic.spawn (fun () -> for _ = 1 to items_total do match Stack.pop_opt stack with | None -> () - | Some _ -> popped := !popped + 1 + | Some v -> popped := v :: !popped + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack 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 stack = Stack.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Stack.try_push stack i |> ignore + done); + + (* consumer *) + let dropped = ref 0 in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Stack.drop_exn stack with + | () -> dropped := !dropped + 1 + | exception Stack.Empty -> () done); (* checks*) Atomic.final (fun () -> Atomic.check (fun () -> let remaining = drain stack in - !popped + remaining = items_total))) + !dropped + remaining = items_total))) -let producer_consumer_with_capacity () = +let push_pop_with_capacity () = Atomic.trace (fun () -> let stack = Stack.create ~capacity:2 () in let items_total = 4 in @@ -67,7 +88,68 @@ let producer_consumer_with_capacity () = true with _ -> false))) -let two_producers () = +let push_set () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + + Atomic.spawn (fun () -> + for i = 1 to items_total do + Stack.try_push stack i |> ignore + done); + + let set_v = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Stack.set_exn stack 42 with + | v -> set_v := v :: !set_v + | exception Stack.Empty -> () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack in + let all_value = List.sort Int.compare (!set_v @ remaining) in + let all_non_42 = List.filter (( <> ) 42) all_value in + all_non_42 = List.init items_total (fun x -> x + 1) + && List.length remaining = items_total))) + +let pop_set () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let n_items = 4 in + List.iter + (fun i -> Stack.try_push stack i |> ignore) + (List.init n_items Fun.id); + + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to n_items do + match Stack.pop_opt stack with + | None -> () + | Some v -> popped := v :: !popped + done); + + let set_v = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to n_items do + match Stack.set_exn stack 42 with + | v -> set_v := v :: !set_v + | exception Stack.Empty -> () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack in + + List.length (List.filter (fun x -> x = 42) (!popped @ remaining)) + = List.length (List.filter (fun x -> x <> 42) !set_v) + && List.filter (fun x -> x <> 42) (!popped @ remaining @ !set_v) + |> List.sort Int.compare = List.init n_items Fun.id))) + +let push_push () = Atomic.trace (fun () -> let stack = Stack.create () in let items_total = 6 in @@ -94,7 +176,7 @@ let two_producers () = Atomic.check (fun () -> List.sort Int.compare odd = List.rev odd); Atomic.check (fun () -> List.sort Int.compare even = List.rev even))) -let two_producers_with_capacity () = +let push_push_with_capacity () = Atomic.trace (fun () -> let capacity = 3 in let stack = Stack.create ~capacity () in @@ -116,7 +198,7 @@ let two_producers_with_capacity () = (* got the same number of items out as in *) Atomic.check (fun () -> capacity = List.length items))) -let two_consumers () = +let pop_pop () = Atomic.trace (fun () -> let stack = Stack.create () in let items_total = 4 in @@ -149,6 +231,118 @@ let two_consumers () = Atomic.check (fun () -> List.sort Int.compare l1 = l1); Atomic.check (fun () -> List.sort Int.compare l2 = l2))) +let push_cap () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Stack.try_push stack i |> ignore + done); + + (* consumer *) + let popped = ref false in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + if Stack.try_compare_and_pop stack 1 then popped := true else () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack in + let all_pushed = List.init items_total (fun x -> x + 1) in + if !popped then + List.rev remaining = List.filter (( <> ) 1) all_pushed + else List.rev remaining = all_pushed))) + +let pop_cap () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + let pushed = List.init items_total (fun x -> x + 1) in + + List.iter (fun i -> Stack.try_push stack i |> ignore) pushed; + + (* producer *) + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + match Stack.pop_opt stack with + | None -> () + | Some v -> popped := v :: !popped + done); + + (* consumer *) + let capp = ref false in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + if Stack.try_compare_and_pop stack 2 then capp := true else () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack in + let all = !popped @ remaining |> List.sort Int.compare in + if !capp then List.filter (fun x -> x <> 2) pushed = all + else all = pushed))) + +let push_cas () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let items_total = 4 in + + (* producer *) + Atomic.spawn (fun () -> + for i = 1 to items_total do + Stack.try_push stack i |> ignore + done); + + (* consumer *) + let is_set = ref false in + Atomic.spawn (fun () -> + for _ = 1 to items_total do + if Stack.try_compare_and_set stack 1 42 then is_set := true else () + done); + + (* checks*) + Atomic.final (fun () -> + Atomic.check (fun () -> + let remaining = Stack.pop_all stack in + let all_pushed = List.init items_total (fun x -> x + 1) in + if !is_set then + List.rev remaining + = List.map (fun x -> if x = 1 then 42 else x) all_pushed + else List.rev remaining = all_pushed))) + +let pop_push_all () = + Atomic.trace (fun () -> + let stack = Stack.create () in + let n_items = 4 in + let items = List.init n_items (fun x -> x + 1) in + + Atomic.spawn (fun () -> Stack.try_push_all stack items |> ignore); + + let popped = ref [] in + Atomic.spawn (fun () -> + for _ = 1 to n_items do + popped := Stack.pop_opt stack :: !popped + done); + + Atomic.final (fun () -> + let popped = + List.filter Option.is_some !popped |> List.map Option.get + in + (* got the same number of items out as in *) + Atomic.check (fun () -> + popped + = List.filteri + (fun i _ -> i >= n_items - List.length popped) + items))) + let two_domains () = Atomic.trace (fun () -> let stack = Stack.create () in @@ -204,7 +398,7 @@ let two_domains_more_pop () = Atomic.spawn (fun () -> List.iter (fun elt -> - Stack.push stack elt; + Stack.try_push stack elt |> ignore; lpop := Stack.pop_opt stack :: !lpop; lpop := Stack.pop_opt stack :: !lpop) lpush) @@ -231,7 +425,7 @@ let two_domains_more_pop () = List.sort Int.compare (lpop1 @ lpop2) = List.init (n1 + n2) (fun i -> i)))) -let two_domains_pop_all () = +let pop_all () = Atomic.trace (fun () -> let stack = Stack.create () in let n_items = 6 in @@ -256,14 +450,21 @@ let () = [ ( "basic", [ - test_case "1-producer-1-consumer" `Slow producer_consumer; + test_case "1-producer-1-consumer" `Slow push_pop; test_case "1-producer-1-consumer-capacity" `Slow - producer_consumer_with_capacity; - test_case "2-producers" `Slow two_producers; - test_case "2-producers-capacity" `Slow two_producers_with_capacity; - test_case "2-consumers" `Slow two_consumers; + push_pop_with_capacity; + test_case "1-push-1-drop" `Slow push_drop; + test_case "1-push-1-set" `Slow push_set; + test_case "1-pop-1-set" `Slow pop_set; + 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; - test_case "2-domains-pops_all" `Slow two_domains_pop_all; + test_case "2-domains-pops_all" `Slow pop_all; + test_case "1-push-1-compare-and-pop" `Slow push_cap; + test_case "1-pop-1-compare-and-pop" `Slow pop_cap; + test_case "1-push-1-compare-and-set" `Slow push_cas; + test_case "1-pop-1-push-all" `Slow pop_push_all; ] ); ] diff --git a/test/bounded_stack/dune b/test/bounded_stack/dune index 4906625e..52434a9c 100644 --- a/test/bounded_stack/dune +++ b/test/bounded_stack/dune @@ -6,7 +6,7 @@ (test (package saturn_lockfree) (name bounded_stack_dscheck) - (libraries picos atomic dscheck alcotest backoff multicore-magic) + (libraries atomic dscheck alcotest backoff multicore-magic) (build_if (and (>= %{ocaml_version} 5) diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index f1d03e69..15557215 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -7,18 +7,39 @@ module Stack = Saturn_lockfree.Bounded_stack module Spec = struct type cmd = | Try_push of int + (* push_exn uses the same function as try_push *) + | Try_push_all of int list + (* push_all_exn and add_seq_exn and try_add_seq uses the same function as + try_push_all*) | Pop_opt + (* peek_exn and drop_exn use the same function as pop_exn*) | Pop_all | Peek_opt + (* peek_exn uses the same function as peek_exn *) + | Try_compare_and_pop of int + | Try_compare_and_set of int * int + | Set_exn of int + (* try_set uses the same function as set_exn *) + | To_seq | Is_empty | Length + let string_of_int_list l = + "[" ^ String.concat "; " (List.map string_of_int l) ^ "]" + let show_cmd c = match c with | Try_push i -> "Try_push " ^ string_of_int i + | Try_push_all l -> "Try_push_all " ^ string_of_int_list l + (* | Push_all_exn l -> "Push_all_exn " ^ string_of_int_list l *) | Pop_opt -> "Pop_opt" | Pop_all -> "Pop_all" | Peek_opt -> "Peek_opt" + | Try_compare_and_pop i -> "Try_compare_and_pop " ^ string_of_int i + | Try_compare_and_set (i, j) -> + "Try_compare_and_set (" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" + | To_seq -> "To_seq" + | Set_exn i -> "Try_set " ^ string_of_int i | Is_empty -> "Is_empty" | Length -> "Length" @@ -31,12 +52,16 @@ module Spec = struct (Gen.oneof [ Gen.map (fun i -> Try_push i) int_gen; + Gen.map (fun l -> Try_push_all l) (Gen.list int_gen); Gen.return Pop_opt; Gen.return Pop_all; - Gen.return Is_empty; - Gen.return Length; Gen.return Peek_opt; + Gen.map (fun i -> Try_compare_and_pop i) int_gen; + Gen.map2 (fun i j -> Try_compare_and_set (i, j)) int_gen int_gen; + Gen.map (fun i -> Set_exn i) int_gen; + Gen.return To_seq; Gen.return Is_empty; + Gen.return Length; ]) let init_state = [] @@ -47,9 +72,19 @@ module Spec = struct let next_state c s = match c with | Try_push i -> if List.length s >= capacity then s else i :: s + | Try_push_all l -> + if List.length s + List.length l > capacity then s else List.rev l @ s + (* | Push_all_exn l -> + if List.length s + List.length l > capacity then s else List.rev l @ s *) | Pop_opt -> ( match s with [] -> s | _ :: s' -> s') | Pop_all -> [] | Peek_opt -> s + | Try_compare_and_pop i -> ( + match s with [] -> [] | hd :: tl -> if hd = i then tl else s) + | Try_compare_and_set (i, j) -> ( + match s with [] -> [] | hd :: tl -> if hd = i then j :: tl else s) + | Set_exn i -> ( match s with [] -> s | _ :: tl -> i :: tl) + | To_seq -> s | Is_empty -> s | Length -> s @@ -58,20 +93,32 @@ module Spec = struct let run c d = match c with | Try_push i -> Res (bool, Stack.try_push d i) + | Try_push_all l -> Res (bool, Stack.try_push_all d l) | Pop_opt -> Res (option int, Stack.pop_opt d) | Pop_all -> Res (list int, Stack.pop_all d) | Peek_opt -> Res (option int, Stack.peek_opt d) + | Try_compare_and_pop i -> Res (bool, Stack.try_compare_and_pop d i) + | Try_compare_and_set (i, j) -> Res (bool, Stack.try_compare_and_set d i j) + | Set_exn i -> Res (result int exn, protect (fun d -> Stack.set_exn d i) d) + | To_seq -> Res (seq int, Stack.to_seq d) | Is_empty -> Res (bool, Stack.is_empty d) | Length -> Res (int, Stack.length d) let postcond c (s : state) res = match (c, res) with | Try_push _, Res ((Bool, _), res) -> List.length s < capacity = res - | Pop_opt, Res ((Option Int, _), res) -> ( + | Try_push_all l, Res ((Bool, _), res) -> + List.length s + List.length l <= capacity = res + | Try_compare_and_pop i, Res ((Bool, _), res) -> ( + match s with [] -> res = false | hd :: _ -> res = (hd = i)) + | Try_compare_and_set (i, _), Res ((Bool, _), res) -> ( + match s with [] -> res = false | hd :: _ -> res = (hd = i)) + | Set_exn _, Res ((Result (Int, Exn), _), res) -> ( + match s with [] -> res = Error Stack.Empty | x :: _ -> res = Ok x) + | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( match s with [] -> res = None | j :: _ -> res = Some j) | Pop_all, Res ((List Int, _), res) -> res = s - | Peek_opt, Res ((Option Int, _), res) -> ( - match s with [] -> res = None | j :: _ -> res = Some j) + | To_seq, Res ((Seq Int, _), res) -> List.of_seq res = s | Is_empty, Res ((Bool, _), res) -> res = (s = []) | Length, Res ((Int, _), res) -> res = List.length s | _, _ -> false From 97d5b1d4da4fb8f6a7c4eae23a089df8931b6931 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 5 Nov 2024 17:44:21 +0100 Subject: [PATCH 03/11] Merge with PR that removes saturn_lockfree package. --- bench/bench_bounded_stack.ml | 2 +- bench/main.ml | 2 +- src/bounded_stack.mli | 10 +++++----- test/bounded_stack/dune | 10 +++++----- test/bounded_stack/stm_bounded_stack.ml | 4 ++-- test/skiplist/stm_skiplist.ml | 2 +- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/bench/bench_bounded_stack.ml b/bench/bench_bounded_stack.ml index 8e8ee045..2dc2b495 100644 --- a/bench/bench_bounded_stack.ml +++ b/bench/bench_bounded_stack.ml @@ -1,5 +1,5 @@ open Multicore_bench -module Stack = Saturn_lockfree.Bounded_stack +module Stack = Saturn.Bounded_stack let run_one_domain ~budgetf ?(n_msgs = 50 * Util.iter_factor) () = let t = Stack.create () in diff --git a/bench/main.ml b/bench/main.ml index 43e6df78..1c9fefb8 100644 --- a/bench/main.ml +++ b/bench/main.ml @@ -7,7 +7,7 @@ let benchmarks = ("Saturn Htbl", Bench_htbl.run_suite); ("Saturn Stack", Bench_stack.run_suite); ("Saturn Work_stealing_deque", Bench_ws_deque.run_suite); - ("Saturn_lockfree Bounded_Stack", Bench_bounded_stack.run_suite); + ("Saturn Bounded_Stack", Bench_bounded_stack.run_suite); ] let () = Multicore_bench.Cmd.run ~benchmarks () diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index a6b3823e..405f0420 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -3,7 +3,7 @@ This module implements a lock-free bounded stack based on Treiber's stack algorithm. Adding a capacity to this algorithm adds a general overhead to the operations, and thus, it is recommended to use the unbounded stack - {!Saturn_lockfree.Stack} if neither the capacity nor the {!length} function + {!Saturn.Stack} if neither the capacity nor the {!length} function is needed. *) @@ -77,7 +77,7 @@ val pop_all : 'a t -> 'a list order. {[ - # open Saturn_lockfree.Bounded_stack + # open Saturn.Bounded_stack # let t : int t = create () val t : int t = # try_push t 1 @@ -176,7 +176,7 @@ the [seq] is too long to fit in the stack. *) (** {1 Examples} An example top-level session: {[ - # open Saturn_lockfree.Bounded_stack + # open Saturn.Bounded_stack # let t : int t = create () val t : int t = # try_push t 42 @@ -192,11 +192,11 @@ the [seq] is too long to fit in the stack. *) # pop_opt t - : int option = None # pop_exn t - Exception: Saturn_lockfree__Bounded_stack.Empty.]} + Exception: Saturn__Bounded_stack.Empty.]} A multicore example: {@ocaml non-deterministic[ - # open Saturn_lockfree.Bounded_stack + # open Saturn.Bounded_stack # let t :int t = create () val t : int t = # let barrier = Atomic.make 2 diff --git a/test/bounded_stack/dune b/test/bounded_stack/dune index 52434a9c..6e291ec1 100644 --- a/test/bounded_stack/dune +++ b/test/bounded_stack/dune @@ -1,10 +1,10 @@ (rule (action - (copy ../../src_lockfree/bounded_stack.ml bounded_stack.ml)) - (package saturn_lockfree)) + (copy ../../src/bounded_stack.ml bounded_stack.ml)) + (package saturn)) (test - (package saturn_lockfree) + (package saturn) (name bounded_stack_dscheck) (libraries atomic dscheck alcotest backoff multicore-magic) (build_if @@ -17,7 +17,7 @@ (modules bounded_stack bounded_stack_dscheck)) (test - (package saturn_lockfree) + (package saturn) (name stm_bounded_stack) (modules stm_bounded_stack) - (libraries saturn_lockfree qcheck-core qcheck-stm.stm stm_run)) + (libraries saturn qcheck-core qcheck-stm.stm stm_run)) diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index 15557215..18b39c97 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -2,7 +2,7 @@ open QCheck open STM -module Stack = Saturn_lockfree.Bounded_stack +module Stack = Saturn.Bounded_stack module Spec = struct type cmd = @@ -124,4 +124,4 @@ module Spec = struct | _, _ -> false end -let () = Stm_run.run ~name:"Saturn_lockfree.Bounded_stack" (module Spec) |> exit +let () = Stm_run.run ~name:"Saturn.Bounded_stack" (module Spec) |> exit diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml index 0ada005b..1cfeba4a 100644 --- a/test/skiplist/stm_skiplist.ml +++ b/test/skiplist/stm_skiplist.ml @@ -64,4 +64,4 @@ module Spec = struct | _, _ -> false end -let () = Stm_run.run ~name:"Lockfree.Skiplist" (module Spec) |> exit +let () = Stm_run.run ~name:"Saturn.Skiplist" (module Spec) |> exit From cfece1f274f6390e272b01fe8e05a37f2498fce3 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 12 Nov 2024 20:34:26 +0100 Subject: [PATCH 04/11] Applied reviews. --- src/bounded_stack.ml | 125 ++++++++---------------- src/bounded_stack.mli | 4 + test/bounded_stack/stm_bounded_stack.ml | 4 +- 3 files changed, 48 insertions(+), 85 deletions(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 3b932a09..20d47283 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -1,15 +1,13 @@ -type 'a node = Nil | Cons of { value : 'a; tail : 'a node; capacity : int } -type 'a t = { head : 'a node Atomic.t; capacity : int } +type 'a t = { head : (int * 'a list) Atomic.t; capacity : int } (* *) let create ?(capacity = Int.max_int) () = - let head = Atomic.make_contended Nil in + let head = Atomic.make_contended (0, []) in { head; capacity = max capacity 1 } |> Multicore_magic.copy_as_padded -let length t = - match Atomic.get t.head with Nil -> 0 | Cons cons -> cons.capacity - -let is_empty t = Atomic.get t.head = Nil +let length t = fst (Atomic.get t.head) +let is_full t = t.capacity = length t +let is_empty t = Atomic.get t.head = (0, []) exception Empty exception Full @@ -17,25 +15,14 @@ exception Full let of_list ?(capacity = Int.max_int) list = if capacity < List.length list then raise Full else - let head = - List.fold_left - (fun (len, acc) elt -> - (len + 1, Cons { value = elt; tail = acc; capacity = len })) - (1, Nil) list - |> snd |> Atomic.make_contended - in + let head = Atomic.make_contended (List.length list, List.rev list) in { head; capacity } |> Multicore_magic.copy_as_padded let of_seq ?(capacity = Int.max_int) seq = if capacity < Seq.length seq then raise Full else - let head = - Seq.fold_left - (fun (len, acc) elt -> - (len + 1, Cons { value = elt; tail = acc; capacity = len })) - (1, Nil) seq - |> snd |> Atomic.make_contended - in + let list = List.of_seq seq in + let head = Atomic.make_contended (List.length list, List.rev list) in { head; capacity } |> Multicore_magic.copy_as_padded (* *) @@ -45,11 +32,10 @@ type ('a, _) poly1 = Option : ('a, 'a option) poly1 | Value : ('a, 'a) poly1 let peek_as : type a r. a t -> (a, r) poly1 -> r = fun t poly -> match Atomic.get t.head with - | Nil -> begin + | _, [] -> begin match poly with Option -> None | Value -> raise_notrace Empty end - | Cons cons_r -> ( - match poly with Option -> Some cons_r.value | Value -> cons_r.value) + | _, value :: _ -> ( match poly with Option -> Some value | Value -> value) let peek_exn t = peek_as t Value let peek_opt t = peek_as t Option @@ -63,18 +49,15 @@ type ('a, _) poly2 = let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = fun t backoff poly -> match Atomic.get t.head with - | Nil -> begin + | _, [] -> begin match poly with | Option -> None | Value -> raise_notrace Empty | Unit -> raise_notrace Empty end - | Cons cons_r as old_head -> - if Atomic.compare_and_set t.head old_head cons_r.tail then - match poly with - | Option -> Some cons_r.value - | Value -> cons_r.value - | Unit -> () + | (len, hd :: tl) as old_head -> + if Atomic.compare_and_set t.head old_head (len - 1, tl) then + match poly with Option -> Some hd | Value -> hd | Unit -> () else pop_as t (Backoff.once backoff) poly let pop_exn t = pop_as t Backoff.default Value @@ -83,29 +66,17 @@ let drop_exn t = pop_as t Backoff.default Unit let rec pop_all t backoff = match Atomic.get t.head with - | Nil -> [] - | old_head -> - if Atomic.compare_and_set t.head old_head Nil then - let[@tail_mod_cons] rec aux = function - | Nil -> [] - | Cons cons -> cons.value :: aux cons.tail - in - aux old_head + | _, [] -> [] + | (_, values) as old_head -> + if Atomic.compare_and_set t.head old_head (0, []) then values else pop_all t (Backoff.once backoff) let pop_all t = pop_all t Backoff.default let to_seq t = match Atomic.get t.head with - | Nil -> Seq.empty - | old_head -> - let rec aux s () = - match s with - | Nil -> Seq.Nil - | Cons cons -> Seq.Cons (cons.value, aux cons.tail) - in - aux old_head - + | _, [] -> Seq.empty + | _, values -> List.to_seq values (* *) type _ mono = Unit : unit mono | Bool : bool mono @@ -113,19 +84,16 @@ type _ mono = Unit : unit mono | Bool : bool mono let rec push_as : type r. 'a t -> Backoff.t -> 'a -> r mono -> r = fun t backoff value mono -> match Atomic.get t.head with - | Nil -> - if - Atomic.compare_and_set t.head Nil - @@ Cons { value; tail = Nil; capacity = 1 } - then match mono with Bool -> true | Unit -> () + | (_, []) as old_head -> + if Atomic.compare_and_set t.head old_head @@ (1, [ value ]) then + match mono with Bool -> true | Unit -> () else push_as t (Backoff.once backoff) value mono - | Cons cons_r as old_head -> - if cons_r.capacity >= t.capacity then + | (len, values) as old_head -> + if len >= t.capacity then match mono with Bool -> false | Unit -> raise Full else - let new_head = - Cons { value; tail = old_head; capacity = cons_r.capacity + 1 } - in + let new_head = (len + 1, value :: values) in + if Atomic.compare_and_set t.head old_head new_head then match mono with Bool -> true | Unit -> () else push_as t (Backoff.once backoff) value mono @@ -138,10 +106,10 @@ type ('a, _) poly3 = Value : ('a, 'a) poly3 | Bool : ('a, bool) poly3 let rec set_as : type v r. v t -> v -> Backoff.t -> (v, r) poly3 -> r = fun t value backoff poly -> match Atomic.get t.head with - | Nil -> ( match poly with Value -> raise_notrace Empty | Bool -> false) - | Cons cons_r as old_head -> - if Atomic.compare_and_set t.head old_head @@ Cons { cons_r with value } - then match poly with Value -> cons_r.value | Bool -> true + | _, [] -> ( match poly with Value -> raise_notrace Empty | Bool -> false) + | (len, hd :: tl) as old_head -> + if Atomic.compare_and_set t.head old_head @@ (len, value :: tl) then + match poly with Value -> hd | Bool -> true else set_as t value (Backoff.once backoff) poly let set_exn t value = set_as t value Backoff.default Value @@ -154,29 +122,22 @@ let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r = else if len > t.capacity then match mono with Unit -> raise Full | Bool -> false else - let rec build_node len acc = function - | [] -> acc - | x :: xs -> - build_node (len + 1) - (Cons { capacity = len + 1; tail = acc; value = x }) - xs - in match Atomic.get t.head with - | Nil -> - if Atomic.compare_and_set t.head Nil (build_node 0 Nil values) then - match mono with Bool -> true | Unit -> () + | (_, []) as old_head -> + if Atomic.compare_and_set t.head old_head (List.length values, values) + then match mono with Bool -> true | Unit -> () else push_all_as t (Backoff.once backoff) values mono - | Cons cons_r as old_head -> - if cons_r.capacity + len > t.capacity then + | (curr_len, prev_values) as old_head -> + if curr_len + len > t.capacity then match mono with Bool -> false | Unit -> raise Full else if Atomic.compare_and_set t.head old_head - @@ build_node cons_r.capacity old_head values + (curr_len + len, values @ prev_values) then match mono with Bool -> true | Unit -> () else push_all_as t (Backoff.once backoff) values mono -let try_push_all t values = push_all_as t Backoff.default values Bool -let push_all_exn t values = push_all_as t Backoff.default values Unit +let try_push_all t values = push_all_as t Backoff.default (List.rev values) Bool +let push_all_exn t values = push_all_as t Backoff.default (List.rev values) Unit let add_seq_exn t seq = push_all_as t Backoff.default (List.of_seq seq) Unit let try_add_seq t seq = push_all_as t Backoff.default (List.of_seq seq) Bool @@ -187,15 +148,13 @@ type op = Set | Pop let try_compare_and_ t old_value new_value op = let rec aux backoff = match Atomic.get t.head with - | Nil -> false - | Cons cons_r as old_head -> - if cons_r.value == old_value then + | _, [] -> false + | (len, hd :: tl) as old_head -> + if hd == old_value then if Atomic.compare_and_set t.head old_head @@ - match op with - | Set -> Cons { cons_r with value = new_value } - | Pop -> cons_r.tail + match op with Set -> (len, new_value :: tl) | Pop -> (len - 1, tl) then true else aux (Backoff.once backoff) else false diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index 405f0420..07cec319 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -26,6 +26,10 @@ val length : 'a t -> int val is_empty : 'a t -> bool (** [is_empty stack] returns [true] if the [stack] is empty, otherwise [false]. *) +val is_full : 'a t -> bool +(** [is_full stack] returns [true] if the [stack] has reached capacity, + otherwise [false]. *) + (** {2 Consumer functions} *) exception Empty diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index 18b39c97..52a4b1f8 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -109,14 +109,14 @@ module Spec = struct | Try_push _, Res ((Bool, _), res) -> List.length s < capacity = res | Try_push_all l, Res ((Bool, _), res) -> List.length s + List.length l <= capacity = res + | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( + match s with [] -> res = None | j :: _ -> res = Some j) | Try_compare_and_pop i, Res ((Bool, _), res) -> ( match s with [] -> res = false | hd :: _ -> res = (hd = i)) | Try_compare_and_set (i, _), Res ((Bool, _), res) -> ( match s with [] -> res = false | hd :: _ -> res = (hd = i)) | Set_exn _, Res ((Result (Int, Exn), _), res) -> ( match s with [] -> res = Error Stack.Empty | x :: _ -> res = Ok x) - | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( - match s with [] -> res = None | j :: _ -> res = Some j) | Pop_all, Res ((List Int, _), res) -> res = s | To_seq, Res ((Seq Int, _), res) -> List.of_seq res = s | Is_empty, Res ((Bool, _), res) -> res = (s = []) From abf658419b91fe440ac7b8f65d36caf3c3f3824a Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Tue, 12 Nov 2024 20:54:40 +0100 Subject: [PATCH 05/11] Remove raise_notrace. --- src/bounded_stack.ml | 10 ++++------ src/bounded_stack.mli | 12 +----------- 2 files changed, 5 insertions(+), 17 deletions(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 20d47283..cd6458ce 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -32,9 +32,7 @@ type ('a, _) poly1 = Option : ('a, 'a option) poly1 | Value : ('a, 'a) poly1 let peek_as : type a r. a t -> (a, r) poly1 -> r = fun t poly -> match Atomic.get t.head with - | _, [] -> begin - match poly with Option -> None | Value -> raise_notrace Empty - end + | _, [] -> begin match poly with Option -> None | Value -> raise Empty end | _, value :: _ -> ( match poly with Option -> Some value | Value -> value) let peek_exn t = peek_as t Value @@ -52,8 +50,8 @@ let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly2 -> r = | _, [] -> begin match poly with | Option -> None - | Value -> raise_notrace Empty - | Unit -> raise_notrace Empty + | Value -> raise Empty + | Unit -> raise Empty end | (len, hd :: tl) as old_head -> if Atomic.compare_and_set t.head old_head (len - 1, tl) then @@ -106,7 +104,7 @@ type ('a, _) poly3 = Value : ('a, 'a) poly3 | Bool : ('a, bool) poly3 let rec set_as : type v r. v t -> v -> Backoff.t -> (v, r) poly3 -> r = fun t value backoff poly -> match Atomic.get t.head with - | _, [] -> ( match poly with Value -> raise_notrace Empty | Bool -> false) + | _, [] -> ( match poly with Value -> raise Empty | Bool -> false) | (len, hd :: tl) as old_head -> if Atomic.compare_and_set t.head old_head @@ (len, value :: tl) then match poly with Value -> hd | Bool -> true diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index 07cec319..bd1e9ac7 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -34,17 +34,7 @@ val is_full : 'a t -> bool exception Empty (** Raised when {!pop_exn}, {!peek_exn}, or {!drop_exn} is applied to an empty - stack. - - This exception is meant to avoid allocations required by an option type. - As such, it does not register backtrace information, and it is recommended to - use the following pattern to catch it. - - {@ocaml skip[ - match pop_exn s with - | value -> () (* ... *) - | exception Empty -> () (* ... *) - ]} *) + stack. *) val peek_exn : 'a t -> 'a (** [peek_exn stack] returns the top element of the [stack] without removing it. From 8cacdaac42783cb4a2f25bcae44ab3242c6892f2 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 10:55:27 +0100 Subject: [PATCH 06/11] Remove compare_and_set, compare_and_op and set functions. --- src/bounded_stack.ml | 39 ----- src/bounded_stack.mli | 29 ---- test/bounded_stack/bounded_stack_dscheck.ml | 153 -------------------- test/bounded_stack/stm_bounded_stack.ml | 25 ---- 4 files changed, 246 deletions(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index cd6458ce..5d79770c 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -99,20 +99,6 @@ let rec push_as : type r. 'a t -> Backoff.t -> 'a -> r mono -> r = let push_exn t value = push_as t Backoff.default value Unit let try_push t value = push_as t Backoff.default value Bool -type ('a, _) poly3 = Value : ('a, 'a) poly3 | Bool : ('a, bool) poly3 - -let rec set_as : type v r. v t -> v -> Backoff.t -> (v, r) poly3 -> r = - fun t value backoff poly -> - match Atomic.get t.head with - | _, [] -> ( match poly with Value -> raise Empty | Bool -> false) - | (len, hd :: tl) as old_head -> - if Atomic.compare_and_set t.head old_head @@ (len, value :: tl) then - match poly with Value -> hd | Bool -> true - else set_as t value (Backoff.once backoff) poly - -let set_exn t value = set_as t value Backoff.default Value -let try_set t value = set_as t value Backoff.default Bool - let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r = fun t backoff values mono -> let len = List.length values in @@ -138,28 +124,3 @@ let try_push_all t values = push_all_as t Backoff.default (List.rev values) Bool let push_all_exn t values = push_all_as t Backoff.default (List.rev values) Unit let add_seq_exn t seq = push_all_as t Backoff.default (List.of_seq seq) Unit let try_add_seq t seq = push_all_as t Backoff.default (List.of_seq seq) Bool - -(* *) - -type op = Set | Pop - -let try_compare_and_ t old_value new_value op = - let rec aux backoff = - match Atomic.get t.head with - | _, [] -> false - | (len, hd :: tl) as old_head -> - if hd == old_value then - if - Atomic.compare_and_set t.head old_head - @@ - match op with Set -> (len, new_value :: tl) | Pop -> (len - 1, tl) - then true - else aux (Backoff.once backoff) - else false - in - aux Backoff.default - -let try_compare_and_pop t value = try_compare_and_ t value value Pop - -let try_compare_and_set t old_value new_value = - try_compare_and_ t old_value new_value Set diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index bd1e9ac7..9b253213 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -59,13 +59,6 @@ val drop_exn : 'a t -> unit @raises Empty if the [stack] 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. *) - val pop_all : 'a t -> 'a list (** [pop_all stack] removes and returns all elements of the [stack] in LIFO order. @@ -124,28 +117,6 @@ val try_push_all : 'a t -> 'a list -> bool ]} *) -(** {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 diff --git a/test/bounded_stack/bounded_stack_dscheck.ml b/test/bounded_stack/bounded_stack_dscheck.ml index fb16bedd..06c7dfb4 100644 --- a/test/bounded_stack/bounded_stack_dscheck.ml +++ b/test/bounded_stack/bounded_stack_dscheck.ml @@ -88,67 +88,6 @@ let push_pop_with_capacity () = true with _ -> false))) -let push_set () = - Atomic.trace (fun () -> - let stack = Stack.create () in - let items_total = 4 in - - Atomic.spawn (fun () -> - for i = 1 to items_total do - Stack.try_push stack i |> ignore - done); - - let set_v = ref [] in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - match Stack.set_exn stack 42 with - | v -> set_v := v :: !set_v - | exception Stack.Empty -> () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = Stack.pop_all stack in - let all_value = List.sort Int.compare (!set_v @ remaining) in - let all_non_42 = List.filter (( <> ) 42) all_value in - all_non_42 = List.init items_total (fun x -> x + 1) - && List.length remaining = items_total))) - -let pop_set () = - Atomic.trace (fun () -> - let stack = Stack.create () in - let n_items = 4 in - List.iter - (fun i -> Stack.try_push stack i |> ignore) - (List.init n_items Fun.id); - - let popped = ref [] in - Atomic.spawn (fun () -> - for _ = 1 to n_items do - match Stack.pop_opt stack with - | None -> () - | Some v -> popped := v :: !popped - done); - - let set_v = ref [] in - Atomic.spawn (fun () -> - for _ = 1 to n_items do - match Stack.set_exn stack 42 with - | v -> set_v := v :: !set_v - | exception Stack.Empty -> () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = Stack.pop_all stack in - - List.length (List.filter (fun x -> x = 42) (!popped @ remaining)) - = List.length (List.filter (fun x -> x <> 42) !set_v) - && List.filter (fun x -> x <> 42) (!popped @ remaining @ !set_v) - |> List.sort Int.compare = List.init n_items Fun.id))) - let push_push () = Atomic.trace (fun () -> let stack = Stack.create () in @@ -231,93 +170,6 @@ let pop_pop () = Atomic.check (fun () -> List.sort Int.compare l1 = l1); Atomic.check (fun () -> List.sort Int.compare l2 = l2))) -let push_cap () = - Atomic.trace (fun () -> - let stack = Stack.create () in - let items_total = 4 in - - (* producer *) - Atomic.spawn (fun () -> - for i = 1 to items_total do - Stack.try_push stack i |> ignore - done); - - (* consumer *) - let popped = ref false in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - if Stack.try_compare_and_pop stack 1 then popped := true else () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = Stack.pop_all stack in - let all_pushed = List.init items_total (fun x -> x + 1) in - if !popped then - List.rev remaining = List.filter (( <> ) 1) all_pushed - else List.rev remaining = all_pushed))) - -let pop_cap () = - Atomic.trace (fun () -> - let stack = Stack.create () in - let items_total = 4 in - let pushed = List.init items_total (fun x -> x + 1) in - - List.iter (fun i -> Stack.try_push stack i |> ignore) pushed; - - (* producer *) - let popped = ref [] in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - match Stack.pop_opt stack with - | None -> () - | Some v -> popped := v :: !popped - done); - - (* consumer *) - let capp = ref false in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - if Stack.try_compare_and_pop stack 2 then capp := true else () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = Stack.pop_all stack in - let all = !popped @ remaining |> List.sort Int.compare in - if !capp then List.filter (fun x -> x <> 2) pushed = all - else all = pushed))) - -let push_cas () = - Atomic.trace (fun () -> - let stack = Stack.create () in - let items_total = 4 in - - (* producer *) - Atomic.spawn (fun () -> - for i = 1 to items_total do - Stack.try_push stack i |> ignore - done); - - (* consumer *) - let is_set = ref false in - Atomic.spawn (fun () -> - for _ = 1 to items_total do - if Stack.try_compare_and_set stack 1 42 then is_set := true else () - done); - - (* checks*) - Atomic.final (fun () -> - Atomic.check (fun () -> - let remaining = Stack.pop_all stack in - let all_pushed = List.init items_total (fun x -> x + 1) in - if !is_set then - List.rev remaining - = List.map (fun x -> if x = 1 then 42 else x) all_pushed - else List.rev remaining = all_pushed))) - let pop_push_all () = Atomic.trace (fun () -> let stack = Stack.create () in @@ -454,17 +306,12 @@ let () = test_case "1-producer-1-consumer-capacity" `Slow push_pop_with_capacity; test_case "1-push-1-drop" `Slow push_drop; - test_case "1-push-1-set" `Slow push_set; - test_case "1-pop-1-set" `Slow pop_set; 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; test_case "2-domains-pops_all" `Slow pop_all; - test_case "1-push-1-compare-and-pop" `Slow push_cap; - test_case "1-pop-1-compare-and-pop" `Slow pop_cap; - test_case "1-push-1-compare-and-set" `Slow push_cas; test_case "1-pop-1-push-all" `Slow pop_push_all; ] ); ] diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index 52a4b1f8..59f08f30 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -16,10 +16,6 @@ module Spec = struct | Pop_all | Peek_opt (* peek_exn uses the same function as peek_exn *) - | Try_compare_and_pop of int - | Try_compare_and_set of int * int - | Set_exn of int - (* try_set uses the same function as set_exn *) | To_seq | Is_empty | Length @@ -35,11 +31,7 @@ module Spec = struct | Pop_opt -> "Pop_opt" | Pop_all -> "Pop_all" | Peek_opt -> "Peek_opt" - | Try_compare_and_pop i -> "Try_compare_and_pop " ^ string_of_int i - | Try_compare_and_set (i, j) -> - "Try_compare_and_set (" ^ string_of_int i ^ ", " ^ string_of_int j ^ ")" | To_seq -> "To_seq" - | Set_exn i -> "Try_set " ^ string_of_int i | Is_empty -> "Is_empty" | Length -> "Length" @@ -56,9 +48,6 @@ module Spec = struct Gen.return Pop_opt; Gen.return Pop_all; Gen.return Peek_opt; - Gen.map (fun i -> Try_compare_and_pop i) int_gen; - Gen.map2 (fun i j -> Try_compare_and_set (i, j)) int_gen int_gen; - Gen.map (fun i -> Set_exn i) int_gen; Gen.return To_seq; Gen.return Is_empty; Gen.return Length; @@ -79,11 +68,6 @@ module Spec = struct | Pop_opt -> ( match s with [] -> s | _ :: s' -> s') | Pop_all -> [] | Peek_opt -> s - | Try_compare_and_pop i -> ( - match s with [] -> [] | hd :: tl -> if hd = i then tl else s) - | Try_compare_and_set (i, j) -> ( - match s with [] -> [] | hd :: tl -> if hd = i then j :: tl else s) - | Set_exn i -> ( match s with [] -> s | _ :: tl -> i :: tl) | To_seq -> s | Is_empty -> s | Length -> s @@ -97,9 +81,6 @@ module Spec = struct | Pop_opt -> Res (option int, Stack.pop_opt d) | Pop_all -> Res (list int, Stack.pop_all d) | Peek_opt -> Res (option int, Stack.peek_opt d) - | Try_compare_and_pop i -> Res (bool, Stack.try_compare_and_pop d i) - | Try_compare_and_set (i, j) -> Res (bool, Stack.try_compare_and_set d i j) - | Set_exn i -> Res (result int exn, protect (fun d -> Stack.set_exn d i) d) | To_seq -> Res (seq int, Stack.to_seq d) | Is_empty -> Res (bool, Stack.is_empty d) | Length -> Res (int, Stack.length d) @@ -111,12 +92,6 @@ module Spec = struct List.length s + List.length l <= capacity = res | (Pop_opt | Peek_opt), Res ((Option Int, _), res) -> ( match s with [] -> res = None | j :: _ -> res = Some j) - | Try_compare_and_pop i, Res ((Bool, _), res) -> ( - match s with [] -> res = false | hd :: _ -> res = (hd = i)) - | Try_compare_and_set (i, _), Res ((Bool, _), res) -> ( - match s with [] -> res = false | hd :: _ -> res = (hd = i)) - | Set_exn _, Res ((Result (Int, Exn), _), res) -> ( - match s with [] -> res = Error Stack.Empty | x :: _ -> res = Ok x) | Pop_all, Res ((List Int, _), res) -> res = s | To_seq, Res ((Seq Int, _), res) -> List.of_seq res = s | Is_empty, Res ((Bool, _), res) -> res = (s = []) From 65febc28057d08a9fedc8110af3ea5bca09c71d2 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 10:58:56 +0100 Subject: [PATCH 07/11] Missing raised exception in documentation. --- src/bounded_stack.mli | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/bounded_stack.mli b/src/bounded_stack.mli index 9b253213..5b79d3db 100644 --- a/src/bounded_stack.mli +++ b/src/bounded_stack.mli @@ -18,7 +18,10 @@ 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 Treiber stack from a list. *) +(** [of_list list] creates a new Treiber stack from a list. + + @raises Full if the [list] is longer than the capacity of the stack. +*) val length : 'a t -> int (** [length stack] returns the number of elements currently in the [stack]. *) @@ -125,7 +128,10 @@ 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. *) +(** [of_seq seq] creates a stack from a [seq]. It must be finite. + + @raises Full if the [list] is longer than the capacity of the stack. +*) 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 From 8bbcfe60ff66acd525be50333597d5e159463c3e Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 16:54:23 +0100 Subject: [PATCH 08/11] Apply reviews. --- src/bounded_stack.ml | 41 +++++++++++++++-------------------------- 1 file changed, 15 insertions(+), 26 deletions(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 5d79770c..62544389 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -81,20 +81,14 @@ type _ mono = Unit : unit mono | Bool : bool mono let rec push_as : type r. 'a t -> Backoff.t -> 'a -> r mono -> r = fun t backoff value mono -> - match Atomic.get t.head with - | (_, []) as old_head -> - if Atomic.compare_and_set t.head old_head @@ (1, [ value ]) then - match mono with Bool -> true | Unit -> () - else push_as t (Backoff.once backoff) value mono - | (len, values) as old_head -> - if len >= t.capacity then - match mono with Bool -> false | Unit -> raise Full - else - let new_head = (len + 1, value :: values) in + let ((len, values) as before) = Atomic.get t.head in + if len >= t.capacity then match mono with Bool -> false | Unit -> raise Full + else + let after = (len + 1, value :: values) in - if Atomic.compare_and_set t.head old_head new_head then - match mono with Bool -> true | Unit -> () - else push_as t (Backoff.once backoff) value mono + if Atomic.compare_and_set t.head before after then + match mono with Bool -> true | Unit -> () + else push_as t (Backoff.once backoff) value mono let push_exn t value = push_as t Backoff.default value Unit let try_push t value = push_as t Backoff.default value Bool @@ -106,19 +100,14 @@ let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r = else if len > t.capacity then match mono with Unit -> raise Full | Bool -> false else - match Atomic.get t.head with - | (_, []) as old_head -> - if Atomic.compare_and_set t.head old_head (List.length values, values) - then match mono with Bool -> true | Unit -> () - else push_all_as t (Backoff.once backoff) values mono - | (curr_len, prev_values) as old_head -> - if curr_len + len > t.capacity then - match mono with Bool -> false | Unit -> raise Full - else if - Atomic.compare_and_set t.head old_head - (curr_len + len, values @ prev_values) - then match mono with Bool -> true | Unit -> () - else push_all_as t (Backoff.once backoff) values mono + let ((curr_len, prev_values) as before) = Atomic.get t.head in + if curr_len + len > t.capacity then + match mono with Bool -> false | Unit -> raise Full + else + let after = (curr_len + len, values @ prev_values) in + if Atomic.compare_and_set t.head before after then + match mono with Bool -> true | Unit -> () + else push_all_as t (Backoff.once backoff) values mono let try_push_all t values = push_all_as t Backoff.default (List.rev values) Bool let push_all_exn t values = push_all_as t Backoff.default (List.rev values) Unit From a37cee91f5c930dc9c928bfab00b6e4fa04bbd4d Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 17:04:45 +0100 Subject: [PATCH 09/11] Add missing stm test for is_full. --- test/bounded_stack/stm_bounded_stack.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index 59f08f30..e52eb5e0 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -18,6 +18,7 @@ module Spec = struct (* peek_exn uses the same function as peek_exn *) | To_seq | Is_empty + | Is_full | Length let string_of_int_list l = @@ -33,6 +34,7 @@ module Spec = struct | Peek_opt -> "Peek_opt" | To_seq -> "To_seq" | Is_empty -> "Is_empty" + | Is_full -> "Is_full" | Length -> "Length" type state = int list @@ -50,6 +52,7 @@ module Spec = struct Gen.return Peek_opt; Gen.return To_seq; Gen.return Is_empty; + Gen.return Is_full; Gen.return Length; ]) @@ -70,6 +73,7 @@ module Spec = struct | Peek_opt -> s | To_seq -> s | Is_empty -> s + | Is_full -> s | Length -> s let precond _ _ = true @@ -83,6 +87,7 @@ module Spec = struct | Peek_opt -> Res (option int, Stack.peek_opt d) | To_seq -> Res (seq int, Stack.to_seq d) | Is_empty -> Res (bool, Stack.is_empty d) + | Is_full -> Res (bool, Stack.is_full d) | Length -> Res (int, Stack.length d) let postcond c (s : state) res = @@ -95,6 +100,7 @@ module Spec = struct | Pop_all, Res ((List Int, _), res) -> res = s | To_seq, Res ((Seq Int, _), res) -> List.of_seq res = s | Is_empty, Res ((Bool, _), res) -> res = (s = []) + | Is_full, Res ((Bool, _), res) -> res = (List.length s = capacity) | Length, Res ((Int, _), res) -> res = List.length s | _, _ -> false end From 05f028c5d7164539c4505386f1ea3e00f9601d32 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 17:42:31 +0100 Subject: [PATCH 10/11] Remove copy_as_padded --- src/bounded_stack.ml | 2 +- test/bounded_stack/stm_bounded_stack.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 62544389..10a8f9d5 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -3,7 +3,7 @@ type 'a t = { head : (int * 'a list) Atomic.t; capacity : int } (* *) let create ?(capacity = Int.max_int) () = let head = Atomic.make_contended (0, []) in - { head; capacity = max capacity 1 } |> Multicore_magic.copy_as_padded + { head; capacity = max capacity 1 } let length t = fst (Atomic.get t.head) let is_full t = t.capacity = length t diff --git a/test/bounded_stack/stm_bounded_stack.ml b/test/bounded_stack/stm_bounded_stack.ml index e52eb5e0..221ea8f4 100644 --- a/test/bounded_stack/stm_bounded_stack.ml +++ b/test/bounded_stack/stm_bounded_stack.ml @@ -57,7 +57,7 @@ module Spec = struct ]) let init_state = [] - let capacity = 8 + let capacity = 16 let init_sut () = Stack.create ~capacity () let cleanup _ = () From 8471c97e562418a1e1cd90c4d29c29bd9a4d8121 Mon Sep 17 00:00:00 2001 From: Carine Morel Date: Thu, 21 Nov 2024 18:23:43 +0100 Subject: [PATCH 11/11] Replace List.(@) by List.rev_append as (@) is not tail rec. --- src/bounded_stack.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/bounded_stack.ml b/src/bounded_stack.ml index 10a8f9d5..0e0f5e26 100644 --- a/src/bounded_stack.ml +++ b/src/bounded_stack.ml @@ -104,7 +104,9 @@ let rec push_all_as : type r. 'a t -> Backoff.t -> 'a list -> r mono -> r = if curr_len + len > t.capacity then match mono with Bool -> false | Unit -> raise Full else - let after = (curr_len + len, values @ prev_values) in + let after = + (curr_len + len, List.rev_append (List.rev values) prev_values) + in if Atomic.compare_and_set t.head before after then match mono with Bool -> true | Unit -> () else push_all_as t (Backoff.once backoff) values mono