edits

[cdsspec-compiler.git] / notes / nondeterm-spec.txt

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index e6dfb057017406083b79491b2aa0fff21693f634..8dca63c150e5efe831f2b5b35d5e175a32aac9f9 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -161,8 +161,7 @@ void store(int *loc, int val);
 
 @Interface: Load
 @PreCondition:
-       Subset(PREV, subset, LOCAL(x) == RET);
-       return Size(subset) > 0;
+       Size(Subset(PREV, LOCAL(x) == RET)) > 0;
 @SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 
@@ -214,21 +213,8 @@ interface label name.
 
 
 *********************************************
-
-TODO:We want subset operation by the equality and inequality of the interface
-name, a specific (or combined) state and a specific (or combined) of the value
-(RET & arguments)
-
-// 1.1 Subset(set, name)  --> to get a subset of method calls by name
-inline vector<MethodCall*>* Subset(vector<MethodCall*> *set, string name) {
-       vector<MethodCall*> _subset = new vector<MethodCall*>;
-       for (int i = 0; i < set->size(); i++) {
-               MethodCall *_m = (*set)[i];
-               if (_m->interfaceName == name)
-                       _subset->push_back(_m);
-       }
-       return _subset;
-}
+// 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()
@@ -284,6 +270,11 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 
 // 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
@@ -312,10 +303,9 @@ void store(int *loc, int val);
        // Auto generated code
        // MethodCall *ME = ((SomeTypeConversion) info)->method;
        
-       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;
+       int count = Size(Subset(Prev, LOCAL(x) == RET)) 
+               + Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET))
+       return count > 0;
 @SideEffect: LOCAL(x) = RET;
 int load(int *loc);
 
@@ -359,9 +349,8 @@ void enq(queue_t *q, int val);
                // Otherwise check there must be other concurrent dequeuers
                ForEach (item, Local(q)) {
                        // Check there's some concurrent dequeuer for this item
-                       Subset(CONCURRENT, concurSet, NAME == "Deq" && VALUE(Deq, RET) &&
-                               *VALUE(Deq, res) == item);
-                       if (Size(concurSet) == 0) return false;
+                       if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) &&
+                               *ARG(Deq, res) == item)) == 0) return false;
                }
                return true;
        } else { // Check the global queue state