edits
authorPeizhao Ou <peizhaoo@uci.edu>
Sat, 30 Jan 2016 05:42:47 +0000 (21:42 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Sat, 30 Jan 2016 05:42:47 +0000 (21:42 -0800)
notes/definition.cc
notes/nondeterm-spec.txt

index 054ff89..bcc01e7 100644 (file)
@@ -16,8 +16,8 @@ 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
+       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*> *next; // Method calls that are hb right after me
        set<MethodCall*> *concurrent; // Method calls that are concurrent with me
@@ -39,34 +39,25 @@ typedef set<int> IntSet;
 #define X(name) CAT(__##name, __LINE__) /* unique variable */
 
 /**
-       The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
-       item would become the MethodCall* type, or the Method type
+       This is a generic ForEach primitive for all the containers that support
+       using iterator to iterate.
 */
-#define ForEach1(item, set) \
-       int X(i) = 0; \
-       for (Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
-               X(i) < (set)->size(); X(i)++, item = X(i) < (set)->size() ? (*(set))[X(i)] : NULL)
-
 #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)
 
-/**
-       The subset operation is only for the MethodCall set
-*/
-
 /**
        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.
+       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
@@ -74,7 +65,7 @@ typedef set<int> IntSet;
 
 #define NAME Name(_M)
 
-#define LOCAL(field) Local(_M, field)
+#define STATE(field) State(_M, field)
 
 #define VALUE(type, field) Value(_M, type, field)
 #define RET(type) VALUE(type, RET)
@@ -93,9 +84,9 @@ typedef set<int> IntSet;
 
 /**
        This operation is specifically for Method set. For example, when we want to
-       construct an integer set from the local state field "x" (which is an
+       construct an integer set from the state field "x" (which is an
        integer) of the previous set of method calls (PREV), and the new set goes to
-       "readSet", we would call "MakeSet(int, PREV, readSet, LOCAL(x));". Then users
+       "readSet", we would call "MakeSet(int, PREV, readSet, STATE(x));". Then users
        can use the "readSet" as an integer set (set<int>)
 */
 #define MakeSet(type, oldset, newset, field) \
@@ -117,8 +108,8 @@ typedef set<int> IntSet;
 /**
        This is a more specific guard designed for the Method (MethodCall*). It
        basically wrap around the GeneralGuard with the type Method. An example to
-       extract the subset of method calls in the PREV set whose local state "x" is
-       equal to "val" would be "Subset(PREV, Guard(Local(x) == val))"
+       extract the subset of method calls in the PREV set whose state "x" is
+       equal to "val" would be "Subset(PREV, Guard(STATE(x) == val))"
 */
 #define Guard(expression) GeneralGuard(Method, expression)
 
@@ -235,7 +226,7 @@ inline MethodSet MakeSet(int count, ...) {
 /********** Method call related operations **********/
 #define Name(method) method->interfaceName
 
-#define Local(method, field) ((StateStruct*) method->localState)->field
+#define State(method, field) ((StateStruct*) method->state)->field
 
 #define Value(method, type, field) ((type*) method->value)->field
 #define Ret(method, type) Value(method, type, RET)
@@ -250,6 +241,10 @@ inline MethodSet MakeSet(int count, ...) {
 #define Concurrent(method) method->concurrent
 #define CONCURRENT  _M->concurrent
 
+
+/***************************************************************************/
+/***************************************************************************/
+
 // This auto-generated struct can have different fields according to the read
 // state declaration. Here it's just a test example
 typedef struct StateStruct {
@@ -269,10 +264,6 @@ typedef struct Load {
        int *loc;
 } Load;
 
-bool f1(Method m) {
-       return true;
-}
-
 int main() {
        set<int> *is1 = new set<int>;
        set<int> *is2 = new set<int>;
@@ -295,7 +286,7 @@ int main() {
        m->interfaceName = "Store";
        StateStruct *ss = new StateStruct;
        ss->x = 1;
-       m->localState = ss;
+       m->state = ss;
        Store *st = new Store;
        st->val = 2;
        m->value = st;
@@ -305,7 +296,7 @@ int main() {
        m->interfaceName= "Store";
        ss = new StateStruct;
        ss->x = 2;
-       m->localState = ss;
+       m->state = ss;
        st = new Store;
        st->val = 0;
        m->value = st;
@@ -315,13 +306,13 @@ int main() {
        m->interfaceName= "Load";
        ss = new StateStruct;
        ss->x = 0;
-       m->localState = ss;
+       m->state = ss;
        Load *ld = new Load;
        ld->RET = 2;
        m->value = ld;
        ms->insert(m);
 
-       MakeSet(int, ms, newis, LOCAL(x));
+       MakeSet(int, ms, newis, STATE(x));
        cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
        ForEach (i, newis) {
                cout << "elem: " << i << endl;
@@ -330,6 +321,6 @@ int main() {
 
        //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
        //cout << "Size=" << Size(Subset(ms, Guard(NAME == "Store" && ARG(Store, val)
-               //>= 0 && LOCAL(x) >= 0 ))) << endl;
+               //>= 0 && STATE(x) >= 0 ))) << endl;
        return 0;
 }
index 5bf44c3..e594157 100644 (file)
@@ -50,18 +50,20 @@ 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 state (for
 preserving composability).
 
-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.
-
 // FIXME: This might break composability!!??!!
-6. FINAL: This is the function that allows users to specify some final check
+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.
 
+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.
+
 IV. Examples
 
 /// Global specification
@@ -87,109 +89,120 @@ IV. Examples
 @PostCondition: // Optional; checking code
 
 
-/// Ordering point specification
-@OPDefine: condition   // If the specified condition satisfied, the atomic
-                                               // operation right before is an ordering point
+/// 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.
 
-@PotentialOP(Label): condition // If the specified condition satisfied, the
-                                                               // atomic operation right before is a potential
-                                                               // ordering point, and we label it with a tag
+*****************************************************************************
+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
+       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;
 
-@OPCheck(Label): condition     // If the specified condition satisfied, the
-                                                       // potential ordering point defined earlier with the
-                                                       // same tag becomes an ordering point
+typedef MethodCall *Method;
+typedef set<Method> *MethodSet;
 
-@OPClear: condition            // If the specified condition satisfied, all the
-                                               // ordering points and potential ordering points will be
-                                               // cleared
+typedef vector<int> IntVector;
+typedef list<int> IntList;
+typedef set<int> IntSet;
+*****************************************************************************
 
-@OPClearDefine: condition      // If the specified condition satisfied, all the
-                                                       // ordering points and potential ordering points will
-                                                       // be cleared, and the atomic operation right before
-                                                       // becomes an ordering point. This is a syntax sugar
-                                                       // as the combination of an "OPClear" and "OPDefine"
-                                                       // statement
+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.
 
-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.
+@State: IntList *queue;
+@Initial: queue = new IntList;
+@...
 
-----------   Interfae   ----------
-void init(atomic_int &loc, int initial);
-int load(atomic_int &loc);
-void store(atomic_int &loc, int val);
-----------   Interfae   ----------
+===>
+typedef struct StateStruct {
+       IntList *queue;
+} StateStruct;
 
-a. The SC atomics --- the classic linearizability approach
-
-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;
+-----------------------------------------------------------------------------
+If we have two interface whose specifications are as follow, we would generate
+two struct accordingly.
 
 @Interface: Store
-@SideEffect: LOCAL(x) = val;
-void store(int *loc, int val);
+@...
+void store(atomic_int *loc, int val) ...
 
 @Interface: Load
-@PreCondition:
-       Size(Subset(PREV, LOCAL(x) == RET)) > 0;
-@SideEffect: LOCAL(x) = RET;
-int load(int *loc);
+@...
+int load(atomic_int *loc) ...
 
-c. The C/C++ atomics (a slightly loose specification)
-// Actually, any concurrent data structures that rely modification-order to be
-// correct would not have a precicely tight specification under our model, and
-// C/C++ relaxed atomics is an example. See the following read-read coherence
-// example.
+===>
+typedef struct Store {
+       atomic_int *loc;
+       int val;
+} Store;
 
-// T1                          // T2
-x = 1;                         x = 2;
+typedef struct Load {
+       int RET;
+       atomic_int *loc;
+} Load;
 
-// T3
-r1 = x; // r1 == 1
-r2 = x; // r2 == 2
-r3 = x; // r3 == 1
+-----------------------------------------------------------------------------
+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.
 
-Our model cannot prevent such a case from happening. However, we can still have
-a slightly loose specification which basically states that a load can read from
-any store that either immediately happens before it or concurrently executes.
+*****************************************************************************
 
 
+// Some nice C/C++ macro definition to make specifications easier to write
 
-// 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;
+-----------------------------------------------------------------------------
+#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 */
 
-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. 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.
 
@@ -266,6 +279,80 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 #define Concurrent(method) mehtod->concurrent
 
 
+/// Ordering point specification
+@OPDefine: condition   // If the specified condition satisfied, the atomic
+                                               // operation right before is an ordering point
+
+@PotentialOP(Label): condition // If the specified condition satisfied, the
+                                                               // atomic operation right before is a potential
+                                                               // ordering point, and we label it with a tag
+
+@OPCheck(Label): condition     // If the specified condition satisfied, the
+                                                       // potential ordering point defined earlier with the
+                                                       // same tag becomes an ordering point
+
+@OPClear: condition            // If the specified condition satisfied, all the
+                                               // ordering points and potential ordering points will be
+                                               // cleared
+
+@OPClearDefine: condition      // If the specified condition satisfied, all the
+                                                       // ordering points and potential ordering points will
+                                                       // be cleared, and the atomic operation right before
+                                                       // becomes an ordering point. This is a syntax sugar
+                                                       // as the combination of an "OPClear" and "OPDefine"
+                                                       // statement
+
+
+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.
+
+----------   Interfae   ----------
+void init(atomic_int &loc, int initial);
+int load(atomic_int &loc);
+void store(atomic_int &loc, int val);
+----------   Interfae   ----------
+
+a. The SC atomics --- the classic linearizability approach
+
+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;
+
+@Interface: Store
+@SideEffect: LOCAL(x) = val;
+void store(int *loc, int val);
+
+@Interface: Load
+@PreCondition:
+       Size(Subset(PREV, LOCAL(x) == RET)) > 0;
+@SideEffect: LOCAL(x) = RET;
+int load(int *loc);
+
+c. The C/C++ atomics (a slightly loose specification)
+// Actually, any concurrent data structures that rely modification-order to be
+// correct would not have a precicely tight specification under our model, and
+// C/C++ relaxed atomics is an example. See the following read-read coherence
+// example.
+
+// T1                          // T2
+x = 1;                         x = 2;
+
+// T3
+r1 = x; // r1 == 1
+r2 = x; // r2 == 2
+r3 = x; // r3 == 1
+
+Our model cannot prevent such a case from happening. However, we can still have
+a slightly loose specification which basically states that a load can read from
+any store that either immediately happens before it or concurrently executes.
+
+
 ----------   Specification   ----------
 @DeclareVar: int x;
 @InitVar: x = 0;