(* ********************************************************************** *) (* ARM/Power Multiprocessor Machine Code Semantics: HOL sources *) (* *) (* *) (* Jade Alglave (2), Anthony Fox (1), Samin Isthiaq (3), *) (* Magnus Myreen (1), Susmit Sarkar (1), Peter Sewell (1), *) (* Francesco Zappa Nardelli (2) *) (* *) (* (1) Computer Laboratory, University of Cambridge *) (* (2) Moscova project, INRIA Paris-Rocquencourt *) (* (3) Microsoft Research Cambridge *) (* *) (* Copyright 2007-2008 *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. Redistributions in binary form must reproduce the above copyright *) (* notice, this list of conditions and the following disclaimer in *) (* the documentation and/or other materials provided with the *) (* distribution. *) (* 3. The names of the authors may not be used to endorse or promote *) (* products derived from this software without specific prior *) (* written permission. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS *) (* OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED *) (* WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE *) (* ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY *) (* DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL *) (* DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE *) (* GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS *) (* INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, *) (* WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING *) (* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS *) (* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) (* *) (* ********************************************************************** *) (* paste this in in interactive mode, as least for HOL-poly: load "wordsTheory"; load "bit_listTheory"; load "listTheory"; load "utilTheory"; *) open HolKernel boolLib bossLib Parse; open wordsTheory bit_listTheory listTheory; open utilTheory common_coretypesTheory common_typesTheory; open HolDoc; val _ = new_theory "ppc_arm_axiomatic_model"; (* **************************************************************************** *) (* basic operations on datatypes *) val loc_def = Define ` loc e = case e.action of Access d l v -> SOME l || _ -> NONE`; val value_of_def = Define ` value_of e = case e.action of Access d l v -> SOME v || _ -> NONE`; val proc_def = Define ` proc e = e.iiid.proc`; val mem_load_def = Define ` mem_load e = case e.action of Access R (Location_mem a) v -> T || _ -> F`; val mem_store_def = Define ` mem_store e = case e.action of Access W (Location_mem a) v -> T || _ -> F`; val mem_access_def = Define ` mem_access e = case e.action of Access d (Location_mem a) v -> T || _ -> F`; val reg_load_def = Define ` reg_load e = case e.action of Access R (Location_reg p r) v -> T || _ -> F`; val reg_store_def = Define ` reg_store e = case e.action of Access W (Location_reg p r) v -> T || _ -> F`; val reg_access_def = Define ` reg_access e = case e.action of Access d (Location_reg p r) v -> T || _ -> F`; val reg_or_mem_location_def = Define ` reg_or_mem_location l = case l of (Location_reg p r) -> T || (Location_mem a) -> T || (Location_res p) -> F || (Location_res_addr p) -> F`; val reg_or_mem_or_resaddr_def = Define ` reg_or_mem_or_resaddr l = case l of (Location_reg p r) -> T || (Location_mem a) -> T || (Location_res p) -> F || (Location_res_addr p) -> T`; val store_def = Define ` store e = case e.action of Access W l v -> T || _ -> F`; val load_def = Define ` load e = case e.action of Access R l v -> T || _ -> F`; val is_barrier_def = Define ` is_barrier e = case e.action of Barrier bar -> T || _ -> F`; val is_sync_def = Define ` is_sync e = case e.action of Barrier Sync -> T || _ -> F`; val procs_def = Define ` procs E = {proc e | e IN E.events}`; val iiids_def = Define ` iiids E = {e.iiid | e IN E.events}`; val writes_def = Define ` writes E = {e | e IN E.events /\ ?l v. e.action = Access W l v}`; val reads_def = Define ` reads E = {e | e IN E.events /\ ?l v. e.action = Access R l v}`; (* **************************************************************************** *) (* program order *) val po_def = Define ` po E = {(e1, e2) | (e1.iiid.proc = e2.iiid.proc) /\ e1.iiid.poi <= e2.iiid.poi /\ e1 IN E.events /\ e2 IN E.events}`; val po_strict_def = Define ` po_strict E = {(e1, e2) | (e1.iiid.proc = e2.iiid.proc) /\ e1.iiid.poi < e2.iiid.poi /\ e1 IN E.events /\ e2 IN E.events}`; val intra_causality_def = Define ` intra_causality E = E.intra_causality_data UNION E.intra_causality_control`; val po_iico_both_def = Define ` po_iico_both E = po_strict E UNION E.intra_causality_data UNION E.intra_causality_control `; val po_iico_data_def = Define ` po_iico_data E = po_strict E UNION E.intra_causality_data `; (* **************************************************************************** *) (* basic structure: E *) val well_formed_event_structure_def = Define ` well_formed_event_structure E = (!e1 e2 :: (E.events). (e1.eiid = e2.eiid) /\ (e1.iiid = e2.iiid) ==> (e1 = e2)) /\ (DOM (intra_causality E)) SUBSET E.events /\ (RANGE (intra_causality E)) SUBSET E.events /\ acyclic (intra_causality E) /\ (!(e1, e2) :: (intra_causality E). (e1.iiid = e2.iiid)) /\ (!(e1 :: writes E) e2. ~(e1 = e2) /\ (e2 IN writes E \/ e2 IN reads E) /\ (e1.iiid = e2.iiid) /\ (loc e1 = loc e2) /\ (?p r. loc e1 = SOME (Location_reg p r)) ==> (e1, e2) IN sTC (intra_causality E)\/ (e2, e1) IN sTC (intra_causality E)) /\ PER E.events E.atomicity /\ (!es :: (E.atomicity). !e1 e2 :: es. (e1.iiid = e2.iiid)) `; (***************************************************************************** *) (* dependency *) (* honest-to-goodness local register dependency, not including dependency across an intervening register write *) val local_register_data_dependency_def = Define ` local_register_data_dependency E p = { (e1,e2) | (e1,e2) IN po_iico_data E /\ (proc e1 = p) /\ (proc e2 = p) /\ (?r v1 v2. (e1.action = Access W (Location_reg p r) v1) /\ (e2.action = Access R (Location_reg p r) v2) /\ (~ (? e3 v3. (e1,e3) IN po_iico_data E /\ (e3,e2) IN po_iico_data E /\ (e3.action = Access W (Location_reg p r) v3))))} `; (* in valid executions we expect v1=v2 *) (* ARM: for load-load, A3-45 bullet 1 para 2 says we don't preserve pure control dependency program order. for load-store, we suspect the ARM does preserve pure control dependency program order, though that's not said explicitly (but A3.45-bullet1-para2 talks explicitly only about load-load, and ppc says something) (we say "pure control dependency" for cases where there's an ARM control dependency but not an ARM address or data dependency) for both load-load and load-store above, we preserve data dependency for load-load and load-store, A3-45 bullet 1 para 1 says we preserve address dependency for store-{load,store}, there can never be any address or control dependency, so we don't have to think about whether we're preserving it. Power: address_or_data_dependency_load_load is the second bullet on 2.05 413 address_or_data_or_control_dependency_load_store is Power 2.05 p414 first para, which is fairly clear that this is preserved in all views. *) val address_or_data_dependency_load_load_def = Define ` address_or_data_dependency_load_load E p = { (e1,e2) | (mem_load e1 /\ mem_load e2 /\ (e1,e2) IN po E /\ (proc e1 = p) /\ (proc e2 = p) /\ (e1,e2) IN (sTC (E.intra_causality_data UNION local_register_data_dependency E p)))}`; val address_or_data_or_control_dependency_load_store_def = Define ` address_or_data_or_control_dependency_load_store E p = { (e1,e2) | (mem_load e1 /\ mem_store e2 /\ (e1,e2) IN po E /\ (proc e1 = p) /\ (proc e2 = p) /\ (e1,e2) IN (sTC (E.intra_causality_data UNION E.intra_causality_control UNION local_register_data_dependency E p)))}`; (* ARM: the following is based on the cookbook, p10, second para and examples. We think this is not necessarily preserved, and the first and second bullets on A3-45 seem consistent with that. At present we don't see any need for pure control dependency in the semantics. *) (* val foo_closure_def = Define foo_closure r1 r2 = sTC (rTC r2 o r1 o rTC r2); -- where rTC is refl tran val control_dependency_arm_def = Define control_dependency_arm E p = { (e1,e2) | (mem_load e1 /\ mem_load e2 /\ (e1,e2) IN po E /\ (proc e1 = p) /\ (proc e2 = p) /\ (e1,e2) IN (foo_closure E.intra_causality_control (local_register_data_dependency E p UNION address_or_data_dependency E p)))}; *) val preserved_program_order_mem_def = Define ` preserved_program_order_mem_loc E p = {(e1, e2) | (e1, e2) IN po_iico_data E /\ (proc e1 = p) /\ (proc e2 = p) /\ (loc e1 = loc e2) /\ mem_access e1 /\ mem_access e2 } `; (* We include all four cases: *) (* (mem_load e1 /\ mem_load e2): if we didn't include this, it would make a nonsense of the coherence order *) (* (mem_load e1 /\ mem_store e2): if we didn't include this, a single-proc load could read from a po-future store *) (* (mem_store e1 /\ mem_store e2): also enforced by preserved coherence order *) (* (mem_store e1 /\ mem_load e2): if we didn't include this, a single-proc load could fail to read from a po-past store (this is superficially stronger than needed, as the e1 store might be long before the load, but any intervening stores to this location will be coherence-order preserved, so that's ok) *) (* It might be arguable that the above should be po_iico_both instead of po_iico_data, but for reasonable RISC-like ISA it would be surprising if it matters *) (* Initially we wrote an analogue of local_register_data_dependency for the store - the case where you store then load from the same location - but it's not a very good analogue, as here other processors writes can be intervening, and if they are, there's no good reason why we should do program-order (or indeed rfmap-) preservation for these. Moreover, while store pairs might be in preserved program order, they must not be in preserved_rfmap, as that explicitly _prevents_ an intervening write by another processor in the view order. We now include all 4 combinations of store accesses to the same location. *) val preserved_program_order_def = Define ` preserved_program_order E p = {(e1, e2) | (e1, e2) IN E.intra_causality_data /\ (proc e1 = p) /\ (proc e2 = p) } UNION {(e1, e2) | (e1, e2) IN E.intra_causality_control /\ (proc e1 = p) /\ (proc e2 = p) } UNION address_or_data_dependency_load_load E p UNION address_or_data_or_control_dependency_load_store E p UNION preserved_program_order_mem_loc E p`; val preserved_coherence_order_def = Define ` preserved_coherence_order E p = {(e1, e2) | (e1, e2) IN po_iico_data E /\ (proc e1 = p) /\ (proc e2 = p) /\ (loc e1 = loc e2) /\ (mem_store e1 /\ mem_store e2 )} `; (* Again it might be debatable whether the above should be po_iico_data or po_iico_both, but for reasonable ISA it would be surprising if there was a different *) (* ********************** View Orders ********************** *) val viewed_events_def = Define ` viewed_events E p = {e | e IN E.events /\ ((proc e = p) \/ mem_store e)}`; (* It seems to suffice to follow our x86-style no-visibility-of-others-reads, and to take linear, not partial view orders. Note that here we take strict linear orders, whereas for x86 they were reflexive - this is just a minor stylistic improvement. Also, in x86 we constrained vo p for all p, not just p::(procs E) *) val view_orders_well_formed_def = Define ` view_orders_well_formed E vo = !p :: (procs E). strict_linear_order (vo p) (viewed_events E p)`; (* write serializations - just as in x86 (except alpha: get_l_stores -> get_mem_l_stores *) val get_mem_l_stores_def = Define ` get_mem_l_stores E l = {e | e IN E.events /\ mem_store e /\ (loc e = SOME l)}`; val write_serialization_candidates_def = Define ` write_serialization_candidates E cand = (!(e1, e2) :: cand. ?l. e1 IN (get_mem_l_stores E l) /\ e2 IN (get_mem_l_stores E l)) /\ (!l. strict_linear_order (RRESTRICT cand (get_mem_l_stores E l)) (get_mem_l_stores E l))`; val state_updates_def = Define ` state_updates E vo e = {ew | ew IN (writes E) /\ (ew,e) IN vo (proc e) /\ (loc ew = loc e) }`; val read_most_recent_value_def = Define ` read_most_recent_value E initial_state vo = ! e :: (E.events). ! l v. ((e.action = Access R l v) /\ reg_or_mem_or_resaddr l) ==> (if (state_updates E vo e) = {} then (SOME v = initial_state l) else ((SOME v) IN { value_of ew | ew IN maximal_elements (state_updates E vo e) (vo (proc e)) }))`; (* ********************** sync/dmb ********************** *) (* We have to make the sync event visible in its own processors' view order (at least, if we don't want to carry the instructions around). But we choose not to make it visible in other processors view orders. And (just for hygiene) we constrain ea and eb to be before and after es, where that is meaningful *) (* Note that for this we still don't seem to need other processors read events (though the 2.05 language looks as if it does have them, talking about "all applicable storage accesses), as they never occur on the left in the fixpoint *) (* Following 2.05 closely, the er below doesn't have to be in group_B *) (* Note that we have a single global group_A and group_B for each sync event, not a processor-indexed family thereof *) val _ = Define ` FIX f x = BIGINTER { X | (f X UNION x) SUBSET X } ` ; val _ = Define ` check_sync_power_2_05 E vos = ! es :: (E.events). (es.action=Barrier Sync) ==> let group_A = { e | ((e,es) IN po E \/ (e,es) IN vos (proc es)) /\ mem_access e } in let group_B_base = { e | (es,e) IN po E /\ mem_access e } in let group_B_ind B0 = { e | mem_access e /\ (~(proc e = proc es)) /\ ? er. mem_load er /\ (er,e) IN vos (proc er) /\ (proc er = proc e) /\ ? ew. mem_store ew /\ ew IN B0 /\ (ew,er) IN vos (proc er) /\ (loc er = loc ew) /\ ( ~ (? ew'. (ew,ew') IN vos (proc er) /\ (ew',er) IN vos (proc er) /\ (loc ew' = loc er) /\ mem_store ew')) } in let group_B = FIX group_B_ind group_B_base in !p :: (procs E). ! ea :: group_A. ! eb :: group_B. (ea IN viewed_events E p /\ eb IN viewed_events E p) ==> if (p=es.iiid.proc) then ((ea,es) IN vos p /\ (es,eb) IN vos p) else (ea,eb) IN vos p `; val _ = Define ` check_dmb_arm E vos = ! es :: (E.events). (es.action=Barrier Sync) ==> let group_A_base = { e | ((e,es) IN vos (proc es)) /\ mem_access e } in let group_A_ind A0 = { er | mem_load er /\ ? e::A0. (er,e) IN vos (proc e) } in let group_B_base = { e | (es,e) IN po E /\ mem_access e } in let group_B_ind B0 = { e | mem_access e /\ ? ew. mem_store ew /\ ew IN B0 /\ (ew,e) IN vos (proc e) } in let group_A = FIX group_A_ind group_A_base in let group_B = FIX group_B_ind group_B_base in !p :: (procs E). ! ea :: group_A. ! eb :: group_B. (ea IN viewed_events E p /\ eb IN viewed_events E p) ==> if (p=es.iiid.proc) then ((ea,es) IN vos p /\ (es,eb) IN vos p) else (ea,eb) IN vos p `; (* (above we interpret "can only occur" as vos (proc e) in the group_B_ind defn) *) (* ************* reservations ***************** *) (* Scheme: there are locations Location_res (notionally carrying just one bit, but embedded in a word32) and Location_res_addr (carrying the reserved address). The latter behaves just like a register, though we know that in the instruction semantics it's only read when the former is 1. Location_res can be read and written by instructions, but the value read is computed by location_res_value below, which walks over the relevant view order to find the most recent reservation (if any) and checks that there have been no intervening memory writes to the same reservation granule. *) (* ARM granules are identified by bits 31 .. n, where n is between 3 and 11 *) (* Power2.05 granules are at least 2^4 bytes. *) val same_granule_def = Define `same_granule E a a' = let f x = x // (1w << E.granule_size_exponent) in (f a = f a') `; (* (31 -- n) a *) val location_res_value_def = Define ` location_res_value E vo e = let prior_reservations = { ew | ew IN (writes E) /\ (ew,e) IN vo (proc e) /\ (loc ew = SOME (Location_res_addr (proc e))) } in if (prior_reservations = {}) then 0w else let reservation = maximal_elements prior_reservations (vo (proc e)) in let intervening_writes = { ew | ? ew'::reservation. ? a'. ? a v. (ew.action = Access W (Location_mem a) v) /\ (ew',ew) IN vo (proc e) /\ (ew,e) IN vo (proc e) /\ (value_of ew' = SOME a') /\ same_granule E a a' } in if intervening_writes = {} then 0w else 1w `; val read_location_res_value_def = Define ` read_location_res_value E initial_state vo = ! e :: (E.events). ! p v. (e.action = Access R (Location_res p) v) ==> (v = location_res_value E vo e) `; val check_atomicity_def = Define ` check_atomicity E vo = !p :: (procs E). !es :: (E.atomicity). !e1 e2:: es. (e1, e2) IN (vo p) ==> !e. (e1, e) IN (vo p) /\ (e, e2) IN (vo p) ==> e IN es`; (* finally, valid execution *) val valid_execution_def = Define ` valid_execution E X = view_orders_well_formed E X.vo /\ read_most_recent_value E X.initial_state X.vo /\ X.write_serialization IN write_serialization_candidates E /\ (! p :: (procs E). preserved_coherence_order E p SUBSET X.write_serialization /\ X.write_serialization SUBSET X.vo p /\ preserved_program_order E p SUBSET X.vo p /\ (*:no intervening writes in local register data dependency:*) local_register_data_dependency E p SUBSET X.vo p /\ (! (e1,e2) :: (local_register_data_dependency E p) . ~ (? e3. (e1,e3) IN X.vo p /\ (e3,e2) IN X.vo p /\ (loc e3 = loc e1) /\ store e3))) /\ (*:no intervening writes before a reg read from initial state:*) (! e :: (E.events). (reg_load e /\ (~ (? e0. (e0,e) IN po_iico_both E /\ reg_store e0 /\ (loc e0 = loc e)))) ==> (~ (? e0. (e0,e) IN X.vo (proc e) /\ reg_store e0 /\ (loc e0 = loc e)))) /\ (*:no intervening writes after a reg write to the final state:*) (! e :: (E.events). (reg_store e /\ (~ (? e1. (e,e1) IN po_iico_both E /\ reg_store e1 /\ (loc e1 = loc e)))) ==> (~ (? e1. (e,e1) IN X.vo (proc e) /\ reg_store e1 /\ (loc e1 = loc e)))) /\ (case E.arch of Power205 -> check_sync_power_2_05 E X.vo || ARMv7 -> check_dmb_arm E X.vo) /\ read_location_res_value E X.initial_state X.vo /\ check_atomicity E X.vo `; val _ = export_theory ();