From: Brian Norris <banorris@uci.edu>
Date: Thu, 27 Sep 2012 17:15:28 +0000 (-0700)
Subject: doc: add release sequence notes
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d16112e0af1dbc6c74347d6979c4003f55e955e5;p=cdsspec-compiler.git

doc: add release sequence notes
---

diff --git a/doc/notes/release-sequence.txt b/doc/notes/release-sequence.txt
new file mode 100644
index 0000000..85e8c0c
--- /dev/null
+++ b/doc/notes/release-sequence.txt
@@ -0,0 +1,99 @@
+-------------------------------------------------------------------------------
+ Release sequence support:
+-------------------------------------------------------------------------------
+
+*******************************
+ From the C++11 specification
+*******************************
+
+1.10.7
+
+A release sequence from a release operation A on an atomic object M is a
+maximal contiguous sub-sequence of side effects in the modification order of
+M, where the first operation is A, and every subsequent operation
+
+- is performed by the same thread that performed A, or
+- is an atomic read-modify-write operation.
+
+29.3.2
+
+An atomic operation A that performs a release operation on an atomic object M
+synchronizes with an atomic operation B that performs an acquire operation on
+M and takes its value from any side effect in the release sequence headed by
+A.
+
+*******************************
+ My Notes
+*******************************
+
+The specification allows for a single acquire to synchronize with more than
+one release operation, as its "reads from" value might be part of more than
+one release sequence.
+
+*******************************
+ Approximate Algorithm
+*******************************
+
+Check read-write chain...
+
+Given:
+current action = curr
+read from = rf
+Cases:
+* rf is NULL: return uncertain
+* rf is RMW:
+	- if rf is release:
+		add rf to release heads
+	- if rf is rel_acq:
+		return certain [note: we don't need to extend release sequence
+		further because this acquire will have synchronized already]
+	  else
+		return (recursively) "get release sequence head of rf"
+* if rf is release:
+	add rf to release heads
+	return certain
+* else, rf is relaxed write (NOT RMW)
+  - check same thread
+
+*******************************
+"check same thread"
+*******************************
+
+let release = max{act in S | samethread(act, rf) && isrelease(act) && act <= rf}
+let t = thread(rf) // == thread(release)
+for all threads t_j != t
+	if exists c in S | c !--mo--> release, rf !--mo--> c, c is write, thread(c) == t_j then
+		return certain;
+[ note: need to check "future ordered" condition ]
+add release to release heads
+return certain;
+
+*******************************
+General fixup steps:
+*******************************
+
+1. process action, find read_from
+2. add initial mo_graph edges
+3. assign read_from, calc initial "get_release_seq_heads()"
+4. perform synchronization with all release heads
+
+synchronization => check for new mo_graph edges
+                => check for resolved release sequences
+		=> check for failed promises
+mo_graph edges  => check for resolved release sequences
+
+*******************************
+Other notes
+*******************************
+
+"cannot determine" means we need to lazily check conditions in the future
+   - check when future writes satisfy "promises"
+
+Read from future? We require that all release heads are "in the past", so that
+we don't form synchronization against the ordering of the program trace. We
+ensure that some execution is explored in which they are ordered the other way,
+so we declare this execution "infeasible."
+
+=> If we *do* establish a synchronization after the fact:
+   - need to recurse through the execution trace and update clock vectors
+   - more