before it. Usually users calculate the state by using the PREV primitive to
access the state of previous method calls.
-IV. Examples
+IV. Specification Details
/// Global specification
@State: // Declare the state structure
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 (local) state
+ // 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
*****************************************************************************
-// Some nice C/C++ macro definition to make specifications easier to write
-
------------------------------------------------------------------------------
-#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 */
-
-
-
------------------------------------------------------------------------------
-1. ForEach --> to iterate a set, list or vector (containers that support using
-iterator to iterate)
-
-#define ForEach(item, container) \
- auto X(_container) = (container); \
- auto X(iter) = X(_container)->begin(); \
- for (auto item = *X(iter); X(iter) != X(_container)->end(); item = ((++X(iter)) != \
- X(_container)->end()) ? *X(iter) : 0)
-
------------------------------------------------------------------------------
-
-/**
- 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 LOCAL(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
- local state of the current method, we use LOCAL(field) (this is a reference
- for read/write).
-*/
-#define ITEM _M
-#define _M ME
-
-
------------------------------------------------------------------------------
-
-// 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
-
-
/// 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)
---------- 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}
-
-
-
-
-