From: Peizhao Ou <peizhaoo@uci.edu>
Date: Sat, 30 Jan 2016 07:28:34 +0000 (-0800)
Subject: edits
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=007d42509b6f84500bd65ffe710773117cb3d77f;p=cdsspec-compiler.git

edits
---

diff --git a/notes/definition.cc b/notes/definition.cc
index 0c5b796..fda4eba 100644
--- a/notes/definition.cc
+++ b/notes/definition.cc
@@ -127,6 +127,21 @@ inline set<T>* Subset(set<T> *original, std::function<bool(T)> condition) {
 	return res;
 }
 
+/**
+	A general set operation that takes a condition and returns if there exists
+	any item for which the boolean guard holds.
+*/
+template <class T>
+inline bool HasItem(set<T> *original, std::function<bool(T)> condition) {
+	ForEach (_M, original) {
+		if (condition(_M))
+			return true;
+	}
+	return false;
+}
+
+
+
 /**
 	A general sublist operation that takes a condition and returns all the item
 	for which the boolean guard holds in the same order as in the old list.
@@ -313,9 +328,10 @@ int main() {
 	ms->insert(m);
 
 	MakeSet(int, ms, newis, STATE(x));
-	cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+	//cout << "Size=" << Size(newis) << " | val= " << Belong(newis, 2) << endl;
+	cout << "HasItem=" << HasItem(ms, Guard(STATE(x) == 2)) << endl;
 	ForEach (i, newis) {
-		cout << "elem: " << i << endl;
+		//cout << "elem: " << i << endl;
 	}
 
 
diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index d1011dc..70383b3 100644
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -64,7 +64,7 @@ the initial state. The other way is to define "@EvaluateState" after
 before it.  Usually users calculate the state by using the PREV primitive to
 access the state of previous method calls.
 
-IV. Examples
+IV. Specification Details
 
 /// Global specification
 @State: // Declare the state structure
@@ -144,13 +144,39 @@ ForEach(item, container) { ... }	// Useful iteration primitive
 
 NewMethodSet		// Create a new method set (set<MethodCall*>*)
 
-MakeSet(NewSetType, oldset, newset, field);		// 
+MakeSet(type, oldset, newset, field);		// Construct a new set from an
+						// old set. We extract a specific field of that set item
+						// and form a new set. Specifically we expect users to
+						// use this on MethodSet. For example, if we want to
+						// construct an integer set from the state "x" of
+						// the previous methods, we use "MakeSet(int, PREV,
+						// newset, STATE(x))", and the newset contains the new
+						// set
 
 Subset(set, condition)	// A generic subset operation that takes a condition and
 						// returns all the item for which the boolean guard
 						// holds. The condition can be specified with GUARD or
 						// GeneralGuard shown as follow.
 
+HasItem(set, condition)	// A generic set operation that takes a condition and
+						// returns if there exists any item in "set" for which
+						// the condition holds. Its syntax is similar to that of
+						// Subset() operation
+
+Size(container)		// Return the size of a container type
+
+Belong(container, item)		// Return if item is in the container
+
+Union(set1, set2)	// Union of two sets
+
+Intesection(set1, set2)		// Intersection of two sets
+
+Subtract(set1, set2)	// Returns the new set that represents the result of
+						// set1-set2
+Insert(set, item)	// Insert item to set
+
+Insert(set, others)		// Insert the whole set "others" to "set"
+
 ITEM	// Used to refer to the set item in the GeneralGuard shown below
 
 GeneralGuard(type, expression)	// Used as a condition for any set<T> type. We
@@ -177,11 +203,11 @@ To make things easier, we have the following helper macros.
 	variables. We basically have two usage scenario:
 	1. In Subset operation, we allow users to specify a condition to extract a
 	subset. In that condition expression, we provide NAME, RET(type), ARG(type,
-	field) and LOCAL(field) to access each item's (method call) information.
+	field) and STATE(field) to access each item's (method call) information.
 	2. In general specification (in pre- & post- conditions and side effects),
 	we would automatically generate an assignment that assign the current
 	MethodCall* pointer to a variable namedd _M. With this, when we access the
-	local state of the current method, we use LOCAL(field) (this is a reference
+	state of the current method, we use STATE(field) (this is a reference
 	for read/write).
 */
 #define ITEM _M
@@ -264,121 +290,6 @@ using our specification checker.
 *****************************************************************************
 
 
-// Some nice C/C++ macro definition to make specifications easier to write
-
------------------------------------------------------------------------------
-#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 */
-
-
-
------------------------------------------------------------------------------
-1. ForEach  --> to iterate a set, list or vector (containers that support using
-iterator to iterate)
-
-#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)
-
------------------------------------------------------------------------------
-
-/**
-	This is a common macro that is used as a constant for the name of specific
-	variables. We basically have two usage scenario:
-	1. In Subset operation, we allow users to specify a condition to extract a
-	subset. In that condition expression, we provide NAME, RET(type), ARG(type,
-	field) and LOCAL(field) to access each item's (method call) information.
-	2. In general specification (in pre- & post- conditions and side effects),
-	we would automatically generate an assignment that assign the current
-	MethodCall* pointer to a variable namedd _M. With this, when we access the
-	local state of the current method, we use LOCAL(field) (this is a reference
-	for read/write).
-*/
-#define ITEM _M
-#define _M ME
-
-
------------------------------------------------------------------------------
-
-// 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()
-
-// 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
-
-// 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
-
-// 5. Prev(method)
-#define Prev(method) mehtod->prev
-
-// 6. Next(method)
-#define Next(method) mehtod->next
-
-// 7. Concurrent(method)
-#define Concurrent(method) mehtod->concurrent
-
-
 /// Ordering point specification
 @OPDefine: condition	// If the specified condition satisfied, the atomic
 						// operation right before is an ordering point
@@ -403,11 +314,12 @@ inline MethodSet Subtract(MethodSet set1, MethodSet set2) {
 							// statement
 
 
+V. Examples
 1. The register examples: Basically, we can think of registers as the cache on a
 memory system. The effect of a load or store basically tells us what the current
 value in the cache line is, and a load can read from values that can be
 potentially in the cache --- either one of the concurrent store update the cache
-or it inherites one of the the previous local state in the execution graph.
+or it inherites one of the the previous state in the execution graph.
 
 ----------   Interfae   ----------
 void init(atomic_int &loc, int initial);
@@ -421,17 +333,21 @@ b. The RA (release/acquire) C/C++ atomics
 // For RA atomics, a load must read its value from a store that happens before
 // it.
 ----------   Specification   ----------
-@DeclareVar: int x;
-@InitVar: x = 0;
+@State: int x;
+@Initial: x = 0;
+@Commutativity: Store <-> Store(true)
+@Commutativity: Load <-> Load(true)
+@Commutativity: Store <-> Load(true)
 
+/** No @Transition */
 @Interface: Store
-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;
 void store(int *loc, int val);
 
 @Interface: Load
 @PreCondition:
-	Size(Subset(PREV, LOCAL(x) == RET)) > 0;
-@SideEffect: LOCAL(x) = RET;
+	return HasItem(PREV, STATE(x) == RET);
+@SideEffect: STATE(x) = RET;
 int load(int *loc);
 
 c. The C/C++ atomics (a slightly loose specification)
@@ -454,11 +370,11 @@ any store that either immediately happens before it or concurrently executes.
 
 
 ----------   Specification   ----------
-@DeclareVar: int x;
-@InitVar: x = 0;
+@State: int x;
+@Initial: x = 0;
 
 @Interface: Store
-@SideEffect: LOCAL(x) = val;
+@SideEffect: STATE(x) = val;
 void store(int *loc, int val);
 
 
@@ -466,11 +382,10 @@ void store(int *loc, int val);
 @PreCondition:
 	// Auto generated code
 	// MethodCall *ME = ((SomeTypeConversion) info)->method;
-	
-	int count = Size(Subset(Prev, LOCAL(x) == RET)) 
-		+ Size(Subset(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET))
-	return count > 0;
-@SideEffect: LOCAL(x) = RET;
+
+	return HasItem(Prev, STATE(x) == RET) || 
+		+ HasItem(CONCURRENT, NAME == "Store" && ARG(Store, val) == RET)
+@SideEffect: STATE(x) = RET;
 int load(int *loc);
 
 d. The C/C++ normal memory accesses
@@ -494,38 +409,36 @@ on the admissible executions
 @Copy: New.q = new vector<int>(Old.q);
 // Fails to dequeue
 @Commutativity: Deq <-> Deq (!_M1.RET || !_M2.RET)
-// The dequeuer doesn't dequeue from that enqueuer
-@Commutativity: Enq <-> Deq (!_M2.RET || (_M2.RET && Enq.val != *Deq.res))
+@Commutativity: Enq <-> Deq (true)
 
 @Interface: Enq
-@SideEffect: q->push_back(val);
+@Transition: q->push_back(val);
 void enq(queue_t *q, int val);
 
 @Interface: Deq
+@Transition: if (RET) q->pop_back();
 @PreCondition:
 	// Check whether the queue is really empty
-	// Either the local state is an empty queue, or for all those remaining
-	// elements in the local queue, there should be some concurrent dequeuers to
+	// Either the state is an empty queue, or for all those remaining
+	// elements in the queue, there should be some concurrent dequeuers to
 	// dequeue them
 	if (!RET) {
-		// Local state is empty
-		if (Local(q)->size() == 0) return true;
+		// State is empty
+		if (STATE(q)->size() == 0) return true;
 		// Otherwise check there must be other concurrent dequeuers
-		ForEach (item, Local(q)) {
+		ForEach (item, State(q)) {
 			// Check there's some concurrent dequeuer for this item
-			if (Size(Subset(CONCURRENT, NAME == "Deq" && RET(Deq) &&
-				*ARG(Deq, res) == item)) == 0) return false;
+			if (!HasItem(CONCURRENT, NAME == "Deq" && RET(Deq) &&
+				*ARG(Deq, res) == item)) return false;
 		}
 		return true;
 	} else { // Check the global queue state
 		return q->back() == *res;
 	}
-@SideEffect:
-	if (RET) q->pop_back();
 bool deq(queue_t *q, int *res);
 
 
-
+*******************************************************************************
 A good example to simulate a queue data structure is as follows.
 Suppose we have a special structure
 typedef struct Q {
@@ -536,45 +449,3 @@ typedef struct Q {
 , and we have two interface on Q, read() and write(), where the write and read
 method calls are synchronized by themselves, and they have to read and write the
 x and y fields in turn.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-----------------------------------------------------------------------------------------
-We also need to think about the non-ordered queue.
-
-####
-Combiming Data Structures --- 
-For example, a queue, a -hb->c, b -hb-> e.
-
-// T1
-enq(1) -> {1} - {$}    // a
-enq(2) -> {1, 2} - {$}   // b
-
-// T2
-deq(1) -> {$} - {1}   // c
-deq($) -> {$} - {1}   // d
-
-// State before this method  
-JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
-deq(2) -> {$} - {1, 2}
-
-
-
-
-