edits

diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt
index f76c46c5f24297745a14a70998817bf142fde305..3608274547634781574c319f9e02fb2c329711d4 100644 (file)
--- a/notes/nondeterm-spec.txt
+++ b/notes/nondeterm-spec.txt
@@ -1,21 +1,81 @@
 Modification to the current specifications.
 Modification to the current specifications.

-1. Local State --- Beside of having one global sequential state (the one that we
-had in the old approach), we also allow each method call to have a local state.
-This local state is the accumulative side effects of the subset of method calls
-that happen before the current method call. 

 
 

-To evaluate the local state of each method call, an obvious approach is
-calculate from the initial state for each. An optimization we can make here is
-that we can start to evaluate the state from the most recent common parent. And
-such a state is only evaluated when needed.
-
-2. CONCURRENT --- an operation that extracts all the methods that are executing
-"concurrently" with the current method.
-"before" the current method.
-
-3. PREV --- an operation that extracts all the methods that execute right
-
-1. The register file examples.
+I. Order
+-- Sequential order (SO): Some total order that is consistent with the union of
+happens-before and SC relation.
+
+II. State
+1. Global state: We allow users to specify a single global state so that when we
+want to execute the sequential replay (execute the sequential order), the whole
+process is similar to executing an sequential program. Such a global state is
+similiar to the internal state of a sequential data structure. We also have this
+in our old version (the rejection of PLDI'16). As an analogy to the cache-memory
+model, the global state we define here is similar to the main memory in the
+sense that there does not exist a real total order to all memory accesses, but
+to some degree (with the non-deterministic specifications) we can have an
+illution that there is some total order.
+
+2. Local State: Beside of having one global state (the one that we have in the
+old approach), we also allow each method call to have a local state.  This local
+state is the accumulative side effects of the subset of method calls that happen
+before the current method call. As an analogy to the cache-memory model, the
+local state we define here is similar to cache, a local state is local to the
+sense that the current method call must have seen those effects. The main goal
+of having this is to support tighter non-deterministic specifications.
+
+To evaluate the local state of each method call, an obvious approach is to
+execute the subset of methods that happen before the current method in the
+sequential order from the initial state. A optimization we can make is that we
+start to evaluate the state from the most recent deviding node which every other
+node in that subset is either hb before or after. Also, since local states are
+not required in specifications all the time, it is only evaluated when needed.
+
+III. Specifications
+Our specification language supports using the following primitives to access
+both global state and local state so that users can use those to write
+specifications with different level of tightness.
+
+To support tighter specifications, we introduce the concept of concurrent set of
+method calls, meaning that for a specific method call, it can basically see the
+effect of two different categories of method calls --- one that happens before
+it, and one that concurrently execute with it. It is worth noting that when two
+two method calls execute concurrently, in general there can be the following two
+effects: 1) those concurrent methods can happen in either order, and the final
+result remains the same. A concurrent FIFO is an example, in which concurrent
+enqueue and dequeue methods can happen in a random order; and 2) the order of
+those concurrent methods will affect the final result. The C/C++11 atomics is an
+example, in which when concurrent stores to the same location execute in
+different order, a later store will have different result.
+
+1. CONCURRENT: This primitive extracts all the methods that executes
+"concurrently" with the current method --- neither hb/SC before nor after the
+current method --- and returns as a set. It is worth noting that the concurrent
+method calls cannot be accessed for calculating local state but only for
+assertions.
+
+2. PREV: This primitive extracts all the methods that execute right before the
+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
+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.
+
+Our specifications allow two ways of calculating the local states, a default way
+and a user-customized way. The default approach is to execute the set of method
+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
+require users to provide such a primitive function because each local state
+should be have its own copy.
+
+IV. Examples
+
+1. The register examples.

 ----------   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);


@@ -23,39 +83,76 @@ void store(atomic_int &loc, int val);
 ----------   Interfae   ----------
 
 a. The SC atomics --- the classic linearizability approach
 ----------   Interfae   ----------
 
 a. The SC atomics --- the classic linearizability approach

-b. The ordered-store acq/rel atomics
-We basically allow a load operation to read form any store that this does not happen
-before

 
 

+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   ----------
 ----------   Specification   ----------

-// Store to the same location should conflict
-@Commutativity: Store <-> Store(Store.loc != Store.loc)
-@Commutativity: Store <-> Load
-@Commutativity: Load <-> Load
-

 @DeclareVar: int x;
 @InitVar: x = 0;
 
 @Interface: Store
 @SideEffect:
 @DeclareVar: int x;
 @InitVar: x = 0;
 
 @Interface: Store
 @SideEffect:

-       x = val;
+       LOCAL.x = val;
+void store(int *loc, int val);

 
 @Interface: Load
 
 @Interface: Load

+@PreCondition:
+       IntegerSet *prevSet = new IntegerSet;
+       for (m in PREV) {
+               prevSet->add(m.LOCAL.x);
+       }
+       return prevSet->contains(RET);

 @SideEffect:
 @SideEffect:

-@PostCondition:
-       __RET__ == x ||
-       {Last.Store(_M.loc == loc)}
+       LOCAL.x = RET;
+int load(int *loc);

 
 

+c. The C/C++ atomics (a slightly loose specification)
+// Actually, any concurrent data structures that rely modification-order to be
+// correct would not have a precicely tight specification under our model, and
+// C/C++ relaxed atomics is an example. See the following read-read coherence
+// example.

 
 

+// T1                          // T2
+x = 1;                         x = 2;
+
+// T3
+r1 = x; // r1 == 1
+r2 = x; // r2 == 2
+r3 = x; // r3 == 1
+
+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;

 
 

-c. The C/C++ atomics
+@Interface: Store
+@SideEffect:
+       LOCAL.x = val;
+void store(int *loc, int val);

 
 

+@Interface: Load
+@PreCondition:
+       IntegerSet *prevSet = new IntegerSet;
+       IntegerSet *concurSet = new IntegerSet;
+       for (m in PREV) {
+               prevSet->add(m.LOCAL.x);
+       }
+       for (m in CONCURRENT("STORE")) {
+               concurSet->add(m.val);
+       }
+       return prevSet->contains(RET) || concurSet->contains(RET);
+@SideEffect:
+       LOCAL.x = RET;
+int load(int *loc);

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

-

 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 {


@@ -68,6 +165,23 @@ method calls are synchronized by themselves, and they have to read and write the
 x and y fields in turn.
 
 
 x and y fields in turn.
 
 

+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

 ----------------------------------------------------------------------------------------
 We also need to think about the non-ordered queue.
 
 ----------------------------------------------------------------------------------------
 We also need to think about the non-ordered queue.