diff --git a/test/bounded_stack/bounded_stack_dscheck.ml b/test/bounded_stack/bounded_stack_dscheck.ml index a22ba2b7..fb16bedd 100644 --- a/test/bounded_stack/bounded_stack_dscheck.ml +++ b/test/bounded_stack/bounded_stack_dscheck.ml @@ -14,19 +14,20 @@ let push_pop () = 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 = drain stack in - !popped + remaining = items_total))) + 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 () -> @@ -114,6 +115,40 @@ let push_set () = 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 @@ -223,6 +258,38 @@ let push_cap () = 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 @@ -388,6 +455,7 @@ let () = 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; @@ -395,6 +463,7 @@ let () = 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; ] );