Skip to content

Commit

Permalink
Add pop-set and pop-cas dscheck test
Browse files Browse the repository at this point in the history
  • Loading branch information
lyrm committed Oct 31, 2024
1 parent b97bdb5 commit cbf8675
Showing 1 changed file with 73 additions and 4 deletions.
77 changes: 73 additions & 4 deletions test/bounded_stack/bounded_stack_dscheck.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 () ->
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -388,13 +455,15 @@ 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;
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;
] );
Expand Down

0 comments on commit cbf8675

Please sign in to comment.