notes/nondeterm-spec.txt

   1 Modification to the current specifications.
   2 1. Local State --- Beside of having one global sequential state (the one that we
   3 had in the old approach), we also allow each method call to have a local state.
   4 This local state is the accumulative side effects of the subset of method calls
   5 that happen before the current method call.
   6
   7 To evaluate the local state of each method call, an obvious approach is
   8 calculate from the initial state for each. An optimization we can make here is
   9 that we can start to evaluate the state from the most recent common parent. And
  10 such a state is only evaluated when needed.
  11
  12 2. CONCURRENT --- an operation that extracts all the methods that are executing
  13 "concurrently" with the current method.
  14 "before" the current method.
  15
  16 3. PREV --- an operation that extracts all the methods that execute right
  17
  18 1. The register file examples.
  19 ----------   Interfae   ----------
  20 void init(atomic_int &loc, int initial);
  21 int load(atomic_int &loc);
  22 void store(atomic_int &loc, int val);
  23 ----------   Interfae   ----------
  24
  25 a. The SC atomics --- the classic linearizability approach
  26 b. The ordered-store acq/rel atomics
  27 We basically allow a load operation to read form any store that this does not happen
  28 before
  29
  30 ----------   Specification   ----------
  31 // Store to the same location should conflict
  32 @Commutativity: Store <-> Store(Store.loc != Store.loc)
  33 @Commutativity: Store <-> Load
  34 @Commutativity: Load <-> Load
  35
  36 @DeclareVar: int x;
  37 @InitVar: x = 0;
  38
  39 @Interface: Store
  40 @SideEffect:
  41         x = val;
  42
  43 @Interface: Load
  44 @SideEffect:
  45 @PostCondition:
  46         __RET__ == x ||
  47         {Last.Store(_M.loc == loc)}
  48
  49
  50
  51 c. The C/C++ atomics
  52
  53
  54 d. The C/C++ normal memory accesses
  55 - Use the admissibility requirement, then the classic linearizability approach
  56 on the admissible executions
  57
  58
  59 A good example to simulate a queue data structure is as follows.
  60 Suppose we have a special structure
  61 typedef struct Q {
  62         atomic_int x;
  63         atomic_int y;
  64 } Q;
  65
  66 , and we have two interface on Q, read() and write(), where the write and read
  67 method calls are synchronized by themselves, and they have to read and write the
  68 x and y fields in turn.
  69
  70
  71 ----------------------------------------------------------------------------------------
  72 We also need to think about the non-ordered queue.
  73
  74 ####
  75 Combiming Data Structures ---
  76 For example, a queue, a -hb->c, b -hb-> e.
  77
  78 // T1
  79 enq(1) -> {1} - {$}    // a
  80 enq(2) -> {1, 2} - {$}   // b
  81
  82 // T2
  83 deq(1) -> {$} - {1}   // c
  84 deq($) -> {$} - {1}   // d
  85
  86 // State before this method
  87 JOIN ({1, 2} - {$}, {$} - {1}) = {2} - {1}
  88 deq(2) -> {$} - {1, 2}
  89
  90
  91
  92
  93