1 Modification to the current specifications.
4 -- Sequential order (SO): Some total order that is consistent with the union of
5 happens-before and SC relation.
8 Previously, we keep a sequential state throughout the process of executing the
9 sequential history. In our model, we keep a state local to each method call.
10 Conceptually, this state is the accumulative side effects of the subset of
11 method calls that happen before the current method call.
13 To evaluate the state of each method call, an obvious approach is to
14 execute the subset of methods that happen before the current method in the
15 sequential order from the initial state. A optimization we can make is that we
16 start to evaluate the state from the most recent deviding node which every other
17 node in that subset is either hb before or after.
20 Our specification language supports using the following primitives to access the
21 state of method calls so that users can use those to write specifications with
22 different level of tightness.
24 To support tighter specifications, we introduce the concept of concurrent set of
25 method calls, meaning that for a specific method call, it can basically see the
26 effect of two different categories of method calls --- one that happens before
27 it, and one that concurrently execute with it. It is worth noting that when two
28 two method calls execute concurrently, in general there can be the following two
29 effects: 1) those concurrent methods can happen in either order, and the final
30 result remains the same. A concurrent FIFO is an example, in which concurrent
31 enqueue and dequeue methods can happen in a random order; and 2) the order of
32 those concurrent methods will affect the final result. The C/C++11 atomics is an
33 example, in which when concurrent stores to the same location execute in
34 different order, a later store will have different result.
36 1. CONCURRENT: This primitive extracts all the methods that executes
37 "concurrently" with the current method --- neither hb/SC before nor after the
38 current method --- and returns as a set. It is worth noting that in order to
39 preserve composability, when evaluating the state, the concurrent method calls'
40 information cannot be used. That is to say, the concurrent set of mehtods are
41 only used for assertions.
43 2. PREV: This primitive extracts all the methods that execute right before the
44 current method in the execution graph --- most recent method calls that are
45 hb/SC before the current method call --- and returns as a set. For each method
46 in this set, the current method's specification can access their state.
48 3. NEXT: This primitive extracts all the methods that execute right after the
49 current method in the execution graph, and returns as a set. For each method in
50 this set, the current method's specification CANNOT access their state (for
51 preserving composability).
53 Our specifications allow two ways of calculating the local states, a default way
54 and a user-customized way. The default approach is to execute the set of method
55 calls that happen before the current method call in the sequential order, and a
56 the user-customized approach supports users to calculate the local state by
57 using the PREV primitive to access the local state of previous method calls.
59 // FIXME: This might break composability!!??!!
60 6. FINAL: This is the function that allows users to specify some final check
61 on the state. This will enable to users to use the graph model (the relaxed
62 atomics can be specified) although the complxity of using that can get quite
67 /// Global specification
68 @State: // Declare the state structure
69 @Initial: // How do we initialize the state
70 @Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return
71 // value and the arguments of the two method calls
73 /// Interface specification
74 @Interface: InterfaceName // Required; a label to represent the interface
75 @Transition: // Optional; the transitional side effect from the initial state to
76 // the current method call by executing such effect on method calls
77 // that are hb/SC before me in sequential order. When this field is
78 // omitted, the current state seen before checking is the same as
80 @EvaluateState: // Optional; to calculate the state before this
81 // method call is checked in a customized fashion. This is
82 // evaluated after "@Transition". If omitted, the state we would
83 // see is the effect after the "@Transition".
84 @PreCondition: // Optional; checking code
85 @SideEffect: // Optional; to calculate the side effect this method call
86 // have on the state after the "@PreCondition".
87 @PostCondition: // Optional; checking code
90 /// Ordering point specification
91 @OPDefine: condition // If the specified condition satisfied, the atomic
92 // operation right before is an ordering point
94 @PotentialOP(Label): condition // If the specified condition satisfied, the
95 // atomic operation right before is a potential
96 // ordering point, and we label it with a tag
98 @OPCheck(Label): condition // If the specified condition satisfied, the
99 // potential ordering point defined earlier with the
100 // same tag becomes an ordering point
102 @OPClear: condition // If the specified condition satisfied, all the
103 // ordering points and potential ordering points will be
106 @OPClearDefine: condition // If the specified condition satisfied, all the
107 // ordering points and potential ordering points will
108 // be cleared, and the atomic operation right before
109 // becomes an ordering point. This is a syntax sugar
110 // as the combination of an "OPClear" and "OPDefine"
114 1. The register examples: Basically, we can think of registers as the cache on a
115 memory system. The effect of a load or store basically tells us what the current
116 value in the cache line is, and a load can read from values that can be
117 potentially in the cache --- either one of the concurrent store update the cache
118 or it inherites one of the the previous local state in the execution graph.
120 ---------- Interfae ----------
121 void init(atomic_int &loc, int initial);
122 int load(atomic_int &loc);
123 void store(atomic_int &loc, int val);
124 ---------- Interfae ----------
126 a. The SC atomics --- the classic linearizability approach
128 b. The RA (release/acquire) C/C++ atomics
129 // For RA atomics, a load must read its value from a store that happens before
131 ---------- Specification ----------
136 @SideEffect: LOCAL(x) = val;
137 void store(int *loc, int val);
141 Size(Subset(PREV, LOCAL(x) == RET)) > 0;
142 @SideEffect: LOCAL(x) = RET;
145 c. The C/C++ atomics (a slightly loose specification)
146 // Actually, any concurrent data structures that rely modification-order to be
147 // correct would not have a precicely tight specification under our model, and
148 // C/C++ relaxed atomics is an example. See the following read-read coherence
159 Our model cannot prevent such a case from happening. However, we can still have
160 a slightly loose specification which basically states that a load can read from
161 any store that either immediately happens before it or concurrently executes.
165 // We define a struct called MethodCall to represent the data we would collect
166 // and communicate between the real execution and the checking process
167 typedef struct MethodCall {
168 string interfaceName; // The interface label name
169 void *value; // The pointer that points to the struct that have the return
170 // value and the arguments
171 void *localState; // The pointer that points to the struct that represents
173 vector<MethodCall*> *prev; // Method calls that are hb right before me
174 vector<MethodCall*> *next; // Method calls that are hb right after me
175 vector<MethodCall*> *concurrent; // Method calls that are concurrent with me
178 We will automatically generate two types of struct. One is the state struct, and
179 we will call it StateStruct. This state is shared by all the global and local
180 state. The other one is a per interface struct, and it wraps the return value
181 (RET) and the arguments as its field. We will name those struct with the
182 interface label name.
184 // Some very nice C/C++ macro definition to make specifications a lot easier
185 // 1. ForEach --> to iterate all
186 #define ForEach(item, list) \
187 for (iterator<MethodCall*> _mIter = list->begin(), \
188 MethodCall *item = *_mIter; _mIter != list->end(); item = (++iter != \
189 list->end()) ? *_mIter : NULL)
192 *********************************************
193 // 1.1 Subset(set, guard) --> to get a subset of method calls by a boolean
194 // expression; This takes advantage of C++11 std::function features and C macros.
196 // 1.2 Size(set) --> to get the size of a method set
197 #define Size(set) set->size()
199 // 1.3 Belong(set, method) --> whether method belongs to set
200 #define Belong(set, method) std::find(set->begin(), set->end(), method) != set->end()
202 // 1.4 Intersect(set1, set2) --> the intersection of two method sets
203 inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
204 MethodSet res = NewSet;
212 // 1.5 Union(set1, set2) --> the union of two method sets
213 inline MethodSet Union(MethodSet set1, MethodSet set2) {
214 MethodSet res = NewSet(set1);
216 if (!Belong(set1, m))
222 // 1.6 Insert(set, method) --> add a method to the set
223 inline bool Insert(MethodSet set, Method m) {
232 // 1.7 Subtract(set1, set2) --> subtract set2 from set1
233 inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
234 MethodSet res = NewSet;
236 if (!Belong(set2, m))
242 // 1.8 MakeSet(count, ...) --> Make a set from the arguments
245 // 2. Local(method, field)
246 #define Local(method, field) ((StateStruct*) method->localState)->field
248 // 3. Value(method, type, field)
249 #define Value(method, type, field) ((type*) method->value)->field
251 #define Ret(method, type) Value(method, type, RET)
253 #define Arg(method, type, arg) Value(method, type, arg)
257 #defien Lable(method) method->interfaceName
260 #define Prev(method) mehtod->prev
263 #define Next(method) mehtod->next
265 // 7. Concurrent(method)
266 #define Concurrent(method) mehtod->concurrent
269 ---------- Specification ----------
274 @SideEffect: LOCAL(x) = val;
275 void store(int *loc, int val);
280 // Auto generated code
281 // MethodCall *ME = ((SomeTypeConversion) info)->method;
283 int count = Size(Subset(Prev, LOCAL(x) == RET))
284 + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET))
286 @SideEffect: LOCAL(x) = RET;
289 d. The C/C++ normal memory accesses
290 - Use the admissibility requirement, then the classic linearizability approach
291 on the admissible executions
293 2. The FIFO queue example.
294 ---------- Specification ----------
295 // A FIFO queue should have the following properties held:
296 // 1. The enq() methods should conflict
297 // 2. The deq() methods that succeed should conflict
298 // 3. Corresponding enq() and deq() methods should conflict
299 // 4. An enqueued item can be dequeued by at most once
300 // 5. A dequeued item must have a corresponding enqueued item
301 // 6. When a queue is NOT "empty" (users can tightly or loosely define
302 // emptiness), and there comes a deq() method, the deq() method should succeed
305 @DeclareVar: vector<int> *q;
306 @InitVar: q = new voctor<int>;
307 @Copy: New.q = new vector<int>(Old.q);
309 @Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET)
310 // The dequeuer doesn't dequeue from that enqueuer
311 @Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
314 @SideEffect: q->push_back(val);
315 void enq(queue_t *q, int val);
319 // Check whether the queue is really empty
320 // Either the local state is an empty queue, or for all those remaining
321 // elements in the local queue, there should be some concurrent dequeuers to
324 // Local state is empty
325 if (Local(q)->size() == 0) return true;
326 // Otherwise check there must be other concurrent dequeuers
327 ForEach (item, Local(q)) {
328 // Check there's some concurrent dequeuer for this item
329 if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) &&
330 *ARG(Deq, res) == item)) == 0) return false;
333 } else { // Check the global queue state
334 return q->back() == *res;
337 if (RET) q->pop_back();
338 bool deq(queue_t *q, int *res);
342 A good example to simulate a queue data structure is as follows.
343 Suppose we have a special structure
349 , and we have two interface on Q, read() and write(), where the write and read
350 method calls are synchronized by themselves, and they have to read and write the
351 x and y fields in turn.
371 ----------------------------------------------------------------------------------------
372 We also need to think about the non-ordered queue.
375 Combiming Data Structures ---
376 For example, a queue, a -hb->c, b -hb-> e.
379 enq(1) -> {1} - {$} // a
380 enq(2) -> {1, 2} - {$} // b
383 deq(1) -> {$} - {1} // c
384 deq($) -> {$} - {1} // d
386 // State before this method
387 JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
388 deq(2) -> {$} - {1, 2}