1+ open Picos_aux_adaptive_backoff
12module Atomic = Multicore_magic. Transparent_atomic
23
3- type 'a t = { head : 'a head Atomic .t ; tail : 'a tail Atomic .t }
4+ type 'a t = {
5+ random_key : int ;
6+ head : 'a head Atomic .t ;
7+ tail : 'a tail Atomic .t ;
8+ }
49
510and ('a, _) tdt =
611 | Cons : {
@@ -27,14 +32,15 @@ and 'a head = H : ('a, [< `Cons | `Head ]) tdt -> 'a head [@@unboxed]
2732and 'a tail = T : ('a, [< `Snoc | `Tail ]) tdt -> 'a tail [@@ unboxed]
2833
2934let create ?padded () =
35+ let random_key = Int64. to_int (Random. bits64 () ) in
3036 let head =
3137 Atomic. make (H (Head { counter = 1 })) |> Multicore_magic. copy_as ?padded
3238 in
3339 let tail =
3440 Atomic. make (T (Tail { counter = 0 ; move = Used }))
3541 |> Multicore_magic. copy_as ?padded
3642 in
37- Multicore_magic. copy_as ?padded { head; tail }
43+ Multicore_magic. copy_as ?padded { random_key; head; tail }
3844
3945let rec rev (suffix : (_, [< `Cons ]) tdt ) = function
4046 | T (Snoc { counter; prefix; value } ) ->
@@ -47,142 +53,164 @@ let rev = function
4753 (Cons { counter; value; suffix = H (Head { counter = counter + 1 }) })
4854 prefix
4955
50- let rec push t value backoff = function
56+ let [@ inline] backoff t =
57+ Adaptive_backoff. once ~random_key: t.random_key ~log_scale: 10
58+
59+ let [@ inline] backoff_unless_alone t =
60+ Adaptive_backoff. once_unless_alone ~random_key: t.random_key ~log_scale: 10
61+
62+ let rec push t value = function
5163 | T (Snoc snoc_r ) as prefix ->
5264 let after = Snoc { counter = snoc_r.counter + 1 ; prefix; value } in
53- if not (Atomic. compare_and_set t.tail prefix (T after)) then
54- let backoff = Backoff. once backoff in
55- push t value backoff (Atomic. fenceless_get t.tail)
65+ if not (Atomic. compare_and_set t.tail prefix (T after)) then begin
66+ backoff t;
67+ push t value (Atomic. fenceless_get t.tail)
68+ end
5669 | T (Tail tail_r ) as prefix -> begin
5770 match tail_r.move with
5871 | Used ->
5972 let after = Snoc { counter = tail_r.counter + 1 ; prefix; value } in
60- if not (Atomic. compare_and_set t.tail prefix (T after)) then
61- let backoff = Backoff. once backoff in
62- push t value backoff (Atomic. fenceless_get t.tail)
73+ if not (Atomic. compare_and_set t.tail prefix (T after)) then begin
74+ backoff t;
75+ push t value (Atomic. fenceless_get t.tail)
76+ end
6377 | Snoc move_r as move ->
64- begin
65- match Atomic. get t.head with
66- | H (Head head_r as head ) when head_r.counter < move_r.counter ->
67- let after = rev move in
68- if
69- Atomic. fenceless_get t.head == H head
70- && Atomic. compare_and_set t.head (H head) (H after)
71- then tail_r.move < - Used
72- | _ -> tail_r.move < - Used
78+ begin match Atomic. get t.head with
79+ | H (Head head_r as head ) when head_r.counter < move_r.counter ->
80+ let after = rev move in
81+ if Atomic. fenceless_get t.head == H head then
82+ if Atomic. compare_and_set t.head (H head) (H after) then
83+ tail_r.move < - Used
84+ else backoff t
85+ | _ -> tail_r.move < - Used
7386 end ;
74- push t value backoff (Atomic. get t.tail)
87+ push t value (Atomic. get t.tail)
7588 end
7689
7790exception Empty
7891
79- let rec pop t backoff = function
92+ let rec pop t = function
8093 | H (Cons cons_r as cons ) ->
8194 if Atomic. compare_and_set t.head (H cons) cons_r.suffix then cons_r.value
82- else
83- let backoff = Backoff. once backoff in
84- pop t backoff (Atomic. fenceless_get t.head)
95+ else begin
96+ backoff t;
97+ pop t (Atomic. fenceless_get t.head)
98+ end
8599 | H (Head head_r as head ) -> begin
86100 match Atomic. get t.tail with
87101 | T (Snoc snoc_r as move ) ->
88102 if head_r.counter = snoc_r.counter then
89103 if Atomic. compare_and_set t.tail (T move) snoc_r.prefix then
90104 snoc_r.value
91- else pop t backoff (Atomic. fenceless_get t.head)
105+ else begin
106+ backoff t;
107+ pop t (Atomic. fenceless_get t.head)
108+ end
92109 else
93110 let (Tail tail_r as tail : (_, [ `Tail ]) tdt ) =
94111 Tail { counter = snoc_r.counter; move }
95112 in
96113 let new_head = Atomic. get t.head in
97- if new_head != H head then pop t backoff new_head
114+ if new_head != H head then pop t new_head
98115 else if Atomic. compare_and_set t.tail (T move) (T tail) then
99116 let (Cons cons_r) = rev move in
100117 let after = cons_r.suffix in
101118 let new_head = Atomic. get t.head in
102- if new_head != H head then pop t backoff new_head
119+ if new_head != H head then pop t new_head
103120 else if Atomic. compare_and_set t.head (H head) after then begin
104121 tail_r.move < - Used ;
105122 cons_r.value
106123 end
107- else
108- let backoff = Backoff. once backoff in
109- pop t backoff (Atomic. fenceless_get t.head)
110- else pop t backoff (Atomic. fenceless_get t.head)
124+ else begin
125+ backoff t;
126+ pop t (Atomic. fenceless_get t.head)
127+ end
128+ else pop t (Atomic. fenceless_get t.head)
111129 | T (Tail tail_r ) -> begin
112130 match tail_r.move with
113131 | Used ->
114132 let new_head = Atomic. get t.head in
115- if new_head != H head then pop t backoff new_head
116- else raise_notrace Empty
133+ if new_head != H head then pop t new_head
134+ else begin
135+ backoff_unless_alone t;
136+ raise_notrace Empty
137+ end
117138 | Snoc move_r as move ->
118139 if head_r.counter < move_r.counter then
119140 let (Cons cons_r) = rev move in
120141 let after = cons_r.suffix in
121142 let new_head = Atomic. get t.head in
122- if new_head != H head then pop t backoff new_head
143+ if new_head != H head then pop t new_head
123144 else if Atomic. compare_and_set t.head (H head) after then begin
124145 tail_r.move < - Used ;
125146 cons_r.value
126147 end
127- else
128- let backoff = Backoff. once backoff in
129- pop t backoff (Atomic. fenceless_get t.head)
148+ else begin
149+ backoff t;
150+ pop t (Atomic. fenceless_get t.head)
151+ end
130152 else
131153 let new_head = Atomic. get t.head in
132- if new_head != H head then pop t backoff new_head
133- else raise_notrace Empty
154+ if new_head != H head then pop t new_head
155+ else begin
156+ backoff_unless_alone t;
157+ raise_notrace Empty
158+ end
134159 end
135160 end
136161
137- let rec push_head t value backoff =
162+ let rec push_head t value =
138163 match Atomic. get t.head with
139164 | H (Cons cons_r ) as suffix ->
140165 let after = Cons { counter = cons_r.counter - 1 ; value; suffix } in
141- if not (Atomic. compare_and_set t.head suffix (H after)) then
142- push_head t value (Backoff. once backoff)
166+ if not (Atomic. compare_and_set t.head suffix (H after)) then begin
167+ backoff t;
168+ push_head t value
169+ end
143170 | H (Head head_r ) as head -> begin
144171 match Atomic. get t.tail with
145172 | T (Snoc snoc_r as move ) ->
146- if Atomic. get t.head != head then push_head t value backoff
173+ if Atomic. get t.head != head then push_head t value
147174 else if head_r.counter = snoc_r.counter then begin
148175 let prefix = T (Snoc { snoc_r with value }) in
149176 let after =
150177 Snoc { snoc_r with counter = snoc_r.counter + 1 ; prefix }
151178 in
152- if not (Atomic. compare_and_set t.tail (T move) (T after)) then
153- push_head t value (Backoff. once backoff)
179+ if not (Atomic. compare_and_set t.tail (T move) (T after)) then begin
180+ backoff t;
181+ push_head t value
182+ end
154183 end
155- else
184+ else begin
156185 let tail = Tail { counter = snoc_r.counter; move } in
157- let backoff =
158- if Atomic. compare_and_set t.tail (T move) (T tail) then backoff
159- else Backoff. once backoff
160- in
161- push_head t value backoff
186+ if not (Atomic. compare_and_set t.tail (T move) (T tail)) then
187+ backoff t;
188+ push_head t value
189+ end
162190 | T (Tail tail_r ) as prefix -> begin
163191 match tail_r.move with
164192 | Used ->
165193 if Atomic. get t.head == head then begin
166194 let tail =
167195 Snoc { counter = tail_r.counter + 1 ; value; prefix }
168196 in
169- if not (Atomic. compare_and_set t.tail prefix (T tail)) then
170- push_head t value (Backoff. once backoff)
197+ if not (Atomic. compare_and_set t.tail prefix (T tail)) then begin
198+ backoff t;
199+ push_head t value
200+ end
171201 end
172- else push_head t value backoff
202+ else push_head t value
173203 | Snoc move_r as move ->
174- begin
175- match Atomic. get t.head with
176- | H (Head head_r as head) when head_r.counter < move_r.counter
177- ->
178- let after = rev move in
179- if
180- Atomic. fenceless_get t.head == H head
181- && Atomic. compare_and_set t.head (H head) (H after)
182- then tail_r.move < - Used
183- | _ -> tail_r.move < - Used
204+ begin match Atomic. get t.head with
205+ | H (Head head_r as head ) when head_r.counter < move_r.counter ->
206+ let after = rev move in
207+ if Atomic. fenceless_get t.head == H head then
208+ if Atomic. compare_and_set t.head (H head) (H after) then
209+ tail_r.move < - Used
210+ else backoff t
211+ | _ -> tail_r.move < - Used
184212 end ;
185- push_head t value backoff
213+ push_head t value
186214 end
187215 end
188216
@@ -207,9 +235,5 @@ let[@inline] length t =
207235 tail_at - head_at + 1
208236
209237let [@ inline] is_empty t = length t == 0
210- let [@ inline] pop_exn t = pop t Backoff. default (Atomic. fenceless_get t.head)
211-
212- let [@ inline] push t value =
213- push t value Backoff. default (Atomic. fenceless_get t.tail)
214-
215- let [@ inline] push_head t value = push_head t value Backoff. default
238+ let [@ inline] pop_exn t = pop t (Atomic. fenceless_get t.head)
239+ let [@ inline] push t value = push t value (Atomic. fenceless_get t.tail)
0 commit comments