Library mcertikos.multicore.semantics.HWSemImpl
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 Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
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 Machregs.
Function get_last_event (l: MultiLogType) :=
match l with
| MultiUndef ⇒ None
| MultiDef nil ⇒ Some OINIT
| MultiDef (e:: l) ⇒
match e with
| TEVENT _ e0 ⇒
match e0 with
| TTICKET e1 ⇒
match e1 with
| INC_TICKET n ⇒ Some (OINC_TICKET n)
| INC_NOW ⇒ Some OINC_NOW
| GET_NOW ⇒ Some OGET_NOW
| HOLD_LOCK ⇒ Some OHOLD_LOCK
| _ ⇒ None
end
| TSHARED (OBUFFERE b) ⇒ Some (OPAGE_COPY b)
| _ ⇒ None
end
end
end.
Section GetPC.
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).
Definition mstate := Asm.state (mem := mwd LDATAOps).
Local Open Scope Z_scope.
Definition genv := Genv.t fundef unit.
Inductive command_predicate (ge: genv): mstate → command → Prop :=
| acq_prim_call:
∀ b ef rs m lid index ofs sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
match ef with
| EF_external eid _ ⇒
if peq eid acquire_shared then True
else False
| _ ⇒ False
end →
command_predicate ge (Asm.State rs m) (ACQ_SHARED lid)
| rel_prim_call:
∀ b ef rs m lid index ofs sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
match ef with
| EF_external eid _ ⇒
if peq eid release_shared then True
else False
| _ ⇒ False
end →
command_predicate ge (Asm.State rs m) (REL_SHARED lid)
| command_prim_atomic:
∀ b ef rs m lid index ofs sig eid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
atomic_id eid →
eid ≠ page_copy →
match ef with
| EF_external eid´ _ ⇒
if peq eid eid´ then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid eid)
| command_prim_page_copy:
∀ b ef rs m lid cv count from sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
if peq eid page_copy then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint cv :: Vint count :: Vint from :: nil) →
index2Z ID_SC (slp_q_id (Int.unsigned cv) 0) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid page_copy)
| command_prim_FAI:
∀ b ef rs m lid index ofs sig bound,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
if peq eid atomic_FAI then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint bound :: Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid atomic_FAI)
| command_internal:
∀ b ofs f rs m,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
command_predicate ge (Asm.State rs m) PRIVATE
| command_prim_private:
∀ b ef rs m,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
private_id eid
| _ ⇒ True
end →
command_predicate ge (Asm.State rs m) PRIVATE.
End GetPC.
Section HWSetting.
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.
Global Instance hdseting: HardWaredSetting :=
{
private_state := mstate;
shared_piece := list Integers.Byte.int;
atomic_event := OtherEvent;
atomic_event_ident := OtherEvent_2_ident;
core_set := cpu_set;
sched_id := 9
}.
Proof.
- intros.
eapply list_eq_dec. intros.
eapply Byte.eq_dec.
- repeat decide equality.
eapply Int.eq_dec.
- trivial.
Defined.
End HWSetting.
Section HARDWARESEMINSTANCE.
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.
Global Instance mboot_acc_def: AccessorsDefined (mboot ⊕ L64) := _.
Global Instance mboot_ec_ops: ExternalCallsOps (mwd LDATAOps) :=
CompatExternalCalls.compatlayer_extcall_ops (mboot ⊕ L64).
Global Instance mboot_ec_prf: ExternalCalls (mwd LDATAOps).
Proof.
eapply compatlayer_extcall_strong.
decision.
Qed.
Lemma mboot_pc_prf: PrimitiveCallsXDefined (mboot ⊕ L64).
Proof.
decision.
Qed.
Global Instance mboot_LC: LayerConfigurationOps (mem := mwd LDATAOps) :=
LC (mboot ⊕ L64).
Inductive private_exec (ge: genv): Z → mstate → mstate → Prop :=
| private_step_internal:
∀ b ofs f i rs (m m´: mwd LDATAOps) rs´ cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some i →
exec_instr ge f i rs m = Next rs´ m´ →
CPU_ID (snd m) = cid →
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_builtin:
∀ b ofs f ef args res rs (m m´: mwd LDATAOps) t vl rs´ cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pbuiltin ef args res)) →
external_call´ (fun _ ⇒ True) ef ge (map rs args) m t vl m´ →
rs´ = nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) →
CPU_ID (snd m) = cid →
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 Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
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 Machregs.
Function get_last_event (l: MultiLogType) :=
match l with
| MultiUndef ⇒ None
| MultiDef nil ⇒ Some OINIT
| MultiDef (e:: l) ⇒
match e with
| TEVENT _ e0 ⇒
match e0 with
| TTICKET e1 ⇒
match e1 with
| INC_TICKET n ⇒ Some (OINC_TICKET n)
| INC_NOW ⇒ Some OINC_NOW
| GET_NOW ⇒ Some OGET_NOW
| HOLD_LOCK ⇒ Some OHOLD_LOCK
| _ ⇒ None
end
| TSHARED (OBUFFERE b) ⇒ Some (OPAGE_COPY b)
| _ ⇒ None
end
end
end.
Section GetPC.
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).
Definition mstate := Asm.state (mem := mwd LDATAOps).
Local Open Scope Z_scope.
Definition genv := Genv.t fundef unit.
Inductive command_predicate (ge: genv): mstate → command → Prop :=
| acq_prim_call:
∀ b ef rs m lid index ofs sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
match ef with
| EF_external eid _ ⇒
if peq eid acquire_shared then True
else False
| _ ⇒ False
end →
command_predicate ge (Asm.State rs m) (ACQ_SHARED lid)
| rel_prim_call:
∀ b ef rs m lid index ofs sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
match ef with
| EF_external eid _ ⇒
if peq eid release_shared then True
else False
| _ ⇒ False
end →
command_predicate ge (Asm.State rs m) (REL_SHARED lid)
| command_prim_atomic:
∀ b ef rs m lid index ofs sig eid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
atomic_id eid →
eid ≠ page_copy →
match ef with
| EF_external eid´ _ ⇒
if peq eid eid´ then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid eid)
| command_prim_page_copy:
∀ b ef rs m lid cv count from sig,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
if peq eid page_copy then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint cv :: Vint count :: Vint from :: nil) →
index2Z ID_SC (slp_q_id (Int.unsigned cv) 0) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid page_copy)
| command_prim_FAI:
∀ b ef rs m lid index ofs sig bound,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
if peq eid atomic_FAI then True
else False
| _ ⇒ False
end →
sig = mksignature (AST.Tint::AST.Tint::AST.Tint::nil) None cc_default →
extcall_arguments rs m sig (Vint bound :: Vint index :: Vint ofs :: nil) →
index2Z (Int.unsigned index) (Int.unsigned ofs) = Some lid →
command_predicate ge (Asm.State rs m) (ATOMIC lid atomic_FAI)
| command_internal:
∀ b ofs f rs m,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
command_predicate ge (Asm.State rs m) PRIVATE
| command_prim_private:
∀ b ef rs m,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
match ef with
| EF_external eid _ ⇒
private_id eid
| _ ⇒ True
end →
command_predicate ge (Asm.State rs m) PRIVATE.
End GetPC.
Section HWSetting.
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.
Global Instance hdseting: HardWaredSetting :=
{
private_state := mstate;
shared_piece := list Integers.Byte.int;
atomic_event := OtherEvent;
atomic_event_ident := OtherEvent_2_ident;
core_set := cpu_set;
sched_id := 9
}.
Proof.
- intros.
eapply list_eq_dec. intros.
eapply Byte.eq_dec.
- repeat decide equality.
eapply Int.eq_dec.
- trivial.
Defined.
End HWSetting.
Section HARDWARESEMINSTANCE.
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.
Global Instance mboot_acc_def: AccessorsDefined (mboot ⊕ L64) := _.
Global Instance mboot_ec_ops: ExternalCallsOps (mwd LDATAOps) :=
CompatExternalCalls.compatlayer_extcall_ops (mboot ⊕ L64).
Global Instance mboot_ec_prf: ExternalCalls (mwd LDATAOps).
Proof.
eapply compatlayer_extcall_strong.
decision.
Qed.
Lemma mboot_pc_prf: PrimitiveCallsXDefined (mboot ⊕ L64).
Proof.
decision.
Qed.
Global Instance mboot_LC: LayerConfigurationOps (mem := mwd LDATAOps) :=
LC (mboot ⊕ L64).
Inductive private_exec (ge: genv): Z → mstate → mstate → Prop :=
| private_step_internal:
∀ b ofs f i rs (m m´: mwd LDATAOps) rs´ cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some i →
exec_instr ge f i rs m = Next rs´ m´ →
CPU_ID (snd m) = cid →
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_builtin:
∀ b ofs f ef args res rs (m m´: mwd LDATAOps) t vl rs´ cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pbuiltin ef args res)) →
external_call´ (fun _ ⇒ True) ef ge (map rs args) m t vl m´ →
rs´ = nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) →
CPU_ID (snd m) = cid →
CertiKOS:test-compcert-disable-extcall-as-builtin We need
to disallow the use of external function calls (EF_external) as
builtins.
CompCertX:test-compcert-wt-builtin We need to prove that registers updated by builtins are
of the same type as the return type of the builtin.
∀ BUILTIN_WT:
subtype_list (proj_sig_res´ (ef_sig ef)) (map typ_of_preg res) = true,
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_annot:
∀ b ofs f ef args rs (m m´: mwd LDATAOps) vargs t v cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pannot ef args)) →
annot_arguments rs m args vargs →
external_call´ (fun _ ⇒ True) ef ge vargs m t v m´ →
CPU_ID (snd m) = cid →
∀ BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
private_exec ge cid (Asm.State rs m)
(Asm.State (nextinstr rs) m´)
| private_step_external:
∀ b ef args res rs (m m´: mwd LDATAOps) t rs´ cid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
external_call´ (fun _ ⇒ True) ef ge args m t res m´ →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs)))
#Asm.PC <- (rs RA) #RA <- Vundef →
CPU_ID (snd m) = cid →
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_prim_call:
∀ b ef rs (m m´: mwd LDATAOps) t rs´ cid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
primitive_call ef ge rs m t rs´ m´ →
CPU_ID (snd m) = cid →
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´).
Inductive get_shared_sem (ge: genv) : mstate → list Integers.Byte.int → mstate → Prop:=
| get_shared_intro:
∀ rs sig m a index ofs id l b size ml0 z,
Genv.find_symbol ge id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ Mem.loadbytes m b 0 size = Some (ByteList l)
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs ::nil) →
∀ (Hindex: index2Z (Int.unsigned index) (Int.unsigned ofs) = Some z)
(Hlog: ZMap.get z (multi_log a) = MultiDef ml0),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
let a´ := a {multi_log: ZMap.set z (MultiDef (TEVENT (CPU_ID a) (TSHARED (OMEME l)) :: ml0))
(multi_log a)} in
get_shared_sem ge (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l
(Asm.State (rs´#RA <- Vundef#Asm.PC <- (rs RA)) (m, a´)).
Inductive set_shared_sem (ge: genv) : mstate → option (list Integers.Byte.int) → mstate → Prop:=
| set_shared_sem_intro:
∀ rs sig m m´ a index ofs id l b size ml0 z,
Genv.find_symbol ge id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
∀ (Hindex: index2Z (Int.unsigned index) (Int.unsigned ofs) = Some z)
(Hlog: ZMap.get z (multi_log a) = MultiDef ml0),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
let a´ := a {multi_log: ZMap.set z (MultiDef (TEVENT (CPU_ID a) (TSHARED OPULL) :: ml0))
(multi_log a)} in
set_shared_sem ge (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l
(Asm.State (rs´#RA <- Vundef#Asm.PC <- (rs RA)) (m´, a´)).
Inductive atomic_exec (ge: genv): Z → Z → mstate → Log → mstate → OtherEvent → Prop :=
| atomic_step_external:
∀ b ef args res rs (m m´: mwd LDATAOps) t rs´ cid e id sl,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
external_call´ (fun _ ⇒ True) ef ge args m t res m´ →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) (undef_regs (map preg_of destroyed_at_call) rs))) #Asm.PC <- (rs RA) #RA <- Vundef →
get_last_event (ZMap.get id (multi_log (snd m´))) = Some e →
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
atomic_exec ge cid id (Asm.State rs m) sl (Asm.State rs´ m´) e
| atomic_step_prim_call:
∀ b ef rs (m m´: mwd LDATAOps) t rs´ cid e id sl,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
primitive_call ef ge rs m t rs´ m´ →
get_last_event (ZMap.get id (multi_log (snd m´))) = Some e →
atomic_exec ge cid id (Asm.State rs m) sl (Asm.State rs´ m´) e.
Section HardSemLemmas.
subtype_list (proj_sig_res´ (ef_sig ef)) (map typ_of_preg res) = true,
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_annot:
∀ b ofs f ef args rs (m m´: mwd LDATAOps) vargs t v cid,
rs Asm.PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pannot ef args)) →
annot_arguments rs m args vargs →
external_call´ (fun _ ⇒ True) ef ge vargs m t v m´ →
CPU_ID (snd m) = cid →
∀ BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
private_exec ge cid (Asm.State rs m)
(Asm.State (nextinstr rs) m´)
| private_step_external:
∀ b ef args res rs (m m´: mwd LDATAOps) t rs´ cid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
external_call´ (fun _ ⇒ True) ef ge args m t res m´ →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs)))
#Asm.PC <- (rs RA) #RA <- Vundef →
CPU_ID (snd m) = cid →
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´)
| private_step_prim_call:
∀ b ef rs (m m´: mwd LDATAOps) t rs´ cid,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
primitive_call ef ge rs m t rs´ m´ →
CPU_ID (snd m) = cid →
private_exec ge cid (Asm.State rs m) (Asm.State rs´ m´).
Inductive get_shared_sem (ge: genv) : mstate → list Integers.Byte.int → mstate → Prop:=
| get_shared_intro:
∀ rs sig m a index ofs id l b size ml0 z,
Genv.find_symbol ge id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ Mem.loadbytes m b 0 size = Some (ByteList l)
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs ::nil) →
∀ (Hindex: index2Z (Int.unsigned index) (Int.unsigned ofs) = Some z)
(Hlog: ZMap.get z (multi_log a) = MultiDef ml0),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
let a´ := a {multi_log: ZMap.set z (MultiDef (TEVENT (CPU_ID a) (TSHARED (OMEME l)) :: ml0))
(multi_log a)} in
get_shared_sem ge (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l
(Asm.State (rs´#RA <- Vundef#Asm.PC <- (rs RA)) (m, a´)).
Inductive set_shared_sem (ge: genv) : mstate → option (list Integers.Byte.int) → mstate → Prop:=
| set_shared_sem_intro:
∀ rs sig m m´ a index ofs id l b size ml0 z,
Genv.find_symbol ge id = Some b
→ id2size (Int.unsigned index) = Some (size, id)
→ match l with
| Some l´ ⇒ Mem.storebytes m b 0 (ByteList l´) = Some m´
| _ ⇒ m´ = m
end
→ sig = mksignature (AST.Tint::AST.Tint::nil) None cc_default
→ extcall_arguments rs m sig (Vint index :: Vint ofs :: nil) →
∀ (Hindex: index2Z (Int.unsigned index) (Int.unsigned ofs) = Some z)
(Hlog: ZMap.get z (multi_log a) = MultiDef ml0),
let rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF
:: IR EAX :: RA :: nil)
(undef_regs (List.map preg_of destroyed_at_call) rs)) in
let a´ := a {multi_log: ZMap.set z (MultiDef (TEVENT (CPU_ID a) (TSHARED OPULL) :: ml0))
(multi_log a)} in
set_shared_sem ge (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l
(Asm.State (rs´#RA <- Vundef#Asm.PC <- (rs RA)) (m´, a´)).
Inductive atomic_exec (ge: genv): Z → Z → mstate → Log → mstate → OtherEvent → Prop :=
| atomic_step_external:
∀ b ef args res rs (m m´: mwd LDATAOps) t rs´ cid e id sl,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
external_call´ (fun _ ⇒ True) ef ge args m t res m´ →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) (undef_regs (map preg_of destroyed_at_call) rs))) #Asm.PC <- (rs RA) #RA <- Vundef →
get_last_event (ZMap.get id (multi_log (snd m´))) = Some e →
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
atomic_exec ge cid id (Asm.State rs m) sl (Asm.State rs´ m´) e
| atomic_step_prim_call:
∀ b ef rs (m m´: mwd LDATAOps) t rs´ cid e id sl,
rs Asm.PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
primitive_call ef ge rs m t rs´ m´ →
get_last_event (ZMap.get id (multi_log (snd m´))) = Some e →
atomic_exec ge cid id (Asm.State rs m) sl (Asm.State rs´ m´) e.
Section HardSemLemmas.
We will need to know that that external function calls yield
empty traces.
Lemma exec_external_E0:
∀ (s: stencil) (M: module) (ge: genv) ef WB args vl t m m´
(Hinstr: external_call´ (mem:= mwd LDATAOps) WB ef ge args m t vl m´)
(Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
s M (mboot ⊕ L64) = ret ge)
(ANNOT_DISABLED: ef_OK ef = OK tt),
t = E0.
Proof.
intros.
destruct Hinstr.
destruct ef eqn:Heq_ef; destruct H; eauto; try solve [inv ANNOT_DISABLED].
- destruct H as [_ []].
decompose [and ex] H.
assumption.
- inv H; auto; rename H1 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H; auto; rename H1 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H1; auto; rename H2 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H1; auto; rename H2 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
Qed.
∀ (s: stencil) (M: module) (ge: genv) ef WB args vl t m m´
(Hinstr: external_call´ (mem:= mwd LDATAOps) WB ef ge args m t vl m´)
(Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
s M (mboot ⊕ L64) = ret ge)
(ANNOT_DISABLED: ef_OK ef = OK tt),
t = E0.
Proof.
intros.
destruct Hinstr.
destruct ef eqn:Heq_ef; destruct H; eauto; try solve [inv ANNOT_DISABLED].
- destruct H as [_ []].
decompose [and ex] H.
assumption.
- inv H; auto; rename H1 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H; auto; rename H1 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H1; auto; rename H2 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
- inv H1; auto; rename H2 into Hvol.
erewrite make_globalenv_not_volatile in Hvol; eauto; inv Hvol.
Qed.
The following lemmas allow us to prove the determinism of
different cases in the semantics above, in a way that can be
efficiently proof-checked by Qed.
Lemma external_call´_determ_bundle:
∀ {WB ef1 ef2} {ge1 ge2: genv} {args1 args2 m1 m2 t1 t2 vl1 vl2 m1´ m2´},
external_call´ WB ef1 ge1 args1 m1 t1 vl1 m1´ →
external_call´ WB ef2 ge2 args2 m2 t2 vl2 m2´ →
ef1 = ef2 →
ge1 = ge2 →
args1 = args2 →
m1 = m2 →
∀ s M (Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
s M (mboot ⊕ L64) = ret ge1),
t1 = t2 ∧ vl1 = vl2 ∧ m1´ = m2´.
Proof.
intros until 0.
intros H1 H2; intros.
destruct (ef_OK ef1) as [[]|] eqn:Hcase.
{
assert (t1 = E0) by eauto using exec_external_E0.
assert (t2 = E0) by (subst; eauto using exec_external_E0).
subst.
destruct H1 as [v1 H1 Hv1], H2 as [v2 H2 Hv2].
destruct (Events.external_call_determ _ _ _ _ _ _ _ _ _ _ _ H1 H2) as [_ Hm].
destruct Hm; eauto.
subst; eauto.
}
{
destruct ef1; try solve [inv Hcase].
× inv H1; inv H2.
inv H; inv H5; auto.
assert (args0 = args) by (eapply eventval_list_match_determ_2; eauto); subst; auto.
× inv H1; inv H2.
inv H; inv H5.
rewrite <- H in H0; inv H0.
assert (arg0 = arg) by (eapply eventval_match_determ_2; eauto); subst; auto.
}
Qed.
Lemma annot_instr_excl:
∀ {ge: genv} b1 b2 {ofs1 ofs2 f1 f2 ef args i rs m rs´ m´},
Genv.find_funct_ptr ge b1 = Some (Internal f1) →
Genv.find_funct_ptr ge b2 = Some (Internal f2) →
find_instr (Int.unsigned ofs1) (fn_code f1) = Some (asm_instruction (Pannot ef args)) →
find_instr (Int.unsigned ofs2) (fn_code f2) = Some i →
b1 = b2 →
ofs1 = ofs2 →
¬ exec_instr ge f2 i rs m = Next rs´ m´.
Proof.
intros until 0.
intros Hb Hofs Hf1 Hf2 Hi1 Hi2.
assert (f1 = f2) by congruence; subst.
assert (i = Pannot ef args) by congruence; subst.
simpl.
discriminate.
Qed.
Lemma builtin_instr_excl:
∀ {ge: genv} b1 b2 {ofs1 ofs2 f1 f2 ef rl rl´ i rs m rs´ m´},
Genv.find_funct_ptr ge b1 = Some (Internal f1) →
Genv.find_funct_ptr ge b2 = Some (Internal f2) →
find_instr (Int.unsigned ofs1) (fn_code f1) = Some (asm_instruction (Pbuiltin ef rl rl´)) →
find_instr (Int.unsigned ofs2) (fn_code f2) = Some i →
b1 = b2 →
ofs1 = ofs2 →
¬ exec_instr ge f2 i rs m = Next rs´ m´.
Proof.
intros until 0.
intros Hb Hofs Hf1 Hf2 Hi1 Hi2.
assert (f1 = f2) by congruence; subst.
assert (i = Pbuiltin ef rl rl´) by congruence; subst.
simpl.
discriminate.
Qed.
End HardSemLemmas.
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.
Global Program Instance hdsem : HardSemantics (hdset:= hdseting)
:=
{
PC := command_predicate ge;
private_step := private_exec ge;
get_shared := get_shared_sem ge;
set_shared := set_shared_sem ge;
atomic_step := atomic_exec ge
}.
∀ {WB ef1 ef2} {ge1 ge2: genv} {args1 args2 m1 m2 t1 t2 vl1 vl2 m1´ m2´},
external_call´ WB ef1 ge1 args1 m1 t1 vl1 m1´ →
external_call´ WB ef2 ge2 args2 m2 t2 vl2 m2´ →
ef1 = ef2 →
ge1 = ge2 →
args1 = args2 →
m1 = m2 →
∀ s M (Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
s M (mboot ⊕ L64) = ret ge1),
t1 = t2 ∧ vl1 = vl2 ∧ m1´ = m2´.
Proof.
intros until 0.
intros H1 H2; intros.
destruct (ef_OK ef1) as [[]|] eqn:Hcase.
{
assert (t1 = E0) by eauto using exec_external_E0.
assert (t2 = E0) by (subst; eauto using exec_external_E0).
subst.
destruct H1 as [v1 H1 Hv1], H2 as [v2 H2 Hv2].
destruct (Events.external_call_determ _ _ _ _ _ _ _ _ _ _ _ H1 H2) as [_ Hm].
destruct Hm; eauto.
subst; eauto.
}
{
destruct ef1; try solve [inv Hcase].
× inv H1; inv H2.
inv H; inv H5; auto.
assert (args0 = args) by (eapply eventval_list_match_determ_2; eauto); subst; auto.
× inv H1; inv H2.
inv H; inv H5.
rewrite <- H in H0; inv H0.
assert (arg0 = arg) by (eapply eventval_match_determ_2; eauto); subst; auto.
}
Qed.
Lemma annot_instr_excl:
∀ {ge: genv} b1 b2 {ofs1 ofs2 f1 f2 ef args i rs m rs´ m´},
Genv.find_funct_ptr ge b1 = Some (Internal f1) →
Genv.find_funct_ptr ge b2 = Some (Internal f2) →
find_instr (Int.unsigned ofs1) (fn_code f1) = Some (asm_instruction (Pannot ef args)) →
find_instr (Int.unsigned ofs2) (fn_code f2) = Some i →
b1 = b2 →
ofs1 = ofs2 →
¬ exec_instr ge f2 i rs m = Next rs´ m´.
Proof.
intros until 0.
intros Hb Hofs Hf1 Hf2 Hi1 Hi2.
assert (f1 = f2) by congruence; subst.
assert (i = Pannot ef args) by congruence; subst.
simpl.
discriminate.
Qed.
Lemma builtin_instr_excl:
∀ {ge: genv} b1 b2 {ofs1 ofs2 f1 f2 ef rl rl´ i rs m rs´ m´},
Genv.find_funct_ptr ge b1 = Some (Internal f1) →
Genv.find_funct_ptr ge b2 = Some (Internal f2) →
find_instr (Int.unsigned ofs1) (fn_code f1) = Some (asm_instruction (Pbuiltin ef rl rl´)) →
find_instr (Int.unsigned ofs2) (fn_code f2) = Some i →
b1 = b2 →
ofs1 = ofs2 →
¬ exec_instr ge f2 i rs m = Next rs´ m´.
Proof.
intros until 0.
intros Hb Hofs Hf1 Hf2 Hi1 Hi2.
assert (f1 = f2) by congruence; subst.
assert (i = Pbuiltin ef rl rl´) by congruence; subst.
simpl.
discriminate.
Qed.
End HardSemLemmas.
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.
Global Program Instance hdsem : HardSemantics (hdset:= hdseting)
:=
{
PC := command_predicate ge;
private_step := private_exec ge;
get_shared := get_shared_sem ge;
set_shared := set_shared_sem ge;
atomic_step := atomic_exec ge
}.
The proof that the command_predicate is deterministic has
6x6 = 36 cases. We use the following lemmas to handle those that
are off the diagonal. The advantage of this is to avoid
duplication for the symmetric case, and accelerate Qed time by
bundling some of the proof in opaque chunks.
Lemma match_ef_determ (rs: regset) b1 b2 ef1 ef2 name1 name2:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
match ef1 with
| EF_external id sig ⇒ if peq id name1 then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external id sig ⇒ if peq id name2 then True else False
| _ ⇒ False
end →
name1 = name2 ∧ True. Proof.
intros Hb1 Hef1 H1 Hb2 Hef2 H2.
destruct ef1; try contradiction.
destruct ef2; try contradiction.
destruct (peq _ name1); try contradiction.
destruct (peq _ name2); try contradiction.
split; eauto; congruence.
Qed.
Lemma excl_internal_external (rs: regset) b1 b2 def1 def2 ofs:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External def1) →
rs Asm.PC = Vptr b2 ofs →
Genv.find_funct_ptr ge b2 = Some (Internal def2) →
False.
Proof.
intros.
congruence.
Qed.
Ltac split_ifs H :=
repeat
match type of H with
| if ?cond then _ else _ ⇒
destruct cond; split_ifs H
end.
Lemma excl_match_ef_atomic (rs: regset) b1 b2 ef1 ef2 name1 name2:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
match ef1 with
| EF_external id sig ⇒ if peq id name1 then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external id sig ⇒ if peq name2 id then True else False
| _ ⇒ False
end →
atomic_id name2 →
name1 ≠ log_get →
name1 ≠ log_incr →
name1 ≠ log_hold →
name1 ≠ log_init →
name1 ≠ page_copy →
False.
Proof.
intros ? ? ? ? ? ? Hat ? ? ?.
destruct ef1; try contradiction.
destruct ef2; try contradiction.
destruct (peq _ name1); try contradiction.
destruct (peq name2 _); try contradiction.
red in Hat.
split_ifs Hat; try congruence.
Qed.
Lemma excl_atomic_private (rs: regset) b1 b2 ef1 ef2 eid:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
atomic_id eid →
match ef1 with
| EF_external eid´ _ ⇒ if peq eid eid´ then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external eid _ ⇒ private_id eid
| _ ⇒ True
end →
False.
Proof.
intros ? ? Heid H1 ? ? H2.
assert (ef1 = ef2) by congruence; subst.
destruct ef2; try contradiction.
red in Heid; red in H2.
destruct (peq eid name); try contradiction; subst.
split_ifs H2; try contradiction.
Qed.
Lemma excl_acquire_private (rs: regset) b1 b2 ef1 ef2:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
match ef1 with
| EF_external eid _ ⇒ if peq eid acquire_shared then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external eid _ ⇒ private_id eid
| _ ⇒ True
end →
False.
Proof.
intros ? ? H1 ? ? H2.
assert (ef1 = ef2) by congruence; subst.
destruct ef2; try contradiction.
red in H2.
split_ifs H2; try contradiction.
Qed.
Lemma excl_release_private (rs: regset) b1 b2 ef1 ef2:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
match ef1 with
| EF_external eid _ ⇒ if peq eid release_shared then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external eid _ ⇒ private_id eid
| _ ⇒ True
end →
False.
Proof.
intros ? ? H1 ? ? H2.
assert (ef1 = ef2) by congruence; subst.
destruct ef2; try contradiction.
red in H2.
split_ifs H2; try contradiction.
Qed.
Lemma excl_FAI_private (rs: regset) b1 b2 ef1 ef2:
rs Asm.PC = Vptr b1 Int.zero →
Genv.find_funct_ptr ge b1 = Some (External ef1) →
match ef1 with
| EF_external eid _ ⇒ if peq eid atomic_FAI then True else False
| _ ⇒ False
end →
rs Asm.PC = Vptr b2 Int.zero →
Genv.find_funct_ptr ge b2 = Some (External ef2) →
match ef2 with
| EF_external eid _ ⇒ private_id eid
| _ ⇒ True
end →
False.
Proof.
intros ? ? H1 ? ? H2.
assert (ef1 = ef2) by congruence; subst.
destruct ef2; try contradiction.
red in H2.
split_ifs H2; try contradiction.
Qed.
Lemma ByteList_injective bl1 bl2:
ByteList bl1 = ByteList bl2 →
bl1 = bl2.
Proof.
clear Hmakege.
revert bl2.
induction bl1.
- simpl.
destruct bl2; try discriminate.
eauto.
- simpl.
destruct bl2; try discriminate.
simpl.
inversion 1.
f_equal.
eauto.
Qed.
Next Obligation. clear Hmakege; destruct H; inversion H0;
try solve
[ edestruct (match_ef_determ rs b b0) as [Hid _]; eauto; discriminate
| eelim (excl_internal_external rs b b0); eauto
| eelim (excl_internal_external rs b0 b); eauto
| eelim (excl_match_ef_atomic rs b b0); eauto; discriminate
| eelim (excl_match_ef_atomic rs b0 b); eauto; discriminate
| eelim (excl_atomic_private rs b0 b); eauto
| eelim (excl_atomic_private rs b b0); eauto
| eelim (excl_acquire_private rs b0 b); eauto
| eelim (excl_acquire_private rs b b0); eauto
| eelim (excl_release_private rs b0 b); eauto
| eelim (excl_release_private rs b b0); eauto
| eelim (excl_FAI_private rs b b0); eauto
| eelim (excl_FAI_private rs b0 b); eauto
].
- subst.
pose proof (extcall_arguments_determ_with_data _ _ _ _ _ H11 H3).
congruence.
- subst.
pose proof (extcall_arguments_determ_with_data _ _ _ _ _ H11 H3).
congruence.
- assert (ef = ef0) by congruence; subst.
pose proof (extcall_arguments_determ_with_data _ _ _ _ _ H16 H6).
destruct ef0; try contradiction.
destruct (peq eid name); try contradiction.
destruct (peq eid0 name); try contradiction.
congruence.
- assert (ef = ef0) by congruence; subst.
destruct ef0; try contradiction.
destruct (peq eid name); subst; try contradiction.
destruct (peq name page_copy); subst; try congruence. contradiction.
- assert (ef = ef0) by congruence; subst.
destruct ef0; try contradiction.
destruct (peq eid name); subst; try contradiction.
destruct (peq name page_copy); subst; try congruence. contradiction.
- subst.
pose proof (extcall_arguments_determ_with_data _ _ _ _ _ H12 H4).
congruence.
- assert (ef = ef0) by congruence; subst.
destruct ef0; try contradiction.
destruct (peq name page_copy); subst; try congruence; contradiction.
- subst.
pose proof (extcall_arguments_determ_with_data _ _ _ _ _ H12 H4).
congruence.
- reflexivity.
- assert (ef = ef0) by congruence; subst.
destruct ef0; try contradiction.
destruct (peq name page_copy); subst; try congruence; contradiction.
- reflexivity.
Qed.
Next we prove that the private_step is deterministic.
Next Obligation.
destruct H; inversion H0; try congruence.
- eelim (builtin_instr_excl b0 b); eauto; try congruence.
congruence. - eelim (annot_instr_excl b0 b); eauto; try congruence.
congruence. - eelim (builtin_instr_excl b b0); eauto; try congruence.
congruence. -
exploit (external_call´_determ_bundle H3 H11); try congruence.
eassumption.
intros [? [? ?]]; congruence.
- eelim (annot_instr_excl b b0); eauto; try congruence.
congruence. -
exploit (external_call´_determ_bundle H4 H13); try congruence.
assert (args = args0) by congruence; subst.
apply (annot_arguments_determ _ _ _ _ _ H3 H11).
eassumption.
intros [? [? ?]]; congruence.
-
edestruct (external_call´_determ_bundle H3 H11) as (? & ? & ?);
eauto;
try congruence.
assert (ef0 = ef) by congruence; subst.
pose proof (extcall_arguments_determ _ _ _ _ _ H2 H10).
assumption.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
destruct (primcall_determ H2 H9) as (_ & _ & ?); eauto.
eapply mboot_pc_prf; eauto.
Qed.
Next Obligation. destruct H; inv H0.
pose proof (extcall_arguments_determ rs m _ _ _ H14 H4) as Hargs.
inv Hargs.
assert (size0 = size) by congruence; subst.
assert (id0 = id) by congruence; subst.
assert (b0 = b) by congruence; subst.
rewrite H10 in H2.
inversion H2.
eapply ByteList_injective in H3.
split; eauto.
f_equal.
unfold a´, a´0.
assert (z0 = z) by congruence; subst.
assert (ml0 = ml1) by congruence; subst.
reflexivity.
Qed.
Next Obligation. destruct H; inv H0.
pose proof (extcall_arguments_determ rs m _ _ _ H14 H4) as Hargs.
inv Hargs.
assert (id0 = id) by congruence; subst.
assert (b0 = b) by congruence; subst.
subst a´ a´0.
assert (z0 = z) by congruence; subst.
assert (ml0 = ml1) by congruence; subst.
destruct l;
assert (m´0 = m´) by congruence; subst;
reflexivity.
Qed.
Next Obligation. destruct H; inv H0.
- edestruct (external_call´_determ_bundle H3 H11) as (? & ? & ?);
eauto;
try congruence.
assert (ef0 = ef) by congruence; subst.
eapply (extcall_arguments_determ _ _ _ _ _ H2 H10); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (primcall_determ H2 H10) as (?&?&?); eauto using mboot_pc_prf.
Qed.
Next Obligation. destruct H; inv H0.
- edestruct (external_call´_determ_bundle H3 H11) as (? & ? & ?);
eauto;
try congruence.
assert (ef0 = ef) by congruence; subst.
eapply (extcall_arguments_determ _ _ _ _ _ H2 H10); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (external_prim_false _); eauto.
- assert (b0 = b) by congruence; subst.
assert (ef0 = ef) by congruence; subst.
edestruct (primcall_determ H2 H10) as (?&?&?); eauto using mboot_pc_prf.
congruence.
Qed. Next Obligation.
intros. inv Hstep.
- eapply atomic_step_external; eauto.
- eapply atomic_step_prim_call; eauto.
Qed.
End WITH_GE.
End HARDWARESEMINSTANCE.