(** ARM/Power Multiprocessor Machine Code Semantics: Coq 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. *) Require Import ZArith. Require Import Ensembles. Require Import util. Ltac decide_equality := decide equality; auto with equality arith. (** This note gives a precise definition of a relaxed memory model for the Power and ARM architectures. The Power definition is based on the Architecture documentation (2.05) and several developer's documents. The ARM definition is based upon the ARM Architecture Reference Manual (particularly Section A3.8) and the Litmus Test Cookbook. *) (** The model is formalised in the Coq proof assistant. *) (** We consider only the basic user-code scenario: coherent write-back memory and no misaligned accesses, no self-modifying code, no page-table changes, etc. *) (** * Basic types *) (** ** Words *) (** We abstract from word-size and alignment issues for now, modelling both memory addresses and the values that may be stored in them by natural numbers. *) Definition Word := nat. (** *** Addresses *) Definition Address := Word. (** *** Values *) Definition Value := Word. (** ** Registers *) (** Processor registers are modelled by the following type. *) Inductive Preg: Set := | R0 : Preg | R1 : Preg | R2 : Preg | R3 : Preg. Lemma eqPreg_dec: forall (x y: Preg), {x=y} + {x<>y}. Proof. decide_equality. Defined. Hint Resolve eqPreg_dec : equality. (** ** Processors *) (** Processors are indexed by natural numbers. *) Definition Proc := nat. Lemma eqProc_dec : forall (x y: Proc), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqProc_dec : equality. (** The model is expressed in terms of allowable orderings on events: individual reads and writes to memory and to registers, and memory barrier events. Each instance of an instruction in a program execution may give rise to multiple events, as described by the instruction semantics. In this document we abstract from the details of instructions, but we record in each event the instruction instance id (an iiid) that gave rise to it, so that we can refer to the program order over the instruction instances. An instruction instance id specifies the processor on which the instruction was executed together with the index of the program-order point at which it was executed (represented by a natural number).*) (** ** Index in program order *) Definition program_order_index := nat. Lemma eqPoi_dec : forall (x y: program_order_index), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqPoi_dec : equality. (** ** Iiid: instruction identifier *) Record Iiid : Set := mkiiid { proc : Proc; poi: program_order_index }. Lemma eqIiid_dec : forall (x y: Iiid), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqIiid_dec : equality. (** Each event has an event instance id (eiid), the associated instruction instance id (iiid), and an action. An action is either an access, with a direction (read or write), a location (a register location specified by a processor and a register, or a memory location specified by an address), and a value. *) (** ** Eiid: unique event identifier *) Definition Eiid := nat. Lemma eqEiid_dec : forall (x y: Eiid), {x=y} + {x<>y}. Proof. decide_equality. Defined. Hint Resolve eqEiid_dec : equality. (** ** Directions i.e. read or write*) Inductive Dirn : Set := | R : Dirn | W : Dirn. Lemma eqDirn_dec : forall (x y: Dirn), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqDirn_dec. (** ** Location: - a register and its associated processor, or - a memory location specified by an address *) Inductive Location : Set := | Location_reg : Proc -> Preg -> Location | Location_mem : Address -> Location | Location_res : Proc -> Location | Location_res_addr : Proc -> Location. Lemma eqLoc_dec : forall (x y: Location), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqLoc_dec : equality. (** ** Action: - an access specified by a polarity, a location and a value, or - a barrier *) (** *** Barriers are synchronization instructions (DMB in ARM, sync in Power, both written as Sync here)*) Inductive Synchronization : Set := | Sync : Synchronization. Lemma eqSync_dec : forall (x y: Synchronization), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqSync_dec : equality. Inductive Action : Set := | Access : Dirn -> Location -> Value -> Action | Barrier : Synchronization -> Action. Lemma eqAction_dec : forall (x y: Action), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqAction_dec : equality. (** ** Event: - an unique identifier; - the associated index in program order and the proc; - the associated action *) Record Event : Set := mkev { eiid : Eiid; iiid : Iiid; action : Action}. Lemma eqEv_dec : forall (x y: Event), {x=y} + {x <> y}. Proof. decide_equality. Defined. Hint Resolve eqEv_dec : equality. (** Finally, an event structure collects the events of a candidate execution. *) (** ** Event structure: - a set of events; - the causality and atomicity relations between events *) (** Here: - events is the set of events, - causality, the intra-instruction causality relation, is an acyclic relation (that does not relate events of different processors or of different instruction instances): we distinguish between dependency on data (_data) and information flow (_control), which are determined by the instructions' semantics. *) (*note that we have to work in Type if we use Ensemble.*) Inductive Architecture : Set := | Power205: Architecture | ARMv7: Architecture. Record Event_struct : Type := mkes { events : set Event; intra_causality_data : set (Event*Event); intra_causality_control : set (Event*Event); atomicity: set (set Event); arch : Architecture ; granule_size_exponent : nat }. Definition Empty_es := mkes (Empty_set _) (Empty_set _) (Empty_set _). (** ** State constraints *) Definition State_constraint := Location -> option Value. (** ** View Orders *) Definition View_orders : Type := Proc -> set (Event*Event). (** ** Execution Witness *) Record Execution_witness : Type := mkew { initial_state : State_constraint; vo : View_orders; write_serialization : set (Event*Event) }. (** * Basic operations on data types *) (** ** Location of an event *) Definition loc (e:Event) : option Location := match e.(action) with | Access _ l _ => Some l | _ => None end. Definition reg_or_mem_location (l:Location) : Prop := match l with | Location_reg _ _ => True | Location_mem _ => True | _ => False end. Definition reg_or_mem_or_resaddr (l:Location) : Prop := match l with | Location_reg _ _ => True | Location_mem _ => True | Location_res_addr _ => True | _ => False end. (** ** Value of an event *) Definition value_of (e:Event) : option Value := match e.(action) with | Access _ _ v => Some v | _ => None end. (** ** Processors *) (** *** Of an event *) Definition proc_of (e:Event) : Proc := e.(iiid).(proc). (** *** Of an event structure *) Definition procs (es: Event_struct) : set Proc := fun p => exists e, In Event es.(events) e /\ p = proc_of e. (** ** Particular events of an event structure *) (** *** Loads *) Definition mem_load (e:Event) : Prop := exists a, exists v, e.(action) = Access R (Location_mem a) v. Definition mem_loads (es:Event_struct) : set Event := fun e => (In _ es.(events) e) -> mem_load e. Definition reg_load (e:Event) : Prop := exists p, exists r, exists v, e.(action) = Access R (Location_reg p r) v. Definition load (e:Event) : Prop := exists l, exists v, e.(action) = Access R l v. Definition reads (es:Event_struct) : set Event := fun e => (In Event es.(events) e) /\ (exists l, exists v, e.(action) = Access R l v). (** *** Stores *) Definition mem_store (e:Event) : Prop := exists a, exists v, e.(action) = Access W (Location_mem a) v. Definition mem_stores (es:Event_struct) : set Event := fun e => (In _ es.(events) e) -> mem_store e. Definition reg_store (e:Event) : Prop := exists p, exists r, exists v, e.(action) = Access W (Location_reg p r) v. Definition store (e:Event) : Prop := exists l, exists v, e.(action) = Access W l v. Definition writes (es:Event_struct) : set Event := fun e => (In Event es.(events) e) /\ (exists l, exists v, e.(action) = Access W l v). (** *** Any access *) Definition mem_access (e:Event) : Prop := mem_store e \/ mem_load e. Definition reg_access (e:Event) : Prop := reg_store e \/ reg_load e. Definition reg_events (es:Event_struct) : set Event := fun e => (In Event es.(events) e) /\ (reg_access e). (** *** Barriers *) Definition is_barrier (e:Event) : Prop := exists b, e.(action) = Barrier b. Definition barriers (es:Event_struct) : set Event := fun e => (In _ es.(events) e) -> is_barrier e. (** **** Sync *) Definition is_sync (e:Event) : Prop := e.(action) = Barrier Sync. Definition syncs (es:Event_struct) : set Event := fun e => (In _ es.(events) e) -> is_sync e. (** * Program order *) (** We define program order as a relation over two events e1 and e2, wrt to an event structure es; two events are in program order if: - both e1 and e2 are in the events of es; - both events have same processor; - the program order index of e1 is less than the program order index of e2.*) Definition po (es: Event_struct) : set (Event*Event) := fun c => match c with (e1,e2) => (* both events have same processor *) (e1.(iiid).(proc) = e2.(iiid).(proc)) /\ (* the program order index of e1 is less than the program order index of e2 *) (le e1.(iiid).(poi) e2.(iiid).(poi)) /\ (* both e1 and e2 are in the events of e *) (In Event es.(events) e1) /\ (In Event es.(events) e2) end. Definition po_strict (es: Event_struct) : set (Event*Event) := fun c => match c with (e1,e2) => (* both events have same processor *) (e1.(iiid).(proc) = e2.(iiid).(proc)) /\ (* the program order index of e1 is strictly less than the program order index of e2 *) (lt e1.(iiid).(poi) e2.(iiid).(poi)) /\ (* both e1 and e2 are in the events of e *) (In Event es.(events) e1) /\ (In Event es.(events) e2) end. (** We build here the determined final state, wrt: - an event structure es; - a constraint on initial state; - view orders; - a total order on stores to the same location. The final state will be the union of: - the initial state; - the last write to each register of any processor p, in p view order, that is: an access that is a write, such that there is no other write to the same location occuring afterwards in p view order, - the last write to each memory location, that is: a write that is in the maximal elements of the total order on stores. *) Definition po_iico_data (es:Event_struct) : set (Event*Event) := Union _ (po_strict es) (es.(intra_causality_data)). Definition intra_causality (es:Event_struct) := Union _ es.(intra_causality_control) es.(intra_causality_data). Definition po_iico_both (es:Event_struct) : set (Event*Event) := Union _ (po_strict es) (intra_causality es). (** * Well-formedness of an event structure *) Definition well_formed_event_structure (E:Event_struct) : Prop := (forall e1 e2, In _ E.(events) e1 -> In _ E.(events) e2 -> (e1.(eiid) = e2.(eiid)) /\ (e1.(iiid) = e2.(iiid)) -> (e1 = e2)) /\ Included _ (domain (intra_causality E)) E.(events) /\ Included _ (range (intra_causality E)) E.(events) /\ acyclic (intra_causality E) /\ (forall e1 e2, In _ (intra_causality E) (e1,e2) -> (e1.(iiid) = e2.(iiid))) /\ (forall e1 e2, In _ (writes E) e1 -> ~(e1 = e2) /\ (In _ (writes E) e2 \/ In _ (reads E) e2) /\ (e1.(iiid) = e2.(iiid)) /\ (loc e1 = loc e2) /\ (exists p, exists r, loc e1 = Some (Location_reg p r)) -> In _ (sTC (intra_causality E)) (e1,e2) \/ In _ (sTC (intra_causality E)) (e2,e1)). (** * Preservation of program order *) (** ** Honest-to-goodness local register dependency, not including dependency across an intervening register write *) Definition local_register_data_dependency (E:Event_struct) (p:Proc) : set (Event*Event) := fun c => match c with (e1,e2) => In _ (po_iico_both E) (e1,e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) /\ (exists r, exists v1, exists v2, (e1.(action) = Access W (Location_reg p r) v1) /\ (e2.(action) = Access R (Location_reg p r) v2) /\ (~ (exists e3, exists v3, In _ (po_iico_both E) (e1,e3) /\ In _ (po_iico_both E) (e3,e2) /\ (e3.(action) = Access W (Location_reg p r) v3)))) end. (** ** Load-load dependency *) Definition address_or_data_dependency_load_load (E:Event_struct) (p:Proc) : set (Event*Event) := fun c => match c with (e1,e2) => (mem_load e1 /\ mem_load e2 /\ In _ (po_strict E) (e1,e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) /\ In _ (sTC (Union _ E.(intra_causality_data) (local_register_data_dependency E p))) (e1,e2) ) end. (** ** Load-store dependency *) Definition address_or_data_or_control_dependency_load_store (E:Event_struct) (p:Proc) : set (Event*Event) := fun c => match c with (e1,e2) => (mem_load e1 /\ mem_store e2 /\ In _ (po_strict E) (e1,e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) /\ In _ (sTC (Union _ (intra_causality E) (local_register_data_dependency E p))) (e1,e2) ) end. (** ** Memory honest to goodness *) Definition preserved_program_order_mem_loc (E:Event_struct) (p:Proc) : set (Event*Event) := fun c => match c with (e1,e2) => In _ (po_iico_data E) (e1,e2) /\ (loc e1 = loc e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) /\ ( (mem_load e1 /\ mem_load e2) \/ (mem_load e1 /\ mem_store e2) \/ (mem_store e1 /\ mem_store e2) \/ (mem_store e1 /\ mem_load e2) ) end. (** Finally, for ARM or Power, the preserved program order *) Definition preserved_program_order (E:Event_struct) (p:Proc) : set (Event*Event) := (* dependencies enforced by iico *) let causality_on_p := fun c => match c with (e1,e2) => In _ (intra_causality E) (e1,e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) end in (* dependency chains through this processor but not via memory *) let load_foo_dep_on_p := Union _ (address_or_data_dependency_load_load E p) (address_or_data_or_control_dependency_load_store E p) in Union _ (Union _ causality_on_p load_foo_dep_on_p) (preserved_program_order_mem_loc E p). (** Preserved coherence order and rfmaps as well *) Definition preserved_coherence_order (E:Event_struct) (p:Proc) : set (Event*Event) := fun c => match c with (e1,e2) => In _ (po_iico_data E) (e1,e2) /\ (loc e1 = loc e2) /\ (proc_of e1 = p) /\ (proc_of e2 = p) /\ (mem_store e1 /\ mem_store e2 ) end. Definition preserved_rfmap (E:Event_struct) (p:Proc) : set (Event*Event) := local_register_data_dependency E p. (** * View Orders *) (** ** Viewed events, per processor *) Definition viewed_events (E:Event_struct) (p:Proc) : set Event := fun e => In _ E.(events) e /\ ((proc_of e = p) \/ mem_store e). (** ** Well-formedness of view orders *) Definition view_orders_well_formed (E:Event_struct) (vo:View_orders) : Prop := forall p, (In _ (procs E) p) -> linear_strict_order (vo p) (viewed_events E p). (** ** Write serializations *) Definition get_mem_l_stores (E:Event_struct) (l:Location) : set Event := fun e => In _ E.(events) e /\ mem_store e /\ (loc e = Some l). Definition write_serialization_candidates (E:Event_struct) (cand:set (Event*Event)) := (forall e1 e2, In _ cand (e1,e2) -> exists l, In _ (get_mem_l_stores E l) e1 /\ In _ (get_mem_l_stores E l) e2) /\ (forall l, linear_strict_order (rrestrict cand (get_mem_l_stores E l)) (get_mem_l_stores E l)). Definition state_updates (E:Event_struct) (vo:View_orders) (e:Event) : set Event := fun ew => In _ (writes E) ew /\ In _ (vo (proc_of e)) (ew,e) /\ (loc ew = loc e). (** ** Building the final state *) Definition check_final (E:Event_struct) (vo:View_orders ) (initial_state final_state:State_constraint) (write_serialization:set (Event*Event)) := forall e, forall l, loc e = Some l -> (Same_set _ (state_updates E vo e) (Empty_set _)) -> (final_state l = initial_state l) \/ (~(Same_set _ (state_updates E vo e) (Empty_set _)) -> (exists ew, loc ew = Some l /\ final_state l = value_of ew /\ In _ (state_updates E vo e) ew)). Definition read_most_recent_value (E:Event_struct) (initial_state:State_constraint) (vo:View_orders) : Prop := forall e l v, In _ E.(events) e -> (e.(action) = Access R l v /\ reg_or_mem_or_resaddr l) -> ((Same_set _ (state_updates E vo e) (Empty_set _)) /\ (initial_state l = Some v)) \/ (~(Same_set _ (state_updates E vo e)) (Empty_set _)) /\ exists ew, loc ew = Some l /\ In _ (state_updates E vo e) ew. (** * Barriers *) Definition power_sync_GrpA (E:Event_struct) (vos:View_orders) (es e:Event) : Prop := In _ E.(events) es -> In _ E.(events) e -> (es.(action)=Barrier Sync) -> (In _ (po E) (e,es)) \/ (In _ (vos (proc_of es)) (e,es)) /\ mem_access e. Inductive power_sync_GrpB (E:Event_struct) (vos:View_orders) (es e:Event) : Prop := | power_sync_base : In _ E.(events) es -> In _ E.(events) e -> (es.(action)=Barrier Sync) -> In _ (po E) (es,e) /\ mem_access e -> (power_sync_GrpB E vos es e) | power_sync_ind : mem_access e /\ ~(proc_of e = proc_of es) -> forall er, mem_load er /\ In _ (vos (proc_of er)) (er,e) /\ (proc_of er = proc_of e) -> forall ew, mem_store ew /\ (power_sync_GrpB E vos es ew) /\ In _ (vos (proc_of er)) (ew,er) /\ (loc er = loc ew) -> ~ (exists ew', In _ (vos (proc_of er)) (ew,ew') /\ In _ (vos (proc_of er)) (ew',er) /\ (loc ew' = loc er) /\ mem_store ew') -> (power_sync_GrpB E vos es e). Definition check_sync_power_2_05 (E:Event_struct) (vos:View_orders) : Prop := forall p ea es eb, (In _ (procs E) p) -> (In _ (viewed_events E p) ea) -> (In _ (viewed_events E p) eb) -> (power_sync_GrpA E vos es ea) -> (power_sync_GrpB E vos es eb) -> if (eqProc_dec p (proc_of es)) then (In _ (vos p) (ea,es) /\ In _ (vos p) (es,eb)) else In _ (vos p) (ea,eb). Inductive BarrierGroupA (E:Event_struct) (vos:View_orders) (es:Event) (a:Event) : Prop := | GrpA_base : (In _ E.(events) es) -> (is_barrier es) -> (In _ (vos (proc_of es)) (a,es)) -> (mem_access a) -> (BarrierGroupA E vos es a) | GrpA_ind : forall (e:Event), (BarrierGroupA E vos es e) -> (In _ (vos (proc_of e)) (a,e)) -> (mem_load a) -> (BarrierGroupA E vos es a). Inductive BarrierGroupB (E:Event_struct) (vos:View_orders) (es:Event) (b:Event) : Prop := | GrpB_base : (In _ E.(events) es) -> (is_barrier es) -> (In _ (po_iico_both E) (b,es)) -> (mem_access b) -> (BarrierGroupB E vos es b) | GrpB_ind : forall (ew:Event), (BarrierGroupB E vos es ew) -> (mem_store ew) -> (In _ (vos (proc_of b)) (ew,b)) -> (mem_access b) -> (BarrierGroupB E vos es b). Definition check_dmb_arm (E:Event_struct) (vos:View_orders) : Prop := forall (p:Proc) (a es b:Event), (In _ (procs E) p) -> (In _ (viewed_events E p) a) -> (In _ (viewed_events E p) b) -> (BarrierGroupA E vos es a) -> (BarrierGroupB E vos es b) -> if (eqProc_dec p (proc_of es)) then (In _ (vos p) (a,es) /\ In _ (vos p) (es,b)) else In _ (vos p) (a,b). (** ** Reservations stuff *) Definition Granule := nat. Definition same_granule (E:Event_struct) (a a':Granule) : Prop := True. Definition prior_reservations (E:Event_struct) (vo:View_orders) (e:Event) : set Event := fun ew => In _ (writes E) ew /\ In _ (vo (proc_of e)) (ew,e) /\ (loc ew = Some (Location_res_addr (proc_of e))). Definition reservation (E:Event_struct) (vo:View_orders) (e:Event) := maximal_elements (prior_reservations E vo e) (vo (proc_of e)). Definition intervening_writes (E:Event_struct) (vo:View_orders) (e:Event) := fun ew => exists ew', In _ (reservation E vo e) ew' -> exists a', exists a, exists v, (ew.(action) = Access W (Location_mem a) v) /\ In _ (vo (proc_of e)) (ew',ew) /\ In _ (vo (proc_of e)) (ew,e) /\ (value_of ew' = Some a') /\ same_granule E a a'. Definition location_res_value (E:Event_struct) (vo:View_orders) (e:Event) (v:Value) : Prop := ((Same_set _ (Empty_set _ ) (prior_reservations E vo e)) /\ v=0) \/ (~(Same_set _ (Empty_set _ ) (prior_reservations E vo e)) /\ (Same_set _ (Empty_set _ ) (intervening_writes E vo e)) /\ v=0) \/ (~(Same_set _ (Empty_set _ ) (prior_reservations E vo e)) /\ ~(Same_set _ (Empty_set _ ) (intervening_writes E vo e)) /\ v=1). Definition read_location_res_value (E:Event_struct) (initial_state:State_constraint) (vo:View_orders) := forall e, In _ E.(events) e -> forall p v, e.(action) = Access R (Location_res p) v -> location_res_value E vo e v. Definition check_atomicity (E:Event_struct) (vo : View_orders) := forall p, In _ (procs E) p -> forall es, In _ E.(atomicity) es -> forall e1 e2, In _ es e1 -> In _ es e2 -> In _ (vo p) (e1,e2) -> forall e, In _ (vo p) (e1,e) /\ In _ (vo p) (e,e2) -> In _ es e. (** ** Finally, definition of a valid execution *) Definition valid_execution (E:Event_struct) (X:Execution_witness) : Prop := view_orders_well_formed E X.(vo) /\ read_most_recent_value E X.(initial_state) X.(vo) /\ In _ (write_serialization_candidates E) X.(write_serialization) /\ (forall p, In _ (procs E) p -> Included _ (preserved_coherence_order E p) (X.(write_serialization))) /\ (forall p, In _ (procs E) p -> Included _ X.(write_serialization) (X.(vo) p)) /\ (forall p, In _ (procs E) p -> Included _ (preserved_program_order E p) (X.(vo) p)) /\ (forall p, In _ (procs E) p -> Included _ (preserved_rfmap E p) (X.(vo) p)) /\ (forall p, In _ (procs E) p -> forall e1 e2, In _ (preserved_rfmap E p) (e1,e2) -> ~ (exists e3, In _ (X.(vo) p) (e1,e3) /\ In _ (X.(vo) p) (e3,e2) /\ (loc e3 = loc e1) /\ store e3)) /\ (forall e, In _ E.(events) e -> (reg_load e /\ (~ (exists e0, In _ (po_iico_both E) (e0,e) /\ reg_store e0 /\ (loc e0 = loc e)))) -> (~ (exists e0, In _ (X.(vo) (proc_of e)) (e0,e) /\ reg_store e0 /\ (loc e0 = loc e)))) /\ (forall e, In _ E.(events) e -> (reg_store e /\ (~ (exists e1, In _ (po_iico_both E) (e,e1) /\ reg_store e1 /\ (loc e1 = loc e)))) -> (~ (exists e1, In _ (X.(vo) (proc_of e)) (e,e1) /\ reg_store e1 /\ (loc e1 = loc e)))) /\ (((E.(arch) = Power205 /\ check_sync_power_2_05 E X.(vo)) \/ (E.(arch) = ARMv7 /\ check_dmb_arm E X.(vo))) /\ read_location_res_value E X.(initial_state) X.(vo)). (** * Sequential execution *) Definition valid_sequential_execution (E:Event_struct) (initial_state:State_constraint) (so:set (Event*Event)) : Prop := linear_strict_order so E.(events) /\ Included _ (po_iico_both E) so /\ read_most_recent_value E initial_state (fun p => rrestrict so (viewed_events E p)).