edits

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

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index f86c661393a7b19a1b6df06c6cfb2afc204f4e6d..e6dfb057017406083b79491b2aa0fff21693f634 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -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);