added files for fine-grained linked list as a set

src/fine_list.ml

@@ -0,0 +1,148 @@
+type 'a node = { value : 'a; mutable next : 'a node option; lock : Mutex.t }
+type 'a t = { head : 'a node }
+
+let create_node value nextptr =
+  { value; next = nextptr; lock = Mutex.create () }
+
+let create key = { head = create_node key None }
+
+(* find the previous node <= key *)
+let find_previous_add t key =
+  let rec aux prev next =
+    match next with
+    | Some node when node.value > key -> prev
+    | Some node -> aux node node.next
+    | None -> prev
+  in
+  aux t.head t.head.next
+
+(* find the previous node < key *)
+let find_previous_remove t key =
+  let rec aux prev next =
+    match next with
+    | Some node when node.value >= key -> prev
+    | Some node -> aux node node.next
+    | None -> prev
+  in
+  aux t.head t.head.next
+
+(* add new node in correct position *)
+let add t value =
+  (* x will point to the new node after insertion *)
+  let insert x =
+    if x.value = value && not (x == t.head) then (
+      Mutex.unlock x.lock;
+      false)
+    else
+      let new_node = create_node value x.next in
+      x.next <- Some new_node;
+      Mutex.unlock x.lock;
+      true
+  in
+  (* check if prev and cur are still in same position after locking *)
+  let rec validate prev cur =
+    Mutex.lock prev.lock;
+    let verify = find_previous_add t value in
+    let temp = verify.next in
+    match temp with
+    | Some _ when temp == cur && prev == verify -> insert prev
+    | None when cur = None && prev == verify -> insert prev
+    | _ ->
+        Mutex.unlock prev.lock;
+        (*Domain.cpu_relax ();*)
+        let again = find_previous_add t value in
+        validate again again.next
+  in
+  let start = find_previous_add t value in
+  validate start start.next
+
+(* remove node from correct position *)
+let remove t value =
+  let erase x y =
+    if y.value <> value then (
+      Mutex.unlock x.lock;
+      Mutex.unlock y.lock;
+      false)
+    else (
+      x.next <- y.next;
+      Mutex.unlock x.lock;
+      Mutex.unlock y.lock;
+      true)
+  in
+  (* check if prev and cur are still in same position after locking *)
+  let rec validate prev cur =
+    Mutex.lock prev.lock;
+    let is_tail = ref false in
+    (* get the node to remove from cur pointer *)
+    let to_remove =
+      match cur with
+      | Some node -> node
+      | _ ->
+          is_tail := true;
+          create_node value None
+    in
+    if !is_tail then (
+      Mutex.unlock prev.lock;
+      false)
+    else (
+      Mutex.lock to_remove.lock;
+      let verify = find_previous_remove t value in
+      let temp = verify.next in
+      match temp with
+      | Some _ when temp == cur && prev == verify -> erase prev to_remove
+      | None when cur = None && prev == verify -> erase prev to_remove
+      | _ ->
+          Mutex.unlock prev.lock;
+          Mutex.unlock to_remove.lock;
+          (* Domain.cpu_relax (); *)
+          let again = find_previous_remove t value in
+          validate again again.next)
+  in
+  let start = find_previous_remove t value in
+  validate start start.next
+
+(* check if key exists in list *)
+let contains t value =
+  let rec validate prev cur =
+    Mutex.lock prev.lock;
+    let is_tail = ref false in
+    let to_find =
+      match cur with
+      | Some node -> node
+      | _ ->
+          is_tail := true;
+          create_node value None
+    in
+    if !is_tail then (
+      Mutex.unlock prev.lock;
+      false)
+    else (
+      Mutex.lock to_find.lock;
+      let verify = find_previous_remove t value in
+      let temp = verify.next in
+      match temp with
+      | Some _ when temp == cur && prev == verify ->
+          let res = to_find.value = value in
+          Mutex.unlock prev.lock;
+          Mutex.unlock to_find.lock;
+          res
+      | None ->
+          Mutex.unlock prev.lock;
+          Mutex.unlock to_find.lock;
+          false
+      | _ ->
+          Mutex.unlock prev.lock;
+          Mutex.unlock to_find.lock;
+          (* Domain.cpu_relax (); *)
+          let again = find_previous_remove t value in
+          validate again again.next)
+  in
+  let start = find_previous_remove t value in
+  validate start start.next
+
+(* check if list is empty *)
+let is_empty t =
+  Mutex.lock t.head.lock;
+  let empty = t.head.next = None in
+  Mutex.unlock t.head.lock;
+  empty

src/fine_list.mli

@@ -0,0 +1,17 @@
+type 'a t
+(** type of fine-grained linked list based on optimistic locking *)
+
+val create : 'a -> 'a t
+(** new linked list with dummy head *)
+
+val add : 'a t -> 'a -> bool
+(** [list l key] to add a new node to the linkedlist if it already does not exist *)
+
+val remove : 'a t -> 'a -> bool
+(** [list l key] to remove a node from the linkedlist if it exists *)
+
+val contains : 'a t -> 'a -> bool
+(** [list l key] check if the keys exists in the list *)
+
+val is_empty : 'a t -> bool
+(** check if [list] is empty or not *)

src/saturn.ml

@@ -32,4 +32,5 @@ module Work_stealing_deque = Lockfree.Work_stealing_deque
 module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue
 module Single_consumer_queue = Lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
+module Fine_list = Fine_list
 module Backoff = Lockfree.Backoff

src/saturn.mli

@@ -36,6 +36,7 @@ module Work_stealing_deque = Lockfree.Work_stealing_deque
 module Single_prod_single_cons_queue = Lockfree.Single_prod_single_cons_queue
 module Single_consumer_queue = Lockfree.Single_consumer_queue
 module Relaxed_queue = Mpmc_relaxed_queue
+module Fine_list = Fine_list
 
 module Backoff = Lockfree.Backoff
 (** {2 Other} *)

test/fine_list/dune

@@ -0,0 +1,11 @@
+(test
+ (name qcheck_fine_list)
+ (libraries saturn qcheck qcheck-alcotest)
+ (modules qcheck_fine_list))
+
+(test
+ (name stm_fine_list)
+ (modules stm_fine_list)
+ (libraries saturn qcheck-stm.sequential qcheck-stm.domain)
+ (action
+  (run %{test} --verbose)))

test/fine_list/qcheck_fine_list.ml

@@ -0,0 +1,123 @@
+open Saturn
+
+let tests_sequential =
+  QCheck.
+    [
+      (* TEST 1: insert *)
+      Test.make ~name:"push" (list int) (fun lpush ->
+          assume (lpush <> []);
+          (* Building a random list *)
+          let llist = Fine_list.create 0 in
+          List.iter (fun ele -> ignore @@ Fine_list.add llist ele) lpush;
+
+          (* Testing property *)
+          not (Fine_list.is_empty llist));
+      (* TEST 2 - insert, remove until empty *)
+      Test.make ~name:"push_pop_until_empty" (list int) (fun lpush ->
+          (* Building a random list *)
+          let llist = Fine_list.create 0 in
+          List.iter (fun ele -> ignore @@ Fine_list.add llist ele) lpush;
+
+          (* Removing until [is_empty l] is true *)
+          List.iter (fun ele -> ignore @@ Fine_list.remove llist ele) lpush;
+
+          (* Testing property *)
+          Fine_list.is_empty llist);
+    ]
+
+let tests_two_domains =
+  QCheck.
+    [
+      (* TEST 1: insert double *)
+      Test.make ~name:"duplicate add" small_nat (fun len ->
+          let lpush1 = List.init len (fun i -> i + 1) in
+          let lpush2 = List.rev lpush1 in
+          let llist = Fine_list.create 0 in
+          let p1 = ref 0 in
+          let p2 = ref 0 in
+          let producer1 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> if Fine_list.add llist ele then incr p1)
+                  lpush1)
+          in
+          let producer2 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> if Fine_list.add llist ele then incr p2)
+                  lpush2)
+          in
+          Domain.join producer1;
+          Domain.join producer2;
+
+          (* Testing property *)
+          len = !p1 + !p2);
+      (* TEST 2: remove double *)
+      Test.make ~name:"duplicate remove" small_nat (fun len ->
+          let lpush1 = List.init len (fun i -> i + 1) in
+          let lpush2 = List.rev lpush1 in
+          let llist = Fine_list.create 0 in
+          List.iter (fun ele -> ignore @@ Fine_list.add llist ele) lpush1;
+          let c1 = ref 0 in
+          let c2 = ref 0 in
+          let consumer1 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> if Fine_list.remove llist ele then incr c1)
+                  lpush1)
+          in
+          let consumer2 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> if Fine_list.remove llist ele then incr c2)
+                  lpush2)
+          in
+          Domain.join consumer1;
+          Domain.join consumer2;
+
+          (* Testing property *)
+          len = !c1 + !c2);
+      (* TEST 3: parallel add followed by parallel remove *)
+      Test.make ~name:"parallel add remove" small_nat (fun len ->
+          let lpush1 = List.init len (fun i -> i + 1) in
+          let lpush2 = List.init len (fun i -> len + i + 1) in
+          let llist = Fine_list.create 0 in
+          let producer1 =
+            Domain.spawn (fun () ->
+                List.iter (fun ele -> ignore @@ Fine_list.add llist ele) lpush1)
+          in
+          let producer2 =
+            Domain.spawn (fun () ->
+                List.iter (fun ele -> ignore @@ Fine_list.add llist ele) lpush2)
+          in
+          Domain.join producer1;
+          Domain.join producer2;
+
+          let consumer1 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> ignore @@ Fine_list.remove llist ele)
+                  lpush1)
+          in
+          let consumer2 =
+            Domain.spawn (fun () ->
+                List.iter
+                  (fun ele -> ignore @@ Fine_list.remove llist ele)
+                  lpush2)
+          in
+          Domain.join consumer1;
+          Domain.join consumer2;
+          (* Testing property *)
+          Fine_list.is_empty llist);
+    ]
+
+let main () =
+  let to_alcotest = List.map QCheck_alcotest.to_alcotest in
+  Alcotest.run "Fine_list"
+    [
+      ("test_sequential", to_alcotest tests_sequential);
+      ("two_domains", to_alcotest tests_two_domains);
+    ]
+;;
+
+main ()