(* x86-TSO Semantics: HOL sources *) (* *) (* Scott Owens, Susmit Sarkar, Peter Sewell *) (* *) (* Computer Laboratory, University of Cambridge *) (* *) (* Copyright 2007-2009 *) (* *) (* 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. *) (* use "axiomatic_memory_modelScript.sml"; List.app load ["pred_setTheory", "wordsTheory", "set_relationTheory", "HolDoc"]; *) open HolKernel boolLib Parse bossLib wordsTheory; open set_relationTheory; open HolDoc; val _ = new_theory "axiomatic_memory_model"; val _ = type_abbrev("Ximm" , ``:word32``); val _ = type_abbrev ("proc", ``:num``); val _ = Hol_datatype `iiid = <| proc : proc ; poi : num |>`; val _ = type_abbrev ("address", ``:Ximm``); val _ = type_abbrev ("value", ``:Ximm``); val _ = type_abbrev ("eiid", ``:num``); val _ = type_abbrev ("reln", ``:'a # 'a -> bool``); val _ = Hol_datatype `dirn = R | W`; val _ = Hol_datatype `location = Location_reg of proc => 'reg | Location_mem of address`; val _ = Hol_datatype `barrier = Lfence | Sfence | Mfence`; val _ = Hol_datatype `action = Access of dirn => ('reg location) => value | Barrier of barrier`; val _ = Hol_datatype `event = <| eiid : eiid ; iiid : iiid ; action : ('reg action) |>`; val _ = Hol_datatype `event_structure = <| procs : proc set ; events : ('reg event) set ; intra_causality : ('reg event) reln ; atomicity : ('reg event) set set |>`; val is_mem_access_def = Define ` is_mem_access e = ?d a v. e.action = Access d (Location_mem a) v`; val _ = Define ` writes E = {e | e IN E.events /\ ?l v. e.action = Access W l v}`; val _ = Define ` reads E = {e | e IN E.events /\ ?l v. e.action = Access R l v}`; val _ = Define ` fences E = {e | e IN E.events /\ (?f. e.action = Barrier f)}`; val _ = Define ` mfences E = {e | e IN E.events /\ (e.action = Barrier Mfence)}`; val _ = Define ` mem_writes E = {e | e IN E.events /\ ?a v. e.action = Access W (Location_mem a) v}`; val _ = Define ` mem_reads E = {e | e IN E.events /\ ?a v. e.action = Access R (Location_mem a) v}`; val _ = Define ` reg_writes E = {e | e IN E.events /\ ?p r v. e.action = Access W (Location_reg p r) v}`; val _ = Define ` reg_reads E = {e | e IN E.events /\ ?p r v. e.action = Access R (Location_reg p r) v}`; val _ = Define ` mem_accesses E = {e | e IN E.events /\ (?d a v. e.action = Access d (Location_mem a) v)}`; val _ = Define ` reg_accesses E = {e | e IN E.events /\ ?d p r v. e.action = Access d (Location_reg p r) v}`; val _ = Define ` loc e = case e.action of Access d l v -> SOME l || Barrier f -> NONE`; val _ = Define ` value_of e = case e.action of Access d l v -> SOME v || Barrier f -> NONE`; val _ = Define ` proc e = e.iiid.proc`; 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 po_iico_def = Define ` po_iico E = po_strict E UNION E.intra_causality`; val well_formed_event_structure_def = Define ` well_formed_event_structure E = (* The set of events is at most countable *) countable E.events /\ (* there are only a finite number of processors *) (FINITE E.procs) /\ (* all events are from one of those processors *) (!e :: (E.events). proc e IN E.procs) /\ (* the eiid and iiid of an event (together) identify it uniquely *) (!e1 e2 :: (E.events). (e1.eiid = e2.eiid) /\ (e1.iiid = e2.iiid) ==> (e1 = e2)) /\ (* intra-instruction causality is a partial order over the events *) partial_order (E.intra_causality) E.events /\ (* ...and moreover, is *intra*-instruction *) (!(e1, e2) :: (E.intra_causality). (e1.iiid = e2.iiid)) /\ (* the atomicity data is a partial equivalence relation: the atomic sets of events are disjoint *) per E.events E.atomicity /\ (* atomic sets are *intra* instruction *) (!es :: (E.atomicity). !e1 e2 :: es. (e1.iiid = e2.iiid)) /\ (* accesses to a register on a processor can only be by that processor *) (!e :: (E.events). !p r. (loc e = SOME (Location_reg p r)) ==> (p = proc e)) /\ (* An event never comes after an infinite number of other events in program order *) finite_prefixes (po_iico E) E.events /\ (* The additional properties below hold, for the ISA fragment dealt with in [SSFN+09], and were useful for the metatheory there, but seem less essential than those above. *) (* there is no intra-causality edge *from* a memory write *) (!(e1, e2) :: (E.intra_causality). e1 <> e2 ==> e1 NOTIN mem_writes E) /\ (* if an instruction two events on a location and one is a write, then there must be an intra-causality edge between them. In other words, there cannot be a local race within an instruction *) (!(e1 :: writes E) e2. (e1 <> e2) /\ (e2 IN writes E \/ e2 IN reads E) /\ (e1.iiid = e2.iiid) /\ (loc e1 = loc e2) ==> (e1, e2) IN E.intra_causality \/ (e2, e1) IN E.intra_causality) /\ (* each atomic set includes all the events of its instruction *) (!es :: (E.atomicity). !e1 :: es. !e2 :: (E.events). (e1.iiid = e2.iiid) ==> e2 IN es) /\ (* all locked instructions include at least one memory read *) (!es :: (E.atomicity). ?e :: es. e IN mem_reads E)`; val _ = Hol_datatype ` execution_witness = <| memory_order : ('reg event) reln; rfmap : ('reg event) reln; initial_state : ('reg location -> value option) |>`; val _ = Define ` previous_writes E er order = {ew' | ew' IN writes E /\ (ew', er) IN order /\ (loc ew' = loc er)}`; (* read events that read from writes read the most recently written value from either memory or program order*) val _ = Define ` check_rfmap_written E X = !(ew, er) :: (X.rfmap). if ew IN mem_accesses E then ew IN maximal_elements (previous_writes E er X.memory_order UNION previous_writes E er (po_iico E)) X.memory_order else (* ew IN reg_accesses E *) ew IN maximal_elements (previous_writes E er (po_iico E)) (po_iico E)`; (* other read events read from the initial state, and there is no intervening write (in either memory or program order) *) val _ = Define ` check_rfmap_initial E X = !er :: (reads E DIFF range X.rfmap). (?l. (loc er = SOME l) /\ (value_of er = X.initial_state l)) /\ (previous_writes E er X.memory_order UNION previous_writes E er (po_iico E) = {})`; val reads_from_map_candidates = Define ` reads_from_map_candidates E rfmap = !(ew, er) :: rfmap. (er IN reads E) /\ (ew IN writes E) /\ (loc ew = loc er) /\ (value_of ew = value_of er)`; val _ = Define ` valid_execution E X = partial_order X.memory_order (mem_accesses E) /\ linear_order (rrestrict X.memory_order (mem_writes E)) (mem_writes E) /\ finite_prefixes X.memory_order (mem_accesses E) /\ (!ew :: (mem_writes E). FINITE { er | er IN E.events /\ (loc er = loc ew) /\ (er, ew) NOTIN X.memory_order /\ (ew, er) NOTIN X.memory_order }) /\ (!er :: (mem_reads E). !e :: (mem_accesses E). (er, e) IN po_iico E ==> (er, e) IN X.memory_order) /\ (!ew1 ew2 :: (mem_writes E). (ew1, ew2) IN po_iico E ==> (ew1, ew2) IN X.memory_order) /\ (!ew :: (mem_writes E). !er :: (mem_reads E). !ef :: (mfences E). (ew, ef) IN po_iico E /\ (ef, er) IN po_iico E ==> (ew, er) IN X.memory_order) /\ (!e1 e2 :: (mem_accesses E). !es :: (E.atomicity). (e1 IN es \/ e2 IN es) /\ (e1, e2) IN po_iico E ==> (e1, e2) IN X.memory_order) /\ (!es :: (E.atomicity). !e :: (mem_accesses E DIFF es). (!e' :: (es INTER mem_accesses E). (e, e') IN X.memory_order) \/ (!e' :: (es INTER mem_accesses E). (e', e) IN X.memory_order)) /\ X.rfmap IN reads_from_map_candidates E /\ check_rfmap_written E X /\ check_rfmap_initial E X`; val _ = Define ` linear_valid_execution E X = linear_order X.memory_order (mem_accesses E) /\ finite_prefixes X.memory_order (mem_accesses E) /\ (!er :: (mem_reads E). !e :: (mem_accesses E). (er, e) IN po_iico E ==> (er, e) IN X.memory_order) /\ (!ew1 ew2 :: (mem_writes E). (ew1, ew2) IN po_iico E ==> (ew1, ew2) IN X.memory_order) /\ (!ew :: (mem_writes E). !er :: (mem_reads E). !ef :: (mfences E). (ew, ef) IN po_iico E /\ (ef, er) IN po_iico E ==> (ew, er) IN X.memory_order) /\ (!e1 e2 :: (mem_accesses E). !es :: (E.atomicity). (e1 IN es \/ e2 IN es) /\ (e1, e2) IN po_iico E ==> (e1, e2) IN X.memory_order) /\ (!es :: (E.atomicity). !e :: (mem_accesses E DIFF es). (!e' :: (es INTER mem_accesses E). (e, e') IN X.memory_order) \/ (!e' :: (es INTER mem_accesses E). (e', e) IN X.memory_order)) /\ X.rfmap IN reads_from_map_candidates E /\ check_rfmap_written E X /\ check_rfmap_initial E X`; val max_state_updates_def = Define ` max_state_updates E X l = {value_of ew | ew IN maximal_elements {ew' | ew' IN writes E /\ (loc ew' = SOME l)} (case l of Location_mem a -> X.memory_order || Location_reg p r -> po_iico E)}`; val check_final_state_def = Define ` (check_final_state E X NONE = ~(FINITE E.events)) /\ (check_final_state E X (SOME final_state) = FINITE E.events /\ (!l. if (max_state_updates E X l) = {} then final_state l = X.initial_state l else final_state l IN max_state_updates E X l))`; val _ = export_theory ();