7eee23d17497ee52919ecd8703f837f7da910778
[cdsspec-compiler.git] / notes / nondeterm-spec.txt
1 Modification to the current specifications.
2
3 I. Order
4 -- Sequential order (SO): Some total order that is consistent with the union of
5 happens-before and SC relation.
6
7 II. State
8 1. Global state: We allow users to specify a single global state so that when we
9 want to execute the sequential replay (execute the sequential order), the whole
10 process is similar to executing an sequential program. Such a global state is
11 similiar to the internal state of a sequential data structure. We also have this
12 in our old version (the rejection of PLDI'16). As an analogy to the cache-memory
13 model, the global state we define here is similar to the main memory in the
14 sense that there does not exist a real total order to all memory accesses, but
15 to some degree (with the non-deterministic specifications) we can have an
16 illution that there is some total order.
17
18 2. Local State: Beside of having one global state (the one that we have in the
19 old approach), we also allow each method call to have a local state.  This local
20 state is the accumulative side effects of the subset of method calls that happen
21 before the current method call. As an analogy to the cache-memory model, the
22 local state we define here is similar to cache, a local state is local to the
23 sense that the current method call must have seen those effects. The main goal
24 of having this is to support tighter non-deterministic specifications.
25
26 To evaluate the local state of each method call, an obvious approach is to
27 execute the subset of methods that happen before the current method in the
28 sequential order from the initial state. A optimization we can make is that we
29 start to evaluate the state from the most recent deviding node which every other
30 node in that subset is either hb before or after. Also, since local states are
31 not required in specifications all the time, it is only evaluated when needed.
32
33 III. Specifications
34 Our specification language supports using the following primitives to access
35 both global state and local state so that users can use those to write
36 specifications with different level of tightness.
37
38 To support tighter specifications, we introduce the concept of concurrent set of
39 method calls, meaning that for a specific method call, it can basically see the
40 effect of two different categories of method calls --- one that happens before
41 it, and one that concurrently execute with it. It is worth noting that when two
42 two method calls execute concurrently, in general there can be the following two
43 effects: 1) those concurrent methods can happen in either order, and the final
44 result remains the same. A concurrent FIFO is an example, in which concurrent
45 enqueue and dequeue methods can happen in a random order; and 2) the order of
46 those concurrent methods will affect the final result. The C/C++11 atomics is an
47 example, in which when concurrent stores to the same location execute in
48 different order, a later store will have different result.
49
50 1. CONCURRENT: This primitive extracts all the methods that executes
51 "concurrently" with the current method --- neither hb/SC before nor after the
52 current method --- and returns as a set. It is worth noting that the concurrent
53 method calls cannot be accessed for calculating local state but only for
54 assertions.
55
56 2. PREV: This primitive extracts all the methods that execute right before the
57 current method in the execution graph --- most recent method calls that are
58 hb/SC before the current method call --- and returns as a set. For each method
59 in this set, the current method's specification can access their local state.
60
61 3. NEXT: This primitive extracts all the methods that execute right after the
62 current method in the execution graph, and returns as a set. For each method in
63 this set, the current method's specification cannot access their local state.
64
65 4. LOCAL: This primitive allows users to access the local state of a method
66 call. It is worth noting that in order to calculate the local state of a method
67 call, one can only access the set of method calls that happen before the current
68 method call.
69
70 Our specifications allow two ways of calculating the local states, a default way
71 and a user-customized way. The default approach is to execute the set of method
72 calls that happen before the current method call in the sequential order, and a
73 the user-customized approach supports users to calculate the local state by
74 using the PREV primitive to access the local state of previous method calls.
75
76 5. COPY: This is the function that users provide to deep-copy the state. We
77 require users to provide such a primitive function because each local state
78 should be have its own copy.
79
80 6. FINALLY: This is the function that allows users to specify some final check
81 on the state. Initially, this check will only access the global state. However,
82 for the concern of expressiveness, we allow users to access the initial state,
83 meaning that users can basically access the whole graph and the local state of
84 each method call. This will enable to users to use the graph model (the relaxed
85 atomics can be specified) although the complxity of using that can get quite
86 complex.
87
88 IV. Examples
89
90 // Global specification
91 @DeclareState: // Declare the state structure
92 @InitState: // How do we initialize the state
93 @CopyState: // A function on how to copy an existing state
94 @Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return
95                 // value and the arguments of the two method calls
96
97 // Interface specification
98 @Interface: InterfaceName // Required; a label to represent the interface
99 @LocalState: // Optional; to calculate the accumulative local state before this
100                          // method call in a customized fashion. If not specified here, the
101                          // local state would be default, which is the result of the
102                          // execution on the subset of method calls in the sequential order
103 @PreCondition: // Optional; checking code
104 @LocalSideEffect: // Optional; to calculate the side effect this method call
105                                   // have on the local state in a customized fashion. If this
106                                   // field is not stated, it means we don't care about it.
107 @SideEffect: // Optional; to calculate the side effect on the global state. When
108                 // the "@LocalSideEffect" specification is ommitted, we also impose the
109                 // same side effect on the set of method calls that happen before this
110                 // method call in the sequential order.
111 @PostCondition: // Optional; checking code
112
113 // Ordering point specification
114 @OPDefine: condition    // If the specified condition satisfied, the atomic
115                                                 // operation right before is an ordering point
116
117 @PotentialOP(Label): condition  // If the specified condition satisfied, the
118                                                                 // atomic operation right before is a potential
119                                                                 // ordering point, and we label it with a tag
120
121 @OPCheck(Label): condition      // If the specified condition satisfied, the
122                                                         // potential ordering point defined earlier with the
123                                                         // same tag becomes an ordering point
124
125 @OPClear: condition             // If the specified condition satisfied, all the
126                                                 // ordering points and potential ordering points will be
127                                                 // cleared
128
129 @OPClearDefine: condition       // If the specified condition satisfied, all the
130                                                         // ordering points and potential ordering points will
131                                                         // be cleared, and the atomic operation right before
132                                                         // becomes an ordering point. This is a syntax sugar
133                                                         // as the combination of an "OPClear" and "OPDefine"
134                                                         // statement
135
136
137 1. The register examples: Basically, we can think of registers as the cache on a
138 memory system. The effect of a load or store basically tells us what the current
139 value in the cache line is, and a load can read from values that can be
140 potentially in the cache --- either one of the concurrent store update the cache
141 or it inherites one of the the previous local state in the execution graph.
142
143 ----------   Interfae   ----------
144 void init(atomic_int &loc, int initial);
145 int load(atomic_int &loc);
146 void store(atomic_int &loc, int val);
147 ----------   Interfae   ----------
148
149 a. The SC atomics --- the classic linearizability approach
150
151 b. The RA (release/acquire) C/C++ atomics
152 // For RA atomics, a load must read its value from a store that happens before
153 // it.
154 ----------   Specification   ----------
155 @DeclareVar: int x;
156 @InitVar: x = 0;
157
158 @Interface: Store
159 @SideEffect:
160         LOCAL.x = val;
161 void store(int *loc, int val);
162
163 @Interface: Load
164 @PreCondition:
165         IntegerSet *prevSet = new IntegerSet;
166         for (m in PREV) {
167                 prevSet->add(m.LOCAL.x);
168         }
169         return prevSet->contains(RET);
170 @SideEffect:
171         LOCAL.x = RET;
172 int load(int *loc);
173
174 c. The C/C++ atomics (a slightly loose specification)
175 // Actually, any concurrent data structures that rely modification-order to be
176 // correct would not have a precicely tight specification under our model, and
177 // C/C++ relaxed atomics is an example. See the following read-read coherence
178 // example.
179
180 // T1                           // T2
181 x = 1;                          x = 2;
182
183 // T3
184 r1 = x; // r1 == 1
185 r2 = x; // r2 == 2
186 r3 = x; // r3 == 1
187
188 Our model cannot prevent such a case from happening. However, we can still have
189 a slightly loose specification which basically states that a load can read from
190 any store that either immediately happens before it or concurrently executes.
191
192 ----------   Specification   ----------
193 @DeclareVar: int x;
194 @InitVar: x = 0;
195
196 @Interface: Store
197 @SideEffect:
198         LOCAL.x = val;
199 void store(int *loc, int val);
200
201 // We define a struct called MethodCall to represent the data we would collect
202 // and communicate between the real execution and the checking process
203 typedef struct MethodCall {
204         string interfaceName; // The interface label name
205         void *value; // The pointer that points to the struct that have the return
206                                  // value and the arguments
207         void *localState; // The pointer that points to the struct that represents
208                                           // the (local) state
209         vector<MethodCall*> *prev; // Method calls that are hb right before me
210         vector<MethodCall*> *next; // Method calls that are hb right after me
211         vector<MethodCall*> *concurrent; // Method calls that are concurrent with me
212 } MethodCall;
213
214 We will automatically generate two types of struct. One is the state struct, and
215 we will call it StateStruct. This state is shared by all the global and local
216 state. The other one is a per interface struct, and it wraps the return value
217 (RET) and the arguments as its field. We will name those struct with the
218 interface label name.
219
220 // Some very nice C/C++ macro definition to make specifications a lot easier
221 // 1. ForEach  --> to iterate all 
222 #define ForEach(item, list) \
223         for (iterator<MethodCall*> _mIter = list->begin(), \
224                 MethodCall *item = *_mIter; _mIter != list->end(); item = (++iter != \
225                 list->end()) ? *_mIter : NULL)
226
227
228 *********************************************
229
230 TODO:We want subset operation by the equality and inequality of the interface
231 name, a specific (or combined) state and a specific (or combined) of the value
232 (RET & arguments)
233
234 // 1.1 Subset(set, name)  --> to get a subset of method calls by name
235 inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
236         vector<MethodCall*> _subset = new vector<MethodCall*>;
237         for (int i = 0; i < set->size(); i++) {
238                 MethodCall *_m = (*set)[i];
239                 if (_m->interfaceName == name)
240                         _subset->push_back(_m);
241         }
242         return _subset;
243 }
244         
245 // 2. Local(method, field)
246 #define Local(method, field) ((StateStruct*) method->localState)->field
247
248 // 3. Value(method, type, field)
249 #define Value(method, type, field) ((type*) method->value)->field
250
251 // 4. Lable(mehtod)
252 #defien Lable(method) method->interfaceName
253
254 // 5. Prev(method)
255 #define Prev(method) mehtod->prev
256
257 // 6. Next(method)
258 #define Next(method) mehtod->next
259
260 // 7. Concurrent(method)
261 #define Concurrent(method) mehtod->concurrent
262
263 @Interface: Load
264 @PreCondition:
265         // Auto generated code
266         // MethodCall *ME = ((SomeTypeConversion) info)->method;
267         // vector<MethodCall*> PREV = Me->prev;
268         // vector<MethodCall*> NEXT = Me->next;
269         // vector<MethodCall*> CONCURRENT = Me->concurrent;
270
271         IntegerSet prevSet, concurSet;
272         ForEach(m, PREV) {
273                 prevSet.add(LOCAL(m, x));
274         }
275         ForEach (m, CONCURRENT("STORE")) {
276                 concurSet->add(m.val);
277         }
278         return prevSet->contains(RET) || concurSet->contains(RET);
279 @SideEffect:
280         LOCAL.x = RET;
281 int load(int *loc);
282
283 d. The C/C++ normal memory accesses
284 - Use the admissibility requirement, then the classic linearizability approach
285 on the admissible executions
286
287 2. The FIFO queue example.
288 ----------   Specification   ----------
289 // A FIFO queue should have the following properties held:
290 // 1. The enq() methods should conflict
291 // 2. The deq() methods that succeed should conflict
292 // 3. Corresponding enq() and deq() methods should conflict
293 // 4. An enqueued item can be dequeued by at most once
294 // 5. A dequeued item must have a corresponding enqueued item
295 // 6. When a queue is NOT "empty" (users can tightly or loosely define
296 // emptiness), and there comes a deq() method, the deq() method should succeed
297
298
299 @DeclareVar: vector<int> *q;
300 @InitVar: q = new voctor<int>;
301 @Copy: New.q = new vector<int>(Old.q);
302 // Fails to dequeue
303 @Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET)
304 // The dequeuer doesn't dequeue from that enqueuer
305 @Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
306
307 @Interface: Enq 
308 @SideEffect:
309         LOCAL.x = val;
310 void enq(queue_t *q, int val);
311
312 @Interface: Deq
313 @PreCondition:
314         // Check whether the queue is really empty
315         // Either the local state is an empty queue, or for all those remaining
316         // elements in the local queue, there should be some concurrent dequeuers to
317         // dequeue them
318         if (!RET) {
319                 // Local state is empty
320                 if (Local.q->size() == 0)
321                         return true;
322                 // Otherwise check there must be other concurrent dequeuers
323                 for (int i = 0; i < Local.q->size(); i++) {
324                         int item = (*Local.q)[i];
325                         // Check there's some concurrent dequeuer for this item
326                         bool flag = false;
327                         for (m in CONCURRENT("Deq")) {
328                                 if (m.RET) {
329                                         if (*m.res == item) flag = true;
330                                 }
331                         }
332                         if (!flag) return false;
333                 }
334                 return true;
335         } else { // Check the global queue state
336                 return q->back() == *res;
337         }
338 @SideEffect:
339         if (RET)
340                 Global.q->back()
341 bool deq(queue_t *q, int *res);
342
343
344
345 A good example to simulate a queue data structure is as follows.
346 Suppose we have a special structure
347 typedef struct Q {
348         atomic_int x;
349         atomic_int y;
350 } Q;
351
352 , and we have two interface on Q, read() and write(), where the write and read
353 method calls are synchronized by themselves, and they have to read and write the
354 x and y fields in turn.
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374 ----------------------------------------------------------------------------------------
375 We also need to think about the non-ordered queue.
376
377 ####
378 Combiming Data Structures --- 
379 For example, a queue, a -hb->c, b -hb-> e.
380
381 // T1
382 enq(1) -> {1} - {$}    // a
383 enq(2) -> {1, 2} - {$}   // b
384
385 // T2
386 deq(1) -> {$} - {1}   // c
387 deq($) -> {$} - {1}   // d
388
389 // State before this method  
390 JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
391 deq(2) -> {$} - {1, 2}
392
393
394
395
396