Add extra ABA tag bits
[linted.git] / src / ada-core / src / linted-lock_free_stack.adb
1 -- Copyright 2017 Steven Stewart-Gallus
2 --
3 -- Licensed under the Apache License, Version 2.0 (the "License");
4 -- you may not use this file except in compliance with the License.
5 -- You may obtain a copy of the License at
6 --
7 --     http://www.apache.org/licenses/LICENSE-2.0
8 --
9 -- Unless required by applicable law or agreed to in writing, software
10 -- distributed under the License is distributed on an "AS IS" BASIS,
11 -- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
12 -- implied.  See the License for the specific language governing
13 -- permissions and limitations under the License.
14 with Linted.Atomics;
15 with Linted.ABAs;
16 with Linted.Sched;
17
18 package body Linted.Lock_Free_Stack with
19      Refined_State =>
20      (State =>
21         (Buf_Contents,
22          Buf_Nodes,
23          Buf_Head,
24          Buf_Free,
25          Head_Contention,
26          Free_Contention))
27 is
28
29    type My_Ix is new Ix with
30         Default_Value => 0;
31
32    package ABA is new ABAs (My_Ix);
33    package Aba_Atomics is new Atomics (ABA.ABA);
34    package Access_Atomics is new Atomics (My_Ix);
35
36    use type ABA.Tag_T;
37
38    type Element_Array is
39      array (My_Ix range 1 .. My_Ix (Ix'Last)) of Element_T with
40         Independent_Components;
41
42    Buf_Contents : Element_Array;
43
44    type Node_Array is
45      array (My_Ix range 1 .. My_Ix (Ix'Last)) of Access_Atomics.Atomic with
46         Independent_Components;
47
48    Buf_Nodes : Node_Array;
49
50    Buf_Head : Aba_Atomics.Atomic;
51    Head_Contention : Sched.Contention;
52
53    Buf_Free : Aba_Atomics.Atomic;
54    Free_Contention : Sched.Contention;
55
56    procedure Allocate (Free : out My_Ix) with
57       Global => (In_Out => (Buf_Nodes, Buf_Free, Free_Contention)),
58       Depends =>
59       (Free => (Buf_Free, Buf_Nodes),
60        Buf_Nodes => (Buf_Nodes, Buf_Free),
61        Free_Contention => (Buf_Free, Buf_Nodes, Free_Contention),
62        Buf_Free => (Buf_Nodes, Buf_Free));
63
64    procedure Deallocate (Head : My_Ix) with
65       Pre => Head /= 0,
66       Global => (In_Out => (Buf_Nodes, Buf_Free, Free_Contention)),
67       Depends =>
68       (Buf_Nodes => (Buf_Nodes, Buf_Free, Head),
69        Free_Contention => (Buf_Free, Head, Free_Contention),
70        Buf_Free => (Buf_Free, Head));
71
72    procedure Push_Node
73      (N : in out Aba_Atomics.Atomic;
74       Contention : in out Sched.Contention;
75       Free : My_Ix) with
76       Pre => Free /= 0,
77       Global => (In_Out => Buf_Nodes),
78       Depends =>
79       (N => (Free, N),
80        Contention => (Free, N, Contention),
81        Buf_Nodes => (Free, Buf_Nodes, N));
82
83    procedure Pop_Node
84      (N : in out Aba_Atomics.Atomic;
85       Contention : in out Sched.Contention;
86       Head : out My_Ix) with
87       Global => (In_Out => Buf_Nodes),
88       Depends =>
89       (Head => (Buf_Nodes, N),
90        Contention => (N, Buf_Nodes, Contention),
91        N => (Buf_Nodes, N),
92        Buf_Nodes => (N, Buf_Nodes));
93
94    procedure Allocate (Free : out My_Ix) is
95    begin
96       Pop_Node (Buf_Free, Free_Contention, Free);
97    end Allocate;
98
99    procedure Deallocate (Head : My_Ix) is
100    begin
101       Push_Node (Buf_Free, Free_Contention, Head);
102    end Deallocate;
103
104    procedure Try_Push (Element : Element_T; Success : out Boolean) with
105       Refined_Global =>
106       (In_Out =>
107          (Buf_Contents,
108           Buf_Nodes,
109           Buf_Head,
110           Buf_Free,
111           Head_Contention,
112           Free_Contention))
113    is
114       Free : My_Ix;
115    begin
116       Allocate (Free);
117
118       if 0 = Free then
119          Success := False;
120       else
121          Buf_Contents (Free) := Element;
122          Push_Node (Buf_Head, Head_Contention, Free);
123          Success := True;
124       end if;
125    end Try_Push;
126
127    procedure Push_Node
128      (N : in out Aba_Atomics.Atomic;
129       Contention : in out Sched.Contention;
130       Free : My_Ix)
131    is
132       Head : ABA.ABA;
133       Swapped : Boolean;
134    begin
135       loop
136          Aba_Atomics.Get (N, Head);
137          Access_Atomics.Set (Buf_Nodes (Free), ABA.Element (Head));
138          Aba_Atomics.Compare_And_Swap
139            (N,
140             Head,
141             ABA.Initialize (Free, ABA.Tag (Head) + 1),
142             Swapped);
143          exit when Swapped;
144          Sched.Backoff (Contention);
145       end loop;
146       Sched.Success (Contention);
147    end Push_Node;
148
149    procedure Try_Pop (Element : out Element_T; Success : out Boolean) with
150       Refined_Global =>
151       (In_Out =>
152          (Buf_Contents,
153           Buf_Nodes,
154           Buf_Head,
155           Buf_Free,
156           Head_Contention,
157           Free_Contention))
158    is
159       Head : My_Ix;
160    begin
161       Pop_Node (Buf_Head, Head_Contention, Head);
162
163       if 0 = Head then
164          declare
165             Dummy : Element_T;
166          begin
167             Element := Dummy;
168          end;
169          Success := False;
170       else
171          Element := Buf_Contents (Head);
172          declare
173             Dummy : Element_T;
174          begin
175             Buf_Contents (Head) := Dummy;
176          end;
177
178          Deallocate (Head);
179          Success := True;
180       end if;
181    end Try_Pop;
182
183    procedure Pop_Node
184      (N : in out Aba_Atomics.Atomic;
185       Contention : in out Sched.Contention;
186       Head : out My_Ix)
187    is
188       New_Head : My_Ix;
189       Swapped : Boolean;
190       ABA_Head : ABA.ABA;
191    begin
192       loop
193          Aba_Atomics.Get (N, ABA_Head);
194          if ABA.Element (ABA_Head) = 0 then
195             exit;
196          end if;
197          Access_Atomics.Get (Buf_Nodes (ABA.Element (ABA_Head)), New_Head);
198          Aba_Atomics.Compare_And_Swap
199            (N,
200             ABA_Head,
201             ABA.Initialize (New_Head, ABA.Tag (ABA_Head) + 1),
202             Swapped);
203          exit when Swapped;
204          Sched.Backoff (Contention);
205       end loop;
206       Sched.Success (Contention);
207       Head := ABA.Element (ABA_Head);
208    end Pop_Node;
209
210 begin
211    declare
212       Old_Node : My_Ix := 0;
213    begin
214       for II in 1 .. My_Ix (Ix'Last) loop
215          Buf_Nodes (II).Set (Old_Node);
216          Old_Node := II;
217       end loop;
218       Buf_Free.Set (ABA.Initialize (Old_Node, 0));
219    end;
220 end Linted.Lock_Free_Stack;