Skip to content

Commit

Permalink
Remove compare_and_set, compare_and_op and set functions.
Browse files Browse the repository at this point in the history
  • Loading branch information
@lyrm
lyrm committed Nov 21, 2024
1 parent 7d39912 commit 7aed3bf
Show file tree
Hide file tree
Showing 4 changed files with 0 additions and 246 deletions.
39 changes: 0 additions & 39 deletions src/bounded_stack.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
29 changes: 0 additions & 29 deletions src/bounded_stack.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
153 changes: 0 additions & 153 deletions test/bounded_stack/bounded_stack_dscheck.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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;
] );
]
25 changes: 0 additions & 25 deletions test/bounded_stack/stm_bounded_stack.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"

Expand All @@ -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;
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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 = [])
Expand Down

0 comments on commit 7aed3bf

Please sign in to comment.