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
NewMethodSet // Create a new method set (set<MethodCall*>*)
-MakeSet(NewSetType, oldset, newset, field); //
+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
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.
+ 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
- local state of the current method, we use LOCAL(field) (this is a reference
+ state of the current method, we use STATE(field) (this is a reference
for read/write).
*/
#define ITEM _M
*****************************************************************************
-// 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
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}
-
-
-
-
-
projects / cdsspec-compiler.git / commitdiff