edits
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 30 Jan 2016 07:28:34 +0000 (23:28 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 30 Jan 2016 07:28:34 +0000 (23:28 -0800)
notes/definition.cc
notes/nondeterm-spec.txt

index 0c5b796..fda4eba 100644 (file)
@@ -127,6 +127,21 @@ inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
        return res;
 }
 
+/**
+       A general set operation that takes a condition and returns if there exists
+       any item for which the boolean guard holds.
+*/
+template <class T>
+inline bool HasItem(set<T> *original, std::function<bool(T)> condition) {
+       ForEach (_M, original) {
+               if (condition(_M))
+                       return true;
+       }
+       return false;
+}
+
+
+
 /**
        A general sublist operation that takes a condition and returns all the item
        for which the boolean guard holds in the same order as in the old list.
@@ -313,9 +328,10 @@ int main() {
        ms->insert(m);
 
        MakeSet(int, ms, newis, STATE(x));
-       cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+       //cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+       cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == 2)) << endl;
        ForEach (i, newis) {
-               cout << "elem: " << i << endl;
+               //cout << "elem: " << i << endl;
        }
 
 
index d1011dc..70383b3 100644 (file)
@@ -64,7 +64,7 @@ the initial state. The other way is to define "@EvaluateState" after
 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
@@ -144,13 +144,39 @@ ForEach(item, container) { ... }  // Useful iteration primitive
 
 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
@@ -177,11 +203,11 @@ To make things easier, we have the following helper macros.
        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
@@ -264,121 +290,6 @@ using our specification checker.
 *****************************************************************************
 
 
-// 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
@@ -403,11 +314,12 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
                                                        // 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);
@@ -421,17 +333,21 @@ b. The RA (release/acquire) C/C++ atomics
 // 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)
@@ -454,11 +370,11 @@ any store that either immediately happens before it or concurrently executes.
 
 
 ----------   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);
 
 
@@ -466,11 +382,10 @@ 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
@@ -494,38 +409,36 @@ on the admissible executions
 @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 {
@@ -536,45 +449,3 @@ 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}
-
-
-
-
-