11module Atomic = Multicore_magic. Transparent_atomic
22
3- type 'a t = { head : 'a head Atomic .t ; tail : 'a tail Atomic .t }
3+ type 'a t = {
4+ random_key : int ;
5+ head : 'a head Atomic .t ;
6+ tail : 'a tail Atomic .t ;
7+ }
48
59and ('a, _) tdt =
610 | Cons : {
@@ -27,14 +31,15 @@ and 'a head = H : ('a, [< `Cons | `Head ]) tdt -> 'a head [@@unboxed]
2731and 'a tail = T : ('a, [< `Snoc | `Tail ]) tdt -> 'a tail [@@ unboxed]
2832
2933let create ?padded () =
34+ let random_key = Int64. to_int (Random. bits64 () ) in
3035 let head =
3136 Atomic. make (H (Head { counter = 1 })) |> Multicore_magic. copy_as ?padded
3237 in
3338 let tail =
3439 Atomic. make (T (Tail { counter = 0 ; move = Used }))
3540 |> Multicore_magic. copy_as ?padded
3641 in
37- Multicore_magic. copy_as ?padded { head; tail }
42+ Multicore_magic. copy_as ?padded { random_key; head; tail }
3843
3944let rec rev (suffix : (_, [< `Cons ]) tdt ) = function
4045 | T (Snoc { counter; prefix; value } ) ->
@@ -47,142 +52,164 @@ let rev = function
4752 (Cons { counter; value; suffix = H (Head { counter = counter + 1 }) })
4853 prefix
4954
50- let rec push t value backoff = function
55+ let [@ inline] backoff t =
56+ Adaptive_backoff. once ~random_key: t.random_key ~log_scale: 10
57+
58+ let [@ inline] backoff_unless_alone t =
59+ Adaptive_backoff. once_unless_alone ~random_key: t.random_key ~log_scale: 10
60+
61+ let rec push t value = function
5162 | T (Snoc snoc_r ) as prefix ->
5263 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)
64+ if not (Atomic. compare_and_set t.tail prefix (T after)) then begin
65+ backoff t;
66+ push t value (Atomic. fenceless_get t.tail)
67+ end
5668 | T (Tail tail_r ) as prefix -> begin
5769 match tail_r.move with
5870 | Used ->
5971 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)
72+ if not (Atomic. compare_and_set t.tail prefix (T after)) then begin
73+ backoff t;
74+ push t value (Atomic. fenceless_get t.tail)
75+ end
6376 | 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
77+ begin match Atomic. get t.head with
78+ | H (Head head_r as head ) when head_r.counter < move_r.counter ->
79+ let after = rev move in
80+ if Atomic. fenceless_get t.head == H head then
81+ if Atomic. compare_and_set t.head (H head) (H after) then
82+ tail_r.move < - Used
83+ else backoff t
84+ | _ -> tail_r.move < - Used
7385 end ;
74- push t value backoff (Atomic. get t.tail)
86+ push t value (Atomic. get t.tail)
7587 end
7688
7789exception Empty
7890
79- let rec pop t backoff = function
91+ let rec pop t = function
8092 | H (Cons cons_r as cons ) ->
8193 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)
94+ else begin
95+ backoff t;
96+ pop t (Atomic. fenceless_get t.head)
97+ end
8598 | H (Head head_r as head ) -> begin
8699 match Atomic. get t.tail with
87100 | T (Snoc snoc_r as move ) ->
88101 if head_r.counter = snoc_r.counter then
89102 if Atomic. compare_and_set t.tail (T move) snoc_r.prefix then
90103 snoc_r.value
91- else pop t backoff (Atomic. fenceless_get t.head)
104+ else begin
105+ backoff t;
106+ pop t (Atomic. fenceless_get t.head)
107+ end
92108 else
93109 let (Tail tail_r as tail : (_, [ `Tail ]) tdt ) =
94110 Tail { counter = snoc_r.counter; move }
95111 in
96112 let new_head = Atomic. get t.head in
97- if new_head != H head then pop t backoff new_head
113+ if new_head != H head then pop t new_head
98114 else if Atomic. compare_and_set t.tail (T move) (T tail) then
99115 let (Cons cons_r) = rev move in
100116 let after = cons_r.suffix in
101117 let new_head = Atomic. get t.head in
102- if new_head != H head then pop t backoff new_head
118+ if new_head != H head then pop t new_head
103119 else if Atomic. compare_and_set t.head (H head) after then begin
104120 tail_r.move < - Used ;
105121 cons_r.value
106122 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)
123+ else begin
124+ backoff t;
125+ pop t (Atomic. fenceless_get t.head)
126+ end
127+ else pop t (Atomic. fenceless_get t.head)
111128 | T (Tail tail_r ) -> begin
112129 match tail_r.move with
113130 | Used ->
114131 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
132+ if new_head != H head then pop t new_head
133+ else begin
134+ backoff_unless_alone t;
135+ raise_notrace Empty
136+ end
117137 | Snoc move_r as move ->
118138 if head_r.counter < move_r.counter then
119139 let (Cons cons_r) = rev move in
120140 let after = cons_r.suffix in
121141 let new_head = Atomic. get t.head in
122- if new_head != H head then pop t backoff new_head
142+ if new_head != H head then pop t new_head
123143 else if Atomic. compare_and_set t.head (H head) after then begin
124144 tail_r.move < - Used ;
125145 cons_r.value
126146 end
127- else
128- let backoff = Backoff. once backoff in
129- pop t backoff (Atomic. fenceless_get t.head)
147+ else begin
148+ backoff t;
149+ pop t (Atomic. fenceless_get t.head)
150+ end
130151 else
131152 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
153+ if new_head != H head then pop t new_head
154+ else begin
155+ backoff_unless_alone t;
156+ raise_notrace Empty
157+ end
134158 end
135159 end
136160
137- let rec push_head t value backoff =
161+ let rec push_head t value =
138162 match Atomic. get t.head with
139163 | H (Cons cons_r ) as suffix ->
140164 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)
165+ if not (Atomic. compare_and_set t.head suffix (H after)) then begin
166+ backoff t;
167+ push_head t value
168+ end
143169 | H (Head head_r ) as head -> begin
144170 match Atomic. get t.tail with
145171 | T (Snoc snoc_r as move ) ->
146- if Atomic. get t.head != head then push_head t value backoff
172+ if Atomic. get t.head != head then push_head t value
147173 else if head_r.counter = snoc_r.counter then begin
148174 let prefix = T (Snoc { snoc_r with value }) in
149175 let after =
150176 Snoc { snoc_r with counter = snoc_r.counter + 1 ; prefix }
151177 in
152- if not (Atomic. compare_and_set t.tail (T move) (T after)) then
153- push_head t value (Backoff. once backoff)
178+ if not (Atomic. compare_and_set t.tail (T move) (T after)) then begin
179+ backoff t;
180+ push_head t value
181+ end
154182 end
155- else
183+ else begin
156184 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
185+ if not (Atomic. compare_and_set t.tail (T move) (T tail)) then
186+ backoff t;
187+ push_head t value
188+ end
162189 | T (Tail tail_r ) as prefix -> begin
163190 match tail_r.move with
164191 | Used ->
165192 if Atomic. get t.head == head then begin
166193 let tail =
167194 Snoc { counter = tail_r.counter + 1 ; value; prefix }
168195 in
169- if not (Atomic. compare_and_set t.tail prefix (T tail)) then
170- push_head t value (Backoff. once backoff)
196+ if not (Atomic. compare_and_set t.tail prefix (T tail)) then begin
197+ backoff t;
198+ push_head t value
199+ end
171200 end
172- else push_head t value backoff
201+ else push_head t value
173202 | 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
203+ begin match Atomic. get t.head with
204+ | H (Head head_r as head ) when head_r.counter < move_r.counter ->
205+ let after = rev move in
206+ if Atomic. fenceless_get t.head == H head then
207+ if Atomic. compare_and_set t.head (H head) (H after) then
208+ tail_r.move < - Used
209+ else backoff t
210+ | _ -> tail_r.move < - Used
184211 end ;
185- push_head t value backoff
212+ push_head t value
186213 end
187214 end
188215
@@ -207,9 +234,5 @@ let[@inline] length t =
207234 tail_at - head_at + 1
208235
209236let [@ 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
237+ let [@ inline] pop_exn t = pop t (Atomic. fenceless_get t.head)
238+ let [@ inline] push t value = push t value (Atomic. fenceless_get t.tail)
0 commit comments