edits
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 29 Jan 2016 01:14:09 +0000 (17:14 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 29 Jan 2016 01:14:09 +0000 (17:14 -0800)
notes/definition.cc
notes/nondeterm-spec.txt

index 46fdc84..457b609 100644 (file)
@@ -1,10 +1,13 @@
 #include <iostream>
 #include <vector>
+#include <list>
 #include <string>
 #include <iterator>
 #include <algorithm>
 #include <set>
 
+#include <stdarg.h>
+
 using namespace std;
 
 typedef struct MethodCall {
@@ -13,17 +16,21 @@ typedef struct MethodCall {
                                 // 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
+       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
 } MethodCall;
 
 typedef MethodCall *Method;
-typedef vector<Method> *MethodSet;
+typedef set<Method> *MethodSet;
+
+typedef vector<int> IntVector;
+typedef list<int> IntList;
+typedef set<int> IntSet;
 
-typedef vector<int> IntList;
+/********** More general specification-related types and operations **********/
 
-#define NewSet new vector<Method>
+#define NewSet new set<Method>
 
 #define CAT(a, b) CAT_HELPER(a, b) /* Concatenate two symbols for macros! */
 #define CAT_HELPER(a, b) a ## b
@@ -33,59 +40,87 @@ typedef vector<int> IntList;
        The set here is a vector<MethodCall*>* type, or the MethodSet type. And the
        item would become the MethodCall* type, or the Method type
 */
-#define ForEach(item, set) \
+#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)
 
-inline MethodSet Subset(MethodSet set, string name) {
-       MethodSet _subset = NewSet;
-       ForEach (_m, set) {
-               if (_m->interfaceName == name)
-                       _subset->push_back(_m);
-       }
-       return _subset;
-}
+#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
+*/
+
+#define _M ME
+
+#define NAME Name(_M)
+
+#define LOCAL(field) Local(_M, field)
+
+#define VALUE(type, field) Value(_M, type, field)
 
-#define Size(set) (set->size())
+#define Subset(s, subset, condition) \
+       MethodSet original = s; \
+       MethodSet subset = NewSet; \
+       ForEach (_M, original) { \
+               if ((condition)) \
+                       subset->insert(_M); \
+       } \
 
-#define Belong(set, method) (std::find(set->begin(), set->end(), method) \
-       != set->end())
+/** General for set, list & vector */
+#define Size(container) ((container)->size())
 
-inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
-       MethodSet res = NewSet;
-       ForEach (m, set1) {
-       if (Belong(set2, m))
-               res->push_back(m);
+#define _BelongHelper(type) \
+       template<class T> \
+       inline bool Belong(type<T> *container, T item) { \
+               return std::find(container->begin(), \
+                       container->end(), item) != container->end(); \
+       }
+
+_BelongHelper(set)
+_BelongHelper(vector)
+_BelongHelper(list)
+
+/** General set operations */
+template<class T>
+inline set<T>* Intersect(set<T> *set1, set<T> *set2) {
+       set<T> *res = new set<T>;
+       ForEach (item, set1) {
+               if (Belong(set2, item))
+                       res->insert(item);
        }
        return res;
 }
 
-inline MethodSet Union(MethodSet set1, MethodSet set2) {
-       MethodSet res = NewSet(*set1);
-       ForEach (m, set2) {
-               if (!Belong(set1, m))
-                       res->push_back(m);
-       }
+template<class T>
+inline set<T>* Union(set<T> *s1, set<T> *s2) {
+       set<T> *res = new set<T>(*s1);
+       ForEach (item, s2)
+               res->insert(item);
        return res;
 }
 
-inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
-       MethodSet res = NewSet;
-       ForEach (m, set1) {
-               if (!Belong(set2, m))
-                       res->push_back(m);
+template<class T>
+inline set<T>* Subtract(set<T> *set1, set<T> *set2) {
+       set<T> *res = new set<T>;
+       ForEach (item, set1) {
+               if (!Belong(set2, item))
+                       res->insert(item);
        }
        return res;
 }
 
-inline bool Insert(MethodSet set, Method m) {
-       if (Belong(set, m))
-               return false;
-       else {
-               set->push_back(m);
-               return true;
-       }
+template<class T>
+inline void Insert(set<T> *s, T item) { s->insert(item); }
+
+template<class T>
+inline void Insert(set<T> *s, set<T> *others) {
+       ForEach (item, others)
+               s->insert(item);
 }
 
 inline MethodSet MakeSet(int count, ...) {
@@ -95,21 +130,20 @@ inline MethodSet MakeSet(int count, ...) {
        va_start (ap, count);
        res = NewSet;
        for (int i = 0; i < count; i++) {
-               Method m = va_arg (ap, Method);
-               if (!Belong(res, m))
-                       res->push_back(m);
+               Method item = va_arg (ap, Method);
+               res->insert(item);
        }
        va_end (ap);
        return res;
 }
 
+/********** Method call related operations **********/
+#define Name(method) method->interfaceName
 
 #define Local(method, field) ((StateStruct*) method->localState)->field
 
 #define Value(method, type, field) ((type*) method->value)->field
 
-#define Label(method) method->interfaceName
-
 #define Prev(method) method->prev
 #define PREV ME->prev
 
@@ -122,7 +156,7 @@ inline MethodSet MakeSet(int count, ...) {
 // This auto-generated struct can have different fields according to the read
 // state declaration. Here it's just a test example
 typedef struct StateStruct {
-       IntList *list;
+       int x;
 } StateStruct;
 
 // These auto-generated struct can have different fields according to the return
@@ -139,19 +173,56 @@ typedef struct Load {
 } Load;
 
 int main() {
-       Method ME = NULL;
-       MethodSet set = NewSet;
-       ForEach (m, Subset(set, "Store")) {
-               IntList *l = Local(m, list);
-               int ret = Value(m, Load, RET);
-               string name = Label(m);
-       }
-       ForEach (m, Prev(ME)) {
-
-       }
-
-       int size = Size(PREV);
-       bool flag = Belong(CONCURRENT, ME);
-       flag = Belong(MakeSet(3, ME, ME, ME), ME);
+       set<int> *is1 = new set<int>;
+       set<int> *is2 = new set<int>;
+
+       list<int> *il1 = new list<int>;
+       list<int> *il2 = new list<int>;
+
+       il1->push_back(2);
+       il1->push_back(3);
+       
+       is1->insert(1);
+       is1->insert(3);
+       
+       is2->insert(4);
+       is2->insert(5);
+
+
+       MethodSet ms = NewSet;
+       Method m = new MethodCall;
+       m->interfaceName = "Store";
+       StateStruct *ss = new StateStruct;
+       ss->x = 1;
+       m->localState = ss;
+       Store *st = new Store;
+       st->val = 2;
+       m->value = st;
+       ms->insert(m);
+
+       m = new MethodCall;
+       m->interfaceName= "Store";
+       ss = new StateStruct;
+       ss->x = 2;
+       m->localState = ss;
+       st = new Store;
+       st->val = 0;
+       m->value = st;
+       ms->insert(m);
+
+       m = new MethodCall;
+       m->interfaceName= "Load";
+       ss = new StateStruct;
+       ss->x = 0;
+       m->localState = ss;
+       Load *ld = new Load;
+       ld->RET = 2;
+       m->value = ld;
+       ms->insert(m);
+       
+       //Subset(ms, sub, NAME == "Store" && VALUE(Store, val) != 0);
+       Subset(ms, sub, NAME == "Store" && VALUE(Store, val) >= 0 && LOCAL(x) == 0);
+
+       cout << "Size=" << Size(sub) << endl;
        return 0;
 }
index f86c661..e6dfb05 100644 (file)
@@ -156,19 +156,14 @@ b. The RA (release/acquire) C/C++ atomics
 @InitVar: x = 0;
 
 @Interface: Store
-@SideEffect:
-       LOCAL.x = val;
+@SideEffect: LOCAL(x) = val;
 void store(int *loc, int val);
 
 @Interface: Load
 @PreCondition:
-       IntegerSet *prevSet = new IntegerSet;
-       for (m in PREV) {
-               prevSet->add(m.LOCAL.x);
-       }
-       return prevSet->contains(RET);
-@SideEffect:
-       LOCAL.x = RET;
+       Subset(PREV, subset, LOCAL(x) == RET);
+       return Size(subset) > 0;
+@SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 
 c. The C/C++ atomics (a slightly loose specification)
@@ -189,14 +184,7 @@ 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;
 
-@Interface: Store
-@SideEffect:
-       LOCAL.x = val;
-void store(int *loc, int val);
 
 // We define a struct called MethodCall to represent the data we would collect
 // and communicate between the real execution and the checking process
@@ -297,7 +285,7 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 // 3. Value(method, type, field)
 #define Value(method, type, field) ((type*) method->value)->field
 
-// 4. Lable(mehtod)
+// 4. Name(mehtod)
 #defien Lable(method) method->interfaceName
 
 // 5. Prev(method)
@@ -309,21 +297,26 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 // 7. Concurrent(method)
 #define Concurrent(method) mehtod->concurrent
 
+
+----------   Specification   ----------
+@DeclareVar: int x;
+@InitVar: x = 0;
+
+@Interface: Store
+@SideEffect: LOCAL(x) = val;
+void store(int *loc, int val);
+
+
 @Interface: Load
 @PreCondition:
        // Auto generated code
        // MethodCall *ME = ((SomeTypeConversion) info)->method;
-
-       IntegerSet prevSet, concurSet;
-       ForEach(m, PREV) {
-               prevSet->insert(LOCAL(m, x));
-       }
-       ForEach (m, Subset(CONCURRENT, "STORE")) {
-               concurSet->insert(Value(m, STORE, val));
-       }
-       return prevSet->contains(RET) || concurSet->contains(RET);
-@SideEffect:
-       LOCAL.x = RET;
+       
+       Subset(Prev, readSet1, LOCAL(x) == RET);
+       if (Size(readSet1) > 0) return true;
+       Subset(Concurrent, readSet2, NAME == "Store" && VALUE(Store, val) == RET);
+       return Size(readSet2) > 0;
+@SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 
 d. The C/C++ normal memory accesses
@@ -350,9 +343,8 @@ on the admissible executions
 // The dequeuer doesn't dequeue from that enqueuer
 @Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
 
-@Interface: Enq 
-@SideEffect:
-       LOCAL.x = val;
+@Interface: Enq
+@SideEffect: q->push_back(val);
 void enq(queue_t *q, int val);
 
 @Interface: Deq
@@ -363,25 +355,20 @@ void enq(queue_t *q, int val);
        // dequeue them
        if (!RET) {
                // Local state is empty
-               if (Local.q->size() == 0) return true;
+               if (Local(q)->size() == 0) return true;
                // Otherwise check there must be other concurrent dequeuers
-               for (int i = 0; i < Local.q->size(); i++) {
-                       int item = (*Local.q)[i];
+               ForEach (item, Local(q)) {
                        // Check there's some concurrent dequeuer for this item
-                       bool flag = false;
-                       ForEach (m, Subset(CONCURRENT, "Deq")) {
-                               if (Value(m, Deq, RET) && *Value(m, Deq, res) == item)
-                                       flag = true;
-                       }
-                       if (!flag) return false;
+                       Subset(CONCURRENT, concurSet, NAME == "Deq" && VALUE(Deq, RET) &&
+                               *VALUE(Deq, res) == item);
+                       if (Size(concurSet) == 0) return false;
                }
                return true;
        } else { // Check the global queue state
                return q->back() == *res;
        }
 @SideEffect:
-       if (RET)
-               Global.q->back()
+       if (RET) q->pop_back();
 bool deq(queue_t *q, int *res);