-
Notifications
You must be signed in to change notification settings - Fork 30
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
added files for fine-grained linked list as a set #79
base: main
Are you sure you want to change the base?
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 ( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It is usually best to give the notion of equality over values as a parameter, i.e. there should be something like There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Actually you want |
||
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 | ||
| _ -> | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. You could also use a simple conditional if prev == verify && cur == verify.next then
insert prev
else
... here. This will also be slightly faster, because there is no need to distinguish between |
||
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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hmm... Is the node created here used for something? |
||
in | ||
if !is_tail then ( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Could you avoid allocating a ref cell for the match cur with
| None ->
Mutex.unlock prev.lock;
false
| Some to_find ->
Mutex.lock to_find.lock;
let verify = find_previous_remove t value in
(* ... *) |
||
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 | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I believe the logic around here could be simplified and the equality check can be moved outside of the critical section. Something like this: let verify = find_previous_remove t value in
if prev == verify && cur == verify.next then begin
Mutex.unlock prev.lock;
Mutex.unlock to_find.lock;
to_find.value = value (* better to use user defined equality *)
end
else begin
Mutex.unlock prev.lock;
Mutex.unlock to_find.lock;
let again = find_previous_remove t value in
validate again again.next
end The common prefix of both branches could also be factored out. |
||
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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 *) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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))) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 () |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Hmm... I wonder whether the logic and
add
andremove
could be modified slightly so that only a singlefind_previous
helper would be needed without impacting performance.