diff --git a/src/treiber_stack.ml b/src/treiber_stack.ml
index 4c5cb7b0..59a39609 100644
--- a/src/treiber_stack.ml
+++ b/src/treiber_stack.ml
@@ -3,29 +3,151 @@
 type 'a node = Nil | Cons of { value : 'a; tail : 'a node }
 type 'a t = 'a node Atomic.t
 
-let create () = Atomic.make Nil |> Multicore_magic.copy_as_padded
+let create () = Atomic.make_contended Nil
 let is_empty t = Atomic.get t == Nil
 
-let rec push t value backoff =
-  let tail = Atomic.get t in
-  let cons = Cons { value; tail } in
-  if not (Atomic.compare_and_set t tail cons) then
-    push t value (Backoff.once backoff)
+let of_list list =
+  List.fold_left (fun acc elt -> Cons { value = elt; tail = acc }) Nil list
+  |> Atomic.make_contended
 
-let push t value = push t value Backoff.default
+let of_seq seq =
+  Seq.fold_left (fun acc elt -> Cons { value = elt; tail = acc }) Nil seq
+  |> Atomic.make_contended
+
+(* *)
 
 exception Empty
 
 type ('a, _) poly = Option : ('a, 'a option) poly | Value : ('a, 'a) poly
 
-let rec pop_as : type a r. a t -> Backoff.t -> (a, r) poly -> r =
+let peek_as : type a r. a t -> (a, r) poly -> r =
+ fun t poly ->
+  match Atomic.get t with
+  | Nil -> begin
+      match poly with Option -> None | Value -> raise_notrace Empty
+    end
+  | Cons cons -> (
+      match poly with Option -> Some cons.value | Value -> cons.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 with
-  | Nil -> begin match poly with Option -> None | Value -> raise Empty end
+  | Nil -> begin
+      match poly with Option -> None | Value | Unit -> raise_notrace Empty
+    end
   | Cons cons_r as cons ->
       if Atomic.compare_and_set t cons cons_r.tail then
-        match poly with Option -> Some cons_r.value | Value -> cons_r.value
+        match poly with
+        | Option -> Some cons_r.value
+        | Value -> cons_r.value
+        | Unit -> ()
       else pop_as t (Backoff.once backoff) poly
 
-let pop t = pop_as t Backoff.default Value
+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 pop_all t backoff =
+  match Atomic.get t with
+  | Nil -> []
+  | old_head ->
+      if Atomic.compare_and_set t old_head Nil then
+        let[@tail_mod_cons] rec aux = function
+          | Nil -> []
+          | Cons cons -> cons.value :: aux cons.tail
+        in
+        aux old_head
+      else pop_all t (Backoff.once backoff)
+
+let pop_all t = pop_all t Backoff.default
+
+let to_seq t =
+  match Atomic.get t 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
+(* *)
+
+let rec push t value backoff =
+  let tail = Atomic.get t in
+  let cons = Cons { value; tail } in
+  if not (Atomic.compare_and_set t tail cons) then
+    push t value (Backoff.once backoff)
+
+let push t value = push t value Backoff.default
+
+(**)
+
+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 with
+  | Nil -> ( match poly with Value -> raise_notrace Empty | Bool -> false)
+  | Cons cons_r as old_head ->
+      if Atomic.compare_and_set t 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_ t backoff values =
+  let rec build_node acc = function
+    | [] -> acc
+    | x :: xs -> build_node (Cons { tail = acc; value = x }) xs
+  in
+  match Atomic.get t with
+  | Nil ->
+      if Atomic.compare_and_set t Nil (build_node Nil values) then ()
+      else push_all_ t (Backoff.once backoff) values
+  | Cons _ as old_head ->
+      if Atomic.compare_and_set t old_head @@ build_node old_head values then ()
+      else push_all_ t (Backoff.once backoff) values
+
+let push_all t values =
+  match values with [] -> () | _ -> push_all_ t Backoff.default values
+
+let add_seq t seq = push_all_ t Backoff.default (List.of_seq seq)
+
+(* *)
+
+type op = Set | Pop
+
+let try_compare_and_ t old_value new_value op =
+  let rec aux backoff =
+    match Atomic.get t with
+    | Nil -> false
+    | Cons cons_r as old_head ->
+        if cons_r.value == old_value then
+          if
+            Atomic.compare_and_set t 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/treiber_stack.mli b/src/treiber_stack.mli
index d489cfd3..b524e857 100644
--- a/src/treiber_stack.mli
+++ b/src/treiber_stack.mli
@@ -1,31 +1,191 @@
 (** Classic multi-producer multi-consumer Treiber stack.
 
-    All function are lockfree. It is the recommended starting point
-    when needing LIFO structure. *)
+  All functions are lock-free. It is the recommended starting point
+  when needing a LIFO structure. *)
+
+(** {1 API} *)
 
 type 'a t
-(** Type of Treiber stack holding items of type [t]. *)
+(** Represents a lock-free Treiber stack holding elements of type ['a]. *)
 
 val create : unit -> 'a t
-(** [create ()] returns a new and empty Treiber stack. *)
+(** [create ()] creates a new empty Treiber stack. *)
+
+val of_list : 'a list -> 'a t
+(** [of_list list] creates a new Treiber stack from a list. *)
 
 val is_empty : 'a t -> bool
-(** [is_empty s] checks whether stack [s] is empty. *)
+(** [is_empty stack] returns [true] if the [stack] is empty, otherwise [false]. *)
 
-val push : 'a t -> 'a -> unit
-(** [push s v] adds the element [v] at the top of stack [s]. *)
+(** {2 Consumer functions} *)
 
 exception Empty
-(** Raised when {!pop} is applied to an empty queue. *)
+(** Raised when {!pop_exn}, {!peek_exn}, {!drop_exn}, or {!set_exn} is 
+  applied to an empty stack.
 
-val pop : 'a t -> 'a
-(** [pop s] removes and returns the topmost element in the
-    stack [s].
+  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.
 
-    @raise Empty if [a] is empty.
-*)
+  {@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. *)
+
+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 s] removes and returns the topmost element in the
-    stack [s], or returns [None] if the stack is empty.
+(** [pop_opt stack] removes and returns [Some] of the top element of the [stack],
+  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 LIFO 
+order. 
+
+  {[
+  # open Saturn_lockfree.Stack
+  # let t : int t = create ()
+  val t : int t = <abstr>
+  # push t 1
+  - : unit = ()
+  # push t 2
+  - : unit = ()
+  # push t 3
+  - : unit = ()
+  # 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]. *)
+
+val push_all : 'a t -> 'a list -> unit
+(** [push_all stack elements] adds all [elements] to the top of the [stack]. 
+  
+  {[
+  # let t : int t = create ()
+  val t : int t = <abstr>
+  # push_all t [1; 2; 3; 4]
+  - : unit = ()
+  # 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.
+
+  @raise 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 top to 
+bottom.
+
+  🐌 This is a linear time operation. *)
+
+val of_seq : 'a Seq.t -> 'a t
+(** [of_seq seq] creates a stack from a [seq]. It must be finite. *)
+
+val add_seq : 'a t -> 'a Seq.t -> unit
+(** [add_seq stack seq] adds all elements of [seq] to the top of the 
+[stack]. [seq] must be finite. *)
+
+(** {1 Examples}
+  An example top-level session:
+  {[
+    # open Saturn_lockfree.Stack
+    # let t : int t = create ()
+    val t : int t = <abstr>
+    # push t 42
+    - : unit = ()
+    # push_all t [1; 2; 3]
+    - : unit = ()
+    # pop_exn t
+    - : int = 3
+    # peek_opt t
+    - : int option = Some 2
+    # pop_all t
+    - : int list = [2; 1; 42]
+    # pop_exn t
+    Exception: Saturn_lockfree__Treiber_stack.Empty.]}
+
+  A multicore example: 
+  {@ocaml non-deterministic[
+    # open Saturn_lockfree.Stack
+    # let t : int t = create ()
+    val t : int t = <abstr>
+    # let barrier =  Atomic.make 2
+    val barrier : int Atomic.t = <abstr>
+    # let pusher () = 
+        Atomic.decr barrier;
+        while Atomic.get barrier != 0 do Domain.cpu_relax () done;
+        push_all t [1;2;3] |> ignore;
+        push t 42;
+        push t 12
+    val pusher : unit -> unit = <fun>
+    # 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 = <fun>
+    # let domain_pusher = Domain.spawn pusher
+    val domain_pusher : unit Domain.t = <abstr>
+    # let domain_popper = Domain.spawn popper
+    val domain_popper : int option list Domain.t = <abstr>
+    # 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/test/treiber_stack/stm_treiber_stack.ml b/test/treiber_stack/stm_treiber_stack.ml
index 7236b497..f250629c 100644
--- a/test/treiber_stack/stm_treiber_stack.ml
+++ b/test/treiber_stack/stm_treiber_stack.ml
@@ -1,20 +1,45 @@
-(** Sequential and Parallel model-based tests of treiber_stack *)
+(** Sequential and Parallel model-based tests of bounded_queue *)
 
 open QCheck
 open STM
-module Treiber_stack = Saturn.Stack
+module Stack = Saturn.Stack
 
 module Spec = struct
-  type cmd = Push of int | Pop | Is_empty
+  type cmd =
+    | Push of int
+    | Push_all of int list
+    | 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
+
+  let string_of_int_list l =
+    "[" ^ String.concat "; " (List.map string_of_int l) ^ "]"
 
   let show_cmd c =
     match c with
     | Push i -> "Push " ^ string_of_int i
-    | Pop -> "Pop"
+    | Push_all l -> "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"
 
   type state = int list
-  type sut = int Treiber_stack.t
+  type sut = int Stack.t
 
   let arb_cmd _s =
     let int_gen = Gen.nat in
@@ -22,35 +47,67 @@ module Spec = struct
       (Gen.oneof
          [
            Gen.map (fun i -> Push i) int_gen;
-           Gen.return Pop;
+           Gen.map (fun l -> Push_all l) (Gen.list int_gen);
+           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;
          ])
 
   let init_state = []
-  let init_sut () = Treiber_stack.create ()
+  let init_sut () = Stack.create ()
   let cleanup _ = ()
 
   let next_state c s =
     match c with
     | Push i -> i :: s
-    | Pop -> ( match s with [] -> s | _ :: s' -> s')
+    | Push_all l -> 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
 
   let precond _ _ = true
 
   let run c d =
     match c with
-    | Push i -> Res (unit, Treiber_stack.push d i)
-    | Pop -> Res (result int exn, protect Treiber_stack.pop d)
-    | Is_empty -> Res (bool, Treiber_stack.is_empty d)
+    | Push i -> Res (unit, Stack.push d i)
+    | Push_all l -> Res (unit, Stack.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)
 
   let postcond c (s : state) res =
     match (c, res) with
-    | Push _, Res ((Unit, _), _) -> true
-    | Pop, Res ((Result (Int, Exn), _), res) -> (
-        match s with
-        | [] -> res = Error Treiber_stack.Empty
-        | j :: _ -> res = Ok j)
+    | Push _, Res ((Unit, _), ()) -> true
+    | Push_all _, Res ((Unit, _), _) -> true
+    | 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 = [])
     | _, _ -> false
 end
diff --git a/test/treiber_stack/treiber_stack_dscheck.ml b/test/treiber_stack/treiber_stack_dscheck.ml
index 48b7065f..69810e15 100644
--- a/test/treiber_stack/treiber_stack_dscheck.ml
+++ b/test/treiber_stack/treiber_stack_dscheck.ml
@@ -1,27 +1,23 @@
-let drain stack =
-  let remaining = ref 0 in
-  while not (Treiber_stack.is_empty stack) do
-    remaining := !remaining + 1;
-    assert (Option.is_some (Treiber_stack.pop_opt stack))
-  done;
-  !remaining
-
-let producer_consumer () =
+module Stack = Treiber_stack
+
+let drain stack = Stack.pop_all stack |> List.length
+
+let push_pop () =
   Atomic.trace (fun () ->
-      let stack = Treiber_stack.create () in
-      let items_total = 3 in
+      let stack = Stack.create () in
+      let items_total = 4 in
 
       (* producer *)
       Atomic.spawn (fun () ->
           for i = 1 to items_total do
-            Treiber_stack.push stack i
+            Stack.push stack i
           done);
 
       (* consumer *)
       let popped = ref 0 in
       Atomic.spawn (fun () ->
           for _ = 1 to items_total do
-            match Treiber_stack.pop_opt stack with
+            match Stack.pop_opt stack with
             | None -> ()
             | Some _ -> popped := !popped + 1
           done);
@@ -32,29 +28,108 @@ let producer_consumer () =
               let remaining = drain stack in
               !popped + remaining = items_total)))
 
-let two_producers () =
+let push_drop () =
   Atomic.trace (fun () ->
-      let stack = Treiber_stack.create () in
+      let stack = Stack.create () in
       let items_total = 4 in
 
+      (* producer *)
+      Atomic.spawn (fun () ->
+          for i = 1 to items_total do
+            Stack.push stack i
+          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
+              !dropped + remaining = items_total)))
+
+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.push stack i
+          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.push stack i) (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
+
       (* 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 *)
-              Treiber_stack.push stack (i + (j * 2))
+              Stack.push stack (i + (j * 2))
             done)
       done;
 
       (* checks*)
       Atomic.final (fun () ->
-          let rec get_items s =
-            if Treiber_stack.is_empty s then []
-            else
-              let item = Option.get (Treiber_stack.pop_opt s) in
-              item :: get_items s
-          in
-          let items = get_items stack in
+          let items = Stack.pop_all stack in
 
           (* got the same number of items out as in *)
           Atomic.check (fun () -> items_total = List.length items);
@@ -65,13 +140,13 @@ 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_consumers () =
+let pop_pop () =
   Atomic.trace (fun () ->
-      let stack = Treiber_stack.create () in
+      let stack = Stack.create () in
       let items_total = 4 in
 
       for i = 1 to items_total do
-        Treiber_stack.push stack i
+        Stack.push stack i
       done;
 
       (* two consumers *)
@@ -81,7 +156,7 @@ let two_consumers () =
           Atomic.spawn (fun () ->
               for _ = 1 to items_total / 2 do
                 (* even nums belong to thr 1, odd nums to thr 2 *)
-                list := Option.get (Treiber_stack.pop_opt stack) :: !list
+                list := Option.get (Stack.pop_opt stack) :: !list
               done)
           |> ignore)
         lists;
@@ -98,9 +173,121 @@ 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.push stack i
+          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.push stack i) 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.push stack i
+          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.push_all stack items);
+
+      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 = Treiber_stack.create () in
+      let stack = Stack.create () in
       let n1, n2 = (1, 2) in
 
       (* two producers *)
@@ -116,8 +303,8 @@ let two_domains () =
               List.iter
                 (fun elt ->
                   (* even nums belong to thr 1, odd nums to thr 2 *)
-                  Treiber_stack.push stack elt;
-                  lpop := Option.get (Treiber_stack.pop_opt stack) :: !lpop)
+                  Stack.push stack elt;
+                  lpop := Option.get (Stack.pop_opt stack) :: !lpop)
                 lpush)
           |> ignore)
         lists;
@@ -138,7 +325,7 @@ let two_domains () =
 
 let two_domains_more_pop () =
   Atomic.trace (fun () ->
-      let stack = Treiber_stack.create () in
+      let stack = Stack.create () in
       let n1, n2 = (2, 1) in
 
       (* two producers *)
@@ -153,9 +340,9 @@ let two_domains_more_pop () =
           Atomic.spawn (fun () ->
               List.iter
                 (fun elt ->
-                  Treiber_stack.push stack elt;
-                  lpop := Treiber_stack.pop_opt stack :: !lpop;
-                  lpop := Treiber_stack.pop_opt stack :: !lpop)
+                  Stack.push stack elt;
+                  lpop := Stack.pop_opt stack :: !lpop;
+                  lpop := Stack.pop_opt stack :: !lpop)
                 lpush)
           |> ignore)
         lists;
@@ -180,16 +367,43 @@ let two_domains_more_pop () =
               List.sort Int.compare (lpop1 @ lpop2)
               = List.init (n1 + n2) (fun i -> i))))
 
+let 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.push stack i
+          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 "treiber_stack_dscheck"
+  run "Stack_dscheck"
     [
       ( "basic",
         [
-          test_case "1-producer-1-consumer" `Slow producer_consumer;
-          test_case "2-producers" `Slow two_producers;
-          test_case "2-consumers" `Slow two_consumers;
+          test_case "1-producer-1-consumer" `Slow push_pop;
+          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-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;
         ] );
     ]