more edits

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index 3608274547634781574c319f9e02fb2c329711d4..7eee23d17497ee52919ecd8703f837f7da910778 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -58,7 +58,11 @@ current method in the execution graph --- most recent method calls that are
 hb/SC before the current method call --- and returns as a set. For each method
 in this set, the current method's specification can access their local state.
 
 hb/SC before the current method call --- and returns as a set. For each method
 in this set, the current method's specification can access their local state.
 

-3. LOCAL: This primitive allows users to access the local state of a method
+3. NEXT: This primitive extracts all the methods that execute right after the
+current method in the execution graph, and returns as a set. For each method in
+this set, the current method's specification cannot access their local state.
+
+4. LOCAL: This primitive allows users to access the local state of a method

 call. It is worth noting that in order to calculate the local state of a method
 call, one can only access the set of method calls that happen before the current
 method call.
 call. It is worth noting that in order to calculate the local state of a method
 call, one can only access the set of method calls that happen before the current
 method call.


@@ -69,13 +73,73 @@ calls that happen before the current method call in the sequential order, and a
 the user-customized approach supports users to calculate the local state by
 using the PREV primitive to access the local state of previous method calls.
 
 the user-customized approach supports users to calculate the local state by
 using the PREV primitive to access the local state of previous method calls.
 

-4. COPY: This is the function that users provide to deep-copy the state. We
+5. COPY: This is the function that users provide to deep-copy the state. We

 require users to provide such a primitive function because each local state
 should be have its own copy.
 
 require users to provide such a primitive function because each local state
 should be have its own copy.
 

+6. FINALLY: This is the function that allows users to specify some final check
+on the state. Initially, this check will only access the global state. However,
+for the concern of expressiveness, we allow users to access the initial state,
+meaning that users can basically access the whole graph and the local state of
+each method call. This will enable to users to use the graph model (the relaxed
+atomics can be specified) although the complxity of using that can get quite
+complex.
+

 IV. Examples
 
 IV. Examples
 

-1. The register examples.
+// Global specification
+@DeclareState: // Declare the state structure
+@InitState: // How do we initialize the state
+@CopyState: // A function on how to copy an existing state
+@Commutativity: Method1 <-> Method2 (Guard) // Guard can only access the return
+               // value and the arguments of the two method calls
+
+// Interface specification
+@Interface: InterfaceName // Required; a label to represent the interface
+@LocalState: // Optional; to calculate the accumulative local state before this
+                        // method call in a customized fashion. If not specified here, the
+                        // local state would be default, which is the result of the
+                        // execution on the subset of method calls in the sequential order
+@PreCondition: // Optional; checking code
+@LocalSideEffect: // Optional; to calculate the side effect this method call
+                                 // have on the local state in a customized fashion. If this
+                                 // field is not stated, it means we don't care about it.
+@SideEffect: // Optional; to calculate the side effect on the global state. When
+               // the "@LocalSideEffect" specification is ommitted, we also impose the
+               // same side effect on the set of method calls that happen before this
+               // method call in the sequential order.
+@PostCondition: // Optional; checking code
+
+// Ordering point specification
+@OPDefine: condition   // If the specified condition satisfied, the atomic
+                                               // operation right before is an ordering point
+
+@PotentialOP(Label): condition // If the specified condition satisfied, the
+                                                               // atomic operation right before is a potential
+                                                               // ordering point, and we label it with a tag
+
+@OPCheck(Label): condition     // If the specified condition satisfied, the
+                                                       // potential ordering point defined earlier with the
+                                                       // same tag becomes an ordering point
+
+@OPClear: condition            // If the specified condition satisfied, all the
+                                               // ordering points and potential ordering points will be
+                                               // cleared
+
+@OPClearDefine: condition      // If the specified condition satisfied, all the
+                                                       // ordering points and potential ordering points will
+                                                       // be cleared, and the atomic operation right before
+                                                       // becomes an ordering point. This is a syntax sugar
+                                                       // as the combination of an "OPClear" and "OPDefine"
+                                                       // statement
+
+
+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.
+

 ----------   Interfae   ----------
 void init(atomic_int &loc, int initial);
 int load(atomic_int &loc);
 ----------   Interfae   ----------
 void init(atomic_int &loc, int initial);
 int load(atomic_int &loc);


@@ -134,14 +198,81 @@ any store that either immediately happens before it or concurrently executes.
        LOCAL.x = val;
 void store(int *loc, int val);
 
        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
+typedef struct MethodCall {
+       string interfaceName; // The interface label name
+       void *value; // The pointer that points to the struct that have the return
+                                // value and the arguments
+       void *localState; // The pointer that points to the struct that represents
+                                         // the (local) state
+       vector<MethodCall*> *prev; // Method calls that are hb right before me
+       vector<MethodCall*> *next; // Method calls that are hb right after me
+       vector<MethodCall*> *concurrent; // Method calls that are concurrent with me
+} MethodCall;
+
+We will automatically generate two types of struct. One is the state struct, and
+we will call it StateStruct. This state is shared by all the global and local
+state. The other one is a per interface struct, and it wraps the return value
+(RET) and the arguments as its field. We will name those struct with the
+interface label name.
+
+// Some very nice C/C++ macro definition to make specifications a lot easier
+// 1. ForEach  --> to iterate all 
+#define ForEach(item, list) \
+       for (iterator<MethodCall*> _mIter = list->begin(), \
+               MethodCall *item = *_mIter; _mIter != list->end(); item = (++iter != \
+               list->end()) ? *_mIter : NULL)
+
+
+*********************************************
+
+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;
+}
+       
+// 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
+
+// 4. Lable(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
+

 @Interface: Load
 @PreCondition:
 @Interface: Load
 @PreCondition:

-       IntegerSet *prevSet = new IntegerSet;
-       IntegerSet *concurSet = new IntegerSet;
-       for (m in PREV) {
-               prevSet->add(m.LOCAL.x);
+       // 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));

        }
        }

-       for (m in CONCURRENT("STORE")) {
+       ForEach (m, CONCURRENT("STORE")) {

                concurSet->add(m.val);
        }
        return prevSet->contains(RET) || concurSet->contains(RET);
                concurSet->add(m.val);
        }
        return prevSet->contains(RET) || concurSet->contains(RET);


@@ -153,6 +284,64 @@ d. The C/C++ normal memory accesses
 - Use the admissibility requirement, then the classic linearizability approach
 on the admissible executions
 
 - Use the admissibility requirement, then the classic linearizability approach
 on the admissible executions
 

+2. The FIFO queue example.
+----------   Specification   ----------
+// A FIFO queue should have the following properties held:
+// 1. The enq() methods should conflict
+// 2. The deq() methods that succeed should conflict
+// 3. Corresponding enq() and deq() methods should conflict
+// 4. An enqueued item can be dequeued by at most once
+// 5. A dequeued item must have a corresponding enqueued item
+// 6. When a queue is NOT "empty" (users can tightly or loosely define
+// emptiness), and there comes a deq() method, the deq() method should succeed
+
+
+@DeclareVar: vector<int> *q;
+@InitVar: q = new voctor<int>;
+@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))
+
+@Interface: Enq 
+@SideEffect:
+       LOCAL.x = val;
+void enq(queue_t *q, int val);
+
+@Interface: Deq
+@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
+       // dequeue them
+       if (!RET) {
+               // Local state is empty
+               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;
+                               }
+                       }
+                       if (!flag) return false;
+               }
+               return true;
+       } else { // Check the global queue state
+               return q->back() == *res;
+       }
+@SideEffect:
+       if (RET)
+               Global.q->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 {
 A good example to simulate a queue data structure is as follows.
 Suppose we have a special structure
 typedef struct Q {