(**************************************************************************) (* 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. *) (* *) (**************************************************************************) open HolKernel boolLib bossLib Parse; open fcpTheory; open arm_astTheory; open arm_typesTheory common_typesTheory; open utilTheory; open HolDoc; val _ = new_theory "arm_event_monad"; (* ------------------------------------------------------------------------ *> We define a monad for constructing an event structure version of the semantics. <* ------------------------------------------------------------------------ *) (* val _ = type_abbrev("Astate",``:arm_state -> ('a # arm_state) option``); *) (* val _ = type_abbrev("M",``:arm_state -> ('a # arm_state) option``); *) val _ = type_abbrev("M",``: eiid_state -> ((eiid_state # 'a # (arm_reg event_structure)) set)``); (* operations on event structures *) val _ = Define `event_structure_empty = <| events := {}; intra_causality_data := {}; intra_causality_control := {}; atomicity := {} |>`; val _ = Define `event_structure_lock es = <| events := es.events; intra_causality_data := es.intra_causality_data; intra_causality_control := es.intra_causality_control; atomicity := if es.events = {} then {} else { es.events } |>`; (* OCAML: =|= *) val _ = Define `event_structure_union es1 es2 = <| events := es1.events UNION es2.events; intra_causality_data := es1.intra_causality_data UNION es2.intra_causality_data; intra_causality_control := es1.intra_causality_control UNION es2.intra_causality_control; atomicity := es1.atomicity UNION es2.atomicity |>`; val _ = Define `event_structure_bigunion (ess : (arm_reg event_structure) set) = <| events := BIGUNION {es.events | es IN ess}; intra_causality_data := BIGUNION {es.intra_causality_data | es IN ess}; intra_causality_control := BIGUNION {es.intra_causality_control | es IN ess}; atomicity := BIGUNION {es.atomicity | es IN ess} |> `; (* OCAML: =*= *) val _ = Define `event_structure_seq_union es1 es2 = <| events := es1.events UNION es2.events; intra_causality_data := es1.intra_causality_data UNION es2.intra_causality_data UNION {(e1,e2) | e1 IN (maximal_elements es1.events es1.intra_causality_data) /\ e2 IN (minimal_elements es2.events es2.intra_causality_data)} ; intra_causality_control := es1.intra_causality_control UNION es2.intra_causality_control; atomicity := es1.atomicity UNION es2.atomicity |>`; val _ = Define `event_structure_control_seq_union es1 es2 = <| events := es1.events UNION es2.events; intra_causality_data := es1.intra_causality_data UNION es2.intra_causality_data; intra_causality_control := es1.intra_causality_control UNION es2.intra_causality_control UNION {(e1,e2) | e1 IN (maximal_elements es1.events es1.intra_causality_control) /\ e2 IN (minimal_elements es2.events es2.intra_causality_control)} ; atomicity := es1.atomicity UNION es2.atomicity |>`; val mapT_ev_def = Define ` (mapT_ev: ('a -> 'b) -> 'a M -> 'b M) f s = \eiid_next:eiid_state. let t = s eiid_next in { (eiid_next', f x, es) | (eiid_next',x,es) IN t }`; val choiceT_ev_def = Define ` (choiceT_ev: 'a M -> 'a M -> 'a M) s s' = \eiid_next:eiid_state. s eiid_next UNION s' eiid_next`; (* monad operations *) (* OCAML: unitT *) val constT_ev_def = Define ` (constT_ev: 'a -> 'a M) x = \eiid_next. {(eiid_next,x,event_structure_empty)}`; (* OCAML: discardT *) val discardT_ev_def = Define ` (discardT_ev: 'a M -> unit M) s = \eiid_next. let (t:(eiid_state # 'a # (arm_reg event_structure)) set)= s eiid_next in IMAGE (\ (eiid_next',v,es). (eiid_next',(),es)) t`; val addT_ev_def = Define ` (addT_ev: 'a -> 'b M -> ('a # 'b) M) x s = \eiid_next. let (t:(eiid_state # 'b # (arm_reg event_structure)) set)= s eiid_next in IMAGE (\ (eiid_next',v,es). (eiid_next',(x,v),es)) t`; val lockT_ev_def = Define ` (lockT_ev: 'a M -> 'a M) s = \eiid_next. let (t:(eiid_state # 'a # (arm_reg event_structure)) set)= s eiid_next in IMAGE (\ (eiid_next',v,es). (eiid_next',v,event_structure_lock es)) t`; val failureT_ev_def = Define ` (failureT_ev: 'a M) = \eiid_next. {}`; (* or we lift the result type to options and blow up in this case *) val condT_ev_def = Define ` (condT_ev : bool -> unit M -> unit M) b s = if b then s else constT_ev () `; val bindT_ev_def = Define ` (bindT_ev: 'a M -> ('a -> 'b M) -> 'b M) s f = \eiid_next:eiid_state. let t = s eiid_next in BIGUNION { let t' = f x eiid_next' in { (eiid_next'',x',event_structure_seq_union es es') | (eiid_next'',x',es') IN t' } | (eiid_next',x,es) IN t }`; val control_seqT_ev_def = Define ` (control_seqT_ev: 'a M -> ('a -> 'b M) -> 'b M) s f = \eiid_next:eiid_state. let t = s eiid_next in BIGUNION { let t' = f x eiid_next' in { (eiid_next'',x',event_structure_control_seq_union es es') | (eiid_next'',x',es') IN t' } | (eiid_next',x,es) IN t }`; val seqT_ev_def = Define ` (seqT_ev: 'a M -> 'b M -> 'b M) s s' = bindT_ev s (\x. s')`; val parT_ev_def = Define ` (parT_ev: 'a M -> 'b M -> ('a # 'b) M) s s' = \eiid_next:eiid_state. let t = s eiid_next in BIGUNION { let t' = s' eiid_next' in { (eiid_next'',(x,x'),event_structure_union es es') | (eiid_next'',x',es') IN t' } | (eiid_next',x,es) IN t }`; val parT_unit_ev_def = Define ` (parT_unit_ev: unit M -> unit M -> unit M) s s' = \eiid_next:eiid_state. let t = s eiid_next in BIGUNION { let t' = s' eiid_next' in { (eiid_next'',(),event_structure_union es es') | (eiid_next'',(),es') IN t' } | (eiid_next',(),es) IN t }`; val syncT_ev_def = Define `(syncT_ev ii):unit M = \eiid_next. { (eiid_next', () , <| events := { <| eiid:=eiid'; iiid:=ii; action:= Barrier Sync |> }; intra_causality_data := {}; intra_causality_control := {}; atomicity := {} |> ) | (eiid',eiid_next') IN next_eiid eiid_next} `; val write_location_ev_def = Define `(write_location_ev ii l x):unit M = \eiid_next. { (eiid_next', () , <| events := { <| eiid:=eiid'; iiid:=ii; action:= Access W l x |> }; intra_causality_data := {}; intra_causality_control := {}; atomicity := {} |> ) | (eiid',eiid_next') IN next_eiid eiid_next} `; val read_location_ev_def = Define `(read_location_ev ii l):value M = \eiid_next. { (eiid_next', x , <| events := { <| eiid:=eiid'; iiid:=ii; action:= Access R l x |> }; intra_causality_data := {}; intra_causality_control := {}; atomicity := {} |> ) | x IN UNIV /\ (eiid',eiid_next') IN next_eiid eiid_next} `; (* register reads/writes always succeed. *) val write_reg_ev_def = Define `(write_reg_ev ii r x):unit M = write_location_ev ii (Location_reg ii.proc (Reg32 r)) x`; val read_reg_ev_def = Define `(read_reg_ev ii r): value M = read_location_ev ii (Location_reg ii.proc (Reg32 r))`; val write_psr_ev_def = Define `(write_psr_ev ii r x):unit M = write_location_ev ii (Location_reg ii.proc (RegPSR r)) (encode_psr x)`; val read_psr_ev_def = Define `(read_psr_ev ii r): ARMstatus M = bindT_ev (read_location_ev ii (Location_reg ii.proc (RegPSR r))) (\psrw. constT_ev (decode_psr psrw))`; (* We atomically read the entire PSR, update relevant bits, and write it back, for updating flags. It is also possible to split and write only particular bits, but we don't do that yet *) val write_flags_ev_def = Define `(write_flags_ev ii (bn,bz,bc,bv)): unit M = lockT_ev (bindT_ev (read_psr_ev ii CPSR) (\psr. write_psr_ev ii CPSR (psr with <| N := bn; Z := bz; C:= bc; V:= bv |>)))`; val read_flags_ev_def = Define `(read_flags_ev ii):(bool # bool # bool # bool) M = bindT_ev (read_psr_ev ii CPSR) (\psr. constT_ev (psr.N,psr.Z,psr.C,psr.V))`; (* TODO: always read constant information now *) val OUR_VERSION_def = Define `OUR_VERSION = ARMv7_A`; val OUR_INFO_def = Define `OUR_INFO = <| version := OUR_VERSION; extensions := {} |>`; val OUR_MODE_def = Define `OUR_MODE = usr`; val OUR_INSR_SET_def = Define `OUR_INSTR_SET = InstrSet_ARM`; val OUR_SCTLR_def = Define `OUR_SCTLR = <| TE:= T; AFE:= T; TRE:= T; NMFI:= T; EE:= T; VE:= T; U:= T; FI:= T; HA:= T; RR:= T; V:= T; I:= T; Z:= T; SW:= T; B:= T; C:= T; A:= T; M:= T |>`; val read_version_ev_def = Define `(read_version_ev ii): num M = constT_ev (version_number OUR_VERSION)`; val read_info_ev_def = Define `(read_info_ev ii):ARMinfo M = constT_ev (OUR_INFO)`; val read_mode_ev_def = Define `(read_mode_ev ii):ARMmode M = constT_ev (OUR_MODE)`; val read_instr_set_ev_def = Define `(read_instr_set_ev ii):InstrSet M = constT_ev (OUR_INSTR_SET)`; val read_sctlr_ev_def = Define `(read_sctlr_ev ii):ARMsctlr M = constT_ev (OUR_SCTLR)`; (* TODO: monitors do not work right for now *) val set_exclusive_monitorsT_ev_def = Define` (set_exclusive_monitorsT_ev ii (a:word32,size:num)) : unit M = failureT_ev`; val exclusive_monitors_passT_ev_def = Define` (exclusive_monitors_passT_ev ii (a:word32,size:num)) : bool M = failureT_ev`; (* Only 32 bit aligned accesses are supported, others bomb out *) val _ = Define `aligned32 a = ((a && 3w) = 0w)`; val write_mem8_ev_def = Define `(write_mem8_ev ii a x):unit M = failureT_ev `; val write_mem16_ev_def = Define `(write_mem16_ev ii a (x:word16)):unit M = failureT_ev `; val write_mem32_ev_def = Define `(write_mem32_ev ii a (x:word32)):unit M = if aligned32 a then write_location_ev ii (Location_mem a) x else failureT_ev `; val read_mem8_ev_def = Define `(read_mem8_ev ii a):word8 M = failureT_ev `; val read_mem16_ev_def = Define `(read_mem16_ev ii a):word16 M = failureT_ev `; val read_mem32_ev_def = Define `(read_mem32_ev ii a):word32 M = if aligned32 a then read_location_ev ii (Location_mem a) else failureT_ev `; val dmbT_ev_def = Define `(dmbT_ev ii (d,t)): unit M = syncT_ev ii`; (* export *) val _ = (Define `(constT: 'a -> 'a M) = constT_ev`; Define `(addT: 'a -> 'b M -> ('a # 'b) M) = addT_ev`; Define `(lockT: unit M -> unit M) = lockT_ev`; Define `(failureT: unit M) = failureT_ev`; Define `(discardT: 'a M -> unit M) = discardT_ev`; Define `(condT: bool -> unit M -> unit M) = condT_ev`; Define `(bindT: 'a M -> (('a -> 'b M) -> 'b M)) = bindT_ev`; Define `(seqT: 'a M -> 'b M -> 'b M) = seqT_ev`; Define `(parT: 'a M -> 'b M -> ('a # 'b) M) = parT_ev`; Define `(parT_unit: unit M -> unit M -> unit M) = parT_unit_ev`; Define `(read_info: iiid -> ARMinfo M) = read_info_ev`; Define `(read_version: iiid -> num M) = read_version_ev`; Define `(write_reg: iiid -> ARMreg -> Aimm -> unit M) = write_reg_ev`; Define `(read_reg: iiid -> ARMreg -> Aimm M) = read_reg_ev`; Define `(write_psr: iiid -> ARMpsr -> ARMstatus -> unit M) = write_psr_ev`; Define `(read_psr: iiid -> ARMpsr -> ARMstatus M) = read_psr_ev`; Define `(write_flags: iiid -> bool # bool # bool # bool -> unit M) = write_flags_ev`; Define `(read_flags: iiid -> (bool # bool # bool # bool) M) = read_flags_ev`; Define `(read_mode: iiid -> ARMmode M) = read_mode_ev`; Define `(read_instr_set: iiid -> InstrSet M) = read_instr_set_ev`; Define `(read_sctlr: iiid -> ARMsctlr M) = read_sctlr_ev`; Define `(write_mem8: iiid -> word32 -> word8 -> unit M) = write_mem8_ev`; Define `(read_mem8: iiid -> word32 -> word8 M) = read_mem8_ev`; Define `(write_mem16: iiid -> word32 -> word16 -> unit M) = write_mem16_ev`; Define `(read_mem16: iiid -> word32 -> word16 M) = read_mem16_ev`; Define `(write_mem32: iiid -> word32 -> word32 -> unit M) = write_mem32_ev`; Define `(read_mem32: iiid -> word32 -> Aimm M) = read_mem32_ev`; Define `(dmbT : iiid -> MBReqDomain # MBReqTypes -> unit M) = dmbT_ev`; Define `(set_exclusive_monitorsT : iiid -> (word32 # num) -> unit M) = set_exclusive_monitorsT_ev`; Define `(exclusive_monitors_passT : iiid -> (word32 # num) -> bool M) = exclusive_monitors_passT_ev`); val _ = export_theory ();