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 // FIXME: This might break composability!!??!!
54 4. FINAL: This is the function that allows users to specify some final check
55 on the state. This will enable to users to use the graph model (the relaxed
56 atomics can be specified) although the complxity of using that can get quite
59 Our specifications allow two ways of evaluating the state of method calls. One
60 way is to define "@Transition" on method calls, and then our checker executes
61 the method calls that are hb/SC before me in the sequential order starting from
62 the initial state. The other way is to define "@EvaluateState" after
63 "@Transition", which can only access the states of method calls that are hb/SC
64 before it. Usually users calculate the state by using the PREV primitive to
65 access the state of previous method calls.
67 IV. Specification Details
69 /// Global specification
70 @State: // Declare the state structure
71 @Initial: // How do we initialize the state
72 @Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return
73 // value and the arguments of the two method calls
75 /// Interface specification
76 @Interface: InterfaceName // Required; a label to represent the interface
77 @Transition: // Optional; the transitional side effect from the initial state to
78 // the current method call by executing such effect on method calls
79 // that are hb/SC before me in sequential order. When this field is
80 // omitted, the current state seen before checking is the same as
82 @EvaluateState: // Optional; to calculate the state before this
83 // method call is checked in a customized fashion. This is
84 // evaluated after "@Transition". If omitted, the state we would
85 // see is the effect after the "@Transition".
86 @PreCondition: // Optional; checking code
87 @SideEffect: // Optional; to calculate the side effect this method call
88 // have on the state after the "@PreCondition".
89 @PostCondition: // Optional; checking code
92 /// Convienient operations
93 We define a struct called MethodCall to represent the data we would collect and
94 communicate between the real execution and the checking process.
97 STATE(field) // A primitive to access the current state in the interface
98 // specification by the name of the field. We can use this as a
99 // lvalue & rvalue ==> "STATE(x) = 1" and "int i = STATE(x)" are
102 // This can also be used to refer to the state of a method item
103 // in the Subset operation (see Subset)
105 NAME // Used to refer to the name of a method item in the Subset
106 // operation (see Subset)
108 RET(type) // Used to refer to the return value of a method item in the
109 // Subset operation (see Subset)
111 ARG(type, arg) // Used to refer to the argument of a method item in the
112 // Subset operation (see Subset)
115 PREV // Represent the set of previous method calls of the current method
118 CONCURRENT // Represent the set of concurrent method calls of the current
121 NEXT // Represent the set of next method calls of the current method
124 Name(method) // The interface label name of the specific method
126 State(method, field) // A primitive to access a specific state field of a
127 // specific method. Also used as lvalue and rvalue
129 Ret(method, type) // The return value of the specific method; type should
130 // be the name of the interface label
132 Arg(method, type, arg) // The arguement by name of the specific method; type should
133 // be the name of the interface label, and arg should be
134 // the name of the argument
136 Prev(method) // Represent the set of previous method calls of the
137 // specific method call
139 Next(method) // Represent the set of next method calls of the specific
142 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
143 ForEach(item, container) { ... } // Useful iteration primitive
145 NewMethodSet // Create a new method set (set<MethodCall*>*)
147 MakeSet(type, oldset, newset, field); // Construct a new set from an
148 // old set. We extract a specific field of that set item
149 // and form a new set. Specifically we expect users to
150 // use this on MethodSet. For example, if we want to
151 // construct an integer set from the state "x" of
152 // the previous methods, we use "MakeSet(int, PREV,
153 // newset, STATE(x))", and the newset contains the new
156 Subset(set, condition) // A generic subset operation that takes a condition and
157 // returns all the item for which the boolean guard
158 // holds. The condition can be specified with GUARD or
159 // GeneralGuard shown as follow.
161 HasItem(set, condition) // A generic set operation that takes a condition and
162 // returns if there exists any item in "set" for which
163 // the condition holds. Its syntax is similar to that of
164 // Subset() operation
166 Size(container) // Return the size of a container type
168 Belong(container, item) // Return if item is in the container
170 Union(set1, set2) // Union of two sets
172 Intesection(set1, set2) // Intersection of two sets
174 Subtract(set1, set2) // Returns the new set that represents the result of
176 Insert(set, item) // Insert item to set
178 Insert(set, others) // Insert the whole set "others" to "set"
180 ITEM // Used to refer to the set item in the GeneralGuard shown below
182 GeneralGuard(type, expression) // Used as a condition for any set<T> type. We
183 // use "ITEM" to refer to a set item. For
184 // example, a subset of positive elements on an
185 // IntSet "s" would be
186 // "Subset(s, GeneralGuard(int, ITEM > 0))"
188 Guard(expression) // Used specifically for MethodSet(set<MethodCall*>). An
189 // example to extract the subset of method calls in the PREV
190 // set that is a "Store" method and whose state "x" is equal
191 // to "val" and the return value is 5 would be
192 // "Subset(PREV, Guard(STATE(x) == val && NAME == "Store" &&
193 // RET(Store) == 5))"
195 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
196 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
199 To make things easier, we have the following helper macros.
200 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
202 This is a common macro that is used as a constant for the name of specific
203 variables. We basically have two usage scenario:
204 1. In Subset operation, we allow users to specify a condition to extract a
205 subset. In that condition expression, we provide NAME, RET(type), ARG(type,
206 field) and STATE(field) to access each item's (method call) information.
207 2. In general specification (in pre- & post- conditions and side effects),
208 we would automatically generate an assignment that assign the current
209 MethodCall* pointer to a variable namedd _M. With this, when we access the
210 state of the current method, we use STATE(field) (this is a reference
216 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
217 #define CAT_HELPER(a, b) a ## b
218 #define X(name) CAT(__##name, __LINE__) /* unique variable */
220 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
222 *****************************************************************************
223 typedef struct MethodCall {
224 string name; // The interface label name
225 void *value; // The pointer that points to the struct that have the return
226 // value and the arguments
227 void *state; // The pointer that points to the struct that represents
229 set<MethodCall*> *prev; // Method calls that are hb right before me
230 set<MethodCall*> *concurrent; // Method calls that are concurrent with me
231 set<MethodCall*> *next; // Method calls that are hb right after me
234 typedef MethodCall *Method;
235 typedef set<Method> *MethodSet;
237 typedef vector<int> IntVector;
238 typedef list<int> IntList;
239 typedef set<int> IntSet;
240 *****************************************************************************
242 We will automatically generate two types of struct. One is the state struct, and
243 we will call it StateStruct. The other one is a per interface struct, and it
244 wraps the return value (RET) and the arguments as its field. We will name those
245 struct with the interface label name.
247 -----------------------------------------------------------------------------
248 For example, if we declare an ordered integer list in the specification state ,
249 we will generate a struct as follow.
251 @State: IntList *queue;
252 @Initial: queue = new IntList;
256 typedef struct StateStruct {
260 -----------------------------------------------------------------------------
261 If we have two interface whose specifications are as follow, we would generate
262 two struct accordingly.
266 void store(atomic_int *loc, int val) ...
270 int load(atomic_int *loc) ...
273 typedef struct Store {
278 typedef struct Load {
283 -----------------------------------------------------------------------------
284 We will put all these generated struct in a automatically-generated header file
285 called "generated.h". This file also includes header files that have commonly
286 used data types that interface (return value and arguments) accesses. In order
287 to make things work, users should include "generated.h" file in the end for
288 using our specification checker.
290 *****************************************************************************
293 /// Ordering point specification
294 @OPDefine: condition // If the specified condition satisfied, the atomic
295 // operation right before is an ordering point
297 @PotentialOP(Label): condition // If the specified condition satisfied, the
298 // atomic operation right before is a potential
299 // ordering point, and we label it with a tag
301 @OPCheck(Label): condition // If the specified condition satisfied, the
302 // potential ordering point defined earlier with the
303 // same tag becomes an ordering point
305 @OPClear: condition // If the specified condition satisfied, all the
306 // ordering points and potential ordering points will be
309 @OPClearDefine: condition // If the specified condition satisfied, all the
310 // ordering points and potential ordering points will
311 // be cleared, and the atomic operation right before
312 // becomes an ordering point. This is a syntax sugar
313 // as the combination of an "OPClear" and "OPDefine"
319 !!!!!!! The register example should be extended to commute if we think of their
320 transitional effects as set operations --- a set operation that will only mask
321 out side the effects of its own previous behavior (things that are hb/SC before
322 it) ---- VERY IMPORTANT note here!!
325 1. The register examples: Basically, we can think of registers as the cache on a
326 memory system. The effect of a load or store basically tells us what the current
327 value in the cache line is, and a load can read from values that can be
328 potentially in the cache --- either one of the concurrent store update the cache
329 or it inherites one of the the previous state in the execution graph.
331 ---------- Interfae ----------
332 void init(atomic_int &loc, int initial);
333 int load(atomic_int &loc);
334 void store(atomic_int &loc, int val);
335 ---------- Interfae ----------
337 a. The SC atomics --- the classic linearizability approach
339 b. The RA (release/acquire) C/C++ atomics
340 // For RA atomics, a load must read its value from a store that happens before
342 ---------- Specification ----------
345 @Commutativity: Store <-> Store(true)
346 @Commutativity: Load <-> Load(true)
347 @Commutativity: Store <-> Load(true)
349 /** No @Transition */
351 @SideEffect: STATE(x) = val;
352 void store(int *loc, int val);
356 return HasItem(PREV, STATE(x) == RET);
357 @SideEffect: STATE(x) = RET;
360 c. The C/C++ atomics (a slightly loose specification)
361 // Actually, any concurrent data structures that rely modification-order to be
362 // correct would not have a precicely tight specification under our model, and
363 // C/C++ relaxed atomics is an example. See the following read-read coherence
374 Our model cannot prevent such a case from happening. However, we can still have
375 a slightly loose specification which basically states that a load can read from
376 any store that either immediately happens before it or concurrently executes.
379 ---------- Specification ----------
384 @SideEffect: STATE(x) = val;
385 void store(int *loc, int val);
390 // Auto generated code
391 // MethodCall *ME = ((SomeTypeConversion) info)->method;
393 return HasItem(Prev, STATE(x) == RET) ||
394 + HasItem(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET)
395 @SideEffect: STATE(x) = RET;
398 d. The C/C++ normal memory accesses
399 - Use the admissibility requirement, then the classic linearizability approach
400 on the admissible executions
402 2. The FIFO queue example.
403 ---------- Specification ----------
404 // A FIFO queue should have the following properties held:
405 // 1. The enq() methods should conflict
406 // 2. The deq() methods that succeed should conflict
407 // 3. Corresponding enq() and deq() methods should conflict
408 // 4. An enqueued item can be dequeued by at most once
409 // 5. A dequeued item must have a corresponding enqueued item
410 // 6. When a queue is NOT "empty" (users can tightly or loosely define
411 // emptiness), and there comes a deq() method, the deq() method should succeed
414 @DeclareVar: vector<int> *q;
415 @InitVar: q = new voctor<int>;
416 @Copy: New.q = new vector<int>(Old.q);
418 @Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET)
419 @Commutativity: Enq <-> Deq (true)
422 @Transition: q->push_back(val);
423 void enq(queue_t *q, int val);
426 @Transition: if (RET) q->pop_back();
428 // Check whether the queue is really empty
429 // Either the state is an empty queue, or for all those remaining
430 // elements in the queue, there should be some concurrent dequeuers to
434 if (STATE(q)->size() == 0) return true;
435 // Otherwise check there must be other concurrent dequeuers
436 ForEach (item, State(q)) {
437 // Check there's some concurrent dequeuer for this item
438 if (!HasItem(CONCURRENT, NAME == "Deq" && RET(Deq) &&
439 *ARG(Deq, res) == item)) return false;
442 } else { // Check the global queue state
443 return q->back() == *res;
445 bool deq(queue_t *q, int *res);
448 *******************************************************************************
449 A good example to simulate a queue data structure is as follows.
450 Suppose we have a special structure
456 , and we have two interface on Q, read() and write(), where the write and read
457 method calls are synchronized by themselves, and they have to read and write the
458 x and y fields in turn.