From e33bfe873fdf0b6b407c1a9b233b0498ca08d7c6 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Tue, 26 Jan 2016 18:17:11 -0800 Subject: [PATCH] edits --- notes/nondeterm-spec.txt | 174 ++++++++++++++++++++++++++++++++------- 1 file changed, 144 insertions(+), 30 deletions(-) diff --git a/notes/nondeterm-spec.txt b/notes/nondeterm-spec.txt index f76c46c..3608274 100644 --- a/notes/nondeterm-spec.txt +++ b/notes/nondeterm-spec.txt @@ -1,21 +1,81 @@ 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); @@ -23,39 +83,76 @@ void store(atomic_int &loc, int val); ---------- 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 ---------- -// 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: - x = val; + 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: -@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 - 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. + + + + + + + + + + + + + + + + + ---------------------------------------------------------------------------------------- We also need to think about the non-ordered queue. -- 2.34.1