(* 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 "typesettingScript.sml"; app load ["lts_memory_modelTheory", "HolDoc", "Net_Hol_reln", "axiomatic_memory_modelTheory"]; *) open HolKernel boolLib Parse bossLib; open axiomatic_memory_modelTheory lts_memory_modelTheory; open HolDoc Net_Hol_reln; val _ = new_theory "typesetting"; val _ = Define `myORDER order = order`; val _ = Define `myIN e e' order = (e,e') IN order`; val _ = Define `myNOTIN e e' order = (e,e') NOTIN order`; (* AXIOMATIC MODEL TYPESETTING *) (* TYPESETTING VERSION ****** *) val _ = Define ` previous_writes E er order = {ew' | ew' IN writes E /\ myIN ew' er 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 (myORDER X.memory_order) UNION previous_writes E er (myORDER (po_iico E))) (myORDER X.memory_order) else (* ew IN reg_accesses E *) ew IN maximal_elements (previous_writes E er (myORDER (po_iico E))) (myORDER (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 (myORDER X.memory_order) UNION previous_writes E er (myORDER (po_iico E)) = {})`; (* the memory order is a partial order on the memory access events *) val ve1_def = Define ` ve1 E X = partial_order (myORDER X.memory_order) (mem_accesses E)`; (* ...and is a linear order when restricted to the memory writes *) (* (mo_non-po_write_write is the otherwise-unforced part of this order)*) val ve2_def = Define ` ve2 E X = linear_order (rrestrict (myORDER X.memory_order) (mem_writes E)) (mem_writes E)`; (* ...and the prefixes of the memory order are all finite. This ensures that *) (* there are no limit points in the memory ordering. *) val ve3_def = Define ` ve3 E X = finite_prefixes (myORDER X.memory_order) (mem_accesses E)`; (* Only a finite number of same-location reads can be unrelated to a write *) val ve4_def = Define ` ve4 E X = !ew :: (mem_writes E). FINITE { er | er IN E.events /\ (loc er = loc ew) /\ myNOTIN er ew X.memory_order /\ myNOTIN ew er X.memory_order }`; (* program order is included in memory order, for a memory read before a memory access (mo_po_read_access)*) val ve5_def = Define ` ve5 E X = !er :: (mem_reads E). !e :: (mem_accesses E). myIN er e (po_iico E) ==> myIN er e X.memory_order`; (* val ve5_def = Define ` ve5 E X = !er :: (mem_reads E). !e :: (mem_accesses E). (er, e) IN po_iico E ==> (er, e) IN X.memory_order`;*) (* program order is included in memory order, for a memory write before a memory write (mo_po_write_write)*) val ve6_def = Define ` ve6 E X = !ew1 ew2 :: (mem_writes E). myIN ew1 ew2 (po_iico E) ==> myIN ew1 ew2 X.memory_order`; (* program order is included in memory order, for a memory write before a memory read, *) (* *if* there is an MFENCE between (mo_po_mfence)*) val ve7_def = Define ` ve7 E X = !ew :: (mem_writes E). !er :: (mem_reads E). !ef :: (mfences E). (myIN ew ef (po_iico E) /\ myIN ef er (po_iico E)) ==> myIN ew er X.memory_order`; (* program order is included in memory order, for any two memory accesses where at least *) (* one is from a LOCK'd instruction (mo_po_access/lock)*) val ve8_def = Define ` ve8 E X = !e1 e2 :: (mem_accesses E). !es :: (E.atomicity). ((e1 IN es \/ e2 IN es) /\ myIN e1 e2 (po_iico E)) ==> myIN e1 e2 X.memory_order`; (* the memory accesses of a LOCK'd instruction occur atomically in memory order (mo_atomicity)*) val ve9_def = Define ` ve9 E X = !es :: (E.atomicity). !e :: (mem_accesses E DIFF es). (!e' :: (es INTER mem_accesses E). myIN e e' X.memory_order) \/ (!e' :: (es INTER mem_accesses E). myIN e' e X.memory_order)`; (* the rfmap only relates reads to writes, of the same location and of the same value *) val ve10_def = Define ` ve10 E X = reads_from_map_candidates E X.rfmap `; (* EXPERIMENT IN USING HOLDOC FOR TRANSITION SYSTEM *) val _ = export_theory ();