doc/notes/release-sequence.txt

   1 -------------------------------------------------------------------------------
   2  Release sequence support:
   3 -------------------------------------------------------------------------------
   4
   5 *******************************
   6  From the C++11 specification
   7 *******************************
   8
   9 1.10.7
  10
  11 A release sequence from a release operation A on an atomic object M is a
  12 maximal contiguous sub-sequence of side effects in the modification order of
  13 M, where the first operation is A, and every subsequent operation
  14
  15 - is performed by the same thread that performed A, or
  16 - is an atomic read-modify-write operation.
  17
  18 29.3.2
  19
  20 An atomic operation A that performs a release operation on an atomic object M
  21 synchronizes with an atomic operation B that performs an acquire operation on
  22 M and takes its value from any side effect in the release sequence headed by
  23 A.
  24
  25 *******************************
  26  My Notes
  27 *******************************
  28
  29 The specification allows for a single acquire to synchronize with more than
  30 one release operation, as its "reads from" value might be part of more than
  31 one release sequence.
  32
  33 *******************************
  34  Approximate Algorithm
  35 *******************************
  36
  37 Check read-write chain...
  38
  39 Given:
  40 current action = curr
  41 read from = rf
  42 Cases:
  43 * rf is NULL: return uncertain
  44 * rf is RMW:
  45         - if rf is release:
  46                 add rf to release heads
  47         - if rf is rel_acq:
  48                 return certain [note: we don't need to extend release sequence
  49                 further because this acquire will have synchronized already]
  50           else
  51                 return (recursively) "get release sequence head of rf"
  52 * if rf is release:
  53         add rf to release heads
  54         return certain
  55 * else, rf is relaxed write (NOT RMW)
  56   - check same thread
  57
  58 *******************************
  59 "check same thread"
  60 *******************************
  61
  62 let release = max{act in S | samethread(act, rf) && isrelease(act) && act <= rf}
  63 let t = thread(rf) // == thread(release)
  64 for all threads t_j != t
  65         if exists c in S | c !--mo--> release, rf !--mo--> c, c is write, thread(c) == t_j then
  66                 return certain;
  67 [ note: need to check "future ordered" condition ]
  68 add release to release heads
  69 return certain;
  70
  71 *******************************
  72 General fixup steps:
  73 *******************************
  74
  75 1. process action, find read_from
  76 2. add initial mo_graph edges
  77 3. assign read_from, calc initial "get_release_seq_heads()"
  78 4. perform synchronization with all release heads
  79
  80 synchronization => check for new mo_graph edges
  81                 => check for resolved release sequences
  82                 => check for failed promises
  83 mo_graph edges  => check for resolved release sequences
  84
  85 *******************************
  86 Other notes
  87 *******************************
  88
  89 "cannot determine" means we need to lazily check conditions in the future
  90    - check when future writes satisfy "promises"
  91
  92 Read from future? We require that all release heads are "in the past", so that
  93 we don't form synchronization against the ordering of the program trace. We
  94 ensure that some execution is explored in which they are ordered the other way,
  95 so we declare this execution "infeasible."
  96
  97 => If we *do* establish a synchronization after the fact:
  98    - need to recurse through the execution trace and update clock vectors
  99    - more