------------------------------------------------------------------------------- Fence support: ------------------------------------------------------------------------------- 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 specifications are pasted here in Appendix A and are applied to our model-checker in these notes. Section 29.3 details the modification order constraints established by sequentially-consistent fences. Section 29.8 details 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. ******************************* Backtracking requirements ******************************* Because we maintain the seq-cst order as consistent with the execution order, seq-cst fences cannot commute with each other, with seq-cst loads, nor with seq-cst stores; we backtrack at all such pairs. Fences extend release/acquire synchronization beyond just store-release/load-acquire. We must backtrack with potentially-synchronizing fences: that is, with any pair of store- or fence-release and load- or fence-acquire, where the release comes after the acquire in the execution order (the other ordering is OK, as we will explore both behaviors; where the pair synchronize and where they don't). Note that, for instance, a fence-release may synchronize with a fence-acquire only in the presence of a appropriate load/store pair (29.8p2); but the synchronization still occurs between the fences, so the backtracking requirements are only placed on the release/acquire fences themselves. ******************************* Seq-cst MO constraints (29.3 p4-p7) ******************************* 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_loc(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 location as A and B prior to Y (note that all prior writes will be ordered prior to X in both SC and MO) * 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_loc(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" seq-cst fence Y from each thread * We only need to examine the "most recent" qualifying store X that precedes Y; all other X will provide a weaker MO constraint * This search can be combined with the r_modification_order search, since we already iterate through the necessary stores X 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_loc(X, A, B) && A != X && A --rf-> B && X --sb-> Y --sc-> Z --sb-> B then X --mo-> A Intuition/Implementation: * We should consider only the "most recent" fence Z in the same thread as B (prior fences may only yield the same or weaker constraints) * We may then consider the "most recent" seq-cst fence Y prior to Z (in SC order) from each thread (prior fences may only yield the same or weaker constraints) * We should consider only the "most recent" store X (to the same location as A, B) in the same thread as Y (prior stores may only yield the same or weaker constraints) * This search can be combined with the r_modification_order search, since we already iterate through the necessary stores X 29.3p7 If is_write(A) && is_write(B) && is_fence(X) && is_fence(Y) && is_seqcst(X) && is_seqcst(Y) && same_loc(A, B) && A --sb-> X --sc-> Y --sb-> B then A --mo-> B Intuition/Implementation: * (Similar to 29.3p6 rules, except using A/B write/write) only search for the most recent fence Y in the same thread; search for the most recent (prior to Y) fence X from each thread; search for the most recent store A prior to X * This search can be combined with the w_modification_order search, since we already iterate through the necessary stores A ********************************************************************** Release/acquire synchronization: extended to fences (29.3 p4-p7) ********************************************************************** [INCOMPLETE] ******************************* 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 ************************************************** Appendix A: 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.