(**************************************************************************) (* 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 wordsTheory bit_listTheory listTheory; open ppc_typesTheory common_typesTheory; open utilTheory; open HolDoc; val _ = new_theory "ppc_event_monad"; (* ---------------------------------------------------------------------------------- *> We define a monad for constructing an event structure version of the semantics. <* ---------------------------------------------------------------------------------- *) (* val _ = type_abbrev("M",``:ppc_state -> ('a # ppc_state) option``); *) val _ = type_abbrev("M",``: eiid_state -> ((eiid_state # 'a # (ppc_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 : (ppc_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)}`; (* val discardT_seq_def = Define ` (discardT_seq: 'a M -> unit M) s = \y. case s y of NONE -> NONE || SOME (z,t) -> SOME ((),t)`; *) val addT_ev_def = Define ` (addT_ev: 'a -> 'b M -> ('a # 'b) M) x s = \eiid_next. let (t:(eiid_state # 'b # (ppc_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 # (ppc_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 seqT_ev_def = Define ` (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_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 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 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} `; 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} `; (* 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_status_ev_def = Define `(write_status_ev ii f x):unit M = case x of SOME b -> write_location_ev ii (Location_reg ii.proc (RegBit f)) (if b then 1w else 0w) || NONE -> choiceT_ev (write_location_ev ii (Location_reg ii.proc (RegBit f)) 1w) (write_location_ev ii (Location_reg ii.proc (RegBit f)) 0w)`; val read_status_ev_def = Define `(read_status_ev ii f):bool M = seqT_ev (read_location_ev ii (Location_reg ii.proc (RegBit f))) (\w. constT_ev (w ' 0))`; (* Only 32 bit aligned accesses are supported, others bomb out *) val _ = Define `aligned32 a = ((a && 3w) = 0w)`; val _ = Define `(write_mem8_ev ii a x) = failureT_ev `; val _ = Define `(read_mem8_ev ii a) = 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_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 `; (* register reads/writes reverse bit and reverse address *) val write_reserve_bit_ev_def = Define `(write_reserve_bit_ev (ii:iiid) x):unit M = write_location_ev ii (Location_res ii.proc) (if x then 1w else 0w)`; val read_reserve_bit_ev_def = Define `(read_reserve_bit_ev (ii:iiid)):bool M = seqT_ev (read_location_ev ii (Location_res ii.proc)) (\w. constT_ev (w ' 0))`; (* register reads/writes reverse bit and reverse address *) val write_reserve_address_ev_def = Define `(write_reserve_address_ev (ii:iiid) x):unit M = write_location_ev ii (Location_res_addr ii.proc) x`; val read_reserve_address_ev_def = Define `(read_reserve_address_ev (ii:iiid)):word32 M = read_location_ev ii (Location_res_addr ii.proc)`; (* export *) val _ = Define `(constT: 'a -> 'a M) = constT_ev`; val _ = Define `(addT: 'a -> 'b M -> ('a # 'b) M) = addT_ev`; val _ = Define `(lockT: unit M -> unit M) = lockT_ev`; val _ = Define `(syncT: iiid -> unit M) = syncT_ev`; val _ = Define `(failureT: unit M) = failureT_ev`; val _ = Define `(seqT: 'a M -> (('a -> 'b M) -> 'b M)) = seqT_ev`; val _ = Define `(control_seqT: 'a M -> (('a -> 'b M) -> 'b M)) = control_seqT_ev`; val _ = Define `(parT: 'a M -> 'b M -> ('a # 'b) M) = parT_ev`; val _ = Define `(parT_unit: unit M -> unit M -> unit M) = parT_unit_ev`; val _ = Define `(write_reg: iiid -> ppc_reg32 -> word32 -> unit M) = write_reg_ev`; val _ = Define `(read_reg: iiid -> ppc_reg32 -> word32 M) = read_reg_ev`; val _ = Define `(write_status: iiid -> ppc_bit -> bool option -> unit M) = write_status_ev`; val _ = Define `(read_status: iiid -> ppc_bit -> bool M) = read_status_ev`; val _ = Define `(write_mem8: iiid -> word32 -> word8 -> unit M) = write_mem8_ev`; val _ = Define `(read_mem8: iiid -> word32 -> word8 M) = read_mem8_ev`; val _ = Define `(write_mem32: iiid -> word32 -> word32 -> unit M) = write_mem32_ev`; val _ = Define `(read_mem32: iiid -> word32 -> word32 M) = read_mem32_ev`; val _ = Define `(write_reserve_bit: iiid -> bool -> unit M) = write_reserve_bit_ev`; val _ = Define `(read_reserve_bit: iiid -> bool M) = read_reserve_bit_ev`; val _ = Define `(write_reserve_address: iiid -> word32 -> unit M) = write_reserve_address_ev`; val _ = Define `(read_reserve_address: iiid -> word32 M) = read_reserve_address_ev`; val _ = export_theory ();