notes/nondeterm-spec.txt

   1 Modification to the current specifications.
   2
   3 I. Order
   4 -- Sequential order (SO): Some total order that is consistent with the union of
   5 happens-before and SC relation.
   6
   7 II. State
   8 1. Global state: We allow users to specify a single global state so that when we
   9 want to execute the sequential replay (execute the sequential order), the whole
  10 process is similar to executing an sequential program. Such a global state is
  11 similiar to the internal state of a sequential data structure. We also have this
  12 in our old version (the rejection of PLDI'16). As an analogy to the cache-memory
  13 model, the global state we define here is similar to the main memory in the
  14 sense that there does not exist a real total order to all memory accesses, but
  15 to some degree (with the non-deterministic specifications) we can have an
  16 illution that there is some total order.
  17
  18 2. Local State: Beside of having one global state (the one that we have in the
  19 old approach), we also allow each method call to have a local state.  This local
  20 state is the accumulative side effects of the subset of method calls that happen
  21 before the current method call. As an analogy to the cache-memory model, the
  22 local state we define here is similar to cache, a local state is local to the
  23 sense that the current method call must have seen those effects. The main goal
  24 of having this is to support tighter non-deterministic specifications.
  25
  26 To evaluate the local state of each method call, an obvious approach is to
  27 execute the subset of methods that happen before the current method in the
  28 sequential order from the initial state. A optimization we can make is that we
  29 start to evaluate the state from the most recent deviding node which every other
  30 node in that subset is either hb before or after. Also, since local states are
  31 not required in specifications all the time, it is only evaluated when needed.
  32
  33 III. Specifications
  34 Our specification language supports using the following primitives to access
  35 both global state and local state so that users can use those to write
  36 specifications with different level of tightness.
  37
  38 To support tighter specifications, we introduce the concept of concurrent set of
  39 method calls, meaning that for a specific method call, it can basically see the
  40 effect of two different categories of method calls --- one that happens before
  41 it, and one that concurrently execute with it. It is worth noting that when two
  42 two method calls execute concurrently, in general there can be the following two
  43 effects: 1) those concurrent methods can happen in either order, and the final
  44 result remains the same. A concurrent FIFO is an example, in which concurrent
  45 enqueue and dequeue methods can happen in a random order; and 2) the order of
  46 those concurrent methods will affect the final result. The C/C++11 atomics is an
  47 example, in which when concurrent stores to the same location execute in
  48 different order, a later store will have different result.
  49
  50 1. CONCURRENT: This primitive extracts all the methods that executes
  51 "concurrently" with the current method --- neither hb/SC before nor after the
  52 current method --- and returns as a set. It is worth noting that the concurrent
  53 method calls cannot be accessed for calculating local state but only for
  54 assertions.
  55
  56 2. PREV: This primitive extracts all the methods that execute right before the
  57 current method in the execution graph --- most recent method calls that are
  58 hb/SC before the current method call --- and returns as a set. For each method
  59 in this set, the current method's specification can access their local state.
  60
  61 3. LOCAL: This primitive allows users to access the local state of a method
  62 call. It is worth noting that in order to calculate the local state of a method
  63 call, one can only access the set of method calls that happen before the current
  64 method call.
  65
  66 Our specifications allow two ways of calculating the local states, a default way
  67 and a user-customized way. The default approach is to execute the set of method
  68 calls that happen before the current method call in the sequential order, and a
  69 the user-customized approach supports users to calculate the local state by
  70 using the PREV primitive to access the local state of previous method calls.
  71
  72 4. COPY: This is the function that users provide to deep-copy the state. We
  73 require users to provide such a primitive function because each local state
  74 should be have its own copy.
  75
  76 IV. Examples
  77
  78 1. The register examples.
  79 ----------   Interfae   ----------
  80 void init(atomic_int &loc, int initial);
  81 int load(atomic_int &loc);
  82 void store(atomic_int &loc, int val);
  83 ----------   Interfae   ----------
  84
  85 a. The SC atomics --- the classic linearizability approach
  86
  87 b. The RA (release/acquire) C/C++ atomics
  88 // For RA atomics, a load must read its value from a store that happens before
  89 // it.
  90 ----------   Specification   ----------
  91 @DeclareVar: int x;
  92 @InitVar: x = 0;
  93
  94 @Interface: Store
  95 @SideEffect:
  96         LOCAL.x = val;
  97 void store(int *loc, int val);
  98
  99 @Interface: Load
 100 @PreCondition:
 101         IntegerSet *prevSet = new IntegerSet;
 102         for (m in PREV) {
 103                 prevSet->add(m.LOCAL.x);
 104         }
 105         return prevSet->contains(RET);
 106 @SideEffect:
 107         LOCAL.x = RET;
 108 int load(int *loc);
 109
 110 c. The C/C++ atomics (a slightly loose specification)
 111 // Actually, any concurrent data structures that rely modification-order to be
 112 // correct would not have a precicely tight specification under our model, and
 113 // C/C++ relaxed atomics is an example. See the following read-read coherence
 114 // example.
 115
 116 // T1                           // T2
 117 x = 1;                          x = 2;
 118
 119 // T3
 120 r1 = x; // r1 == 1
 121 r2 = x; // r2 == 2
 122 r3 = x; // r3 == 1
 123
 124 Our model cannot prevent such a case from happening. However, we can still have
 125 a slightly loose specification which basically states that a load can read from
 126 any store that either immediately happens before it or concurrently executes.
 127
 128 ----------   Specification   ----------
 129 @DeclareVar: int x;
 130 @InitVar: x = 0;
 131
 132 @Interface: Store
 133 @SideEffect:
 134         LOCAL.x = val;
 135 void store(int *loc, int val);
 136
 137 @Interface: Load
 138 @PreCondition:
 139         IntegerSet *prevSet = new IntegerSet;
 140         IntegerSet *concurSet = new IntegerSet;
 141         for (m in PREV) {
 142                 prevSet->add(m.LOCAL.x);
 143         }
 144         for (m in CONCURRENT("STORE")) {
 145                 concurSet->add(m.val);
 146         }
 147         return prevSet->contains(RET) || concurSet->contains(RET);
 148 @SideEffect:
 149         LOCAL.x = RET;
 150 int load(int *loc);
 151
 152 d. The C/C++ normal memory accesses
 153 - Use the admissibility requirement, then the classic linearizability approach
 154 on the admissible executions
 155
 156 A good example to simulate a queue data structure is as follows.
 157 Suppose we have a special structure
 158 typedef struct Q {
 159         atomic_int x;
 160         atomic_int y;
 161 } Q;
 162
 163 , and we have two interface on Q, read() and write(), where the write and read
 164 method calls are synchronized by themselves, and they have to read and write the
 165 x and y fields in turn.
 166
 167
 168
 169
 170
 171
 172
 173
 174
 175
 176
 177
 178
 179
 180
 181
 182
 183
 184
 185 ----------------------------------------------------------------------------------------
 186 We also need to think about the non-ordered queue.
 187
 188 ####
 189 Combiming Data Structures ---
 190 For example, a queue, a -hb->c, b -hb-> e.
 191
 192 // T1
 193 enq(1) -> {1} - {$}    // a
 194 enq(2) -> {1, 2} - {$}   // b
 195
 196 // T2
 197 deq(1) -> {$} - {1}   // c
 198 deq($) -> {$} - {1}   // d
 199
 200 // State before this method
 201 JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
 202 deq(2) -> {$} - {1, 2}
 203
 204
 205
 206
 207