@@ -48,32 +48,91 @@ let rev = function
48
48
prefix
49
49
50
50
let rec push t value backoff = function
51
- | T (Snoc snoc_r as snoc ) -> push_with t value backoff snoc_r.counter (T snoc)
52
- | T (Tail tail_r as tail ) -> begin
51
+ | T (Snoc snoc_r ) as prefix ->
52
+ 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)
56
+ | T (Tail tail_r ) as prefix -> begin
53
57
match tail_r.move with
54
- | Used -> push_with t value backoff tail_r.counter (T tail)
55
- | Snoc move_r as move -> begin
56
- match Atomic. get t.head with
57
- | H (Head head_r as head ) when head_r.counter < move_r.counter ->
58
- let after = rev move in
59
- if
60
- Atomic. fenceless_get t.head == H head
61
- && Atomic. compare_and_set t.head (H head) (H after)
62
- then tail_r.move < - Used ;
63
- let new_tail = Atomic. fenceless_get t.tail in
64
- if new_tail != T tail then push t value backoff new_tail
65
- else push_with t value backoff tail_r.counter (T tail)
66
- | _ -> push_with t value backoff tail_r.counter (T tail)
67
- end
58
+ | Used ->
59
+ 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)
63
+ | 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
73
+ end ;
74
+ push t value backoff (Atomic. get t.tail)
68
75
end
69
76
70
- and push_with t value backoff counter prefix =
71
- let after = Snoc { counter = counter + 1 ; prefix; value } in
72
- if not (Atomic. compare_and_set t.tail prefix (T after)) then
73
- let backoff = Backoff. once backoff in
74
- push t value backoff (Atomic. fenceless_get t.tail)
77
+ exception Empty
75
78
76
- let push t value = push t value Backoff. default (Atomic. fenceless_get t.tail)
79
+ let rec pop t backoff = function
80
+ | H (Cons cons_r as cons ) ->
81
+ 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)
85
+ | H (Head head_r as head ) -> begin
86
+ match Atomic. get t.tail with
87
+ | T (Snoc snoc_r as move ) ->
88
+ if head_r.counter = snoc_r.counter then
89
+ if Atomic. compare_and_set t.tail (T move) snoc_r.prefix then
90
+ snoc_r.value
91
+ else pop t backoff (Atomic. fenceless_get t.head)
92
+ else
93
+ let (Tail tail_r as tail : (_, [ `Tail ]) tdt ) =
94
+ Tail { counter = snoc_r.counter; move }
95
+ in
96
+ let new_head = Atomic. get t.head in
97
+ if new_head != H head then pop t backoff new_head
98
+ else if Atomic. compare_and_set t.tail (T move) (T tail) then
99
+ let (Cons cons_r) = rev move in
100
+ let after = cons_r.suffix in
101
+ let new_head = Atomic. get t.head in
102
+ if new_head != H head then pop t backoff new_head
103
+ else if Atomic. compare_and_set t.head (H head) after then begin
104
+ tail_r.move < - Used ;
105
+ cons_r.value
106
+ 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)
111
+ | T (Tail tail_r ) -> begin
112
+ match tail_r.move with
113
+ | Used ->
114
+ 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
117
+ | Snoc move_r as move ->
118
+ if head_r.counter < move_r.counter then
119
+ let (Cons cons_r) = rev move in
120
+ let after = cons_r.suffix in
121
+ let new_head = Atomic. get t.head in
122
+ if new_head != H head then pop t backoff new_head
123
+ else if Atomic. compare_and_set t.head (H head) after then begin
124
+ tail_r.move < - Used ;
125
+ cons_r.value
126
+ end
127
+ else
128
+ let backoff = Backoff. once backoff in
129
+ pop t backoff (Atomic. fenceless_get t.head)
130
+ else
131
+ 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
134
+ end
135
+ end
77
136
78
137
let rec push_head t value backoff =
79
138
match Atomic. get t.head with
@@ -121,63 +180,29 @@ let rec push_head t value backoff =
121
180
Atomic. fenceless_get t.head == H head
122
181
&& Atomic. compare_and_set t.head (H head) (H after)
123
182
then tail_r.move < - Used
124
- | _ -> ()
183
+ | _ -> tail_r.move < - Used
125
184
end ;
126
185
push_head t value backoff
127
186
end
128
187
end
129
188
130
- let push_head t value = push_head t value Backoff. default
131
-
132
- exception Empty
133
-
134
- let rec pop t backoff = function
135
- | H (Cons cons_r as cons ) ->
136
- if Atomic. compare_and_set t.head (H cons) cons_r.suffix then cons_r.value
137
- else
138
- let backoff = Backoff. once backoff in
139
- pop t backoff (Atomic. fenceless_get t.head)
140
- | H (Head head_r as head ) -> begin
141
- match Atomic. get t.tail with
142
- | T (Snoc snoc_r as move ) ->
143
- if head_r.counter = snoc_r.counter then
144
- if Atomic. compare_and_set t.tail (T move) snoc_r.prefix then
145
- snoc_r.value
146
- else pop t backoff (Atomic. fenceless_get t.head)
147
- else
148
- let tail = Tail { counter = snoc_r.counter; move } in
149
- let new_head = Atomic. get t.head in
150
- if new_head != H head then pop t backoff new_head
151
- else if Atomic. compare_and_set t.tail (T move) (T tail) then
152
- pop_moving t backoff head move tail
153
- else pop t backoff (Atomic. fenceless_get t.head)
154
- | T (Tail tail_r as tail ) -> begin
155
- match tail_r.move with
156
- | Used -> pop_emptyish t backoff head
157
- | Snoc _ as move -> pop_moving t backoff head move tail
158
- end
159
- end
160
-
161
- and pop_moving t backoff (Head head_r as head : (_, [ `Head ]) tdt )
162
- (Snoc move_r as move : (_, [ `Snoc ]) tdt )
163
- (Tail tail_r : (_, [ `Tail ]) tdt ) =
164
- if head_r.counter < move_r.counter then
165
- match rev move with
166
- | Cons cons_r ->
167
- let after = cons_r.suffix in
168
- let new_head = Atomic. get t.head in
169
- if new_head != H head then pop t backoff new_head
170
- else if Atomic. compare_and_set t.head (H head) after then begin
171
- tail_r.move < - Used ;
172
- cons_r.value
173
- end
174
- else
175
- let backoff = Backoff. once backoff in
176
- pop t backoff (Atomic. fenceless_get t.head)
177
- else pop_emptyish t backoff head
178
-
179
- and pop_emptyish t backoff head =
180
- let new_head = Atomic. get t.head in
181
- if new_head == H head then raise_notrace Empty else pop t backoff new_head
182
-
183
- let pop_exn t = pop t Backoff. default (Atomic. fenceless_get t.head)
189
+ let rec length t =
190
+ let head = Atomic. get t.head in
191
+ let tail = Atomic. fenceless_get t.tail in
192
+ if head != Atomic. get t.head then length t
193
+ else
194
+ let head_at =
195
+ match head with H (Cons r ) -> r.counter | H (Head r ) -> r.counter
196
+ in
197
+ let tail_at =
198
+ match tail with T (Snoc r ) -> r.counter | T (Tail r ) -> r.counter
199
+ in
200
+ tail_at - head_at + 1
201
+
202
+ let [@ inline] is_empty t = length t == 0
203
+ let [@ inline] pop_exn t = pop t Backoff. default (Atomic. fenceless_get t.head)
204
+
205
+ let [@ inline] push t value =
206
+ push t value Backoff. default (Atomic. fenceless_get t.tail)
207
+
208
+ let [@ inline] push_head t value = push_head t value Backoff. default
0 commit comments