From 2e6ca9b8a0867325e07a6a12b4bbf9152f666a0a Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 27 Jun 2023 19:14:00 +0200
Subject: [PATCH 1/9] Lockfree skiplist.

---
 bench/bench_atomic_skiplist.ml                |  59 ++++++
 bench/main.ml                                 |   4 +
 src/atomicskiplist.ml                         | 200 ++++++++++++++++++
 src/atomicskiplist.mli                        |   6 +
 src_lockfree/saturn_lockfree.ml               |   1 +
 src_lockfree/saturn_lockfree.mli              |   1 +
 .../atomicskiplist/atomic_skiplist_dscheck.ml |  16 ++
 test/atomicskiplist/dune                      |  15 ++
 test/atomicskiplist/qcheck_atomic_skiplist.ml | 187 ++++++++++++++++
 9 files changed, 489 insertions(+)
 create mode 100644 bench/bench_atomic_skiplist.ml
 create mode 100644 src/atomicskiplist.ml
 create mode 100644 src/atomicskiplist.mli
 create mode 100644 test/atomicskiplist/atomic_skiplist_dscheck.ml
 create mode 100644 test/atomicskiplist/dune
 create mode 100644 test/atomicskiplist/qcheck_atomic_skiplist.ml

diff --git a/bench/bench_atomic_skiplist.ml b/bench/bench_atomic_skiplist.ml
new file mode 100644
index 00000000..a92977fb
--- /dev/null
+++ b/bench/bench_atomic_skiplist.ml
@@ -0,0 +1,59 @@
+open Lockfree
+
+let max_height = 10
+
+let workload num_elems num_threads add remove =
+  let sl = Atomicskiplist.create max_height in
+  let elems = Array.init num_elems (fun _ -> Random.int 10000) in
+  let push () =
+    Domain.spawn (fun () ->
+        let start_time = Unix.gettimeofday () in
+        for i = 0 to (num_elems - 1) / num_threads do
+          Domain.cpu_relax ();
+          let prob = Random.float 1.0 in
+          if prob < add then Atomicskiplist.add sl (Random.int 10000) |> ignore
+          else if prob >= add && prob < add +. remove then
+            Atomicskiplist.remove sl (Random.int 10000) |> ignore
+          else Atomicskiplist.mem sl elems.(i) |> ignore
+        done;
+        start_time)
+  in
+  let threads = List.init num_threads (fun _ -> push ()) in
+  let start_time_threads =
+    List.map (fun domain -> Domain.join domain) threads
+  in
+  let end_time = Unix.gettimeofday () in
+  let time_diff = end_time -. List.nth start_time_threads 0 in
+  time_diff
+
+(* A write heavy workload with threads with 50% adds and 50% removes. *)
+let write_heavy_workload num_elems num_threads =
+  workload num_elems num_threads 0.5 0.5
+
+(* A regular workload with 90% reads, 9% adds and 1% removes. *)
+let read_heavy_workload num_elems num_threads =
+  workload num_elems num_threads 0.09 0.01
+
+let moderate_heavy_workload num_elems num_threads =
+  workload num_elems num_threads 0.2 0.1
+
+let balanced_heavy_workload num_elems num_threads =
+  workload num_elems num_threads 0.3 0.2
+
+let bench ~workload_type ~num_elems ~num_threads () =
+  let workload =
+    if workload_type = "read_heavy" then read_heavy_workload
+    else if workload_type = "moderate_heavy" then moderate_heavy_workload
+    else if workload_type = "balanced_heavy" then balanced_heavy_workload
+    else write_heavy_workload
+  in
+  let results = ref [] in
+  for i = 1 to 10 do
+    let time = workload num_elems num_threads in
+    if i > 1 then results := time :: !results
+  done;
+  let results = List.sort Float.compare !results in
+  let median_time = List.nth results 4 in
+  let median_throughput = Float.of_int num_elems /. median_time in
+  Benchmark_result.create_generic ~median_time ~median_throughput
+    ("atomic_skiplist_" ^ workload_type)
diff --git a/bench/main.ml b/bench/main.ml
index 95632970..ab536444 100644
--- a/bench/main.ml
+++ b/bench/main.ml
@@ -16,6 +16,10 @@ let benchmark_list =
     Mpmc_queue.bench ~use_cas:true ~takers:4 ~pushers:4;
     Mpmc_queue.bench ~use_cas:true ~takers:1 ~pushers:8;
     Mpmc_queue.bench ~use_cas:true ~takers:8 ~pushers:1;
+    Bench_atomic_skiplist.bench ~workload_type:"read_heavy" ~num_elems:2000000
+      ~num_threads:2;
+    Bench_atomic_skiplist.bench ~workload_type:"moderate_heavy"
+      ~num_elems:2000000 ~num_threads:2;
   ]
   @ backoff_benchmarks
 
diff --git a/src/atomicskiplist.ml b/src/atomicskiplist.ml
new file mode 100644
index 00000000..4c9a21c5
--- /dev/null
+++ b/src/atomicskiplist.ml
@@ -0,0 +1,200 @@
+type 'a markable_reference = { node : 'a; marked : bool }
+(** markable reference: stores a reference to a node and has a field to specify if it is marked *)
+
+exception Failed_snip
+
+type node = {
+  key : int;
+  height : int;
+  next : node markable_reference Atomic.t array;
+}
+
+type t = { head : node; max_height : int }
+
+let null_node = { key = Int.max_int; height = 0; next = [||] }
+
+(** create_new_node: creates a new node with some value and height *)
+let create_new_node value height =
+  let next =
+    Array.init (height + 1) (fun _ ->
+        Atomic.make { node = null_node; marked = false })
+  in
+  { key = value; height; next }
+
+(** create_dummy_node_array: Creates a new array with the different node for each index *)
+let create_dummy_node_array sl =
+  let arr = Array.make (sl.max_height + 1) null_node in
+  arr
+
+(** Get a random level from 1 till max_height (both included) *)
+let get_random_level sl =
+  let rec count_level cur_level =
+    if cur_level == sl.max_height || Random.bool () then cur_level
+    else count_level (cur_level + 1)
+  in
+  count_level 1
+
+(** Create a new skiplist *)
+let create max_height =
+  let tail = create_new_node Int.max_int max_height in
+  let next =
+    Array.init (max_height + 1) (fun _ ->
+        Atomic.make { node = tail; marked = false })
+  in
+  let head = { key = Int.min_int; height = max_height; next } in
+  { head; max_height }
+
+(** Compares old_node and old_mark with the atomic reference and if they are the same then 
+    Replaces the value in the atomic with node and mark *)
+let compare_and_set_mark_ref (atomic, old_node, old_mark, node, mark) =
+  let current = Atomic.get atomic in
+  let set_mark_ref () =
+    Atomic.compare_and_set atomic current { node; marked = mark }
+  in
+  let current_node = current.node in
+  current_node == old_node && current.marked = old_mark
+  && ((current_node == node && current.marked = mark) || set_mark_ref ())
+
+(** Returns true if key is found within the skiplist else false;
+    Irrespective of return value, fills the preds and succs array with 
+    the predecessors nodes with smaller key and successors nodes with greater than 
+    or equal to key 
+  *)
+let find_in (key, preds, succs, sl) =
+  let head = sl.head in
+  let rec iterate (prev, curr, succ, mark, level) =
+    if mark then
+      let snip =
+        compare_and_set_mark_ref (prev.next.(level), curr, false, succ, false)
+      in
+      if not snip then raise Failed_snip
+      else
+        let { node = curr; marked = _ } = Atomic.get prev.next.(level) in
+        let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
+        iterate (prev, curr, succ, mark, level)
+    else if curr.key < key then
+      let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
+      iterate (curr, succ, new_succ, mark, level)
+    else (prev, curr)
+  in
+  let rec update_arrays prev level =
+    let { node = curr; marked = _ } = Atomic.get prev.next.(level) in
+    let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
+    try
+      let prev, curr = iterate (prev, curr, succ, mark, level) in
+      preds.(level) <- prev;
+      succs.(level) <- curr;
+      if level > 0 then update_arrays prev (level - 1) else curr.key == key
+    with Failed_snip -> update_arrays head sl.max_height
+  in
+  update_arrays head sl.max_height
+
+(** Adds a new key to the skiplist sl. *)
+let add sl key =
+  let top_level = get_random_level sl in
+  let preds = create_dummy_node_array sl in
+  let succs = create_dummy_node_array sl in
+  let rec repeat () =
+    let found = find_in (key, preds, succs, sl) in
+    if found then false
+    else
+      let new_node_next =
+        Array.map
+          (fun element ->
+            let mark_ref = { node = element; marked = false } in
+            Atomic.make mark_ref)
+          succs
+      in
+      let new_node = { key; height = top_level; next = new_node_next } in
+      let pred = preds.(0) in
+      let succ = succs.(0) in
+      if
+        not
+          (compare_and_set_mark_ref
+             (pred.next.(0), succ, false, new_node, false))
+      then repeat ()
+      else
+        let rec update_levels level =
+          let rec set_next () =
+            let pred = preds.(level) in
+            let succ = succs.(level) in
+            if
+              compare_and_set_mark_ref
+                (pred.next.(level), succ, false, new_node, false)
+            then ()
+            else (
+              find_in (key, preds, succs, sl) |> ignore;
+              set_next ())
+          in
+          set_next ();
+          if level < top_level then update_levels (level + 1)
+        in
+        update_levels 1;
+        true
+  in
+  repeat ()
+
+(** Returns true if the key is within the skiplist, else returns false *)
+let mem sl key =
+  let rec search (pred, curr, succ, mark, level) =
+    if mark then
+      let curr = succ in
+      let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
+      search (pred, curr, succ, mark, level)
+    else if curr.key < key then
+      let pred = curr in
+      let curr = succ in
+      let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
+      search (pred, curr, succ, mark, level)
+    else if level > 0 then
+      let level = level - 1 in
+      let { node = curr; marked = _ } = Atomic.get pred.next.(level) in
+      let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
+      search (pred, curr, succ, mark, level)
+    else curr.key == key
+  in
+  let pred = sl.head in
+  let { node = curr; marked = _ } = Atomic.get pred.next.(sl.max_height) in
+  let { node = succ; marked = mark } = Atomic.get curr.next.(sl.max_height) in
+  search (pred, curr, succ, mark, sl.max_height)
+
+(** Returns true if the removal was successful and returns false if the key is not present within the skiplist *)
+let remove sl key =
+  let preds = create_dummy_node_array sl in
+  let succs = create_dummy_node_array sl in
+  let found = find_in (key, preds, succs, sl) in
+  if not found then false
+  else
+    let nodeToRemove = succs.(0) in
+    let nodeHeight = nodeToRemove.height in
+    let rec mark_levels succ level =
+      let _ =
+        compare_and_set_mark_ref
+          (nodeToRemove.next.(level), succ, false, succ, true)
+      in
+      let { node = succ; marked = mark } =
+        Atomic.get nodeToRemove.next.(level)
+      in
+      if not mark then mark_levels succ level
+    in
+    let rec update_upper_levels level =
+      let { node = succ; marked = mark } =
+        Atomic.get nodeToRemove.next.(level)
+      in
+      if not mark then mark_levels succ level;
+      if level > 1 then update_upper_levels (level - 1)
+    in
+    let rec update_bottom_level succ =
+      let iMarkedIt =
+        compare_and_set_mark_ref (nodeToRemove.next.(0), succ, false, succ, true)
+      in
+      let { node = succ; marked = mark } = Atomic.get succs.(0).next.(0) in
+      if iMarkedIt then (
+        find_in (key, preds, succs, sl) |> ignore;
+        true)
+      else if mark then false
+      else update_bottom_level succ
+    in
+    update_upper_levels nodeHeight;
+    let { node = succ; marked = _ } = Atomic.get nodeToRemove.next.(0) in
+    update_bottom_level succ
\ No newline at end of file
diff --git a/src/atomicskiplist.mli b/src/atomicskiplist.mli
new file mode 100644
index 00000000..b21bdc46
--- /dev/null
+++ b/src/atomicskiplist.mli
@@ -0,0 +1,6 @@
+type t
+
+val create : int -> t
+val mem : t -> int -> bool
+val add : t -> int -> bool
+val remove : t -> int -> bool
diff --git a/src_lockfree/saturn_lockfree.ml b/src_lockfree/saturn_lockfree.ml
index ca2e063a..449eb385 100644
--- a/src_lockfree/saturn_lockfree.ml
+++ b/src_lockfree/saturn_lockfree.ml
@@ -33,3 +33,4 @@ module Single_prod_single_cons_queue = Spsc_queue
 module Single_consumer_queue = Mpsc_queue
 module Relaxed_queue = Mpmc_relaxed_queue
 module Backoff = Backoff
+module Atomicskiplist = Atomicskiplist
diff --git a/src_lockfree/saturn_lockfree.mli b/src_lockfree/saturn_lockfree.mli
index d70939f5..032d323b 100644
--- a/src_lockfree/saturn_lockfree.mli
+++ b/src_lockfree/saturn_lockfree.mli
@@ -40,3 +40,4 @@ module Relaxed_queue = Mpmc_relaxed_queue
 (** {2 Other} *)
 
 module Backoff = Backoff
+module Atomicskiplist = Atomicskiplist
diff --git a/test/atomicskiplist/atomic_skiplist_dscheck.ml b/test/atomicskiplist/atomic_skiplist_dscheck.ml
new file mode 100644
index 00000000..926f81dc
--- /dev/null
+++ b/test/atomicskiplist/atomic_skiplist_dscheck.ml
@@ -0,0 +1,16 @@
+(* This dscheck testcase is not terminating. *)
+let two_producers () =
+  Atomic.trace (fun () ->
+      let sl = Atomicskiplist.create 10 in
+
+      Atomic.spawn (fun () -> Atomicskiplist.mem sl 2 |> ignore);
+      Atomic.spawn (fun () -> Atomicskiplist.mem sl 3 |> ignore);
+
+      Atomic.final (fun () ->
+          (* Atomic.check (fun () -> !present) *)
+          Atomic.check (fun () -> true)))
+
+let () =
+  let open Alcotest in
+  run "atomic_skiplist_dscheck"
+    [ ("basic", [ test_case "2-producers" `Slow two_producers ]) ]
diff --git a/test/atomicskiplist/dune b/test/atomicskiplist/dune
new file mode 100644
index 00000000..6091f00a
--- /dev/null
+++ b/test/atomicskiplist/dune
@@ -0,0 +1,15 @@
+(rule
+ (copy ../../src/backoff.ml backoff.ml))
+
+(rule
+ (copy ../../src/atomicskiplist.ml atomicskiplist.ml))
+
+(test
+ (name atomic_skiplist_dscheck)
+ (libraries atomic dscheck alcotest)
+ (modules atomicskiplist atomic_skiplist_dscheck))
+
+(test
+ (name qcheck_atomic_skiplist)
+ (libraries lockfree qcheck qcheck-alcotest)
+ (modules qcheck_atomic_skiplist))
diff --git a/test/atomicskiplist/qcheck_atomic_skiplist.ml b/test/atomicskiplist/qcheck_atomic_skiplist.ml
new file mode 100644
index 00000000..dbd1649a
--- /dev/null
+++ b/test/atomicskiplist/qcheck_atomic_skiplist.ml
@@ -0,0 +1,187 @@
+module Atomicskiplist = Lockfree.Atomicskiplist
+
+let max_height = 10
+
+let tests_sequential =
+  QCheck.
+    [
+      (* TEST 1: add*)
+      Test.make ~name:"add" (list int) (fun lpush ->
+          assume (lpush <> []);
+          let sl = Atomicskiplist.create max_height in
+          let rec add_all_elems l =
+            match l with
+            | h :: t ->
+                if Atomicskiplist.add sl h then add_all_elems t else false
+            | [] -> true
+          in
+          add_all_elems lpush);
+      (*TEST 2: add_remove*)
+      Test.make ~name:"add_remove" (list int) (fun lpush ->
+          let lpush = List.sort_uniq Int.compare lpush in
+          let sl = Atomicskiplist.create max_height in
+          List.iter (fun key -> ignore (Atomicskiplist.add sl key)) lpush;
+          let rec remove_all_elems l =
+            match l with
+            | h :: t ->
+                if Atomicskiplist.remove sl h then remove_all_elems t else false
+            | [] -> true
+          in
+          remove_all_elems lpush);
+      (*TEST 3: add_find*)
+      Test.make ~name:"add_find" (list int) (fun lpush ->
+          let lpush = List.sort_uniq Int.compare lpush in
+          let lpush = Array.of_list lpush in
+          let sl = Atomicskiplist.create max_height in
+          let len = Array.length lpush in
+          let pos = Array.sub lpush 0 (len / 2) in
+          let neg = Array.sub lpush (len / 2) (len / 2) in
+          Array.iter (fun key -> ignore @@ Atomicskiplist.add sl key) pos;
+          let rec check_pos index =
+            if index < len / 2 then
+              if Atomicskiplist.mem sl pos.(index) then check_pos (index + 1)
+              else false
+            else true
+          in
+          let rec check_neg index =
+            if index < len / 2 then
+              if not @@ Atomicskiplist.mem sl neg.(index) then
+                check_neg (index + 1)
+              else false
+            else true
+          in
+          check_pos 0 && check_neg 0);
+      (* TEST 4: add_remove_find *)
+      Test.make ~name:"add_remove_find" (list int) (fun lpush ->
+          let lpush = List.sort_uniq Int.compare lpush in
+          let sl = Atomicskiplist.create max_height in
+          List.iter (fun key -> ignore @@ Atomicskiplist.add sl key) lpush;
+          List.iter (fun key -> ignore @@ Atomicskiplist.remove sl key) lpush;
+          let rec not_find_all_elems l =
+            match l with
+            | h :: t ->
+                if not @@ Atomicskiplist.mem sl h then not_find_all_elems t
+                else false
+            | [] -> true
+          in
+
+          not_find_all_elems lpush);
+    ]
+
+let tests_two_domains =
+  QCheck.
+    [
+      (* TEST 1: Two domains doing multiple adds *)
+      Test.make ~name:"parallel_add" (pair small_nat small_nat)
+        (fun (npush1, npush2) ->
+          let sl = Atomicskiplist.create max_height in
+          let sema = Semaphore.Binary.make false in
+          let lpush1 = List.init npush1 (fun i -> i) in
+          let lpush2 = List.init npush2 (fun i -> i + npush1) in
+          let work lpush =
+            List.map
+              (fun elt ->
+                let completed = Atomicskiplist.add sl elt in
+                Domain.cpu_relax ();
+                completed)
+              lpush
+          in
+
+          let domain1 =
+            Domain.spawn (fun () ->
+                Semaphore.Binary.release sema;
+                work lpush1)
+          in
+          let popped2 =
+            while not (Semaphore.Binary.try_acquire sema) do
+              Domain.cpu_relax ()
+            done;
+            work lpush2
+          in
+          let popped1 = Domain.join domain1 in
+          let rec compare_all_true l =
+            match l with
+            | true :: t -> compare_all_true t
+            | false :: _ -> false
+            | [] -> true
+          in
+          compare_all_true popped1 && compare_all_true popped2);
+      (* TEST 2: Two domains doing multiple one push and one pop in parallel *)
+      Test.make ~count:10000 ~name:"parallel_add_remove"
+        (pair small_nat small_nat) (fun (npush1, npush2) ->
+          let sl = Atomicskiplist.create max_height in
+          let sema = Semaphore.Binary.make false in
+
+          let lpush1 = List.init npush1 (fun i -> i) in
+          let lpush2 = List.init npush2 (fun i -> i + npush1) in
+
+          let work lpush =
+            List.map
+              (fun elt ->
+                ignore @@ Atomicskiplist.add sl elt;
+                Domain.cpu_relax ();
+                Atomicskiplist.remove sl elt)
+              lpush
+          in
+
+          let domain1 =
+            Domain.spawn (fun () ->
+                Semaphore.Binary.release sema;
+                work lpush1)
+          in
+          let _ =
+            while not (Semaphore.Binary.try_acquire sema) do
+              Domain.cpu_relax ()
+            done;
+            work lpush2
+          in
+          let _ = Domain.join domain1 in
+
+          let rec check_none_present l =
+            match l with
+            | h :: t ->
+                if Atomicskiplist.mem sl h then false else check_none_present t
+            | [] -> true
+          in
+          check_none_present lpush1 && check_none_present lpush2);
+      (* TEST 3: Parallel push and pop using the same elements in two domains
+ *)
+      Test.make ~name:"parallel_add_remove_same_list" (list int) (fun lpush ->
+          let sl = Atomicskiplist.create max_height in
+          let sema = Semaphore.Binary.make false in
+          let add_all_elems l = List.map (Atomicskiplist.add sl) l in
+          let remove_all_elems l = List.map (Atomicskiplist.remove sl) l in
+
+          let domain1 =
+            Domain.spawn (fun () ->
+                Semaphore.Binary.release sema;
+                Domain.cpu_relax ();
+                let add1 = add_all_elems lpush in
+                let remove1 = remove_all_elems lpush in
+                (add1, remove1))
+          in
+          let _, _ =
+            while not (Semaphore.Binary.try_acquire sema) do
+              Domain.cpu_relax ()
+            done;
+            let add2 = add_all_elems lpush in
+            let remove2 = remove_all_elems lpush in
+            (add2, remove2)
+          in
+          let _, _ = Domain.join domain1 in
+          let rec check_none_present l =
+            match l with
+            | h :: t ->
+                if Atomicskiplist.mem sl h then false else check_none_present t
+            | [] -> true
+          in
+          check_none_present lpush);
+    ]
+
+let () =
+  let to_alcotest = List.map QCheck_alcotest.to_alcotest in
+  Alcotest.run "Atomic Skip List"
+    [
+      ("test_sequential", to_alcotest tests_sequential);
+      ("tests_two_domains", to_alcotest tests_two_domains);
+    ]

From 0efac799c6020da419b12b14f8ad78a7af3edf60 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 27 Jun 2023 17:41:39 +0200
Subject: [PATCH 2/9] Add stm and more dscheck tests.

---
 bench/bench_atomic_skiplist.ml                |  4 +-
 src/atomicskiplist.ml                         | 22 ++---
 src/atomicskiplist.mli                        |  2 +-
 .../atomicskiplist/atomic_skiplist_dscheck.ml | 99 +++++++++++++++++--
 test/atomicskiplist/dune                      |  7 ++
 test/atomicskiplist/qcheck_atomic_skiplist.ml | 16 ++-
 test/atomicskiplist/stm_atomicskiplist.ml     | 70 +++++++++++++
 7 files changed, 185 insertions(+), 35 deletions(-)
 create mode 100644 test/atomicskiplist/stm_atomicskiplist.ml

diff --git a/bench/bench_atomic_skiplist.ml b/bench/bench_atomic_skiplist.ml
index a92977fb..111fe27c 100644
--- a/bench/bench_atomic_skiplist.ml
+++ b/bench/bench_atomic_skiplist.ml
@@ -1,9 +1,7 @@
 open Lockfree
 
-let max_height = 10
-
 let workload num_elems num_threads add remove =
-  let sl = Atomicskiplist.create max_height in
+  let sl = Atomicskiplist.create () in
   let elems = Array.init num_elems (fun _ -> Random.int 10000) in
   let push () =
     Domain.spawn (fun () ->
diff --git a/src/atomicskiplist.ml b/src/atomicskiplist.ml
index 4c9a21c5..3c6e35af 100644
--- a/src/atomicskiplist.ml
+++ b/src/atomicskiplist.ml
@@ -1,13 +1,9 @@
-type 'a markable_reference = { node : 'a; marked : bool }
+type markable_reference = { node : node; marked : bool }
 (** markable reference: stores a reference to a node and has a field to specify if it is marked *)
 
-exception Failed_snip
+and node = { key : int; height : int; next : markable_reference Atomic.t array }
 
-type node = {
-  key : int;
-  height : int;
-  next : node markable_reference Atomic.t array;
-}
+exception Failed_snip
 
 type t = { head : node; max_height : int }
 
@@ -35,7 +31,7 @@ let get_random_level sl =
   count_level 1
 
 (** Create a new skiplist *)
-let create max_height =
+let create ?(max_height=10) () =
   let tail = create_new_node Int.max_int max_height in
   let next =
     Array.init (max_height + 1) (fun _ ->
@@ -44,7 +40,7 @@ let create max_height =
   let head = { key = Int.min_int; height = max_height; next } in
   { head; max_height }
 
-(** Compares old_node and old_mark with the atomic reference and if they are the same then 
+(** Compares old_node and old_mark with the atomic reference and if they are the same then
     Replaces the value in the atomic with node and mark *)
 let compare_and_set_mark_ref (atomic, old_node, old_mark, node, mark) =
   let current = Atomic.get atomic in
@@ -56,9 +52,9 @@ let compare_and_set_mark_ref (atomic, old_node, old_mark, node, mark) =
   && ((current_node == node && current.marked = mark) || set_mark_ref ())
 
 (** Returns true if key is found within the skiplist else false;
-    Irrespective of return value, fills the preds and succs array with 
-    the predecessors nodes with smaller key and successors nodes with greater than 
-    or equal to key 
+    Irrespective of return value, fills the preds and succs array with
+    the predecessors nodes with smaller key and successors nodes with greater than
+    or equal to key
   *)
 let find_in (key, preds, succs, sl) =
   let head = sl.head in
@@ -197,4 +193,4 @@ let remove sl key =
     in
     update_upper_levels nodeHeight;
     let { node = succ; marked = _ } = Atomic.get nodeToRemove.next.(0) in
-    update_bottom_level succ
\ No newline at end of file
+    update_bottom_level succ
diff --git a/src/atomicskiplist.mli b/src/atomicskiplist.mli
index b21bdc46..3a07487b 100644
--- a/src/atomicskiplist.mli
+++ b/src/atomicskiplist.mli
@@ -1,6 +1,6 @@
 type t
 
-val create : int -> t
+val create : ?max_height:int -> unit -> t
 val mem : t -> int -> bool
 val add : t -> int -> bool
 val remove : t -> int -> bool
diff --git a/test/atomicskiplist/atomic_skiplist_dscheck.ml b/test/atomicskiplist/atomic_skiplist_dscheck.ml
index 926f81dc..a3eb521b 100644
--- a/test/atomicskiplist/atomic_skiplist_dscheck.ml
+++ b/test/atomicskiplist/atomic_skiplist_dscheck.ml
@@ -1,16 +1,97 @@
-(* This dscheck testcase is not terminating. *)
-let two_producers () =
+open Atomicskiplist
+
+let _two_mem () =
+  Atomic.trace (fun () ->
+      Random.init 0;
+      let sl = create ~max_height:2 () in
+      let added1 = ref false in
+      let found1 = ref false in
+      let found2 = ref false in
+
+      Atomic.spawn (fun () ->
+          added1 := add sl 1;
+          found1 := mem sl 1);
+
+      Atomic.spawn (fun () -> found2 := mem sl 2);
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () -> !added1 && !found1 && not !found2)))
+
+let _two_add () =
+  Atomic.trace (fun () ->
+      Random.init 0;
+      let sl = create ~max_height:2 () in
+      let added1 = ref false in
+      let added2 = ref false in
+
+      Atomic.spawn (fun () -> added1 := add sl 1);
+      Atomic.spawn (fun () -> added2 := add sl 2);
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () -> !added1 && !added2 && mem sl 1 && mem sl 2)))
+
+let _two_add_same () =
+  Atomic.trace (fun () ->
+      Random.init 0;
+      let sl = create ~max_height:2 () in
+      let added1 = ref false in
+      let added2 = ref false in
+
+      Atomic.spawn (fun () -> added1 := add sl 1);
+      Atomic.spawn (fun () -> added2 := add sl 1);
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              (!added1 && not !added2)
+              || (((not !added1) && !added2) && mem sl 1))))
+
+let _two_remove_same () =
+  Atomic.trace (fun () ->
+      Random.init 0;
+      let sl = create ~max_height:1 () in
+      let added1 = ref false in
+      let removed1 = ref false in
+      let removed2 = ref false in
+
+      Atomic.spawn (fun () ->
+          added1 := add sl 1;
+          removed1 := remove sl 1);
+      Atomic.spawn (fun () -> removed2 := remove sl 1);
+
+      Atomic.final (fun () ->
+          Atomic.check (fun () ->
+              !added1
+              && ((!removed1 && not !removed2) || ((not !removed1) && !removed2))
+              && not (mem sl 1))))
+
+let _two_remove () =
   Atomic.trace (fun () ->
-      let sl = Atomicskiplist.create 10 in
+      Random.init 0;
+      let sl = create ~max_height:1 () in
+      let added1 = ref false in
+      let removed1 = ref false in
+      let removed2 = ref false in
 
-      Atomic.spawn (fun () -> Atomicskiplist.mem sl 2 |> ignore);
-      Atomic.spawn (fun () -> Atomicskiplist.mem sl 3 |> ignore);
+      Atomic.spawn (fun () ->
+          added1 := add sl 1;
+          removed1 := remove sl 1);
+      Atomic.spawn (fun () -> removed2 := remove sl 2);
 
       Atomic.final (fun () ->
-          (* Atomic.check (fun () -> !present) *)
-          Atomic.check (fun () -> true)))
+          Atomic.check (fun () ->
+              let found1 = mem sl 1 in
+              !added1 && !removed1 && not !removed2 && not found1)))
 
 let () =
   let open Alcotest in
-  run "atomic_skiplist_dscheck"
-    [ ("basic", [ test_case "2-producers" `Slow two_producers ]) ]
+  run "skiplist_dscheck"
+    [
+      ( "basic",
+        [
+          test_case "2-mem" `Slow _two_mem;
+          test_case "2-add-same" `Slow _two_add_same;
+          test_case "2-add" `Slow _two_add;
+          test_case "2-remove-same" `Slow _two_remove_same;
+          test_case "2-remove" `Slow _two_remove;
+        ] );
+    ]
diff --git a/test/atomicskiplist/dune b/test/atomicskiplist/dune
index 6091f00a..0dadbae8 100644
--- a/test/atomicskiplist/dune
+++ b/test/atomicskiplist/dune
@@ -13,3 +13,10 @@
  (name qcheck_atomic_skiplist)
  (libraries lockfree qcheck qcheck-alcotest)
  (modules qcheck_atomic_skiplist))
+
+(test
+ (name stm_atomicskiplist)
+ (modules stm_atomicskiplist)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))
\ No newline at end of file
diff --git a/test/atomicskiplist/qcheck_atomic_skiplist.ml b/test/atomicskiplist/qcheck_atomic_skiplist.ml
index dbd1649a..9e55f102 100644
--- a/test/atomicskiplist/qcheck_atomic_skiplist.ml
+++ b/test/atomicskiplist/qcheck_atomic_skiplist.ml
@@ -1,14 +1,12 @@
 module Atomicskiplist = Lockfree.Atomicskiplist
 
-let max_height = 10
-
 let tests_sequential =
   QCheck.
     [
       (* TEST 1: add*)
       Test.make ~name:"add" (list int) (fun lpush ->
           assume (lpush <> []);
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           let rec add_all_elems l =
             match l with
             | h :: t ->
@@ -19,7 +17,7 @@ let tests_sequential =
       (*TEST 2: add_remove*)
       Test.make ~name:"add_remove" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           List.iter (fun key -> ignore (Atomicskiplist.add sl key)) lpush;
           let rec remove_all_elems l =
             match l with
@@ -32,7 +30,7 @@ let tests_sequential =
       Test.make ~name:"add_find" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
           let lpush = Array.of_list lpush in
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           let len = Array.length lpush in
           let pos = Array.sub lpush 0 (len / 2) in
           let neg = Array.sub lpush (len / 2) (len / 2) in
@@ -54,7 +52,7 @@ let tests_sequential =
       (* TEST 4: add_remove_find *)
       Test.make ~name:"add_remove_find" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           List.iter (fun key -> ignore @@ Atomicskiplist.add sl key) lpush;
           List.iter (fun key -> ignore @@ Atomicskiplist.remove sl key) lpush;
           let rec not_find_all_elems l =
@@ -74,7 +72,7 @@ let tests_two_domains =
       (* TEST 1: Two domains doing multiple adds *)
       Test.make ~name:"parallel_add" (pair small_nat small_nat)
         (fun (npush1, npush2) ->
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           let sema = Semaphore.Binary.make false in
           let lpush1 = List.init npush1 (fun i -> i) in
           let lpush2 = List.init npush2 (fun i -> i + npush1) in
@@ -109,7 +107,7 @@ let tests_two_domains =
       (* TEST 2: Two domains doing multiple one push and one pop in parallel *)
       Test.make ~count:10000 ~name:"parallel_add_remove"
         (pair small_nat small_nat) (fun (npush1, npush2) ->
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           let sema = Semaphore.Binary.make false in
 
           let lpush1 = List.init npush1 (fun i -> i) in
@@ -147,7 +145,7 @@ let tests_two_domains =
       (* TEST 3: Parallel push and pop using the same elements in two domains
  *)
       Test.make ~name:"parallel_add_remove_same_list" (list int) (fun lpush ->
-          let sl = Atomicskiplist.create max_height in
+          let sl = Atomicskiplist.create () in
           let sema = Semaphore.Binary.make false in
           let add_all_elems l = List.map (Atomicskiplist.add sl) l in
           let remove_all_elems l = List.map (Atomicskiplist.remove sl) l in
diff --git a/test/atomicskiplist/stm_atomicskiplist.ml b/test/atomicskiplist/stm_atomicskiplist.ml
new file mode 100644
index 00000000..ce4054fc
--- /dev/null
+++ b/test/atomicskiplist/stm_atomicskiplist.ml
@@ -0,0 +1,70 @@
+(** Sequential and Parallel model-based tests of ws_deque *)
+
+open QCheck
+open STM
+module Skiplist = Lockfree.Atomicskiplist
+
+module WSDConf = struct
+  type cmd = Mem of int | Add of int | Remove of int
+
+  let show_cmd c =
+    match c with
+    | Mem i -> "Mem " ^ string_of_int i
+    | Add i -> "Add " ^ string_of_int i
+    | Remove i -> "Remove " ^ string_of_int i
+
+  module Sint = Set.Make (
+                    struct
+                      type t = int
+                      let compare = compare
+                    end)
+
+  type state = Sint.t
+  type sut = Skiplist.t
+
+  let arb_cmd _s =
+    let int_gen = Gen.nat in
+    QCheck.make ~print:show_cmd
+      (Gen.oneof
+         [
+           Gen.map (fun i -> Add i) int_gen;
+           Gen.map (fun i -> Mem i) int_gen;
+           Gen.map (fun i -> Remove i) int_gen;
+         ])
+
+  let init_state = Sint.empty
+  let init_sut () = Skiplist.create ()
+  let cleanup _ = ()
+
+  let next_state c s =
+    match c with
+    | Add i -> Sint.add i s
+    | Remove i -> Sint.remove i s
+    | Mem _ -> s
+
+  let precond _ _ = true
+
+  let run c d =
+    match c with
+    | Add i -> Res (bool, Skiplist.add d i)
+    | Remove i -> Res (bool, Skiplist.remove d i)
+    | Mem i -> Res (bool, Skiplist.mem d i)
+
+  let postcond c (s : state) res =
+    match (c, res) with
+    | Add i, Res ((Bool, _), res) -> Sint.mem i s = not res
+    | Remove i, Res ((Bool, _), res) -> Sint.mem i s = res
+    | Mem i, Res ((Bool, _), res) -> Sint.mem i s = res
+    | _, _ -> false
+end
+
+module WSDT_seq = STM_sequential.Make (WSDConf)
+module WSDT_dom = STM_domain.Make (WSDConf)
+
+let () =
+  let count = 1000 in
+  QCheck_base_runner.run_tests_main
+    [
+      WSDT_seq.agree_test ~count ~name:"STM Lockfree.Skiplist test sequential";
+      WSDT_dom.agree_test_par ~count ~name:"STM Lockfree.Skiplist test parallel";
+       ]

From ad8782afc1d7149fe90dcf14c96da530753831b9 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 27 Jun 2023 17:48:47 +0200
Subject: [PATCH 3/9] Renaming atomicskiplist to skiplist

---
 ...h_atomic_skiplist.ml => bench_skiplist.ml} |  8 +--
 bench/main.ml                                 |  6 +--
 src/{atomicskiplist.ml => skiplist.ml}        |  2 +-
 src/{atomicskiplist.mli => skiplist.mli}      |  0
 src_lockfree/saturn_lockfree.ml               |  2 +-
 src_lockfree/saturn_lockfree.mli              |  2 +-
 test/atomicskiplist/dune                      | 22 --------
 test/skiplist/dune                            | 22 ++++++++
 .../qcheck_skiplist.ml}                       | 53 +++++++++----------
 .../skiplist_dscheck.ml}                      |  4 +-
 .../stm_skiplist.ml}                          | 14 ++---
 11 files changed, 66 insertions(+), 69 deletions(-)
 rename bench/{bench_atomic_skiplist.ml => bench_skiplist.ml} (88%)
 rename src/{atomicskiplist.ml => skiplist.ml} (99%)
 rename src/{atomicskiplist.mli => skiplist.mli} (100%)
 delete mode 100644 test/atomicskiplist/dune
 create mode 100644 test/skiplist/dune
 rename test/{atomicskiplist/qcheck_atomic_skiplist.ml => skiplist/qcheck_skiplist.ml} (75%)
 rename test/{atomicskiplist/atomic_skiplist_dscheck.ml => skiplist/skiplist_dscheck.ml} (96%)
 rename test/{atomicskiplist/stm_atomicskiplist.ml => skiplist/stm_skiplist.ml} (88%)

diff --git a/bench/bench_atomic_skiplist.ml b/bench/bench_skiplist.ml
similarity index 88%
rename from bench/bench_atomic_skiplist.ml
rename to bench/bench_skiplist.ml
index 111fe27c..70cde512 100644
--- a/bench/bench_atomic_skiplist.ml
+++ b/bench/bench_skiplist.ml
@@ -1,7 +1,7 @@
 open Lockfree
 
 let workload num_elems num_threads add remove =
-  let sl = Atomicskiplist.create () in
+  let sl = Skiplist.create () in
   let elems = Array.init num_elems (fun _ -> Random.int 10000) in
   let push () =
     Domain.spawn (fun () ->
@@ -9,10 +9,10 @@ let workload num_elems num_threads add remove =
         for i = 0 to (num_elems - 1) / num_threads do
           Domain.cpu_relax ();
           let prob = Random.float 1.0 in
-          if prob < add then Atomicskiplist.add sl (Random.int 10000) |> ignore
+          if prob < add then Skiplist.add sl (Random.int 10000) |> ignore
           else if prob >= add && prob < add +. remove then
-            Atomicskiplist.remove sl (Random.int 10000) |> ignore
-          else Atomicskiplist.mem sl elems.(i) |> ignore
+            Skiplist.remove sl (Random.int 10000) |> ignore
+          else Skiplist.mem sl elems.(i) |> ignore
         done;
         start_time)
   in
diff --git a/bench/main.ml b/bench/main.ml
index ab536444..ecae2a54 100644
--- a/bench/main.ml
+++ b/bench/main.ml
@@ -16,10 +16,10 @@ let benchmark_list =
     Mpmc_queue.bench ~use_cas:true ~takers:4 ~pushers:4;
     Mpmc_queue.bench ~use_cas:true ~takers:1 ~pushers:8;
     Mpmc_queue.bench ~use_cas:true ~takers:8 ~pushers:1;
-    Bench_atomic_skiplist.bench ~workload_type:"read_heavy" ~num_elems:2000000
+    Bench_skiplist.bench ~workload_type:"read_heavy" ~num_elems:2000000
+      ~num_threads:2;
+    Bench_skiplist.bench ~workload_type:"moderate_heavy" ~num_elems:2000000
       ~num_threads:2;
-    Bench_atomic_skiplist.bench ~workload_type:"moderate_heavy"
-      ~num_elems:2000000 ~num_threads:2;
   ]
   @ backoff_benchmarks
 
diff --git a/src/atomicskiplist.ml b/src/skiplist.ml
similarity index 99%
rename from src/atomicskiplist.ml
rename to src/skiplist.ml
index 3c6e35af..b81e806e 100644
--- a/src/atomicskiplist.ml
+++ b/src/skiplist.ml
@@ -31,7 +31,7 @@ let get_random_level sl =
   count_level 1
 
 (** Create a new skiplist *)
-let create ?(max_height=10) () =
+let create ?(max_height = 10) () =
   let tail = create_new_node Int.max_int max_height in
   let next =
     Array.init (max_height + 1) (fun _ ->
diff --git a/src/atomicskiplist.mli b/src/skiplist.mli
similarity index 100%
rename from src/atomicskiplist.mli
rename to src/skiplist.mli
diff --git a/src_lockfree/saturn_lockfree.ml b/src_lockfree/saturn_lockfree.ml
index 449eb385..35795c3f 100644
--- a/src_lockfree/saturn_lockfree.ml
+++ b/src_lockfree/saturn_lockfree.ml
@@ -33,4 +33,4 @@ module Single_prod_single_cons_queue = Spsc_queue
 module Single_consumer_queue = Mpsc_queue
 module Relaxed_queue = Mpmc_relaxed_queue
 module Backoff = Backoff
-module Atomicskiplist = Atomicskiplist
+module Skiplist = Skiplist
diff --git a/src_lockfree/saturn_lockfree.mli b/src_lockfree/saturn_lockfree.mli
index 032d323b..c0a59720 100644
--- a/src_lockfree/saturn_lockfree.mli
+++ b/src_lockfree/saturn_lockfree.mli
@@ -40,4 +40,4 @@ module Relaxed_queue = Mpmc_relaxed_queue
 (** {2 Other} *)
 
 module Backoff = Backoff
-module Atomicskiplist = Atomicskiplist
+module Skiplist = Skiplist
diff --git a/test/atomicskiplist/dune b/test/atomicskiplist/dune
deleted file mode 100644
index 0dadbae8..00000000
--- a/test/atomicskiplist/dune
+++ /dev/null
@@ -1,22 +0,0 @@
-(rule
- (copy ../../src/backoff.ml backoff.ml))
-
-(rule
- (copy ../../src/atomicskiplist.ml atomicskiplist.ml))
-
-(test
- (name atomic_skiplist_dscheck)
- (libraries atomic dscheck alcotest)
- (modules atomicskiplist atomic_skiplist_dscheck))
-
-(test
- (name qcheck_atomic_skiplist)
- (libraries lockfree qcheck qcheck-alcotest)
- (modules qcheck_atomic_skiplist))
-
-(test
- (name stm_atomicskiplist)
- (modules stm_atomicskiplist)
- (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
- (action
-  (run %{test} --verbose)))
\ No newline at end of file
diff --git a/test/skiplist/dune b/test/skiplist/dune
new file mode 100644
index 00000000..1a75d05f
--- /dev/null
+++ b/test/skiplist/dune
@@ -0,0 +1,22 @@
+(rule
+ (copy ../../src/backoff.ml backoff.ml))
+
+(rule
+ (copy ../../src/skiplist.ml skiplist.ml))
+
+(test
+ (name skiplist_dscheck)
+ (libraries atomic dscheck alcotest)
+ (modules skiplist skiplist_dscheck))
+
+(test
+ (name qcheck_skiplist)
+ (libraries lockfree qcheck qcheck-alcotest)
+ (modules qcheck_skiplist))
+
+(test
+ (name stm_skiplist)
+ (modules stm_skiplist)
+ (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))
diff --git a/test/atomicskiplist/qcheck_atomic_skiplist.ml b/test/skiplist/qcheck_skiplist.ml
similarity index 75%
rename from test/atomicskiplist/qcheck_atomic_skiplist.ml
rename to test/skiplist/qcheck_skiplist.ml
index 9e55f102..484bdeac 100644
--- a/test/atomicskiplist/qcheck_atomic_skiplist.ml
+++ b/test/skiplist/qcheck_skiplist.ml
@@ -1,4 +1,4 @@
-module Atomicskiplist = Lockfree.Atomicskiplist
+module Skiplist = Lockfree.Skiplist
 
 let tests_sequential =
   QCheck.
@@ -6,23 +6,22 @@ let tests_sequential =
       (* TEST 1: add*)
       Test.make ~name:"add" (list int) (fun lpush ->
           assume (lpush <> []);
-          let sl = Atomicskiplist.create () in
+          let sl = Skiplist.create () in
           let rec add_all_elems l =
             match l with
-            | h :: t ->
-                if Atomicskiplist.add sl h then add_all_elems t else false
+            | h :: t -> if Skiplist.add sl h then add_all_elems t else false
             | [] -> true
           in
           add_all_elems lpush);
       (*TEST 2: add_remove*)
       Test.make ~name:"add_remove" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
-          let sl = Atomicskiplist.create () in
-          List.iter (fun key -> ignore (Atomicskiplist.add sl key)) lpush;
+          let sl = Skiplist.create () in
+          List.iter (fun key -> ignore (Skiplist.add sl key)) lpush;
           let rec remove_all_elems l =
             match l with
             | h :: t ->
-                if Atomicskiplist.remove sl h then remove_all_elems t else false
+                if Skiplist.remove sl h then remove_all_elems t else false
             | [] -> true
           in
           remove_all_elems lpush);
@@ -30,21 +29,20 @@ let tests_sequential =
       Test.make ~name:"add_find" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
           let lpush = Array.of_list lpush in
-          let sl = Atomicskiplist.create () in
+          let sl = Skiplist.create () in
           let len = Array.length lpush in
           let pos = Array.sub lpush 0 (len / 2) in
           let neg = Array.sub lpush (len / 2) (len / 2) in
-          Array.iter (fun key -> ignore @@ Atomicskiplist.add sl key) pos;
+          Array.iter (fun key -> ignore @@ Skiplist.add sl key) pos;
           let rec check_pos index =
             if index < len / 2 then
-              if Atomicskiplist.mem sl pos.(index) then check_pos (index + 1)
+              if Skiplist.mem sl pos.(index) then check_pos (index + 1)
               else false
             else true
           in
           let rec check_neg index =
             if index < len / 2 then
-              if not @@ Atomicskiplist.mem sl neg.(index) then
-                check_neg (index + 1)
+              if not @@ Skiplist.mem sl neg.(index) then check_neg (index + 1)
               else false
             else true
           in
@@ -52,14 +50,13 @@ let tests_sequential =
       (* TEST 4: add_remove_find *)
       Test.make ~name:"add_remove_find" (list int) (fun lpush ->
           let lpush = List.sort_uniq Int.compare lpush in
-          let sl = Atomicskiplist.create () in
-          List.iter (fun key -> ignore @@ Atomicskiplist.add sl key) lpush;
-          List.iter (fun key -> ignore @@ Atomicskiplist.remove sl key) lpush;
+          let sl = Skiplist.create () in
+          List.iter (fun key -> ignore @@ Skiplist.add sl key) lpush;
+          List.iter (fun key -> ignore @@ Skiplist.remove sl key) lpush;
           let rec not_find_all_elems l =
             match l with
             | h :: t ->
-                if not @@ Atomicskiplist.mem sl h then not_find_all_elems t
-                else false
+                if not @@ Skiplist.mem sl h then not_find_all_elems t else false
             | [] -> true
           in
 
@@ -72,14 +69,14 @@ let tests_two_domains =
       (* TEST 1: Two domains doing multiple adds *)
       Test.make ~name:"parallel_add" (pair small_nat small_nat)
         (fun (npush1, npush2) ->
-          let sl = Atomicskiplist.create () in
+          let sl = Skiplist.create () in
           let sema = Semaphore.Binary.make false in
           let lpush1 = List.init npush1 (fun i -> i) in
           let lpush2 = List.init npush2 (fun i -> i + npush1) in
           let work lpush =
             List.map
               (fun elt ->
-                let completed = Atomicskiplist.add sl elt in
+                let completed = Skiplist.add sl elt in
                 Domain.cpu_relax ();
                 completed)
               lpush
@@ -107,7 +104,7 @@ let tests_two_domains =
       (* TEST 2: Two domains doing multiple one push and one pop in parallel *)
       Test.make ~count:10000 ~name:"parallel_add_remove"
         (pair small_nat small_nat) (fun (npush1, npush2) ->
-          let sl = Atomicskiplist.create () in
+          let sl = Skiplist.create () in
           let sema = Semaphore.Binary.make false in
 
           let lpush1 = List.init npush1 (fun i -> i) in
@@ -116,9 +113,9 @@ let tests_two_domains =
           let work lpush =
             List.map
               (fun elt ->
-                ignore @@ Atomicskiplist.add sl elt;
+                ignore @@ Skiplist.add sl elt;
                 Domain.cpu_relax ();
-                Atomicskiplist.remove sl elt)
+                Skiplist.remove sl elt)
               lpush
           in
 
@@ -138,17 +135,17 @@ let tests_two_domains =
           let rec check_none_present l =
             match l with
             | h :: t ->
-                if Atomicskiplist.mem sl h then false else check_none_present t
+                if Skiplist.mem sl h then false else check_none_present t
             | [] -> true
           in
           check_none_present lpush1 && check_none_present lpush2);
       (* TEST 3: Parallel push and pop using the same elements in two domains
  *)
       Test.make ~name:"parallel_add_remove_same_list" (list int) (fun lpush ->
-          let sl = Atomicskiplist.create () in
+          let sl = Skiplist.create () in
           let sema = Semaphore.Binary.make false in
-          let add_all_elems l = List.map (Atomicskiplist.add sl) l in
-          let remove_all_elems l = List.map (Atomicskiplist.remove sl) l in
+          let add_all_elems l = List.map (Skiplist.add sl) l in
+          let remove_all_elems l = List.map (Skiplist.remove sl) l in
 
           let domain1 =
             Domain.spawn (fun () ->
@@ -170,7 +167,7 @@ let tests_two_domains =
           let rec check_none_present l =
             match l with
             | h :: t ->
-                if Atomicskiplist.mem sl h then false else check_none_present t
+                if Skiplist.mem sl h then false else check_none_present t
             | [] -> true
           in
           check_none_present lpush);
@@ -178,7 +175,7 @@ let tests_two_domains =
 
 let () =
   let to_alcotest = List.map QCheck_alcotest.to_alcotest in
-  Alcotest.run "Atomic Skip List"
+  Alcotest.run "Skip List"
     [
       ("test_sequential", to_alcotest tests_sequential);
       ("tests_two_domains", to_alcotest tests_two_domains);
diff --git a/test/atomicskiplist/atomic_skiplist_dscheck.ml b/test/skiplist/skiplist_dscheck.ml
similarity index 96%
rename from test/atomicskiplist/atomic_skiplist_dscheck.ml
rename to test/skiplist/skiplist_dscheck.ml
index a3eb521b..e620dcd3 100644
--- a/test/atomicskiplist/atomic_skiplist_dscheck.ml
+++ b/test/skiplist/skiplist_dscheck.ml
@@ -1,4 +1,4 @@
-open Atomicskiplist
+open Skiplist
 
 let _two_mem () =
   Atomic.trace (fun () ->
@@ -80,7 +80,7 @@ let _two_remove () =
       Atomic.final (fun () ->
           Atomic.check (fun () ->
               let found1 = mem sl 1 in
-              !added1 && !removed1 && not !removed2 && not found1)))
+              !added1 && !removed1 && (not !removed2) && not found1)))
 
 let () =
   let open Alcotest in
diff --git a/test/atomicskiplist/stm_atomicskiplist.ml b/test/skiplist/stm_skiplist.ml
similarity index 88%
rename from test/atomicskiplist/stm_atomicskiplist.ml
rename to test/skiplist/stm_skiplist.ml
index ce4054fc..50d96da5 100644
--- a/test/atomicskiplist/stm_atomicskiplist.ml
+++ b/test/skiplist/stm_skiplist.ml
@@ -2,7 +2,7 @@
 
 open QCheck
 open STM
-module Skiplist = Lockfree.Atomicskiplist
+module Skiplist = Lockfree.Skiplist
 
 module WSDConf = struct
   type cmd = Mem of int | Add of int | Remove of int
@@ -13,11 +13,11 @@ module WSDConf = struct
     | Add i -> "Add " ^ string_of_int i
     | Remove i -> "Remove " ^ string_of_int i
 
-  module Sint = Set.Make (
-                    struct
-                      type t = int
-                      let compare = compare
-                    end)
+  module Sint = Set.Make (struct
+    type t = int
+
+    let compare = compare
+  end)
 
   type state = Sint.t
   type sut = Skiplist.t
@@ -67,4 +67,4 @@ let () =
     [
       WSDT_seq.agree_test ~count ~name:"STM Lockfree.Skiplist test sequential";
       WSDT_dom.agree_test_par ~count ~name:"STM Lockfree.Skiplist test parallel";
-       ]
+    ]

From 1d49325578e4cf89e71c8cf9f619816c3a7b607b Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 24 Oct 2023 15:03:44 +0200
Subject: [PATCH 4/9] Merge with main.

---
 bench/bench_skiplist.ml            | 2 +-
 src/saturn.ml                      | 3 +++
 src/saturn.mli                     | 4 +++-
 src_lockfree/saturn_lockfree.ml    | 3 ++-
 src_lockfree/saturn_lockfree.mli   | 2 +-
 {src => src_lockfree}/skiplist.ml  | 0
 {src => src_lockfree}/skiplist.mli | 0
 test/skiplist/dune                 | 8 ++++----
 test/skiplist/qcheck_skiplist.ml   | 2 +-
 test/skiplist/stm_skiplist.ml      | 2 +-
 10 files changed, 16 insertions(+), 10 deletions(-)
 rename {src => src_lockfree}/skiplist.ml (100%)
 rename {src => src_lockfree}/skiplist.mli (100%)

diff --git a/bench/bench_skiplist.ml b/bench/bench_skiplist.ml
index 70cde512..285dc450 100644
--- a/bench/bench_skiplist.ml
+++ b/bench/bench_skiplist.ml
@@ -1,4 +1,4 @@
-open Lockfree
+open Saturn
 
 let workload num_elems num_threads add remove =
   let sl = Skiplist.create () in
diff --git a/src/saturn.ml b/src/saturn.ml
index d3b71e46..5ac904f4 100644
--- a/src/saturn.ml
+++ b/src/saturn.ml
@@ -35,4 +35,7 @@ module Single_prod_single_cons_queue =
 
 module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
+module Skiplist = Saturn_lockfree.Skiplist
+
+
 module Backoff = Saturn_lockfree.Backoff
diff --git a/src/saturn.mli b/src/saturn.mli
index 1a9d56f5..e05f38bf 100644
--- a/src/saturn.mli
+++ b/src/saturn.mli
@@ -40,5 +40,7 @@ module Single_prod_single_cons_queue =
 module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
 
-module Backoff = Saturn_lockfree.Backoff
+module Skiplist = Saturn_lockfree.Skiplist
+
 (** {2 Other} *)
+module Backoff = Saturn_lockfree.Backoff
diff --git a/src_lockfree/saturn_lockfree.ml b/src_lockfree/saturn_lockfree.ml
index 35795c3f..8e76bc86 100644
--- a/src_lockfree/saturn_lockfree.ml
+++ b/src_lockfree/saturn_lockfree.ml
@@ -32,5 +32,6 @@ module Work_stealing_deque = Ws_deque
 module Single_prod_single_cons_queue = Spsc_queue
 module Single_consumer_queue = Mpsc_queue
 module Relaxed_queue = Mpmc_relaxed_queue
-module Backoff = Backoff
 module Skiplist = Skiplist
+
+module Backoff = Backoff
diff --git a/src_lockfree/saturn_lockfree.mli b/src_lockfree/saturn_lockfree.mli
index c0a59720..683eb6a9 100644
--- a/src_lockfree/saturn_lockfree.mli
+++ b/src_lockfree/saturn_lockfree.mli
@@ -36,8 +36,8 @@ module Work_stealing_deque = Ws_deque
 module Single_prod_single_cons_queue = Spsc_queue
 module Single_consumer_queue = Mpsc_queue
 module Relaxed_queue = Mpmc_relaxed_queue
+module Skiplist = Skiplist
 
 (** {2 Other} *)
 
 module Backoff = Backoff
-module Skiplist = Skiplist
diff --git a/src/skiplist.ml b/src_lockfree/skiplist.ml
similarity index 100%
rename from src/skiplist.ml
rename to src_lockfree/skiplist.ml
diff --git a/src/skiplist.mli b/src_lockfree/skiplist.mli
similarity index 100%
rename from src/skiplist.mli
rename to src_lockfree/skiplist.mli
diff --git a/test/skiplist/dune b/test/skiplist/dune
index 1a75d05f..3ffaa883 100644
--- a/test/skiplist/dune
+++ b/test/skiplist/dune
@@ -1,8 +1,8 @@
 (rule
- (copy ../../src/backoff.ml backoff.ml))
+ (copy ../../src_lockfree/backoff.ml backoff.ml))
 
 (rule
- (copy ../../src/skiplist.ml skiplist.ml))
+ (copy ../../src_lockfree/skiplist.ml skiplist.ml))
 
 (test
  (name skiplist_dscheck)
@@ -11,12 +11,12 @@
 
 (test
  (name qcheck_skiplist)
- (libraries lockfree qcheck qcheck-alcotest)
+ (libraries saturn qcheck qcheck-alcotest)
  (modules qcheck_skiplist))
 
 (test
  (name stm_skiplist)
  (modules stm_skiplist)
- (libraries lockfree qcheck-stm.sequential qcheck-stm.domain)
+ (libraries saturn qcheck-stm.sequential qcheck-stm.domain)
  (action
   (run %{test} --verbose)))
diff --git a/test/skiplist/qcheck_skiplist.ml b/test/skiplist/qcheck_skiplist.ml
index 484bdeac..94b65f81 100644
--- a/test/skiplist/qcheck_skiplist.ml
+++ b/test/skiplist/qcheck_skiplist.ml
@@ -1,4 +1,4 @@
-module Skiplist = Lockfree.Skiplist
+module Skiplist = Saturn.Skiplist
 
 let tests_sequential =
   QCheck.
diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml
index 50d96da5..7e6619b7 100644
--- a/test/skiplist/stm_skiplist.ml
+++ b/test/skiplist/stm_skiplist.ml
@@ -2,7 +2,7 @@
 
 open QCheck
 open STM
-module Skiplist = Lockfree.Skiplist
+module Skiplist = Saturn.Skiplist
 
 module WSDConf = struct
   type cmd = Mem of int | Add of int | Remove of int

From dcf3df2ebd607fc991c1c4dfe5292fb3d685d170 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 7 Nov 2023 17:52:51 +0100
Subject: [PATCH 5/9] Make skiplist polymorphic.

---
 src_lockfree/skiplist.ml      | 42 +++++++++++++++++++++--------------
 src_lockfree/skiplist.mli     | 10 ++++-----
 test/skiplist/stm_skiplist.ml |  2 +-
 3 files changed, 31 insertions(+), 23 deletions(-)

diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml
index b81e806e..c264402f 100644
--- a/src_lockfree/skiplist.ml
+++ b/src_lockfree/skiplist.ml
@@ -1,29 +1,34 @@
-type markable_reference = { node : node; marked : bool }
+type 'a markable_reference = { node : 'a node; marked : bool }
 (** markable reference: stores a reference to a node and has a field to specify if it is marked *)
 
-and node = { key : int; height : int; next : markable_reference Atomic.t array }
+and 'a node = {
+  key : 'a;
+  height : int;
+  next : 'a markable_reference Atomic.t array;
+}
 
 exception Failed_snip
 
-type t = { head : node; max_height : int }
+type 'a t = { head : 'a node; max_height : int }
 
-let null_node = { key = Int.max_int; height = 0; next = [||] }
+let min = Obj.new_block 5 5 |> Obj.obj
+let max = Obj.new_block 5 5 |> Obj.obj
+let null_node = { key = max; height = 0; next = [||] }
+
+(** create_dummy_node_array: Creates a new array with the different node for each index *)
+let[@inline] create_dummy_node_array sl =
+  Array.make (sl.max_height + 1) null_node
 
 (** create_new_node: creates a new node with some value and height *)
-let create_new_node value height =
+let[@inline] create_new_node value height =
   let next =
     Array.init (height + 1) (fun _ ->
         Atomic.make { node = null_node; marked = false })
   in
   { key = value; height; next }
 
-(** create_dummy_node_array: Creates a new array with the different node for each index *)
-let create_dummy_node_array sl =
-  let arr = Array.make (sl.max_height + 1) null_node in
-  arr
-
 (** Get a random level from 1 till max_height (both included) *)
-let get_random_level sl =
+let[@inline] get_random_level sl =
   let rec count_level cur_level =
     if cur_level == sl.max_height || Random.bool () then cur_level
     else count_level (cur_level + 1)
@@ -32,12 +37,12 @@ let get_random_level sl =
 
 (** Create a new skiplist *)
 let create ?(max_height = 10) () =
-  let tail = create_new_node Int.max_int max_height in
+  let tail = create_new_node max max_height in
   let next =
     Array.init (max_height + 1) (fun _ ->
         Atomic.make { node = tail; marked = false })
   in
-  let head = { key = Int.min_int; height = max_height; next } in
+  let head = { key = min; height = max_height; next } in
   { head; max_height }
 
 (** Compares old_node and old_mark with the atomic reference and if they are the same then
@@ -68,7 +73,7 @@ let find_in (key, preds, succs, sl) =
         let { node = curr; marked = _ } = Atomic.get prev.next.(level) in
         let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
         iterate (prev, curr, succ, mark, level)
-    else if curr.key < key then
+    else if curr.key != max && curr.key < key then
       let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
       iterate (curr, succ, new_succ, mark, level)
     else (prev, curr)
@@ -80,7 +85,9 @@ let find_in (key, preds, succs, sl) =
       let prev, curr = iterate (prev, curr, succ, mark, level) in
       preds.(level) <- prev;
       succs.(level) <- curr;
-      if level > 0 then update_arrays prev (level - 1) else curr.key == key
+      if level > 0 then update_arrays prev (level - 1)
+      else if curr.key == max then false
+      else curr.key = key
     with Failed_snip -> update_arrays head sl.max_height
   in
   update_arrays head sl.max_height
@@ -137,7 +144,7 @@ let mem sl key =
       let curr = succ in
       let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
       search (pred, curr, succ, mark, level)
-    else if curr.key < key then
+    else if curr.key != max && curr.key < key then
       let pred = curr in
       let curr = succ in
       let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
@@ -147,7 +154,8 @@ let mem sl key =
       let { node = curr; marked = _ } = Atomic.get pred.next.(level) in
       let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
       search (pred, curr, succ, mark, level)
-    else curr.key == key
+    else if curr.key == max then false
+    else curr.key = key
   in
   let pred = sl.head in
   let { node = curr; marked = _ } = Atomic.get pred.next.(sl.max_height) in
diff --git a/src_lockfree/skiplist.mli b/src_lockfree/skiplist.mli
index 3a07487b..36e1294d 100644
--- a/src_lockfree/skiplist.mli
+++ b/src_lockfree/skiplist.mli
@@ -1,6 +1,6 @@
-type t
+type 'a t
 
-val create : ?max_height:int -> unit -> t
-val mem : t -> int -> bool
-val add : t -> int -> bool
-val remove : t -> int -> bool
+val create : ?max_height:int -> unit -> 'a t
+val mem : 'a t -> 'a -> bool
+val add : 'a t -> 'a -> bool
+val remove : 'a t -> 'a -> bool
diff --git a/test/skiplist/stm_skiplist.ml b/test/skiplist/stm_skiplist.ml
index 7e6619b7..0831c4c9 100644
--- a/test/skiplist/stm_skiplist.ml
+++ b/test/skiplist/stm_skiplist.ml
@@ -20,7 +20,7 @@ module WSDConf = struct
   end)
 
   type state = Sint.t
-  type sut = Skiplist.t
+  type sut = int Skiplist.t
 
   let arb_cmd _s =
     let int_gen = Gen.nat in

From f7339444e6e0fd6af61c2484f3e64d164048c354 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Tue, 7 Nov 2023 18:42:36 +0100
Subject: [PATCH 6/9] Debug level issues.

---
 src_lockfree/skiplist.ml          | 21 +++++++++++----------
 test/skiplist/skiplist_dscheck.ml |  8 ++++----
 2 files changed, 15 insertions(+), 14 deletions(-)

diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml
index c264402f..78772596 100644
--- a/src_lockfree/skiplist.ml
+++ b/src_lockfree/skiplist.ml
@@ -27,23 +27,24 @@ let[@inline] create_new_node value height =
   in
   { key = value; height; next }
 
-(** Get a random level from 1 till max_height (both included) *)
+(** Get a random level from 0 till max_height - 1 *)
 let[@inline] get_random_level sl =
   let rec count_level cur_level =
-    if cur_level == sl.max_height || Random.bool () then cur_level
+    if  Random.bool () then cur_level
+    else if cur_level == sl.max_height then count_level 0
     else count_level (cur_level + 1)
   in
-  count_level 1
+  if sl.max_height = 0 then 0 else count_level 0
 
 (** Create a new skiplist *)
 let create ?(max_height = 10) () =
-  let tail = create_new_node max max_height in
+  let max_height = Int.max max_height 1 in
+  let tail = create_new_node max (max_height - 1) in
   let next =
-    Array.init (max_height + 1) (fun _ ->
-        Atomic.make { node = tail; marked = false })
+    Array.init max_height (fun _ -> Atomic.make { node = tail; marked = false })
   in
-  let head = { key = min; height = max_height; next } in
-  { head; max_height }
+  let head = { key = min; height = max_height - 1; next } in
+  { head; max_height = max_height - 1 }
 
 (** Compares old_node and old_mark with the atomic reference and if they are the same then
     Replaces the value in the atomic with node and mark *)
@@ -132,7 +133,7 @@ let add sl key =
           set_next ();
           if level < top_level then update_levels (level + 1)
         in
-        update_levels 1;
+        if top_level > 0 then update_levels 1;
         true
   in
   repeat ()
@@ -199,6 +200,6 @@ let remove sl key =
       else if mark then false
       else update_bottom_level succ
     in
-    update_upper_levels nodeHeight;
+    if nodeHeight > 0 then update_upper_levels nodeHeight;
     let { node = succ; marked = _ } = Atomic.get nodeToRemove.next.(0) in
     update_bottom_level succ
diff --git a/test/skiplist/skiplist_dscheck.ml b/test/skiplist/skiplist_dscheck.ml
index e620dcd3..283ced0e 100644
--- a/test/skiplist/skiplist_dscheck.ml
+++ b/test/skiplist/skiplist_dscheck.ml
@@ -20,7 +20,7 @@ let _two_mem () =
 let _two_add () =
   Atomic.trace (fun () ->
       Random.init 0;
-      let sl = create ~max_height:2 () in
+      let sl = create ~max_height:3 () in
       let added1 = ref false in
       let added2 = ref false in
 
@@ -33,7 +33,7 @@ let _two_add () =
 let _two_add_same () =
   Atomic.trace (fun () ->
       Random.init 0;
-      let sl = create ~max_height:2 () in
+      let sl = create ~max_height:3 () in
       let added1 = ref false in
       let added2 = ref false in
 
@@ -48,7 +48,7 @@ let _two_add_same () =
 let _two_remove_same () =
   Atomic.trace (fun () ->
       Random.init 0;
-      let sl = create ~max_height:1 () in
+      let sl = create ~max_height:2 () in
       let added1 = ref false in
       let removed1 = ref false in
       let removed2 = ref false in
@@ -67,7 +67,7 @@ let _two_remove_same () =
 let _two_remove () =
   Atomic.trace (fun () ->
       Random.init 0;
-      let sl = create ~max_height:1 () in
+      let sl = create ~max_height:2 () in
       let added1 = ref false in
       let removed1 = ref false in
       let removed2 = ref false in

From 6eb5303289e9835962ecb89b0d2477fc2d44d762 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Wed, 8 Nov 2023 18:52:51 +0100
Subject: [PATCH 7/9] Cleanup and documentation.

---
 src_lockfree/skiplist.ml  | 20 ++++++--------------
 src_lockfree/skiplist.mli | 20 +++++++++++++++++++-
 2 files changed, 25 insertions(+), 15 deletions(-)

diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml
index 78772596..8c4494be 100644
--- a/src_lockfree/skiplist.ml
+++ b/src_lockfree/skiplist.ml
@@ -1,5 +1,4 @@
 type 'a markable_reference = { node : 'a node; marked : bool }
-(** markable reference: stores a reference to a node and has a field to specify if it is marked *)
 
 and 'a node = {
   key : 'a;
@@ -15,11 +14,9 @@ let min = Obj.new_block 5 5 |> Obj.obj
 let max = Obj.new_block 5 5 |> Obj.obj
 let null_node = { key = max; height = 0; next = [||] }
 
-(** create_dummy_node_array: Creates a new array with the different node for each index *)
 let[@inline] create_dummy_node_array sl =
   Array.make (sl.max_height + 1) null_node
 
-(** create_new_node: creates a new node with some value and height *)
 let[@inline] create_new_node value height =
   let next =
     Array.init (height + 1) (fun _ ->
@@ -27,16 +24,14 @@ let[@inline] create_new_node value height =
   in
   { key = value; height; next }
 
-(** Get a random level from 0 till max_height - 1 *)
 let[@inline] get_random_level sl =
   let rec count_level cur_level =
-    if  Random.bool () then cur_level
+    if Random.bool () then cur_level
     else if cur_level == sl.max_height then count_level 0
     else count_level (cur_level + 1)
   in
   if sl.max_height = 0 then 0 else count_level 0
 
-(** Create a new skiplist *)
 let create ?(max_height = 10) () =
   let max_height = Int.max max_height 1 in
   let tail = create_new_node max (max_height - 1) in
@@ -49,13 +44,12 @@ let create ?(max_height = 10) () =
 (** Compares old_node and old_mark with the atomic reference and if they are the same then
     Replaces the value in the atomic with node and mark *)
 let compare_and_set_mark_ref (atomic, old_node, old_mark, node, mark) =
-  let current = Atomic.get atomic in
-  let set_mark_ref () =
-    Atomic.compare_and_set atomic current { node; marked = mark }
+  let ({ node = current_node; marked = current_marked } as current) =
+    Atomic.get atomic
   in
-  let current_node = current.node in
-  current_node == old_node && current.marked = old_mark
-  && ((current_node == node && current.marked = mark) || set_mark_ref ())
+  current_node == old_node && current_marked = old_mark
+  && ((current_node == node && current_marked = mark)
+     || Atomic.compare_and_set atomic current { node; marked = mark })
 
 (** Returns true if key is found within the skiplist else false;
     Irrespective of return value, fills the preds and succs array with
@@ -138,7 +132,6 @@ let add sl key =
   in
   repeat ()
 
-(** Returns true if the key is within the skiplist, else returns false *)
 let mem sl key =
   let rec search (pred, curr, succ, mark, level) =
     if mark then
@@ -163,7 +156,6 @@ let mem sl key =
   let { node = succ; marked = mark } = Atomic.get curr.next.(sl.max_height) in
   search (pred, curr, succ, mark, sl.max_height)
 
-(** Returns true if the removal was successful and returns false if the key is not present within the skiplist *)
 let remove sl key =
   let preds = create_dummy_node_array sl in
   let succs = create_dummy_node_array sl in
diff --git a/src_lockfree/skiplist.mli b/src_lockfree/skiplist.mli
index 36e1294d..bc18575e 100644
--- a/src_lockfree/skiplist.mli
+++ b/src_lockfree/skiplist.mli
@@ -1,6 +1,24 @@
+(** Skiplist TODO
+
+    [key] values are compared with [=] and thus should not be functions or
+    objects.
+*)
+
 type 'a t
+(** The type of lock-free skiplist. *)
 
 val create : ?max_height:int -> unit -> 'a t
-val mem : 'a t -> 'a -> bool
+(** [create ~max_height ()] returns a new empty skiplist. [~max_height] is the
+    number of level used to distribute nodes. Its default value is 10 by default
+    and can not be less than 1. *)
+
 val add : 'a t -> 'a -> bool
+(** [add s v] adds [v] to [s] if [v] is not already in [s] and returns
+    [true]. If [v] is already in [s], it returns [false] and [v] is unchanged. *)
+
 val remove : 'a t -> 'a -> bool
+(** [remove s v] removes [v] of [s] if [v] is in [s] and returns [true]. If [v]
+    is not in [s], it returns [false] and [v] is unchanged. *)
+
+val mem : 'a t -> 'a -> bool
+(** [mem s v] returns [true] if v is in s and [false] otherwise. *)

From 20355ce2151999737abab7e8458dfe7c01e1cb51 Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Thu, 9 Nov 2023 10:28:25 +0100
Subject: [PATCH 8/9] Remove unnecessary Atomic.get

---
 src_lockfree/skiplist.ml | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/src_lockfree/skiplist.ml b/src_lockfree/skiplist.ml
index 8c4494be..936eb82b 100644
--- a/src_lockfree/skiplist.ml
+++ b/src_lockfree/skiplist.ml
@@ -65,9 +65,8 @@ let find_in (key, preds, succs, sl) =
       in
       if not snip then raise Failed_snip
       else
-        let { node = curr; marked = _ } = Atomic.get prev.next.(level) in
-        let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
-        iterate (prev, curr, succ, mark, level)
+        let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
+        iterate (prev, succ, new_succ, mark, level)
     else if curr.key != max && curr.key < key then
       let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
       iterate (curr, succ, new_succ, mark, level)
@@ -135,14 +134,11 @@ let add sl key =
 let mem sl key =
   let rec search (pred, curr, succ, mark, level) =
     if mark then
-      let curr = succ in
-      let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
-      search (pred, curr, succ, mark, level)
+      let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
+      search (pred, succ, new_succ, mark, level)
     else if curr.key != max && curr.key < key then
-      let pred = curr in
-      let curr = succ in
-      let { node = succ; marked = mark } = Atomic.get curr.next.(level) in
-      search (pred, curr, succ, mark, level)
+      let { node = new_succ; marked = mark } = Atomic.get succ.next.(level) in
+      search (curr, succ, new_succ, mark, level)
     else if level > 0 then
       let level = level - 1 in
       let { node = curr; marked = _ } = Atomic.get pred.next.(level) in

From 1aeae3377e395821f9a79f2d4a6f575ef166b9cf Mon Sep 17 00:00:00 2001
From: Carine Morel <carine@tarides.com>
Date: Thu, 9 Nov 2023 10:32:46 +0100
Subject: [PATCH 9/9] Format.

---
 src/saturn.ml                   | 2 --
 src/saturn.mli                  | 3 +--
 src_lockfree/saturn_lockfree.ml | 1 -
 3 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/saturn.ml b/src/saturn.ml
index 5ac904f4..e0f53cad 100644
--- a/src/saturn.ml
+++ b/src/saturn.ml
@@ -36,6 +36,4 @@ module Single_prod_single_cons_queue =
 module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
 module Skiplist = Saturn_lockfree.Skiplist
-
-
 module Backoff = Saturn_lockfree.Backoff
diff --git a/src/saturn.mli b/src/saturn.mli
index e05f38bf..b68db595 100644
--- a/src/saturn.mli
+++ b/src/saturn.mli
@@ -39,8 +39,7 @@ module Single_prod_single_cons_queue =
 
 module Single_consumer_queue = Saturn_lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
-
 module Skiplist = Saturn_lockfree.Skiplist
 
-(** {2 Other} *)
 module Backoff = Saturn_lockfree.Backoff
+(** {2 Other} *)
diff --git a/src_lockfree/saturn_lockfree.ml b/src_lockfree/saturn_lockfree.ml
index 8e76bc86..fcbf4fbf 100644
--- a/src_lockfree/saturn_lockfree.ml
+++ b/src_lockfree/saturn_lockfree.ml
@@ -33,5 +33,4 @@ module Single_prod_single_cons_queue = Spsc_queue
 module Single_consumer_queue = Mpsc_queue
 module Relaxed_queue = Mpmc_relaxed_queue
 module Skiplist = Skiplist
-
 module Backoff = Backoff