From e5f218ae84d6a4751af2b098fdde55c6c4e50b62 Mon Sep 17 00:00:00 2001 From: DeltaCube23 Date: Wed, 12 Jul 2023 15:30:05 +0200 Subject: [PATCH] added files for fine-grained linked list as a set --- src/fine_list.ml | 148 +++++++++++++++++++++++++++++ src/fine_list.mli | 17 ++++ src/saturn.ml | 1 + src/saturn.mli | 1 + test/fine_list/dune | 11 +++ test/fine_list/qcheck_fine_list.ml | 123 ++++++++++++++++++++++++ test/fine_list/stm_fine_list.ml | 87 +++++++++++++++++ 7 files changed, 388 insertions(+) create mode 100644 src/fine_list.ml create mode 100644 src/fine_list.mli create mode 100644 test/fine_list/dune create mode 100644 test/fine_list/qcheck_fine_list.ml create mode 100644 test/fine_list/stm_fine_list.ml diff --git a/src/fine_list.ml b/src/fine_list.ml new file mode 100644 index 00000000..065ee60f --- /dev/null +++ b/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 diff --git a/src/fine_list.mli b/src/fine_list.mli new file mode 100644 index 00000000..d2e0a23b --- /dev/null +++ b/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 *) diff --git a/src/saturn.ml b/src/saturn.ml index a71a9903..ed7ba4bc 100644 --- a/src/saturn.ml +++ b/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 diff --git a/src/saturn.mli b/src/saturn.mli index 7a5aa1fa..2d2f90c1 100644 --- a/src/saturn.mli +++ b/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} *) diff --git a/test/fine_list/dune b/test/fine_list/dune new file mode 100644 index 00000000..d9ef45fa --- /dev/null +++ b/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))) diff --git a/test/fine_list/qcheck_fine_list.ml b/test/fine_list/qcheck_fine_list.ml new file mode 100644 index 00000000..b18a028c --- /dev/null +++ b/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 () diff --git a/test/fine_list/stm_fine_list.ml b/test/fine_list/stm_fine_list.ml new file mode 100644 index 00000000..d405db3b --- /dev/null +++ b/test/fine_list/stm_fine_list.ml @@ -0,0 +1,87 @@ +(** Sequential and Parallel model-based tests of fine_list *) + +open QCheck +open STM +module Fine_list = Saturn.Fine_list + +module FLConf = struct + type cmd = Add of int | Remove of int | Contains of int | Is_empty + + (* possible operations *) + let show_cmd c = + match c with + | Add i -> "Add " ^ string_of_int i + | Remove i -> "Remove " ^ string_of_int i + | Contains i -> "Contains " ^ string_of_int i + | Is_empty -> "Is_empty" + + (* model state and system state *) + type state = int list + type sut = int Fine_list.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 -> Remove i) int_gen; + Gen.map (fun i -> Contains i) int_gen; + Gen.return Is_empty; + ]) + + let init_state = [] + let init_sut () = Fine_list.create 0 + let cleanup _ = () + + (* next stage after performing operation on current state *) + let next_state c s = + match c with + | Add i -> + let rec sortlist l e = + match l with + | [] -> [ e ] + | x :: ys -> + if e = x then x :: ys + else if e < x then e :: x :: ys + else x :: sortlist ys e + in + sortlist s i + | Remove i -> + let rec sortlist l e = + match l with + | [] -> [] + | x :: ys -> if e = x then ys else x :: sortlist ys e + in + sortlist s i + | Contains _ -> s + | Is_empty -> s + + let precond _ _ = true + + let run c d = + match c with + | Add i -> Res (bool, Fine_list.add d i) + | Remove i -> Res (bool, Fine_list.remove d i) + | Contains i -> Res (bool, Fine_list.contains d i) + | Is_empty -> Res (bool, Fine_list.is_empty d) + + let postcond c (s : state) res = + match (c, res) with + | Add ele, Res ((Bool, _), res) -> res = not (List.mem ele s) + | Remove ele, Res ((Bool, _), res) -> res = List.mem ele s + | Contains ele, Res ((Bool, _), res) -> res = List.mem ele s + | Is_empty, Res ((Bool, _), res) -> res = (s = []) + | _, _ -> false +end + +module FL_seq = STM_sequential.Make (FLConf) +module FL_dom = STM_domain.Make (FLConf) + +let () = + let count = 500 in + QCheck_base_runner.run_tests_main + [ + FL_seq.agree_test ~count ~name:"STM Fine_list test sequential"; + FL_dom.agree_test_par ~count ~name:"STM Fine_list test parallel"; + ]