From: Brian Norris
Date: Wed, 5 Dec 2012 02:23:52 +0000 (-0800)
Subject: doc: notes: add fences note
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=68e1d8d46e038e70ad838aae104f84da29981b31
doc: notes: add fences note
This note is incomplete.
---
diff --git a/doc/notes/fence.txt b/doc/notes/fence.txt
new file mode 100644
index 00000000..b42ad94f
--- /dev/null
+++ b/doc/notes/fence.txt
@@ -0,0 +1,196 @@
+-------------------------------------------------------------------------------
+ Fence support:
+-------------------------------------------------------------------------------
+
+[refer to release sequence notes for some definitions and similar (but simpler)
+algorithm]
+
+Fences provide a few new modification order constraints as well as an
+interesting extension to release sequences, detailed in 29.3 (p4-p7) and 29.8
+(p2-p4).
+
+The Section 29.3 references detail the modification order constraints
+established by sequentially-consistent fences.
+
+The Section 29.8 references detail the behavior of release and acquire fences
+(note that memory_order_seq_cst is both release and acquire).
+
+The text of these rules are provided at the end of this document for reference.
+
+*******************************
+Seq-cst MO constraints (29.3 p4-p7)
+*******************************
+
+[INCOMPLETE]
+
+The statements given in the specification regarding sequentially consistent
+fences can be transformed into the following 4 modification order constraints.
+
+29.3p4
+
+If
+ is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
+ is_seqcst(X) && is_seqcst(Y) && A != X &&
+ same_var(X, A, B) &&
+ A --rf-> B &&
+ X --sc-> Y --sb-> B
+then
+ X --mo-> A
+
+Intuition/Implementation:
+ * We may (but don't currently) limit our considertion of X to only the most
+ recent (in the SC order) store to the same variable as A and B
+ * We should consider the "most recent" seq-cst fence Y that precedes B
+ * This search can be combined with the r_modification_order search, since we
+ already iterate through the necessary stores X
+
+29.3p5
+
+If
+ is_write(A) && is_read(B) && is_write(X) && is_fence(Y) &&
+ is_seqcst(B) && is_seqcst(Y) &&
+ same_var(X, A, B) &&
+ A != X &&
+ A --rf-> B &&
+ X --sb-> Y --sc-> B
+then
+ X --mo-> A
+
+Intuition/Implementation:
+ * We only need to examine the "most recent" qualifying store X that precedes Y;
+ all other X will provide a weaker MO constraint
+ * Search for the most recent fence Y in the same thread as A
+ * We should consider the "most recent" write
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there is a memory_order_seq_cst fence X such that A is
+sequenced before X and B follows X in S, then B observes either the effects of
+A or a later modification of M in its modification order.
+
+29.3p6
+
+If
+ is_write(A) && is_read(B) && is_write(X) && is_fence(Y) is_fence(Z) &&
+ is_seqcst(Y) && is_seqcst(Z) &&
+ same_var(X, A, B) &&
+ A != X &&
+ A --rf-> B &&
+ X --sb-> Y --sc-> Z --sb-> B
+then
+ X --mo-> A
+
+Intuition/Implementation:
+ * We should consider the "most recent" write
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there are memory_order_seq_cst fences X and Y such that A
+is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
+observes either the effects of A or a later modification of M in its
+modification order.
+
+29.3p7
+
+For atomic operations A and B on an atomic object M, if there are
+memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
+sequenced before B, and X precedes Y in S, then B occurs later than A in the
+modification order of M.
+
+
+*******************************
+Miscellaneous Notes
+*******************************
+
+fence(memory_order_consume) acts like memory_order_release, so if we ever
+support consume, we must alias consume -> release
+
+fence(memory_order_relaxed) is a no-op
+
+*******************************
+ Approximate Algorithm [incomplete; just copied from the (out-of-date) release
+ sequence notes
+*******************************
+
+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
+
+**************************************
+ From the C++11 specification (N3337)
+**************************************
+
+-------------
+Section 29.3
+-------------
+
+29.3p4
+
+For an atomic operation B that reads the value of an atomic object M, if there
+is a memory_order_seq_cst fence X sequenced before B, then B observes either
+the last memory_order_seq_cst modification of M preceding X in the total order
+S or a later modification of M in its modification order.
+
+29.3p5
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there is a memory_order_seq_cst fence X such that A is
+sequenced before X and B follows X in S, then B observes either the effects of
+A or a later modification of M in its modification order.
+
+29.3p6
+
+For atomic operations A and B on an atomic object M, where A modifies M and B
+takes its value, if there are memory_order_seq_cst fences X and Y such that A
+is sequenced before X, Y is sequenced before B, and X precedes Y in S, then B
+observes either the effects of A or a later modification of M in its
+modification order.
+
+29.3p7
+
+For atomic operations A and B on an atomic object M, if there are
+memory_order_seq_cst fences X and Y such that A is sequenced before X, Y is
+sequenced before B, and X precedes Y in S, then B occurs later than A in the
+modification order of M.
+
+-------------
+Section 29.8
+-------------
+
+29.8p2
+
+A release fence A synchronizes with an acquire fence B if there exist atomic
+operations X and Y, both operating on some atomic object M, such that A is
+sequenced before X, X modifies M, Y is sequenced before B, and Y reads the value
+written by X or a value written by any side effect in the hypothetical release
+sequence X would head if it were a release operation.
+
+29.8p3
+
+A release fence A synchronizes with an atomic operation B that performs an
+acquire operation on an atomic object M if there exists an atomic operation X
+such that A is sequenced before X, X modifies M, and B reads the value written
+by X or a value written by any side effect in the hypothetical release sequence
+X would head if it were a release operation.
+
+29.8p4
+
+An atomic operation A that is a release operation on an atomic object M
+synchronizes with an acquire fence B if there exists some atomic operation X on
+M such that X is sequenced before B and reads the value written by A or a value
+written by any side effect in the release sequence headed by A.