Library mcertikos.multicore.semantics.HWStepSemImpl
This file provide the semantics for the Asm instructions. Since we introduce paging mechanisms, the semantics of memory load and store are different from Compcert Asm
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.
Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.
Require Import Machregs.
Require Import DeviceStateDataType.
Require Import liblayers.compat.CompatGenSem.
Require Import FutureTactic.
Section HWSTEPSEM.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Context `{zset_op: ZSet_operation}.
Existing Instance hdseting.
Section WITH_GE.
Variables (ge: genv) (sten: stencil) (M: module).
Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
sten M (mboot ⊕ L64) = ret ge}.
Local Obligation Tactic := intros.
Definition hdsem_instance := @hdsem mem memory_model_ops Hmem Hmwd real_params_ops oracle_ops0
oracle_ops big_ops builtin_idents_norepet_prf ge sten M Hmakege.
Definition hw_step_aux :=
@hardware_step hdseting hdsem_instance pmap current_CPU_ID.
Inductive hw_step_aux_ge : genv → hstate → trace → hstate → Prop :=
| hw_step_aux_ge_intro :
∀ s t s´,
hw_step_aux s t s´ → hw_step_aux_ge ge s t s´.
Inductive hwstep_initial_state (p: AST.program fundef unit):
(hstate (hdset := hdseting)) → Prop :=
| initial_hwstep_state_intro:
∀ (m0: mwd LDATAOps),
Genv.init_mem p = Some m0 →
let ge := Genv.globalenv p in
let rs0 :=
(Pregmap.init Vundef)
# Asm.PC <- (symbol_offset ge p.(prog_main) Int.zero)
# ESP <- Vzero in
hwstep_initial_state p (HState current_CPU_ID (pinit (B := core_set) (Asm.State rs0 m0)) nil).
Definition hwstep_final_state (s : hstate (hdset := hdseting)) (i : int) : Prop :=
False.
Ltac subst_except v :=
repeat match goal with
| [ H: v = _ |- _ ] ⇒ generalize H; clear H
| [ H: _ = v |- _ ] ⇒ generalize H; clear H
end; subst; intros.
Ltac clear_eq v :=
repeat match goal with
| [ H: v = _ |- _ ] ⇒ clear H
| [ H: _ = v |- _ ] ⇒ clear H
end.
Definition hwstep_semantics (p: program) :=
Smallstep.Semantics hw_step_aux_ge (hwstep_initial_state p)
hwstep_final_state (Genv.globalenv p).
Lemma hwstep_semantics_single_events:
∀ p, single_events (hwstep_semantics p).
Proof.
intros p s t s´ Hstep; inversion Hstep.
inversion H.
simpl; omega.
Qed.
Lemma hwstep_semantics_receptive (pl: program):
receptive (hwstep_semantics pl).
Proof.
intros; constructor.
- inversion 1.
inversion H0.
substx; try solve [inversion 1; substx; eauto].
intros.
inversion H8; substx.
∃ s1.
simpl.
unfold hw_step_aux.
simpl in H1.
rewrite <- H1.
eapply hw_step_aux_ge_intro.
unfold hw_step_aux.
rewrite <- H7.
econstructor; eauto.
- eapply hwstep_semantics_single_events.
Qed.
End WITH_GE.
End HWSTEPSEM.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.
Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.
Require Import Machregs.
Require Import DeviceStateDataType.
Require Import liblayers.compat.CompatGenSem.
Require Import FutureTactic.
Section HWSTEPSEM.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{fair: Fairness}.
Context `{zset_op: ZSet_operation}.
Existing Instance hdseting.
Section WITH_GE.
Variables (ge: genv) (sten: stencil) (M: module).
Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
sten M (mboot ⊕ L64) = ret ge}.
Local Obligation Tactic := intros.
Definition hdsem_instance := @hdsem mem memory_model_ops Hmem Hmwd real_params_ops oracle_ops0
oracle_ops big_ops builtin_idents_norepet_prf ge sten M Hmakege.
Definition hw_step_aux :=
@hardware_step hdseting hdsem_instance pmap current_CPU_ID.
Inductive hw_step_aux_ge : genv → hstate → trace → hstate → Prop :=
| hw_step_aux_ge_intro :
∀ s t s´,
hw_step_aux s t s´ → hw_step_aux_ge ge s t s´.
Inductive hwstep_initial_state (p: AST.program fundef unit):
(hstate (hdset := hdseting)) → Prop :=
| initial_hwstep_state_intro:
∀ (m0: mwd LDATAOps),
Genv.init_mem p = Some m0 →
let ge := Genv.globalenv p in
let rs0 :=
(Pregmap.init Vundef)
# Asm.PC <- (symbol_offset ge p.(prog_main) Int.zero)
# ESP <- Vzero in
hwstep_initial_state p (HState current_CPU_ID (pinit (B := core_set) (Asm.State rs0 m0)) nil).
Definition hwstep_final_state (s : hstate (hdset := hdseting)) (i : int) : Prop :=
False.
Ltac subst_except v :=
repeat match goal with
| [ H: v = _ |- _ ] ⇒ generalize H; clear H
| [ H: _ = v |- _ ] ⇒ generalize H; clear H
end; subst; intros.
Ltac clear_eq v :=
repeat match goal with
| [ H: v = _ |- _ ] ⇒ clear H
| [ H: _ = v |- _ ] ⇒ clear H
end.
Definition hwstep_semantics (p: program) :=
Smallstep.Semantics hw_step_aux_ge (hwstep_initial_state p)
hwstep_final_state (Genv.globalenv p).
Lemma hwstep_semantics_single_events:
∀ p, single_events (hwstep_semantics p).
Proof.
intros p s t s´ Hstep; inversion Hstep.
inversion H.
simpl; omega.
Qed.
Lemma hwstep_semantics_receptive (pl: program):
receptive (hwstep_semantics pl).
Proof.
intros; constructor.
- inversion 1.
inversion H0.
substx; try solve [inversion 1; substx; eauto].
intros.
inversion H8; substx.
∃ s1.
simpl.
unfold hw_step_aux.
simpl in H1.
rewrite <- H1.
eapply hw_step_aux_ge_intro.
unfold hw_step_aux.
rewrite <- H7.
econstructor; eauto.
- eapply hwstep_semantics_single_events.
Qed.
End WITH_GE.
End HWSTEPSEM.