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 singlethreaded 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 *)
(*
[readfrom]
(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
(*
[programorder]
(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 traceorder before
the one from [b]) is traceorder 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 programorder 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++ happensbefore 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 releasesequence relation are by definition
either equal or related by the modificationorder. 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 programorder 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 programorder 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 swedge, 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 rfedge is a
rfeedge.
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
*)
(* interthread 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 traceorder 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
traceorder 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 traceorder 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 traceorder 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 traceorder 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 programorder 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 inflight instruction" transition that W2 ==to==> W1. For a coherence
edge to exists, the two writes it relates must be committed. Hence the
coiedge 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 coiedge 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 programorder before W2 and the two writes are
coherenceorder related, hence they are at the same location. So by the 4th
precondition of "Commit inflight 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 propBefore))
(*
PROOF
Trivial by the definition of the "Commit inflight 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 storagesubsystem, hence (traceorder) 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 traceorder
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 programorder related, and
using (b) and by transitivity of the programorder relation, we have:
(S, W2) IN po
We must have S ==to==> W2 by the CommitPrevBarrierLS precondition of Commit inflight 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 traceorder 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 traceorder
between E1 and E2.
So we conclude by transitivity of the traceorder.
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 traceorder 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 traceorder 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 machineithb *)
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 traceorder.
* 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 traceorder.
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_to", 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
traceorder.
* 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 traceorder.
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 traceorder, "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 traceorder 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 scorder 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 hbrelation restricted to
sc atomics, showing that the edges from which we build an hbedge 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) Nonatomic location ("consistent_non_atomic_read_values")
A read R at a nonatomic location must read from a visible sideeffect, that
is a write W happensbefore R such that there is no write W' happensafter W
and happensbefore R.
Assume the contrary, there are three possible situations:
 R reads from a write happensafter
 R reads from a write hbhidden: there exists a W' happensbetween W
and R
 R reads from a write hbunrelated.
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".
** hbafter
If the hbsequence is only made of sbedges, 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 inflight instruction" transition, we have:
R ==to==> W
But we assume that R readsfrom W, so (W, R) IN rf, hence using "rf_to" we
have:
W ==to==> R
By transitivity of the traceorder we get R ==to==> R which is a
contradiction since to is irreflexive.
If the hbsequence is in fact a ithbsequence, 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.

** hbhidden
If both hbsequences are only made of sbedges, 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 inflight 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 inflight 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 inflight 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 inflight 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 coherencebefore 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
sideeffect for R, then R reads from some write that is not happensafter R.
Otherwise, R doesn't read from anything.
They are therefore two forbidden situations.
1) R has a visible sideeffect, but reads from some write that is
happensafter
.> R .
rf   hb
' W <'
Like before, we translate the reasoning into the POWER trace. Either R is
programorder 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 programorder 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 traceorder, this is a contradiction.
2) R don't have a visible sideeffect, ie. there is not write happensbefore 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 memoryorder
relation with respect to the happensbefore and readsfrom relations. Three
situations are specified where some actions are related by the two last
relations and for which a memoryorder 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 memoryorder related are coherenceorder
related.
For CoRR and CoWR, we have two writes and some read that reads from one of the
writes and is somehow hbrelated to the other write. We have to show that the
write hbrelated 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 traceorder, since the
"Propagate write to another thread" transition will then force the
coherenceordering.
For CoRW and CoWW, we have two writes somehow hbrelated and have to show that
they are coherenceorder related with respect to the hbordering. 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 hbedge is just a sequencebeforeedge, 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 rfedge), 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) programorder 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 inflight 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
coherenceafter 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 rfedges 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 hbedge comes from a ithbedge, 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 readfrom edge, then if the hbedge comes from a sbedge,
we know that either the two write are equal or W' is programorder 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 hbedge comes from a ithbedge, 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 hbedge is just a sequencebeforeedge, 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 inflight 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 hbedge comes from a ithbedge, 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 SCpreceding
write at the same location, or it reads from a nonSC write W and the last
SCpreceding write W'_sc is not happensafter W.
So we have two kind of wrong situation
1) R_sc reads from some W_sc that is not the last SCpreceding write. This
is similar to the "hbafter", "hdhidden" we had for nonatomic
locations.
* scafter:
.> R_sc .
rf   sc
' W_sc <'
By the definition of ERF (in notes08SCorder.txt), the rfedge is also an
ERFedge. So we have a sccycle, which is a contradiction.
* schidden:
. W_sc .
  sc
rf  W'_sc <'
  sc
'> R_sc <'
Using the Lemma 3.5 from note08SCorder, 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 sccycle, which is a contradiction.
2) R_sc reads from some nonsc write W that is happensafter
. W .
  hb
rf  
 '> W'_sc .
  sc
'> R_sc <'
If the hbedge is only made of sbedges, then in POWER:
(W, W'_sc) IN po^+
Since they are at the same location, using the 4th precondition of the
"Commit inflight 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 scorder, we have:
(R_sc, W'_sc) IN FR
Hence we have found a sccycle, which is a contradiction.
*)
(* 
5 well_formed_reads_from_mapping_simple actions lk rf
This predicate only states some "well formation" properties about the
readfrom 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".
*)