edits
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 28 Jan 2016 11:20:26 +0000 (03:20 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 28 Jan 2016 11:20:26 +0000 (03:20 -0800)
notes/definition.cc
notes/nondeterm-spec.txt

index 51fdd81..46fdc84 100644 (file)
@@ -2,6 +2,8 @@
 #include <vector>
 #include <string>
 #include <iterator>
+#include <algorithm>
+#include <set>
 
 using namespace std;
 
@@ -19,16 +21,137 @@ typedef struct MethodCall {
 typedef MethodCall *Method;
 typedef vector<Method> *MethodSet;
 
+typedef vector<int> IntList;
+
 #define NewSet new vector<Method>
 
+#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 */
+
 /**
        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) \
-       for (int i = 0, Method item = (set)->size() > 0 ? (*(set))[0] : NULL; \
-               i < (set)->size(); i++, 
+       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 Size(set) (set->size())
+
+#define Belong(set, method) (std::find(set->begin(), set->end(), method) \
+       != set->end())
+
+inline MethodSet Intersect(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet;
+       ForEach (m, set1) {
+       if (Belong(set2, m))
+               res->push_back(m);
+       }
+       return res;
+}
+
+inline MethodSet Union(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet(*set1);
+       ForEach (m, set2) {
+               if (!Belong(set1, m))
+                       res->push_back(m);
+       }
+       return res;
+}
+
+inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
+       MethodSet res = NewSet;
+       ForEach (m, set1) {
+               if (!Belong(set2, m))
+                       res->push_back(m);
+       }
+       return res;
+}
+
+inline bool Insert(MethodSet set, Method m) {
+       if (Belong(set, m))
+               return false;
+       else {
+               set->push_back(m);
+               return true;
+       }
+}
+
+inline MethodSet MakeSet(int count, ...) {
+       va_list ap;
+       MethodSet res;
+
+       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);
+       }
+       va_end (ap);
+       return res;
+}
+
+
+#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
+
+#define Next(method) method->next
+#define NEXT ME->next
+
+#define Concurrent(method) method->concurrent
+#define CONCURRENT  ME->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 {
+       IntList *list;
+} StateStruct;
+
+// These auto-generated struct can have different fields according to the return
+// value and arguments of the corresponding interface. The struct will have the
+// same name as the interface name. Here it's just a test example
+typedef struct Store {
+       int *loc;
+       int val;
+} Store;
+
+typedef struct Load {
+       int RET;
+       int *loc;
+} 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);
        return 0;
 }
index 7eee23d..f86c661 100644 (file)
@@ -241,6 +241,55 @@ inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
        }
        return _subset;
 }
+
+// 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
@@ -264,16 +313,13 @@ inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
 @PreCondition:
        // Auto generated code
        // MethodCall *ME = ((SomeTypeConversion) info)->method;
-       // vector<MethodCall*> PREV = Me->prev;
-       // vector<MethodCall*> NEXT = Me->next;
-       // vector<MethodCall*> CONCURRENT = Me->concurrent;
 
        IntegerSet prevSet, concurSet;
        ForEach(m, PREV) {
-               prevSet.add(LOCAL(m, x));
+               prevSet->insert(LOCAL(m, x));
        }
-       ForEach (m, CONCURRENT("STORE")) {
-               concurSet->add(m.val);
+       ForEach (m, Subset(CONCURRENT, "STORE")) {
+               concurSet->insert(Value(m, STORE, val));
        }
        return prevSet->contains(RET) || concurSet->contains(RET);
 @SideEffect:
@@ -317,17 +363,15 @@ 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];
                        // Check there's some concurrent dequeuer for this item
                        bool flag = false;
-                       for (m in CONCURRENT("Deq")) {
-                               if (m.RET) {
-                                       if (*m.res == item) flag = true;
-                               }
+                       ForEach (m, Subset(CONCURRENT, "Deq")) {
+                               if (Value(m, Deq, RET) && *Value(m, Deq, res) == item)
+                                       flag = true;
                        }
                        if (!flag) return false;
                }