edits

diff --git a/notes/definition.cc b/notes/definition.cc
index 0c5b7965174727e5414f005c0421f33188937e35..fda4ebac8765b298d3726e669281bf32882f8145 100644 (file)
--- a/notes/definition.cc
+++ b/notes/definition.cc
@@ -127,6 +127,21 @@ inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
        return res;
 }
 
        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.
 /**
        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));
        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) {
        ForEach (i, newis) {

-               cout << "elem: " << i << endl;
+               //cout << "elem: " << i << endl;

        }
 
 
        }
 
 

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index d1011dce5e81e83fddcc5eb1bdeb8d8fd810dedb..70383b31e544e2e94168adbcb061958c78e68167 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -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.
 
 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
 
 /// 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*>*)
 
 
 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.
 
 
 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
 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,
        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
        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
        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
 /// 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
 
 
                                                        // 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
 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);
 
 ----------   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   ----------
 // 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
 @Interface: Store

-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;

 void store(int *loc, int val);
 
 @Interface: Load
 @PreCondition:
 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)
 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   ----------
 
 
 ----------   Specification   ----------

-@DeclareVar: int x;
-@InitVar: x = 0;
+@State: int x;
+@Initial: x = 0;

 
 @Interface: Store
 
 @Interface: Store

-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;

 void store(int *loc, int 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;
 @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
 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)
 @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
 
 @Interface: Enq

-@SideEffect: q->push_back(val);
+@Transition: q->push_back(val);

 void enq(queue_t *q, int val);
 
 @Interface: Deq
 void enq(queue_t *q, int val);
 
 @Interface: Deq

+@Transition: if (RET) q->pop_back();

 @PreCondition:
        // Check whether the queue is really empty
 @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) {
        // 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
                // 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
                        // 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;
        }
                }
                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);
 
 
 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 {
 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.
 , 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}
-
-
-
-
-