(* -------------------- Lem preliminaries -------------------- *) (* Paths through labelled transition systems, following the HOL4 path theory. *) (* Should be in Lem's library *) (* The type of paths with 'a state components and 'b labels *) type ('a, 'b) path (* Checks that a path is through the (curried) relation *) val okpath : forall 'a 'b. ('a->'b->'a->bool) -> ('a,'b) path -> bool (* Is the path finite *) val is_stopped : forall 'a 'b. ('a,'b) path -> bool (* The set of all number that can be used to index the path (i.e., all numbers for infinite paths, and those less than the length for other paths) *) val PL : forall 'a 'b. ('a,'b) path -> num set val first : forall 'a 'b. ('a,'b) path -> 'a val last : forall 'a 'b. ('a,'b) path -> 'a val nth : forall 'a 'b. num -> ('a,'b) path -> 'a val nth_label : forall 'a 'b. num -> ('a,'b) path -> 'b (* Some relation theory that should be in Lem's library *) type 'a reln = ('a * 'a) set val rrestrict : forall 'a. 'a reln -> 'a set -> 'a reln let rrestrict r s = { (x,y) | forall ((x,y) IN r) | x IN s && y IN s } val down_closed : forall 'a. 'a set -> 'a reln -> bool let down_closed s r = forall x (y IN s). (x,y) IN r --> x IN s (* Relation composition *) val (@@) : forall 'a. 'a reln -> 'a reln -> 'a reln let (@@) r1 r2 = { (x,z) | exist y. (x,y) IN r1 && (y,z) IN r2 } let rc r s = r union { (x,x) | forall (x IN s) | true } val tc : forall 'a. 'a reln -> 'a reln val reln_subst : forall 'a. 'a reln -> 'a -> 'a -> 'a reln (* Replace x with x' in relation r *) let reln_subst r x' x = { (a,b) | forall ((a,b) IN r) | a <> x && b <> x } union { (a,x') | forall a | (a,x) IN r } union { (x',a) | forall a | (x,a) IN r } (* extend to a strict linear order; should only be applied to strict partial orders *) val strict_linearize : forall 'a. 'a reln -> 'a reln val is_acyclic : forall 'a. 'a reln -> bool val image : forall 'a 'b. ('a -> 'b) -> 'a set -> 'b set let image f xs = { f x | forall (x IN xs) | true } (* -------------------- Naming preliminaries -------------------- *) type c_action = Atomic.action type p_action = MachineDefTypes.action type i_action = Intermediate_actions.action type c_thread_id = Atomic.thread_id type p_thread_id = MachineDefTypes.thread_id type c_value = Atomic.value type p_value = MachineDefValue.value let c_happens_before = Atomic.happens_before let c_is_write = Atomic.is_write let c_is_load = Atomic.is_load let c_is_read = Atomic.is_read (* Note that Atomic has a constructor Atomic, so that we cannot say Atomic.v after the open *) open Atomic open Atomic_simple open MachineDefTypes open MachineDefSystem open MachineDefValue open Intermediate_actions (* -------------------- C++ thread semantics -------------------- *) (* opinfo collects the information that arises from the thread semantics The lk field contains the dynamic kind of each location (i.e., Atomic or Non_atomic). The sb, asw, and dd fields contains the sequenced before, additional synchronizes with, and data dependence information information required by the memory model. The cd field contains a semantic notion of control dependence that compilation must respect, and which is necessary in opsem_add_read_axiom below. *) type opinfo = <| lk : location -> location_kind; sb : c_action reln; asw : c_action reln; dd : c_action reln; cd : c_action reln; |> let restrict_opinfo o actions = <| lk = o.lk; sb = rrestrict o.sb actions; asw = rrestrict o.asw actions; dd = rrestrict o.dd actions; cd = rrestrict o.cd actions; |> let subst_opinfo o x' x = <| lk = o.lk; sb = reln_subst o.sb x' x; asw = reln_subst o.asw x' x; dd = reln_subst o.dd x' x; cd = reln_subst o.cd x' x; |> (* We'll fix an abstract type of single-threaded C++ programs *) type c_program_thread (* And we'll fix a semantics for the thread-local behaviour of such programs *) val single_thread_opsem : c_program_thread -> (c_action set * opinfo) set (* Given a single-threaded C++ program, single_thread_opsem returns a (possibly infinite) set of results of that program. Each result contains the set of actions that occurred, and the other relevant operational information. The intention is that memory reads can non-deterministically read any value; this is captured formally in opsem_add_read_axiom below. *) (* A C++ program is a mapping from thread ids to single-threaded C++ programs *) type c_program = (c_thread_id, c_program_thread) Pmap.map (* opsem combines the single-threaded results *) val opsem : c_program -> (c_action set * c_thread_id set * opinfo) set let opsem p = let c_tids = { tid | Pmap.mem tid p } in { (actions, c_tids, o) | forall actions o | { thread_id_of a | forall (a IN actions) | true } subset c_tids && (forall ((a,b) IN o.sb). thread_id_of a = thread_id_of b) && (forall ((a,b) IN o.asw). thread_id_of a = thread_id_of b) && (forall ((a,b) IN o.dd). thread_id_of a = thread_id_of b) && (forall ((a,b) IN o.cd). thread_id_of a = thread_id_of b) && (forall (c_tid IN c_tids). let t_actions = { a | forall (a IN actions) | thread_id_of a = c_tid } in ((t_actions, restrict_opinfo o t_actions) IN single_thread_opsem (Pmap.find c_tid p))) } (* Is the set actions' a subset of a complete opsem that respects data and control dependency, but not necessarily sequenced-before *) val opsem_prefix : c_program -> c_action set -> c_action set -> c_thread_id set -> opinfo -> bool let opsem_prefix p actions' actions c_tids o = (actions, c_tids, o) IN opsem p && actions' subset actions && down_closed actions' (tc (o.dd union o.cd)) (* Replaces the value read or written by an action with all possibilities *) val all_values : c_action -> c_action set let all_values a = match a with | Load aid tid loc v -> { Load aid tid loc v' | forall v' | true } | Atomic_load aid tid mo loc v -> { Atomic_load aid tid mo loc v' | forall v' | true } | Store aid tid loc v -> { Store aid tid loc v' | forall v' | true } | Atomic_store aid tid mo loc v -> { Atomic_store aid tid mo loc v' | forall v' | true } end (* We require this property of opsem that allows the value read at a certain point to be changed arbitrarily without disturbing future data+control independent actions *) let opsem_add_read_axiom = forall p actions' actions c_tids o (a IN actions \ actions') (a' IN all_values a). opsem_prefix p actions' actions c_tids o && c_is_read a && (forall (b IN actions). (b,a) IN tc (o.dd union o.cd) --> b IN actions') --> (exist new_actions new_o. let unchanged_actions = { b | forall (b IN actions \ actions') | b <> a && not ((a,b) IN tc (o.dd union o.cd)) } in let staying_actions = actions' union unchanged_actions in (new_actions inter staying_actions = {}) && (subst_opinfo (restrict_opinfo o (staying_actions union {a})) a' a = restrict_opinfo new_o (staying_actions union {a'})) && (forall ((x,y) IN tc (new_o.dd union new_o.cd)). x IN new_actions --> not (y IN staying_actions union {a'})) && (staying_actions union {a'} union new_actions, c_tids, new_o) IN opsem p) (* The following lemma lets us add writes to an opsem_prefix, without changing their value. It follows immediately from the definition of opsem_prefix *) let opsem_add_write_lem = forall p actions' actions c_tids o (a IN actions \ actions'). opsem_prefix p actions' actions c_tids o && (c_is_write a) && (forall (b IN actions). (b,a) IN tc (o.dd union o.cd) --> b IN actions') --> (let actions'' = {a} union actions' in opsem_prefix p actions'' actions c_tids o) (* We also require that the operational semantics produces well-formed threads *) let opsem_wfthreads_axiom = forall p actions c_tids o. (actions, c_tids, o) IN opsem p --> well_formed_threads actions c_tids o.lk o.sb o.asw o.dd o.cd (* -------------------- C++ memory model prelimiaries -------------------- *) let build_sw actions o rf mo = synchronizes_with_set_simple actions o.asw rf (release_sequence_set actions o.lk mo) (hypothetical_release_sequence_set actions o.lk mo) let build_dob actions o rf mo = dependency_ordered_before_set actions rf (release_sequence_set actions o.lk mo) (carries_a_dependency_to_set actions o.sb o.dd rf) let build_ithb actions o rf mo = inter_thread_happens_before actions o.sb (build_sw actions o rf mo) (build_dob actions o rf mo) let build_hb actions o rf mo = happens_before actions o.sb (build_ithb actions o rf mo) (* The memory model, simplified for the situation we treat in this proof *) let consistent_ex actions o rf mo sc = no_vsse_consistent_execution_simple actions o.lk o.sb o.asw o.dd o.cd rf mo sc (* Programs that have no undefined behaviour *) val drf : c_program -> bool let drf p = let executions = { (actions,c_tids,o,rf,mo,sc) | (actions,c_tids,o) IN opsem p && consistent_ex actions o rf mo sc } in (forall ((actions,c_tids,o,rf,mo,sc) IN executions). indeterminate_reads actions rf = {} && unsequenced_races actions o.sb = {} && data_races actions (build_hb actions o rf mo) = {}) val c_semantics : c_program -> (c_action set * c_action reln) set option let c_semantics p = if drf p then Some { (actions,rf) | exist c_tids o mo sc. (actions,c_tids,o) IN opsem p && consistent_ex actions o rf mo sc } else None (* -------------------- Power preliminaries -------------------- *) type p_program = p_value -> instruction option let our_model_params = <| ss = <| coherence_commit = Partial_CC; pcc_deadlock_avoid = true; coherence_points = false; |>; t = <| thread_loose_tight = Thread_loose; thread_lwsync = Lwsync_read_restart; |>; |> type trace = (system_state, trans) path val machine_execution_prefix : p_program -> p_thread_id set -> trace set let machine_execution_prefix p tids = let is = initial_system_state tids (fun tid r -> zero) [] our_model_params in { path | okpath (system_label_trans p) path && (first path = is) } val machine_executions : p_program -> p_thread_id set -> trace set let machine_executions p tids = { path | forall (path IN machine_execution_prefix p tids) | (is_stopped path --> not (exist l s'. system_label_trans p (last path) l s')) } (* -------------------- The compiler -------------------- *) (* Assume we can translate the basics from C++ to Power *) val r_aid_comp : r_eiid -> action_id val w_aid_comp : w_eiid -> action_id val tid_comp : c_thread_id -> p_thread_id val loc_comp : location -> address val val_comp : c_value -> p_value (* Paul's chart, interpreted as mapping C++ actions to i_actions, along with what kind of fences must precede and follow the Power action. We produce i_actions, which correspond to the relevant parts of Power transition labels *) val action_comp : c_action -> fence option * i_action * fence option let action_comp a = match a with | Load aid tid l v -> (None, Read aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Store aid tid l v -> (None, Write aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Atomic_load aid tid Mo_seq_cst l v -> (Some Hwsync, Read aid (tid_comp tid) (loc_comp l) (val_comp v), Some Ctrlisync) | Atomic_load aid tid Mo_relaxed l v -> (None, Read aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Atomic_load aid tid Mo_acquire l v -> (None, Read aid (tid_comp tid) (loc_comp l) (val_comp v), Some Ctrlisync) | Atomic_load aid tid Mo_consume l v -> (None, Read aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Atomic_store aid tid Mo_seq_cst l v -> (Some Hwsync, Write aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Atomic_store aid tid Mo_relaxed l v -> (None, Write aid (tid_comp tid) (loc_comp l) (val_comp v), None) | Atomic_store aid tid Mo_release l v -> (Some Lwsync, Write aid (tid_comp tid) (loc_comp l) (val_comp v), None) end val action_to_i_action : c_action -> i_action let action_to_i_action a = match action_comp a with | (_,a,_) -> a end val action_to_pre_fence : c_action -> fence option let action_to_pre_action a = match action_comp a with | (a,_,_) -> a end val action_to_post_fence : c_action -> fence option let action_to_post_action a = match action_comp a with | (_,_,a) -> a end (* -------------------- Observable behaviour -------------------- *) (* Definition of when a C++ execution and a Power trace have the same observable behaviour *) val reads_of_trace : trace -> read_response set let reads_of_trace t = { r | exist idx tid i b rrs. idx + 1 IN PL t && nth_label idx t = Commit_read tid i rrs && r IN rrs } (* Convert the trace's notion of reads-from to i_actions *) val trace_to_rf : trace -> i_action reln let trace_to_rf t = { (Write (w_aid_comp r.rr_write.w_eiid) r.rr_write.w_thread r.rr_write.w_addr r.rr_write.w_value, Read (r_aid_comp r.rr_eiid) r.rr_thread r.rr_write.w_addr r.rr_write.w_value) | forall (r IN reads_of_trace t) | true } val trace_to_rfe : trace -> i_action reln let trace_to_rfe t = { (x,y) | forall ((x,y) IN trace_to_rf t) | get_thread x <> get_thread y } val trace_to_rfi : trace -> i_action reln let trace_to_rfi t = { (x,y) | forall ((x,y) IN trace_to_rf t) | get_thread x = get_thread y } (* Create the relevant set of i_actions from the commit labels of the trace. Also get the ioid *) val commit_to_inter : trans -> (num * i_action) set let commit_to_inter c = match c with | Commit_read tid i rrs -> { (i.ioid,Read (r_aid_comp r.rr_eiid) r.rr_thread r.rr_write.w_addr r.rr_write.w_value) | forall r | r IN rrs } | Commit_write tid i ws -> { (i.ioid,Write (w_aid_comp w.w_eiid) w.w_thread w.w_addr w.w_value) | forall w | w IN ws } | _ -> {} end val trace_to_actions : trace -> i_action set let trace_to_actions t = bigunion { image snd (commit_to_inter l) | forall l | exist i. i + 1 IN PL t && nth_label i t = l} (* A Power trace and set of C++ actions are have the same observable behaviour when the i_actions built from the commit labels of the trace correspond to those created by compiling the C++ actions with the chart *) val obs : trace -> (c_action set) -> c_action reln -> bool let obs t actions rf = (trace_to_actions t = image action_to_i_action actions) && (trace_to_rf t = { (action_to_i_action w, action_to_i_action r) | forall ((w,r) IN rf) | true }) (* -------------------- Good single-threaded compilers -------------------- *) (* We axiomatize what it means for a compiler to be correct with respect to the single-threaded semantics *) (* We extract dependency and program order relations (and later, coherence) from the trace. These pick an arbitrary state in the trace of the Power machine LTS, relying on the fact that the relations 1--4 grow monotonically as the trace extends: 1. Program order (for committed instructions) -- Justification: The Power machine may fetch new instructions, but no transition removes committed instructions from the state (however, in-flight instructions can be aborted). 2. Data Dependency (for committed instructions) -- Justification: as discussed above, the program order relation changes monotonically for committed instructions, and for each instruction instance, its input and output registers is statically determined. Since data dependency is built out of these two, it grows monotonically as well. 3. Control Dependency (for committed instructions) -- Justification: as discussed in 1, the program order relation changes monotonically for committed instructions, and for each instruction instance, its input and output registers, and whether or not it is a branch instruction, is statically determined. Since control dependency is built out of these two, it grows monotonically as well. 4. Coherence -- Justification: Some transitions (partial coherence commit, accept write request) can add coherence edges, but no transition removes coherence edges. *) (* The label ordering given by the trace *) val trace_to_order : trace -> trans reln let trace_to_order t = { (nth_label i t,nth_label j t) | forall i j | exist i j l1 l2. i + 1 IN PL t && j + 1 IN PL t && i < j } (* Convenience function to pick, given a system state, all instruction instances associated with each of the thread states *) val instrs_and_threads_of_state : system_state -> (thread_state * instruction_instance set) set let instrs_and_threads_of_state s = let thread_states = { (s.thread_states tid) | forall (tid IN s.storage_subsystem.threads) | true } in { (ts, ts.in_flight_instructions union ts.committed_instructions) | forall (ts IN thread_states) | true } (* Extract the program order relation from a trace *) val trace_to_po : trace -> i_action reln let trace_to_po t = let tr_actions_with_ioid = bigunion { commit_to_inter l | exist i. i + 1 IN PL t && nth_label i t = l } in {(ia1,ia2) | forall ((i1,ia1) IN tr_actions_with_ioid) ((i2,ia2) IN tr_actions_with_ioid) | exist n ts iis ii1 ii2. n + 1 IN PL t && (ts,iis) IN instrs_and_threads_of_state (nth n t) && ii1 IN iis && ii1.ioid = i1 && ii2 IN iis && ii2.ioid = i2 && ii2 IN MachineDefThreadSubsystem.strict_program_order_suffix ts ii1} (* Extract the data dependence relation from a trace Here ii2 is data dependent on ii1 if ii2 is strictly program order after ii1, and there is data flow through registers from ii1 to ii2 *) val trace_to_dd : trace -> i_action reln let trace_to_dd t = let tr_actions_with_ioid = bigunion { commit_to_inter l | exist i. i + 1 IN PL t && nth_label i t = l } in {(ia1,ia2) | forall ((i1,ia1) IN tr_actions_with_ioid) ((i2,ia2) IN tr_actions_with_ioid) | exist n ts iis ii1 ii2. n + 1 IN PL t && (ts,iis) IN instrs_and_threads_of_state (nth n t) && ii1 IN iis && ii1.ioid = i1 && ii2 IN iis && ii2.ioid = i2 && ii2 IN MachineDefThreadSubsystem.strict_dependent_suffix ts ii1} (* Extract the control dependency relation from a trace Here ii2 is control dependent on ii1 if ii2 is strictly program order after ii1, and there is a branch instruction instance iib, with data flow through registers from ii1 to iib and program order between iib and ii2. *) val trace_to_cd : trace -> i_action reln let trace_to_cd t = let tr_actions_with_ioid = bigunion { commit_to_inter l | exist i. i + 1 IN PL t && nth_label i t = l } in {(ia1,ia2) | forall ((i1,ia1) IN tr_actions_with_ioid) ((i2,ia2) IN tr_actions_with_ioid) | exist n ts iis ii1 ii2 iib ib. n + 1 IN PL t && (ts,iis) IN instrs_and_threads_of_state (nth n t) && ii1 IN iis && ii1.ioid = i1 && ii2 IN iis && ii2.ioid = i2 && iib IN iis && iib.ioid = ib && iib.is_branch && (* iib is dependent on ii1 && ii2 is po after iib *) iib IN MachineDefThreadSubsystem.strict_dependent_suffix ts ii1 && ii2 IN MachineDefThreadSubsystem.strict_program_order_suffix ts iib} (* Extract the control-isync dependency relation from a trace Here ii2 is control-isync dependent on ii1 if ii2 is strictly program order after ii1, and there is a branch instruction instance iib and an isync instruction instance iiisync, with data flow through registers from ii1 to iib and program order between iib and iiisync and iiisync and ii2. *) val trace_to_ctrlisync : trace -> i_action reln let trace_to_ctrlisync t = let tr_actions_with_ioid = bigunion { commit_to_inter l | exist i. i + 1 IN PL t && nth_label i t = l } in {(ia1,ia2) | forall ((i1,ia1) IN tr_actions_with_ioid) ((i2,ia2) IN tr_actions_with_ioid) | exist n ts iis ii1 ii2 iib ib iiisync iisync. n + 1 IN PL t && (ts,iis) IN instrs_and_threads_of_state (nth n t) && ii1 IN iis && ii1.ioid = i1 && ii2 IN iis && ii2.ioid = i2 && iib IN iis && iib.ioid = ib && iib.is_branch && iiisync IN iis && iiisync.ioid = iisync && iiisync.is_isync && (* iib is dependent on ii1 && ii2 is po after iiisync && iiisync is po after iib *) iib IN MachineDefThreadSubsystem.strict_dependent_suffix ts ii1 && iiisync IN MachineDefThreadSubsystem.strict_program_order_suffix ts iib && ii2 IN MachineDefThreadSubsystem.strict_program_order_suffix ts iiisync} (* Extract the xsync relation from a trace. Two actions on the same thread are xsync related if there is a fence of the given type on the trace between them and on the same thread *) val trace_to_xsync : trace -> barrier_type -> i_action reln let trace_to_xsync t x = { (a,c) | forall (a IN trace_to_actions t) (c IN trace_to_actions t) | exist a' b c' tid ii eiid. (a',b) IN trace_to_order t && (b,c') IN trace_to_order t && a IN image snd (commit_to_inter a') && c IN image snd (commit_to_inter c') && b = Commit_barrier tid ii <| b_thread = tid; b_eiid = eiid ; b_barrier_type = x |> && tid = get_thread a && tid = get_thread c } (* Checks that C++ sequenced before is preserved in Power program order *) val preserved_po : trace -> c_action set -> c_action reln -> bool let preserved_po t actions sb = let i_po = { (action_to_i_action a1, action_to_i_action a2) | forall ((a1,a2) IN sb) | true } in i_po subset trace_to_po t (* Checks that C++ data dependency is preserved in Power data dependency *) val preserved_dd : trace -> c_action set -> c_action reln -> bool let preserved_dd t actions dd = let i_dd = { (action_to_i_action a1, action_to_i_action a2) | forall ((a1,a2) IN dd) | true } in i_dd subset trace_to_dd t (* Checks that C++ control dependency is preserved in Power control dependency *) val preserved_cd : trace -> c_action set -> c_action reln -> bool let preserved_cd t actions cd = let i_cd = { (action_to_i_action a1, action_to_i_action a2) | forall ((a1,a2) IN cd) | true } in i_cd subset trace_to_cd t (* Checks that the fences required by action_comp are present in the Power trace. Note that we check with respect to Power program order instead of C++ sequenced-before since the latter might not be total when restricted to a single thread. *) val preserved_xsync : trace -> fence -> c_action set -> bool let preserved_xsync t x actions = let i_xsync : i_action reln = { (action_to_i_action a, action_to_i_action c) | forall (a IN actions) (c IN actions) | (action_to_i_action a, action_to_i_action c) IN trace_to_po t && (action_to_post_fence a = Some x || action_to_pre_fence c = Some x || (exist (b IN actions). (action_to_i_action a, action_to_i_action b) IN trace_to_po t && (action_to_i_action b, action_to_i_action c) IN trace_to_po t && (action_to_post_fence b = Some x || action_to_pre_fence b = Some x))) } in let x' = match x with | Hwsync -> Sync | Lwsync -> LwSync end in i_xsync subset trace_to_xsync t x' (* Checks that the Power trace has a control-isync where required *) val preserved_ctrlisync : trace -> c_action set -> bool let preserved_ctrlisync t actions = let i_ctrlisync = { (action_to_i_action a, action_to_i_action c) | forall (a IN actions) (c IN actions) | (action_to_i_action a, action_to_i_action c) IN trace_to_po t && (action_to_post_fence a = Some Ctrlisync) } in i_ctrlisync subset trace_to_ctrlisync t (* A compiler must arrange that any behaviour of the target Power program is accepted by the C++ opsem, and that all of the single-threaded dependencies above are preserved *) val threadwise_good_compiler : (c_program -> (p_program * p_thread_id set)) -> bool let threadwise_good_compiler comp = forall c_prog t. (let (power_prog,p_tids) = comp c_prog in t IN machine_executions power_prog p_tids --> (exist actions c_tids o rf. obs t actions rf && (actions,c_tids,o) IN opsem c_prog && preserved_po t actions o.sb && preserved_dd t actions o.dd && preserved_cd t actions o.cd && preserved_xsync t Hwsync actions && preserved_xsync t Lwsync actions && preserved_ctrlisync t actions)) (* -------------------- The correctness statement -------------------- *) let correct_compiler_thm = forall comp c_prog. threadwise_good_compiler comp && drf c_prog --> (let (power_prog,p_tids) = comp c_prog in (forall (t IN machine_executions power_prog p_tids). (exist actions c_tids o rf mo sc. obs t actions rf && (actions,c_tids,o) IN opsem c_prog && consistent_ex actions o rf mo sc))) (* -------------------- C++ modification and sc ordering -------------------- *) (* Define when a C++ modification order and C++ sequential consistency order are consistent with a Power trace *) (* Get the coherence ordering for a single address. Relies on the Power trace's property that the coherence order of earlier states is a subset of later states (as discussed at the start of "Good single-threaded compilers" above) *) val addr_trace_to_co : address -> trace -> i_action reln let addr_trace_to_co a t = { (Write (w_aid_comp w1.w_eiid) w1.w_thread w1.w_addr w1.w_value, Write (w_aid_comp w2.w_eiid) w2.w_thread w2.w_addr w2.w_value) | forall w1 w2 | w1.w_addr = a && w2.w_addr = a && (exist i. i IN PL t && (w1,w2) IN (nth i t).storage_subsystem.coherence) } (* A per memory address strict total order on memory stores *) val trace_to_co : trace -> i_action reln let trace_to_co t = bigunion { strict_linearize (addr_trace_to_co a t) | forall a | true } let trace_to_coe t = { (x,y) | forall ((x,y) IN trace_to_co t) | get_thread x <> get_thread y } val trace_to_coi : trace -> i_action reln let trace_to_coi t = { (x,y) | forall ((x,y) IN trace_to_co t) | get_thread x = get_thread y } (* Checks that the given modification order is well-formed and consistent with the coherence order extracted from the trace *) val good_mo : trace -> c_action set -> (location -> location_kind) -> c_action reln -> bool let good_mo t actions lk mo = let t_mo = { (a,b) | forall ((a,b) IN trace_to_co t) | exist l. lk l = Atomic && get_address a = loc_comp l } in let mo_in_intermediate : i_action reln = { (action_to_i_action w1, action_to_i_action w2) | forall ((w1,w2) IN mo) | true } in mo_in_intermediate = t_mo (* Checks that the given sequential consistency order is well-formed and consistent with the trace *) let good_sc t actions sc = let sc_actions = { a | forall (a IN actions) | is_seq_cst a } in let sc_intermediate_actions = image action_to_i_action sc_actions in let sc_intermediate = { (action_to_i_action a, action_to_i_action b) | forall ((a,b) IN sc) | true } in let fr = { (r,w) | forall (r IN sc_intermediate_actions) (w IN sc_intermediate_actions) | exist w'. (w',r) IN trace_to_rf t && (w',w) IN trace_to_co t } in let extended_rf = { (w,r) | forall (r IN sc_intermediate_actions) (w IN sc_intermediate_actions) | exist w'. (w',r) IN trace_to_rf t && (w,w') IN rc (trace_to_co t) sc_intermediate_actions && (forall (w'' IN sc_intermediate_actions). not ((w,w'') IN trace_to_co t && (w'',w') IN trace_to_co t)) } in strict_total_order_over sc_actions sc && (forall ((x,y) IN trace_to_po t). (x,y) IN sc_intermediate) && (forall ((x,y) IN trace_to_co t). (x,y) IN sc_intermediate) && (forall ((x,y) IN fr). (x,y) IN sc_intermediate) && (forall ((x,y) IN extended_rf). (x,y) IN sc_intermediate) (* -------------------- -------------------- *) (* A predicate checking whether the C++ reads from follows happens-before. This is the property that a C++ execution requires, but might not be respected by a Power trace. However, in that case, we can show that the program is racy. *) val rf_in_hb_condition : (c_action set) -> opinfo -> c_action reln -> c_action reln -> bool let rf_in_hb_condition actions o rf mo = let hb = build_hb actions o rf mo in forall ((x,y) IN rf). (is_atomic_load y --> (exist x'. c_is_write x' && same_location x' y && (x',y) IN hb)) && (c_is_load y --> (x,y) IN hb)