happens-before and SC relation.
II. State
-1. Global state: We allow users to specify a single global state so that when we
-want to execute the sequential replay (execute the sequential order), the whole
-process is similar to executing an sequential program. Such a global state is
-similiar to the internal state of a sequential data structure. We also have this
-in our old version (the rejection of PLDI'16). As an analogy to the cache-memory
-model, the global state we define here is similar to the main memory in the
-sense that there does not exist a real total order to all memory accesses, but
-to some degree (with the non-deterministic specifications) we can have an
-illution that there is some total order.
-
-2. Local State: Beside of having one global state (the one that we have in the
-old approach), we also allow each method call to have a local state. This local
-state is the accumulative side effects of the subset of method calls that happen
-before the current method call. As an analogy to the cache-memory model, the
-local state we define here is similar to cache, a local state is local to the
-sense that the current method call must have seen those effects. The main goal
-of having this is to support tighter non-deterministic specifications.
-
-To evaluate the local state of each method call, an obvious approach is to
+Previously, we keep a sequential state throughout the process of executing the
+sequential history. In our model, we keep a state local to each method call.
+Conceptually, this state is the accumulative side effects of the subset of
+method calls that happen before the current method call.
+
+To evaluate the state of each method call, an obvious approach is to
execute the subset of methods that happen before the current method in the
sequential order from the initial state. A optimization we can make is that we
start to evaluate the state from the most recent deviding node which every other
-node in that subset is either hb before or after. Also, since local states are
-not required in specifications all the time, it is only evaluated when needed.
+node in that subset is either hb before or after.
III. Specifications
-Our specification language supports using the following primitives to access
-both global state and local state so that users can use those to write
-specifications with different level of tightness.
+Our specification language supports using the following primitives to access the
+state of method calls so that users can use those to write specifications with
+different level of tightness.
To support tighter specifications, we introduce the concept of concurrent set of
method calls, meaning that for a specific method call, it can basically see the
1. CONCURRENT: This primitive extracts all the methods that executes
"concurrently" with the current method --- neither hb/SC before nor after the
-current method --- and returns as a set. It is worth noting that the concurrent
-method calls cannot be accessed for calculating local state but only for
-assertions.
+current method --- and returns as a set. It is worth noting that in order to
+preserve composability, when evaluating the state, the concurrent method calls'
+information cannot be used. That is to say, the concurrent set of mehtods are
+only used for assertions.
2. PREV: This primitive extracts all the methods that execute right before the
current method in the execution graph --- most recent method calls that are
hb/SC before the current method call --- and returns as a set. For each method
-in this set, the current method's specification can access their local state.
+in this set, the current method's specification can access their state.
3. NEXT: This primitive extracts all the methods that execute right after the
current method in the execution graph, and returns as a set. For each method in
-this set, the current method's specification cannot access their local state.
-
-4. LOCAL: This primitive allows users to access the local state of a method
-call. It is worth noting that in order to calculate the local state of a method
-call, one can only access the set of method calls that happen before the current
-method call.
-
-Our specifications allow two ways of calculating the local states, a default way
-and a user-customized way. The default approach is to execute the set of method
-calls that happen before the current method call in the sequential order, and a
-the user-customized approach supports users to calculate the local state by
-using the PREV primitive to access the local state of previous method calls.
-
-5. COPY: This is the function that users provide to deep-copy the state. We
-require users to provide such a primitive function because each local state
-should be have its own copy.
-
-6. FINALLY: This is the function that allows users to specify some final check
-on the state. Initially, this check will only access the global state. However,
-for the concern of expressiveness, we allow users to access the initial state,
-meaning that users can basically access the whole graph and the local state of
-each method call. This will enable to users to use the graph model (the relaxed
+this set, the current method's specification CANNOT access their state (for
+preserving composability).
+
+// FIXME: This might break composability!!??!!
+4. FINAL: This is the function that allows users to specify some final check
+on the state. This will enable to users to use the graph model (the relaxed
atomics can be specified) although the complxity of using that can get quite
complex.
-IV. Examples
+Our specifications allow two ways of evaluating the state of method calls. One
+way is to define "@Transition" on method calls, and then our checker executes
+the method calls that are hb/SC before me in the sequential order starting from
+the initial state. The other way is to define "@EvaluateState" after
+"@Transition", which can only access the states of method calls that are hb/SC
+before it. Usually users calculate the state by using the PREV primitive to
+access the state of previous method calls.
-// Global specification
-@DeclareState: // Declare the state structure
-@InitState: // How do we initialize the state
-@CopyState: // A function on how to copy an existing state
+IV. Specification Details
+
+/// Global specification
+@State: // Declare the state structure
+@Initial: // How do we initialize the state
@Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return
// value and the arguments of the two method calls
-// Interface specification
+/// Interface specification
@Interface: InterfaceName // Required; a label to represent the interface
-@LocalState: // Optional; to calculate the accumulative local state before this
- // method call in a customized fashion. If not specified here, the
- // local state would be default, which is the result of the
- // execution on the subset of method calls in the sequential order
+@Transition: // Optional; the transitional side effect from the initial state to
+ // the current method call by executing such effect on method calls
+ // that are hb/SC before me in sequential order. When this field is
+ // omitted, the current state seen before checking is the same as
+ // the initial state.
+@EvaluateState: // Optional; to calculate the state before this
+ // method call is checked in a customized fashion. This is
+ // evaluated after "@Transition". If omitted, the state we would
+ // see is the effect after the "@Transition".
@PreCondition: // Optional; checking code
-@LocalSideEffect: // Optional; to calculate the side effect this method call
- // have on the local state in a customized fashion. If this
- // field is not stated, it means we don't care about it.
-@SideEffect: // Optional; to calculate the side effect on the global state. When
- // the "@LocalSideEffect" specification is ommitted, we also impose the
- // same side effect on the set of method calls that happen before this
- // method call in the sequential order.
+@SideEffect: // Optional; to calculate the side effect this method call
+ // have on the state after the "@PreCondition".
@PostCondition: // Optional; checking code
-// Ordering point specification
+
+/// Convienient operations
+We define a struct called MethodCall to represent the data we would collect and
+communicate between the real execution and the checking process.
+
+
+STATE(field) // A primitive to access the current state in the interface
+ // specification by the name of the field. We can use this as a
+ // lvalue & rvalue ==> "STATE(x) = 1" and "int i = STATE(x)" are
+ // both okay
+
+ // This can also be used to refer to the state of a method item
+ // in the Subset operation (see Subset)
+
+NAME // Used to refer to the name of a method item in the Subset
+ // operation (see Subset)
+
+RET(type) // Used to refer to the return value of a method item in the
+ // Subset operation (see Subset)
+
+ARG(type, arg) // Used to refer to the argument of a method item in the
+ // Subset operation (see Subset)
+
+
+PREV // Represent the set of previous method calls of the current method
+ // call
+
+CONCURRENT // Represent the set of concurrent method calls of the current
+ // method call
+
+NEXT // Represent the set of next method calls of the current method
+ // call
+
+Name(method) // The interface label name of the specific method
+
+State(method, field) // A primitive to access a specific state field of a
+ // specific method. Also used as lvalue and rvalue
+
+Ret(method, type) // The return value of the specific method; type should
+ // be the name of the interface label
+
+Arg(method, type, arg) // The arguement by name of the specific method; type should
+ // be the name of the interface label, and arg should be
+ // the name of the argument
+
+Prev(method) // Represent the set of previous method calls of the
+ // specific method call
+
+Next(method) // Represent the set of next method calls of the specific
+ // method call
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+ForEach(item, container) { ... } // Useful iteration primitive
+
+NewMethodSet // Create a new method set (set<MethodCall*>*)
+
+MakeSet(type, oldset, newset, field); // Construct a new set from an
+ // old set. We extract a specific field of that set item
+ // and form a new set. Specifically we expect users to
+ // use this on MethodSet. For example, if we want to
+ // construct an integer set from the state "x" of
+ // the previous methods, we use "MakeSet(int, PREV,
+ // newset, STATE(x))", and the newset contains the new
+ // set
+
+Subset(set, condition) // A generic subset operation that takes a condition and
+ // returns all the item for which the boolean guard
+ // holds. The condition can be specified with GUARD or
+ // GeneralGuard shown as follow.
+
+HasItem(set, condition) // A generic set operation that takes a condition and
+ // returns if there exists any item in "set" for which
+ // the condition holds. Its syntax is similar to that of
+ // Subset() operation
+
+Size(container) // Return the size of a container type
+
+Belong(container, item) // Return if item is in the container
+
+Union(set1, set2) // Union of two sets
+
+Intesection(set1, set2) // Intersection of two sets
+
+Subtract(set1, set2) // Returns the new set that represents the result of
+ // set1-set2
+Insert(set, item) // Insert item to set
+
+Insert(set, others) // Insert the whole set "others" to "set"
+
+ITEM // Used to refer to the set item in the GeneralGuard shown below
+
+GeneralGuard(type, expression) // Used as a condition for any set<T> type. We
+ // use "ITEM" to refer to a set item. For
+ // example, a subset of positive elements on an
+ // IntSet "s" would be
+ // "Subset(s, GeneralGuard(int, ITEM > 0))"
+
+Guard(expression) // Used specifically for MethodSet(set<MethodCall*>). An
+ // example to extract the subset of method calls in the PREV
+ // set that is a "Store" method and whose state "x" is equal
+ // to "val" and the return value is 5 would be
+ // "Subset(PREV, Guard(STATE(x) == val && NAME == "Store" &&
+ // RET(Store) == 5))"
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+
+To make things easier, we have the following helper macros.
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+/**
+ This is a common macro that is used as a constant for the name of specific
+ variables. We basically have two usage scenario:
+ 1. In Subset operation, we allow users to specify a condition to extract a
+ subset. In that condition expression, we provide NAME, RET(type), ARG(type,
+ field) and STATE(field) to access each item's (method call) information.
+ 2. In general specification (in pre- & post- conditions and side effects),
+ we would automatically generate an assignment that assign the current
+ MethodCall* pointer to a variable namedd _M. With this, when we access the
+ state of the current method, we use STATE(field) (this is a reference
+ for read/write).
+*/
+#define ITEM _M
+#define _M ME
+
+#define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
+#define CAT_HELPER(a, b) a ## b
+#define X(name) CAT(__##name, __LINE__) /* unique variable */
+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
+
+*****************************************************************************
+typedef struct MethodCall {
+ string name; // The interface label name
+ void *value; // The pointer that points to the struct that have the return
+ // value and the arguments
+ void *state; // The pointer that points to the struct that represents
+ // the state
+ set<MethodCall*> *prev; // Method calls that are hb right before me
+ set<MethodCall*> *concurrent; // Method calls that are concurrent with me
+ set<MethodCall*> *next; // Method calls that are hb right after me
+} MethodCall;
+
+typedef MethodCall *Method;
+typedef set<Method> *MethodSet;
+
+typedef vector<int> IntVector;
+typedef list<int> IntList;
+typedef set<int> IntSet;
+*****************************************************************************
+
+We will automatically generate two types of struct. One is the state struct, and
+we will call it StateStruct. The other one is a per interface struct, and it
+wraps the return value (RET) and the arguments as its field. We will name those
+struct with the interface label name.
+
+-----------------------------------------------------------------------------
+For example, if we declare an ordered integer list in the specification state ,
+we will generate a struct as follow.
+
+@State: IntList *queue;
+@Initial: queue = new IntList;
+@...
+
+===>
+typedef struct StateStruct {
+ IntList *queue;
+} StateStruct;
+
+-----------------------------------------------------------------------------
+If we have two interface whose specifications are as follow, we would generate
+two struct accordingly.
+
+@Interface: Store
+@...
+void store(atomic_int *loc, int val) ...
+
+@Interface: Load
+@...
+int load(atomic_int *loc) ...
+
+===>
+typedef struct Store {
+ atomic_int *loc;
+ int val;
+} Store;
+
+typedef struct Load {
+ int RET;
+ atomic_int *loc;
+} Load;
+
+-----------------------------------------------------------------------------
+We will put all these generated struct in a automatically-generated header file
+called "generated.h". This file also includes header files that have commonly
+used data types that interface (return value and arguments) accesses. In order
+to make things work, users should include "generated.h" file in the end for
+using our specification checker.
+
+*****************************************************************************
+
+
+/// Ordering point specification
@OPDefine: condition // If the specified condition satisfied, the atomic
// operation right before is an ordering point
// statement
+V. Examples
+
+!!!!!!! The register example should be extended to commute if we think of their
+transitional effects as set operations --- a set operation that will only mask
+out side the effects of its own previous behavior (things that are hb/SC before
+it) ---- VERY IMPORTANT note here!!
+
+
1. The register examples: Basically, we can think of registers as the cache on a
memory system. The effect of a load or store basically tells us what the current
value in the cache line is, and a load can read from values that can be
potentially in the cache --- either one of the concurrent store update the cache
-or it inherites one of the the previous local state in the execution graph.
+or it inherites one of the the previous state in the execution graph.
---------- Interfae ----------
void init(atomic_int &loc, int initial);
// For RA atomics, a load must read its value from a store that happens before
// it.
---------- Specification ----------
-@DeclareVar: int x;
-@InitVar: x = 0;
+@State: int x;
+@Initial: x = 0;
+@Commutativity: Store <-> Store(true)
+@Commutativity: Load <-> Load(true)
+@Commutativity: Store <-> Load(true)
+/** No @Transition */
@Interface: Store
-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;
void store(int *loc, int val);
@Interface: Load
@PreCondition:
- Size(Subset(PREV, LOCAL(x) == RET)) > 0;
-@SideEffect: LOCAL(x) = RET;
+ return HasItem(PREV, STATE(x) == RET);
+@SideEffect: STATE(x) = RET;
int load(int *loc);
c. The C/C++ atomics (a slightly loose specification)
any store that either immediately happens before it or concurrently executes.
-
-// We define a struct called MethodCall to represent the data we would collect
-// and communicate between the real execution and the checking process
-typedef struct MethodCall {
- string interfaceName; // The interface label name
- void *value; // The pointer that points to the struct that have the return
- // value and the arguments
- void *localState; // The pointer that points to the struct that represents
- // the (local) state
- vector<MethodCall*> *prev; // Method calls that are hb right before me
- vector<MethodCall*> *next; // Method calls that are hb right after me
- vector<MethodCall*> *concurrent; // Method calls that are concurrent with me
-} MethodCall;
-
-We will automatically generate two types of struct. One is the state struct, and
-we will call it StateStruct. This state is shared by all the global and local
-state. The other one is a per interface struct, and it wraps the return value
-(RET) and the arguments as its field. We will name those struct with the
-interface label name.
-
-// Some very nice C/C++ macro definition to make specifications a lot easier
-// 1. ForEach --> to iterate all
-#define ForEach(item, list) \
- for (iterator<MethodCall*> _mIter = list->begin(), \
- MethodCall *item = *_mIter; _mIter != list->end(); item = (++iter != \
- list->end()) ? *_mIter : NULL)
-
-
-*********************************************
-// 1.1 Subset(set, guard) --> to get a subset of method calls by a boolean
-// expression; This takes advantage of C++11 std::function features and C macros.
-
-// 1.2 Size(set) --> to get the size of a method set
-#define Size(set) set->size()
-
-// 1.3 Belong(set, method) --> whether method belongs to set
-#define Belong(set, method) std::find(set->begin(), set->end(), method) != set->end()
-
-// 1.4 Intersect(set1, set2) --> the intersection of two method sets
-inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
- MethodSet res = NewSet;
- ForEach (m, set1) {
- if (Belong(set2, m))
- res->push_back(m);
- }
- return res;
-}
-
-// 1.5 Union(set1, set2) --> the union of two method sets
-inline MethodSet Union(MethodSet set1, MethodSet set2) {
- MethodSet res = NewSet(set1);
- ForEach (m, set2) {
- if (!Belong(set1, m))
- res->push_back(m);
- }
- return res;
-}
-
-// 1.6 Insert(set, method) --> add a method to the set
-inline bool Insert(MethodSet set, Method m) {
- if (Belong(set, m))
- return false;
- else {
- set->push_back(m);
- return true;
- }
-}
-
-// 1.7 Subtract(set1, set2) --> subtract set2 from set1
-inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
- MethodSet res = NewSet;
- ForEach (m, set1) {
- if (!Belong(set2, m))
- res->push_back(m);
- }
- return res;
-}
-
-// 1.8 MakeSet(count, ...) --> Make a set from the arguments
-
-
-// 2. Local(method, field)
-#define Local(method, field) ((StateStruct*) method->localState)->field
-
-// 3. Value(method, type, field)
-#define Value(method, type, field) ((type*) method->value)->field
-3.1 Return
-#define Ret(method, type) Value(method, type, RET)
-3.2 Arguments
-#define Arg(method, type, arg) Value(method, type, arg)
-
-
-// 4. Name(mehtod)
-#defien Lable(method) method->interfaceName
-
-// 5. Prev(method)
-#define Prev(method) mehtod->prev
-
-// 6. Next(method)
-#define Next(method) mehtod->next
-
-// 7. Concurrent(method)
-#define Concurrent(method) mehtod->concurrent
-
-
---------- Specification ----------
-@DeclareVar: int x;
-@InitVar: x = 0;
+@State: int x;
+@Initial: x = 0;
@Interface: Store
-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;
void store(int *loc, int val);
@PreCondition:
// Auto generated code
// MethodCall *ME = ((SomeTypeConversion) info)->method;
-
- int count = Size(Subset(Prev, LOCAL(x) == RET))
- + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET))
- return count > 0;
-@SideEffect: LOCAL(x) = RET;
+
+ return HasItem(Prev, STATE(x) == RET) ||
+ + HasItem(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET)
+@SideEffect: STATE(x) = RET;
int load(int *loc);
d. The C/C++ normal memory accesses
@Copy: New.q = new vector<int>(Old.q);
// Fails to dequeue
@Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET)
-// The dequeuer doesn't dequeue from that enqueuer
-@Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
+@Commutativity: Enq <-> Deq (true)
@Interface: Enq
-@SideEffect: q->push_back(val);
+@Transition: q->push_back(val);
void enq(queue_t *q, int val);
@Interface: Deq
+@Transition: if (RET) q->pop_back();
@PreCondition:
// Check whether the queue is really empty
- // Either the local state is an empty queue, or for all those remaining
- // elements in the local queue, there should be some concurrent dequeuers to
+ // Either the state is an empty queue, or for all those remaining
+ // elements in the queue, there should be some concurrent dequeuers to
// dequeue them
if (!RET) {
- // Local state is empty
- if (Local(q)->size() == 0) return true;
+ // State is empty
+ if (STATE(q)->size() == 0) return true;
// Otherwise check there must be other concurrent dequeuers
- ForEach (item, Local(q)) {
+ ForEach (item, State(q)) {
// Check there's some concurrent dequeuer for this item
- if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) &&
- *ARG(Deq, res) == item)) == 0) return false;
+ if (!HasItem(CONCURRENT, NAME == "Deq" && RET(Deq) &&
+ *ARG(Deq, res) == item)) return false;
}
return true;
} else { // Check the global queue state
return q->back() == *res;
}
-@SideEffect:
- if (RET) q->pop_back();
bool deq(queue_t *q, int *res);
-
+*******************************************************************************
A good example to simulate a queue data structure is as follows.
Suppose we have a special structure
typedef struct Q {
, and we have two interface on Q, read() and write(), where the write and read
method calls are synchronized by themselves, and they have to read and write the
x and y fields in turn.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-----------------------------------------------------------------------------------------
-We also need to think about the non-ordered queue.
-
-####
-Combiming Data Structures ---
-For example, a queue, a -hb->c, b -hb-> e.
-
-// T1
-enq(1) -> {1} - {$} // a
-enq(2) -> {1, 2} - {$} // b
-
-// T2
-deq(1) -> {$} - {1} // c
-deq($) -> {$} - {1} // d
-
-// State before this method
-JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
-deq(2) -> {$} - {1, 2}
-
-
-
-
-
projects / cdsspec-compiler.git / blobdiff