X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=blobdiff_plain;f=notes%2Fnondeterm-spec.txt;h=e6dfb057017406083b79491b2aa0fff21693f634;hp=f86c661393a7b19a1b6df06c6cfb2afc204f4e6d;hb=911fd6cd65c43d3338eb6a6b3928423d69b874ed;hpb=bf88290ca3ad6dc68caefb4ebe4a67d42baeeeef

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index f86c661..e6dfb05 100644
--- 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);