more edits
authorPeizhao Ou <peizhaoo@uci.edu>
Thu, 28 Jan 2016 02:31:07 +0000 (18:31 -0800)
committerPeizhao Ou <peizhaoo@uci.edu>
Thu, 28 Jan 2016 02:31:07 +0000 (18:31 -0800)
notes/nondeterm-spec.txt

index 3608274..7eee23d 100644 (file)
@@ -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.
 
-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.
@@ -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.
 
-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.
 
+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
 
-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);
@@ -134,14 +198,81 @@ any store that either immediately happens before it or concurrently executes.
        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:
-       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);
@@ -153,6 +284,64 @@ d. The C/C++ normal memory accesses
 - 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 {