open Atomic open MachineDefTypes open Atomic_simple open Intermediate_actions open Statement (* Given the following assumptions: *) (* A Power trace and C++ execution with the same behaviour *) val t : trace val actions : c_action set val c_rf : c_action reln let _ = obs t actions c_rf (* The Power trace comes from a Power program, and might not be complete *) val power_prog : p_program val p_tids : p_thread_id set let _ = t IN machine_execution_prefix power_prog p_tids (* The C++ execution comes from a C++ program, according to the opsem *) val c_prog : c_program val actions' : c_action set val c_tids : c_thread_id set val o' : opinfo let _ = opsem_prefix c_prog actions actions' c_tids o' (* The compiler has preserved all of the necessary single-threaded dependency information *) val o : opinfo let o = restrict_opinfo o' actions let _ = preserved_po t actions o.sb let _ = preserved_dd t actions o.dd let _ = preserved_xsync t Hwsync actions let _ = preserved_xsync t Lwsync actions let _ = preserved_ctrlisync t actions (* We have built good mo and sc orders, and the rf_in_hb_condition holds *) val mo : c_action reln val sc : c_action reln let _ = good_mo t actions o.lk mo let _ = good_sc t actions sc let _ = rf_in_hb_condition actions o c_rf mo (* we prove *) let _ = consistent_ex actions o c_rf mo sc (*-------------------- Preliminaries -------------------- *) (* First we build some relations from the Power trace *) (* [read-from] (w,r) IN rf If and only if [w] is write, [r] is a read and [r] reads from the value of [w]. *) val rf : i_action reln let rf = trace_to_rf t (* [program-order] (a,b) IN po If and only if the POWER instruction corresponding to [a] is program order before the POWER instruction corresponding to [b]. (Hence the two instruction are on the same thread) *) val po : i_action reln let po = trace_to_po t (* [coherence] For each address, relate all the pair of writes at address such that they are coherence related (preserve the order) at some point in the trace (by looking at the storage subsystem state). The [co] relation is the union over all addresses of linearization of the previously described relations. *) val co : i_action reln let co = trace_to_co t (* [separated by a sync or lwsync] (a,b) IN xsync If and only if the POWER instruction corresponding to [a] and [b] are on the same thread, and the commit transitions of [a] (which is trace-order before the one from [b]) is trace-order separated from the commit transition of [b] by the commit transition of a sync or lwsync, from the same thread as [a] and [b]. *) val xsync : i_action reln let xsync = trace_to_xsync t Sync union trace_to_xsync t LwSync (* [separated by a ctrlisync dependency] The definition of the following relation is the analogue for the ctrlisync dependency of the [xsync] relation. *) val ctrlisync : i_action reln let ctrlisync = trace_to_ctrlisync t (* [address and data dependency] 1) (r, e) IN addr If and only if [r] is a read, [e] is some program-order later read or write such that there is a data flow path from [r], through registers and arithmetic/logical operations (but not through memory accesses), to the address of [e]. 2) (r,w) IN data If and only if [r] is a read and [w] is a write such that there is an analogous path to the value written. *) val addr_data : i_action reln let addr_data = tc (trace_to_rfi t union trace_to_dd t) (* And some restrictions or reflective closures of the previous relations *) (* Restriction of [rf] to pair of corresponding to instructions from two different threads *) val rfe : i_action reln let rfe = trace_to_rfe t val rfi : i_action reln let rfi = trace_to_rfi t (* Restriction of [co] to pair of corresponding to instructions from a same thread *) val coi : i_action reln let coi = trace_to_coi t val coi_refl : i_action reln let coi_refl = rc coi { a | forall (a IN image action_to_i_action actions) | is_write a } val po_refl : i_action reln let po_refl = rc (trace_to_po t) (image action_to_i_action actions) val sync_refl : i_action reln let xsync_refl = rc xsync (image action_to_i_action actions) val ctrlisync_refl : i_action reln let ctrlisync_refl = rc ctrlisync (image action_to_i_action actions) val addr_data_refl : i_action reln let addr_data_refl = rc addr_data (image action_to_i_action actions) (* and we need our C++ relations *) val rs : c_action reln let rs = release_sequence_set actions o.lk mo val sw : c_action reln let sw = build_sw actions o c_rf mo val dob : c_action reln let dob = build_dob actions o c_rf mo val ithb : c_action reln let ithb = build_ithb actions o c_rf mo val hb : c_action reln let hb = build_hb actions o c_rf mo (* -------------------- Power happens before -------------------- *) (* Now we show how C++ happens-before related actions are related on the Power trace *) (* Release sequences *) let rs_POWERpo = forall ((a,b) IN rs). (action_to_i_action a, action_to_i_action b) IN coi_refl (* Two C++0x writes related by the release-sequence relation are by definition either equal or related by the modification-order. By the "good_mo" hypothesis we therefore have: (action_to_i_action a, action_to_i_action b) IN co_refl The definition also says that they are on the same thread, hence: (action_to_i_action a, action_to_i_action b) IN coi_refl *) (* Reminder: @@ is relation composition *) (* Synchronizes with *) let sw_POWERshape = forall ((a,b) IN rc o.sb actions @@ sw @@ rc o.sb actions). (action_to_i_action a, action_to_i_action b) IN xsync_refl @@ coi_refl @@ rfe @@ ctrlisync_refl (* PROOF We have (a,b) IN sb^+; sw; sb^+, hence there exists some actions c d on two different threads such that: (a,c) IN sb^= and (c,d) IN sw and (d,b) IN sb^=. where [c] is a release and [d] is an acquire. Hence, by the compilation mapping there is a sync of lwsync directly program-order before [c] (here we use the two "preserved_xsync" hypothesis), hence either [a] and [c] are equal or they are separated by that barrier, by definition this is: (a,d) IN xsync_refl The same way, since [d] is an acquire, by the compilation mapping there is a ctrlisync dependency directly program-order after (here we use the "preserved_ctrlisync" hypothesis). Hence either [d] and [b] are equal or they are separated by that dependency, by definition this is: (d,b) IN ctrlsync_refl Now by definition of the sw-edge, there exists some action [e] such that (c,e) IN rs and (e,d) IN c_rf Using rs_POWERpo we have: (action_to_i_action c, action_to_i_action e) IN coi_refl By the hypothesis "obs t actions c_rf", we know that: (action_to_i_action e, action_to_id_action d) IN rf And since the two actions are on two different threads, this rf-edge is a rfe-edge. The result follows by concatenation. QED *) (* Dependency ordered before *) let dob_POWERshape = forall ((a,d) IN rc o.sb actions @@ dob). (action_to_i_action a, action_to_i_action d) IN xsync_refl @@ coi_refl @@ rfe @@ addr_data_refl (* PROOF First we remark from the definition and by the fact that dd is a subset of sb, that the relation cad is a subset of sb: (a,b) IN cad iff (a,b) IN rc ((c_rf inter sb) union dd) actions By unfolding of the definition of the dob relation, there exists the actions [b] (a consume) and [e] such that: (a,e) IN rs and (e,b) IN c_rf, such that e and b are on different threads. and (b,d) IN cad or b=d Using the same reasoning as for sw_POWERshape, but using also this time the "preserved_dd" hypothesis, the result follows. QED *) (* inter-thread happens before *) let ithb_POWERshape = forall ((a,b) IN ithb). (action_to_i_action a, action_to_i_action b) IN tc (xsync_refl @@ coi_refl @@ rfe @@ (ctrlisync_refl union addr_data_refl)) (* PROOF This proof is direct by unfolding of the definition of the ithb relation and by application of sw_POWERshape and dob_POWERshape. QED *) (* happens before *) let hb_POWERshape = forall ((a,b) IN hb). (action_to_i_action a, action_to_i_action b) IN po union tc (xsync_refl @@ coi_refl @@ rfe @@ (ctrlisync_refl union addr_data_refl)) (* PROOF This proof is direct by unfolding of the definition of the hb relation and by application of ithb_POWERshape. QED *) (* -------------------- Some other tools -------------------- *) open Power_thread_lemmas (* The set of intermediate actions present in the trace [t]. *) val i_actions: i_action set let i_actions = image action_to_i_action actions (* Restriction to the write commits. *) val write_i_actions: i_action set let write_i_actions = { ia | forall (ia IN i_actions). is_write ia} (* Restriction to the read commits. *) val read_i_actions: i_action set let read_i_actions = { ia | forall (ia IN i_actions). is_read ia} (* The trace order of the transitions in the trace [t] *) val t_order: trans reln let t_order = trace_to_order t val t_trans : trans set let t_trans = { l | exist i. i + 1 IN PL t && nth_label i t = l } (* From the definition of the trace order, it is trivial that it is a strict total order of the transitions *) let irrefl_t_order = irrefl t_trans t_order (* Extract the write intermediate action and thread id from a write propagate transition. *) val write_propagate_to_inter : trans -> (i_action * thread_id) option let write_propagate_to_inter c = match c with | Write_propagate_to_thread w tid -> Some (Write (w_aid_comp w.w_eiid) w.w_thread w.w_addr w.w_value, tid) | _ -> None end (* Return the propagation transition for some write to some thread (if it exists). *) val write_propagate_of: trace -> i_action -> thread_id -> trans option let write_propagate_of t ia tid = let s = { l | exist i. i + 1 IN PL t && nth_label i t = l && Some (ia, tid) = write_propagate_to_inter l } in if Set.is_empty s then None else Some (Set.choose s) (* Test whether a transition is trace-order before the last satisfy transition of some read. (NOTE: if [ia] is not a read or if has not "last satisfy" the test is vacuously satisfied. *) val is_before_lastSat: trans -> i_action -> bool let is_before_lastSat c ia = let s = last_satisfy_transition_of t ia in forall (c' IN s). (c, c') IN t_order (* Test whether a transition is a barrier commit *) val is_barrier_commit: trans -> bool let is_barrier_commit c = match c with | Commit_barrier _ _ _ -> true | _ -> false end (* Return the thread id when given a barrier commit transition *) val get_thread_of_barrier: trans -> thread_id option let get_thread_of_barrier c = match c with | Commit_barrier tid _ _ -> Some tid | _ -> None end (* Return the propagation transition for some barrier to some thread (if it exists). *) val barrier_propagate_of: trace -> trans -> thread_id -> trans option let barrier_propagate_of t c tid = let match_propag c = match c with | Commit_barrier tid _ b -> Some (tid,b) | _ -> None end in match c with | Commit_barrier _ _ b -> let s = {l | exist i. i + 1 IN PL t && nth_label i t = l && Some (tid,b) = match_propag l} in if Set.is_empty s then None else Some (Set.choose s) | _ -> None end (* In the proofs we will use the following naming and notation conventions: We represent an execution of a POWER program by a trace: a totally ordered set (E, to) of transitions of the POWER PLDI LTS. We restrict the reasoning to the commit transitions of writes, reads and barriers, and the propagation transitions of writes and barriers. We call them 'labels" and write E ==to==> E' when (E, E') IN to. We call "memory commit label" a write or read commit label. propBefore captures the propagation label of E1 to the thread of E2. Notice that propBefore is not necessarily total. propBefore is defined over trans labels (always commit labels) instead of i_actions because barriers don't appear in i_actions. *) (* The propagation relation: (E1, E2) IN propBefore iff *) val propBefore: trans reln let propBefore = (* ** E1 and E2 are NOT on the same thread: E1 is a barrier commit label AND E2 is a read commit label AND the propagation label of E1 to thread of E2 exists and is trace-order before the last "satisfy" transition of E2. *) { (e1, commit_transition_of t e2) | forall (e1 IN t_trans) (e2 IN read_i_actions) | is_barrier_commit e1 && (match get_thread_of_barrier e1 with Some tid -> tid <> get_thread e2 | _ -> true end) && (exist l. Some l = barrier_propagate_of t e1 (get_thread e2) && is_before_lastSat l e2) } union (* OR E1 is a write commit label AND E2 is a read commit label AND there exists some write commit label W either equal to E1 or (E1, W) IN co, such that the propagation label of W to thread of E2 exists and is trace-order before the last "satisfy" transition of E2. *) { (commit_transition_of t e1, commit_transition_of t e2) | forall (e1 IN write_i_actions) (e2 IN read_i_actions) | get_thread e1 <> get_thread e2 && (exist (w IN write_i_actions). (w=e1 || (e1, w) IN co) && (exist l. Some l = write_propagate_of t w (get_thread e2) && is_before_lastSat l e2)) } union (* OR E1 and E2 are both write commit labels AND there exists some write commit label W either equal to E1 or a coherence successor of E1, such that the propagation label of W to thread of E2 exists and is trace-order before E2. *) { (commit_transition_of t e1, commit_transition_of t e2) | forall (e1 IN write_i_actions) (e2 IN write_i_actions) | get_thread e1 <> get_thread e2 && (exist (w IN write_i_actions). (w=e1 || (e1, w) IN co) && (exist l. Some l = write_propagate_of t w (get_thread e2) && (l, commit_transition_of t e2) IN t_order)) } union (* ** E1 and E2 are on the same thread: E2 is a read commit label AND E1 is either a write and is read by E2 or is trace-order before the last "satisfy" transition of E2. *) { (commit_transition_of t e1, commit_transition_of t e2) | forall (e1 IN i_actions) (e2 IN read_i_actions) | get_thread e1 = get_thread e2 && (e1, e2) IN rfi || is_before_lastSat (commit_transition_of t e1) e2 } union (* OR E2 is a write commit label AND E1 ==to==> E2 *) { (commit_transition_of t e1, commit_transition_of t e2) | forall (e1 IN i_actions) (e2 IN write_i_actions) | get_thread e1 = get_thread e2 && (commit_transition_of t e1, commit_transition_of t e2) IN t_order } (* The POWER machine analogue to the ithb relation from C++0X, (see ithb_POWERshape). *) let machine_ithb = tc (xsync_refl @@ coi_refl @@ rfe @@ (ctrlisync_refl union addr_data_refl)) (* A "message passing" relation, which is a simplification of the previous one. *) let mp_rel = tc (xsync_refl @@ coi_refl @@ rfe) (* ------------------- Some auxiliary lemmas about POWER -------------------- *) let coi_po = forall ((w1, w2) IN coi). (w1, w2) IN po (* PROOF Consider (W1, W2) IN coi, by definition we have: (W1, W2) IN co and they are on the same thread. Hence they are program-order related. We only have to show that (W2, W1) IN po is not possible. Assume the contrary, since the two write or at a same location (because they are coherence related), we now by the 4th precondition of the "Commit in-flight instruction" transition that W2 ==to==> W1. For a coherence edge to exists, the two writes it relates must be committed. Hence the coi-edge from W1 to W2 must be added after W1 is committed, but by the 3rd action of the storage subsystem's part of the commit transition of W1, a coherence edge from W2 to W1 is created. So the coi-edge we assume in our hypothesis cannot have been added later. QED *) let coi_to = forall ((w1, w2) IN coi). (commit_transition_of t w1, commit_transition_of t w2) IN t_order (* PROOF By hypothesis and coi_po, W1 is program-order before W2 and the two writes are coherence-order related, hence they are at the same location. So by the 4th precondition of "Commit in-flight instruction", W1 must be committed before W2. QED *) let lastSat_to = forall (r IN i_actions). (exist (w IN i_actions). (w,r) IN rf --> (forall (l IN last_satisfy_transition_of t r). (l, commit_transition_of t r) IN t_order)) (* PROOF Trivial by the definition of the "Commit in-flight instruction" transition. QED *) let rf_propBefore = forall ((w, r) IN rf). (commit_transition_of t w, commit_transition_of t r) IN propBefore (* PROOF If W and R are on the same thread, then it is trivial by the definition of the propBefore relation. Otherwise, R cannot have been satisfied by forwarding. So R has been satisfied from the storage-subsystem, hence (trace-order) before R was last satisfied, W must have been part of the storage subsystem's "events_propagated_to" list for the thread of R. Since W and R are not on the same thread, it was the "Propagated write to another thread" transition, that added W to the list. Hence W was propagated to the thread of R before R was last "satisfied", this falls into the definition of the propBefore relation. QED *) let rf_to = forall ((w, r) IN rf). (commit_transition_of t w, commit_transition_of t r) IN t_order (* PROOF Using "rf_propBefore", we have: (W, R) IN propBefore We then conclude using "lastSat_to" and by transitivity of the trace-order relation. QED *) (* LEMMA [Xsync_groupA] Consider a POWER trace with E1 and E2, two memory commit labels such that: (E1, E2) IN Xsync, and two write commit labels W1 and W2 such that: (a) W1 = E1 or (W1, E1) IN propBefore; (b) (E2, W2) IN po. Then for any thread t, if the label W2_prop_t exists, then: there exits W a write commit label either equal to W1 or (W1, W) IN co, such that the label W_prop_t exists and W_prop_t ==to==> W2_prop_t. *) let xsync_groupA = forall ((e1,e2) IN xsync) (w1 IN write_i_actions) (w2 IN write_i_actions). (w1=e1 || (commit_transition_of t w1,commit_transition_of t e1) IN propBefore) && (e2,w2) IN po --> (forall tid. (exist l. Some l = write_propagate_of t w2 tid) --> (exist l. Some l = write_propagate_of t w2 tid && (exist (w IN write_i_actions). (w=w1 || (w1,w) IN co) && (exist l'. Some l' = write_propagate_of t w tid && (l,l') IN t_order)))) (* PROOF By the definition of the Xsync, there exists a barrier commit label S from the same thread as E1 and E2 such that : E1 ==to==> S ==to==> E2 Case analyze W1 and E1 are on different or same thread. In the case of different threads, the definition of the propBefore relation immediately gives (using transitivity of the trace order) that W1 is in the group A of S. The case where W1 and E1 are on the same thread puts W1 in the group A of S by using the commits before S. Since S and E2 are on the same thread they are program-order related, and using (b) and by transitivity of the program-order relation, we have: (S, W2) IN po We must have S ==to==> W2 by the CommitPrevBarrierLS precondition of Commit in-flight instruction. Hence, if W2 propagates to t, by the 3rd precondition of the transition "Propagated write to another thread", we have: the S propagates to t before W2 propagates to t. Hence, by the 2nd precondition of the "Propagated a barrier to another thread" transition, we have: there exists some write commit label W, either equal to W1 or (W1, W) IN co, such that W propagates to t before S does. We conclude by transitivity of the trace-order relation. QED *) let xsync_to = forall ((e1, e2) IN xsync). (commit_transition_of t e1, commit_transition_of t e2) IN t_order (* PROOF By the definition of Xsync, there is a barrier label S trace-order between E1 and E2. So we conclude by transitivity of the trace-order. QED *) (* LEMMA [ctrlisync_to] Consider a POWER trace with E1 and E2, two memory commit labels such that: (E1, E2) IN ctrlisync, then if E2 is a read commit label, E1 is trace-order before the last "satisfy" of E2, otherwise E1 ==to==> E2. *) let ctrlisync_to = forall ((e1,e2) IN ctrlisync). (is_read e2 --> (forall (l IN last_satisfy_transition_of t e2). (commit_transition_of t e1, l) IN t_order) && is_write e2 --> (commit_transition_of t e1, commit_transition_of t e2) IN t_order) (* LEMMA [addr+data_to] Consider a POWER trace with E1 and E2, two memory commit labels such that: (E1, E2) IN (addr+data)^+, then if E2 is a read commit label, E1 is trace-order before the last "satisfy" of E2, otherwise E1 ==to==> E2. *) let addr_data_to = forall ((e1,e2) IN addr_data). (is_read e2 --> (forall (l IN last_satisfy_transition_of t e2). (commit_transition_of t e1, l) IN t_order) && is_write e2 --> (commit_transition_of t e1, commit_transition_of t e2) IN t_order) (* Lemma 10: Trace order respects machine-ithb *) let to_lemma = forall ((e,e') IN machine_ithb). (commit_transition_of t e,commit_transition_of t e') IN t_order (* PROOF The proof is by structural induction over the outer [.]^+ of the big relation. * base case: E --. | Xsync + = .-- W1 <-' coi* | '-> W2 -. | rfe R3 <-' \ | ctrlisync + (addr+data)^+ + = E' <--' -------------------------------------------------------------------------- Using "Xsync_to" on (E, W1), we have: E = W1 or E ==to==> W1 Using "coi_to" on (W1, W2), we have: W1 = W2 or W1 ==to==> W2. Using "rf_to" on (W2, R3), we have: W2 ==to==> R3. Using "ctrlisync_to", "lastSat_to" and "addr+data_to" on (R3, E'), we have: R3 = E' or R3 ==to==> E' We conclude by transitivity of the trace-order. * inductive step: E --. | Xsync + = .-- W1 <-' coi* | '-> W2 -. | rfe R3 <-' \ | ctrlisync + (addr+data)* + = .- E4 <--' | | [(Xsync + =); coi*; rfe; ( ctrlisync + (addr+data)^+ + =)]* | '-> E' -------------------------------------------------------------------------- Using the same reasoning as for the base case, we have: E ==to==> E4 Either E4 = E' or using the induction hypothesis on (E4, E') we have: E4 ==to==> E' We conclude by transitivity of the trace-order. QED *) (* Lemma 8: Propagation *) (* NOTE: by the "type" of mp_rel, it is implied that [r] is a read commit label *) let propBefore_lemma = forall ((e,r) IN mp_rel). (is_write e --> (commit_transition_of t e,commit_transition_of t r) IN propBefore) && (is_read e --> (forall (w IN i_actions). is_write w && (commit_transition_of t w, commit_transition_of t e) IN propBefore --> (commit_transition_of t w, commit_transition_of t r) IN propBefore)) (* PROOF The proof is by structural induction in the [.]^+. * base case: E ---. | XSync + = .-- W1 <-' coi* | '-> W2 -. | rfe R <-' -------------------------------------------------------------------------- Using "rf_propBefore" on (W2, R), we have: [1] (W2, R) IN propBefore From [1], by the definition of the propBefore relation we have: [2] the W2 is propagated to the thread of R Using "coi_po", we have: [3] (W1, W2) IN po If E is a write, either E = W1 and then since W2 is a coherence successor, we are done by [1]. Or (E, W1) IN Xsync, so using [2], [3] and "Xsync_groupA, we have: there exists a write commit label W, either equal to E or (E, W) IN co, such that W is propagated to the thread of R before W2 is. If E is a read, we know that E /= W1, so (E, W1) IN Xsync, for any write commit label W such that: (W, E) IN propBefore we have using "Xsync_groupA": there exists a write commit label W', either equal to W or (W, W') IN co, such that the W' is propagated to the thread of R before W2 is. In either case, we conclude using [1] and by transitivity of the trace-order. * inductive step: E ---. | XSync + = .-- W1 <-' coi* | '-> W2 -. | rfe .- R' <-' | | [(Xsync + =); coi*; rfe]* | '-> R -------------------------------------------------------------------------- Using the same arguments as for the base case, if E is a write then E or a coherence successor is propagated to the thread of R' before R' is last satisfied; if E is read, any write W propagated to the thread of E before E is last satisfied, is propagated to the thread of R' before R' is last satisfied. Either R' = R or using the induction hypothesis: any write propagated to the thread of R' before R' is committed is propagated to the thread of R before R is last satisfied. We conclude by transitivity of the trace-order. QED *) (* Corollary 9 - 1. *) let propBefore_read = forall (r IN i_actions) (e IN i_actions). (is_read r && (r, e) IN machine_ithb) --> (forall (w IN i_actions). is_write w && (commit_transition_of t w, commit_transition_of t r) IN propBefore --> (commit_transition_of t w, commit_transition_of t e) IN propBefore) (* PROOF Since ctrlisync and (addr+data) are subsets of po and by the definition of the Xsync relation, we can rewrite: [(Xsync + =); coi*; rfe; (ctrlisync + (addr+data)* + =)]^+ as: [(Xsync + =); coi*; rfe]^+; (ctrlisync + (addr+data)* + =) We get the following situation: .-- R [(Xsync + =); coi*; rfe]^+ | '-> R1 -. | (ctrlisync + (addr+data)* + =) E <-' Using "propBefore_lemma", we have: (W, R1) IN propBefore We can then conclude by transitivity of the trace-order, "ctrlisync_to" and "addr+data_to" QED *) (* Corollary 9 - 1. *) let propBefore_write = forall (w IN i_actions) (e IN i_actions). (is_write w && (w, e) IN machine_ithb) --> (commit_transition_of t w, commit_transition_of t e) IN propBefore (* PROOF The proof follows the one for "propBefore_read" QED *) let propBefore2_rf_to = forall (r IN i_actions) (w IN i_actions) (w' IN i_actions). is_read r && is_write w && is_write w' && (commit_transition_of t w, commit_transition_of t r) IN propBefore && (commit_transition_of t w', commit_transition_of t r) IN propBefore && (w, r) IN rf --> w=w' || (exist l l'. Some l = write_propagate_of t w (get_thread r) && Some l' = write_propagate_of t w' (get_thread r) && (l',l) IN t_order) (* PROOF By the definition of the propBefore relation, we have that both W and W' propagate to the thread of R, in trace order before R. Since R reads from W, that write must be the last one to be propagated to the thread of R, the conclusion is immediate. QED *) let propBefore_to_propBefore = forall (e1 IN i_actions) (e2 IN i_actions) (e3 IN i_actions). (commit_transition_of t e1, commit_transition_of t e2) IN propBefore && (commit_transition_of t e2, commit_transition_of t e3) IN t_order && get_thread e2 = get_thread e3 --> (commit_transition_of t e1, commit_transition_of t e3) IN propBefore (* PROOF By the definition of the propBefore relation, if E2 is a write, E1 is propagated to the thread of E2 before E2 is committed. If E2 is a read, it is propagated before E2 is last satisfied, by lastSat_to. We then conclude directly by transitivity of the trace-order relation. QED *) (****************************************************************************** We now verify all the clauses of [consistent_ex actions o c_rf mo sc] ****************************************************************************** 1- consistent_inter_thread_happens_before actions ithb = irrefl actions ithb Using ithb_POWERshape, it is sufficient to show: *) let _ = irrefl i_actions machine_ithb (* PROOF Consider [ia] an intermediate action such that (ia, ia) IN machine_ithb, then by "to_lemma", we have: (commit_transition_of t ia, commit_transition_of t ia) IN t_order Which leads to a contradiction using "irrefl_t_order" QED *) (* -------------------------------------------------------------------------- 2- consistent_sc_order actions mo sc hb This precidate requires: a) sc is a strict total order over the sc atomics b) hb restricted to the sc atomics is a subset of sc c) mo restricted to the sc atomics is a subset of sc The construction of the sc-order in "build_sc_order.lem" defines it as the union of "fr_sc", "erf_sc", "po_sc" and "co_sc". Hence c) is follows directly. b) follows by unfolding of the definition of the hb-relation restricted to sc atomics, showing that the edges from which we build an hb-edge are from one of the four previous relations. a) follows from "acyclic_sc_relns_lemma" in "build_sc_order.lem" *) (* -------------------------------------------------------------------------- 3- consistent_modification_order_simple actions lk mo hb This predicate requires [mo] to be empty on non atomic locations, this is directly enforced by the definition of "good_mo". And also requires that for any atomic location [l]: a) the restriction of [mo] to actions at the location [l] is a strict total order. This is also by the definition of "good_mo" and "trace_to_co" b) [hb] is a subset of the restriction of [mo] to actions at [l]. This statement correspond to the coherence diagram "CoWW". Let W, W' be some C++ actions working on a same atomic location such that: W x | | hb v W' x CLAIM: W --mo--> W'. PROOF The rest of the coherence diagrams are stated in the predicate "coherent_memory_use" inside the predicate "no_vsse_consistent_reads_from_mapping_simple". The proof for the current statement is very similar to the proof for "CoRW" (except that here we don't need to use "rf_propBefore"), found later in this document. *) (* 4- [no_vsse_consistent_reads_from_mapping_simple actions lk rf sc mo hb vse] The definition is divided in four predicates: a) Non-atomic location ("consistent_non_atomic_read_values") A read R at a non-atomic location must read from a visible side-effect, that is a write W happens-before R such that there is no write W' happens-after W and happens-before R. Assume the contrary, there are three possible situations: - R reads from a write happens-after - R reads from a write hb-hidden: there exists a W' happens-between W and R - R reads from a write hb-unrelated. The last situation is discarded by the "rf_in_hb_condition" hypothesis and will be taken care of in the negative part of the proof. Like before we will transpose the reasoning into POWER using "rf_POWERshape" and "hb_POWERshape". ** hb-after If the hb-sequence is only made of sb-edges, then in POWER (R, W) IN po^+: .-> R --. rf | | po^+ '-- W <-' R and W are at the same location, so by the 4th precondition of the "Commit in-flight instruction" transition, we have: R ==to==> W But we assume that R reads-from W, so (W, R) IN rf, hence using "rf_to" we have: W ==to==> R By transitivity of the trace-order we get R ==to==> R which is a contradiction since to is irreflexive. If the hb-sequence is in fact a ithb-sequence, then we have: .-> R --. rf | | [(Xsync + =); coi*; rfe; '-- W <-' (ctrlisync +(addr+data)* + =)]^+ Using "to_lemma" we have: R ==to==> W Using "rf_to" we conclude exactly like for the previous case. ---------------------------------------------------------------------------- ** hb-hidden If both hb-sequences are only made of sb-edges, then in POWER we have: .-> W ---. | | po^+ rf | W' <-' | | po^+ '-- R <--' -------------------------------------------------------------------------- W, W' and R are at the same location, so by the 4th precondition of the "Commit in-flight instruction" transition, we have: W ==to==> W' ==to==> R Even if R is first satisfied by W (before W' is committed), when W' is committed the 1st action of the "Commit in-flight instruction" transition restart R and this time it will read rom W'. Otherwise, we have three possible case: 1) .-> W ---. | | [(Xsync + =); coi*; rfe; | | (ctrlisync +(addr+data)* + =)]^+ rf | W' <-' | | po^+ '-- R <--' -------------------------------------------------------------------------- Using "propBefore_write", we have: (W, W') IN propBefore And since W' and R are at the same location, by the 4th precondition of the "Commit in-flight instruction" transition, we have: W' ==to==> R W and R are not of the same thread, otherwise we would by in the previous case, so even if R is satisfied by W in a first time, when W' is committed the 1st action of the "Commit in-flight instruction" transition restarts R and this time it will read rom W'. 2) .-> W ---. | | po^+ rf | W' <-' | | [(Xsync + =); coi*; rfe; | | (ctrlisync +(addr+data)* + =)]^+ '-- R <--' -------------------------------------------------------------------------- W and W' are at the same location, so using (W, W') IN po^+ and the 3rd action of the "Accept write request" transition, we have: (W, W') IN co Using "propBefore_write", we have: (W', R) IN propBefore By the 2nd precondition of the "Propagate write to another thread" transition, this implies that either W is not propagated to the thread of R or it is propagated before W' is. This contradict the fact that R reads from W. 3) .-> W ---. | | [(Xsync + =); coi*; rfe; | | (ctrlisync +(addr+data)* + =)]^+ rf | W' <-' | | [(Xsync + =); coi*; rfe; | | (ctrlisync +(addr+data)* + =)]^+ '-- R <--' -------------------------------------------------------------------------- The reasoning is the same as for the previous, except that this time we get that W is coherence-before W' using "propBefore_write" and the 3rd action of the "Accept write request" transition. ================================================================================ b) Atomic location ("no_vsse_consistent_atomic_read_values") For a read R at an atomic location, if there is exists some visible side-effect for R, then R reads from some write that is not happens-after R. Otherwise, R doesn't read from anything. They are therefore two forbidden situations. 1) R has a visible side-effect, but reads from some write that is happens-after .-> R --. rf | | hb '-- W <-' Like before, we translate the reasoning into the POWER trace. Either R is program-order before W, in which case since they are instructions at the same location, W must be committed after R, and since forwarding is only possible for program-order before writes, there is no way for R to read from W. Or R and W are related by the relation in ithb_POWERshape. By rf_to we have: W ==to==> R And by to_lemma we have: R ==to==> W. We have found a cycle in the trace-order, this is a contradiction. 2) R don't have a visible side-effect, ie. there is not write happens-before R, but R still reads from some W. This case directly contradicts the "rf_in_hb_condition" hypothesis. ================================================================================ c) Coherence diagrams ("coherent_memory_use") The "coherent_memory_use" predicate shapes the behaviour of the memory-order relation with respect to the happens-before and reads-from relations. Three situations are specified where some actions are related by the two last relations and for which a memory-order edge must be present. Using the "hb_POWERshape" and "rf_POWERshape" lemmata, we transpose the reasoning into a corresponding POWER trace. From this trace we show that the labels corresponding to actions that must be memory-order related are coherence-order related. For CoRR and CoWR, we have two writes and some read that reads from one of the writes and is somehow hb-related to the other write. We have to show that the write hb-related to the read is either equal or coherence before the other write. To do so, it is sufficient to show that they are propagated to the thread of the read in the proper trace-order, since the "Propagate write to another thread" transition will then force the coherence-ordering. For CoRW and CoWW, we have two writes somehow hb-related and have to show that they are coherence-order related with respect to the hb-ordering. To do so, it is sufficient to show that the first write is propagated to the thread of the second write before it is committed. Then using the 3rd action of "Accept write request", we know that the storage subsystem adds at the commit of W the pair (W, W') to the coherence relation. * CoRR Let W, W', R and R' be some C++ actions working on a same atomic location such that: rf W x ---> R x | | hb rf v W' x ---> R' x CLAIM: W = W' or W --mo--> W' PROOF Using "rf_propBefore", we have: (W, R) IN propBefore (W', R') IN propBefore If the hb-edge is just a sequence-before-edge, then the POWER trace we consider have the following labels: .- W rf | '-> R ---. | .- W' | po rf | | '--> R' <-' Assume both W and W' are on the same thread of R and R'. If R' is satisfied from the storage subsystem (by W', given the rf-edge), it must read from the last write to be committed before it is last satisfied. Hence we must have either have W=W' or W ==to==> W'. In the second case, the 3rd action of the storage subsystem's part of the write commit transition will add the coherence edge we are looking for. If R' is satisfied by forwarding, then W' must the last write (at the location we are considering) program-order before R'. Hence (W, W') IN po, since W and W' are two memory accessing instruction at a same location, by the 4th precondition of the "Commit in-flight instruction", the have: W' ==to==> W We can then conclude the same way as for the previous case. If we have (W', R') IN rfe and (W, R) IN rfi, then assuming the two writes are different, W' cannot be propagated to the thread of W, R and R' before W is committed, otherwise when is committed, R' will be forced to read from it (possibly by redoing of the satisfaction transition). But is must also be propagated after R is satisfied (from W). By "rf_to", we have: W ==to==> R, hence: either W=W' or W ==to==> W'_prop_"thread of W, R and R'" In the second case, by the 2nd precondition of the "Propagate write to another thread" transition, we know that W' must be coherence-after any write already propagated to the thread of R' (hence W). The case where (W', R') IN rfi and (W, R) IN rfe, we argue in the same way that W must be propagated before R' is satisfied (from W'), hence the coherence ordering by the 3rd action of the storage subsystem's part of the write commit transition. If both rf-edges are external, then we argue that we must have: W=W' or W propagates to the thread of R (and R') before W' does. And we can conclude like before. Otherwise, if the hb-edge comes from a ithb-edge, by "propBefore_lemma", we have: (W, R') IN propBefore By "propBefore2_rf_to", we have either W'=W or W propagates to the thread of R' before W' does. For the second case, we conclude like before. -------------------------------------------------------------------------------- * CoWR Let W, W' and R be some C++ actions working a same atomic location such that: W x | | hb rf v W' x ---> R x CLAIM: Then either W = W' or W --mo--> W'. PROOF The reasoning is very similar to the one for CoRR. Using "rf_propBefore", we have: (W', R') IN propBefore Because of the read-from edge, then if the hb-edge comes from a sb-edge, we know that either the two write are equal or W' is program-order after W. Hence when it is committed (after W, since they are at the same location), the 3rd action of the storage subsystem's part of the commit add the coherence edge we are looking for. If the hb-edge comes from a ithb-edge, then we use "propBefore_lemma" to have: (W, R) IN propBefore Like for CoRR, in the case where the two writes are different, we have a case analysis on whether W' and R are on the same thread or not. In the first case argue that W must be propagated before W' is committed, hence the semantics of the commit transition for a write add the coherence edge. In the second case, we argue that W' must be propagated to the thread of R after W and therefore the semantics of the "Propagate write to another thread" transition produce the coherence edge. -------------------------------------------------------------------------------- * CoRW Let W, W' and R be some C++ actions working on a same atomic location such that: rf W x ---> R x | | hb v W' x CLAIM: W --mo--> W'. PROOF If the hb-edge is just a sequence-before-edge, the POWER trace we consider have the following labels: W -. | rf .- R <-----' po^+ | '-> W' Either W and R are on the same thread and by "rf_to", we have: W ==to==> R So when W' is committed, W is in the storage subsystem's "events propagated to" list, hence the 3rd action of the "Accept write request" transition adds (W, W') IN co. Or they are not, and using "rf_propBefore" on (W, R) IN rf, we have: (W, R) IN propBefore R and W' are on the same location and the same thread, so by the 4th precondition of "Commit in-flight instruction", we have: R ==to==> W' Hence by "propBefore_to_propBefore": (W, W') IN propBefore We can now conclude as stated in the introduction. If the hb-edge comes from a ithb-edge, using "propBefore_read" we directly get that (W, W') IN propBefore, and can conclude as before. ================================================================================ d) SC reads ("sc_reads_restricted") A sequentially consistent read R_sc either reads from the last SC-preceding write at the same location, or it reads from a non-SC write W and the last SC-preceding write W'_sc is not happens-after W. So we have two kind of wrong situation 1) R_sc reads from some W_sc that is not the last SC-preceding write. This is similar to the "hb-after", "hd-hidden" we had for non-atomic locations. * sc-after: .-> R_sc ---. rf | | sc '-- W_sc <--' By the definition of ERF (in notes08-SC-order.txt), the rf-edge is also an ERF-edge. So we have a sc-cycle, which is a contradiction. * sc-hidden: .-- W_sc ---. | | sc rf | W'_sc <-' | | sc '-> R_sc <--' Using the Lemma 3.5 from note08-SC-order, we have: (W_sc, W'_sc) IN co + = In this situation the write are different, otherwise there wouldn't be any problem. So by definition, we have: (R_sc, W'_sc) IN RF Hence we have found a sc-cycle, which is a contradiction. 2) R_sc reads from some non-sc write W that is happens-after .- W -. | | hb rf | | | '-> W'_sc -. | | sc '-> R_sc <-------' If the hb-edge is only made of sb-edges, then in POWER: (W, W'_sc) IN po^+ Since they are at the same location, using the 4th precondition of the "Commit in-flight instruction" transition, we have: W ==to==> W'_sc Hence by the 3rd action of the "Accept write request" transition, we have: (W, W') IN co Now using the FR relation defined in the construction of sc-order, we have: (R_sc, W'_sc) IN FR Hence we have found a sc-cycle, which is a contradiction. *) (* -------------------------------------------------------------------------- 5- well_formed_reads_from_mapping_simple actions lk rf This predicate only states some "well formation" properties about the read-from mapping, like the fact that a read reads from at most one write, or that the read and the write must be at the same location. This is satisfied by the fact that the "input" C++0x program is assume consistent, by the construction of the read from mapping and the hypothesis "obs t actions c_rf". *)