Library mcertikos.multithread.lowrefins.E2PBThreadGenLemmaINITMATCH
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import AsmX.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import LAsm.
Require Import LoadStoreSem3.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import I64Layer.
Require Import AlgebraicMem.
Require Import Decision.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import SingleConfiguration.
Require Import ObjPHBFlatMem.
Require Import PHBThread.
Require Import AsmE2L.
Require Import AuxSingleAbstractDataType.
Require Import SingleOracleImpl.
Require Import E2PBThreadComposeData.
Require Import LoadStoreSemPHB.
Require Import ObjPHBThreadDEV.
Require Import ObjPHBThreadINTELVIRT.
Require Import ObjPHBThreadIPC.
Require Import ObjPHBThreadReplayFunction.
Require Import ObjPHBThreadSCHED.
Require Import ObjPHBThreadVMM.
Require Import ObjInterruptManagement.
Require Import ObjConsole.
Require Import ObjInterruptController.
Require Import ObjSerialDevice.
Require Import OracleInstances.
Require Import ObjVMMFun.
Require Import ObjVMMGetSet.
Require Import ObjVMMDef.
Require Import ObjCV.
Require Import ObjCPU.
Require Import ObjVMX.
Require Import ObjVMCS.
Require Import ObjProc.
Require Import ObjBigThread.
Require Import ObjContainer.
Require Import ObjMultiprocessor.
Require Import ObjThread.
Require Import BigLogThreadConfigFunction.
Require Import BigLogThreadConfigFunctionProp.
Require Import StencilImpl.
Require Import E2PBThreadGenDef.
Section E2PBThreadGenLemmaINITMATCHFILE.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{s_oracle_ops : SingleOracleOps}.
Context `{s_threads_ops: ThreadsConfigurationOps}.
Local Instance s_oracle_prf : SingleOracle := SingleOracleImpl.s_oracle_prf.
Context `{s_threads_prf: !ThreadsConfiguration (s_oracle := s_oracle_prf)}.
Context `{s_oracle_basic_prop_prf: !SingleOracleBasicProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_prop_prf : SingleOracleProp := SingleOracleImpl.s_oracle_prop_prf.
Context `{Hstencil : Stencil (stencil := stencil)}.
Local Instance s_config : SingleConfiguration mem := s_config.
Context `{s_oracle_basic_link_prop_prf: !SingleOracleBasicLinkProp (single_oracle_prf := s_oracle_prf)
(s_threads_ops := s_threads_ops)}.
Local Instance s_oracle_link_prop_prf : SingleOracleLinkProp := SingleOracleImpl.s_oracle_link_prop_prf.
Local Instance s_link_config : SingleLinkConfiguration mem := s_link_config.
Context `{acc_def: !AccessorsDefined (mem := mem) (stencil := stencil) (stencil_ops := stencil_ops)
(memory_model_ops := memory_model_ops)
(phbthread (s_config := s_config) ⊕ L64)}.
Opaque full_thread_list.
Opaque Z.add Z.mul Z.sub Z.div.
Lemma abs_rel_init_match_aux:
∃ kctxt_pool : KContextPool,
relate_RData kctxt_pool init_shared_adt
(EAsmCommon.initial_map None (fun i : Z ⇒ Some (thread_init_dproc i))
full_thread_list) (init_adt multi_oracle_init7).
Proof.
∃ (ZMap.init (Pregmap.init Vundef)).
induction full_thread_list.
- simpl.
constructor; simpl; auto.
+ intros.
rewrite ZMap.gi.
constructor.
reflexivity.
destruct (zle_lt 0 GlobalOracle.current_CPU_ID 8).
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
omega.
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
repeat (rewrite ZMap.gso; try (intros contra; subst; rewrite contra in o; try omega)).
rewrite ZMap.gi; auto.
+ intros.
rewrite ZMap.gi.
constructor; simpl; intros; auto; simpl.
+ constructor; simpl; intros; auto; simpl.
× intros.
eapply dirty_ppage´_init.
intros contra.
rewrite ZMap.gi in contra.
inv contra.
× rewrite ZMap.gi; auto.
× rewrite ZMap.gi; auto.
× unfold valid_AT_log_type_B; intros; simpl; inv Hdef.
× unfold valid_TCB_log_type_B; intros; simpl; inv Hdef.
× inversion multi_oracle_prop; auto.
× inv H0.
+ constructor.
intros.
rewrite ZMap.gi in H0, H1; inv H0.
- simpl.
constructor; simpl; auto.
+ rewrite ZMap.gi.
destruct (zle_lt 0 GlobalOracle.current_CPU_ID 8).
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
omega.
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
repeat (rewrite ZMap.gso; try (intros contra; subst; rewrite contra in o; try omega)).
rewrite ZMap.gi; auto.
+ intros.
case_eq (zeq i a); intros; subst.
× rewrite ZMap.gss; auto.
clear IHl.
rename a into i.
{ case_eq (zeq i main_thread); intros; subst.
{ unfold thread_init_dproc.
rewrite zeq_true.
unfold thread_init_dproc_aux.
rewrite zeq_true.
assert (Htemp: match match init_log with
| nil ⇒ Some main_init_dproc
| _ :: _ ⇒ None
end with
| Some init_dproc_val ⇒ init_dproc_val
| None ⇒ main_init_dproc
end = main_init_dproc).
{ destruct init_log; auto. }
rewrite Htemp; clear Htemp.
constructor; simpl; eauto;
try (case_eq (zeq main_thread (ZMap.get GlobalOracle.current_CPU_ID (init_real_cidpool (ZMap.init 0))));
intros; subst; eauto; fail);
try (case_eq (zeq main_thread dev_handling_cid); intros; subst; eauto; fail);
try (rewrite ZMap.gi; eauto; fail);
try (unfold pperm_inject; intros; rewrite ZMap.gi; auto; fail);
try (eapply FlatMem.flatmem_empty_inj; fail).
- rewrite ZMap.gi.
split; auto.
destruct (zle_lt 0 GlobalOracle.current_CPU_ID 8).
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
omega.
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
repeat (rewrite ZMap.gso; try (intros contra; subst; rewrite contra in o; try omega)).
rewrite ZMap.gi; auto.
- unfold relate_AC_per_pd; simpl.
rewrite zeq_true; auto.
rewrite ZMap.gi; auto.
- rewrite zeq_true; auto.
- rewrite zeq_true; auto.
- unfold relate_SyncChanPool_per_pd.
unfold init_shared_adt; simpl.
rewrite zeq_true; auto.
- unfold relate_uctxt_per_pd; simpl.
rewrite zeq_true; auto.
rewrite ZMap.gi; auto.
- rewrite ZMap.gi; auto; case_eq (zeq main_thread vm_handling_cid); intros; auto.
- rewrite ZMap.gi; auto; case_eq (zeq main_thread vm_handling_cid); intros; auto.
- rewrite ZMap.gi; auto; case_eq (zeq main_thread vm_handling_cid); intros; auto.
- constructor.
intros.
eapply dirty_ppage´_init.
intro contra.
rewrite ZMap.gi in contra.
inv contra. }
{ unfold thread_init_dproc.
unfold thread_init_dproc_aux.
rewrite zeq_false; auto.
rewrite zeq_false; eauto.
case_eq (thread_init_dproc_iter i init_log); intros; subst.
- generalize (thread_init_dproc_iter_preserve_fields _ _ _ H1).
intros.
blast H2.
constructor; simpl; try reflexivity;
try (case_eq (zeq i (ZMap.get GlobalOracle.current_CPU_ID (init_real_cidpool (ZMap.init 0))));
intros; subst; trivial; fail);
try (rewrite zeq_false; trivial; fail);
try (case_eq (zeq i dev_handling_cid); intros; subst; trivial; fail).
+ rewrite ZMap.gi.
split; auto.
destruct (zle_lt 0 GlobalOracle.current_CPU_ID 8).
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
omega.
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
repeat (rewrite ZMap.gso; try (intros contra; subst; rewrite contra in o; try omega)).
rewrite ZMap.gi; auto.
+ intros.
rewrite H13 in H48.
rewrite ZMap.gi in H48.
inv H48.
+ unfold relate_AC_per_pd; simpl.
rewrite zeq_false; eauto.
unfold thread_init_dproc.
simpl.
unfold thread_init_dproc_aux; simpl.
rewrite zeq_false; eauto.
rewrite H1.
destruct (zlt_lt 8 i 1024); auto.
+ rewrite H13; simpl.
unfold pperm_inject; intros; rewrite ZMap.gi; auto.
+ unfold relate_SyncChanPool_per_pd.
simpl; rewrite zeq_false; auto.
+ unfold relate_uctxt_per_pd; simpl.
rewrite zeq_false; eauto.
unfold thread_init_dproc.
simpl.
unfold thread_init_dproc_aux; simpl.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
rewrite H1.
destruct (zlt_lt 8 i 1024); auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ constructor.
intros.
rewrite H11.
eapply dirty_ppage´_init.
intro contra.
rewrite ZMap.gi in contra.
inv contra.
- constructor; simpl; eauto;
try (case_eq (zeq i (ZMap.get GlobalOracle.current_CPU_ID (init_real_cidpool (ZMap.init 0))));
intros; subst; eauto; fail);
try (case_eq (zeq i dev_handling_cid); intros; subst; eauto; fail);
try (rewrite ZMap.gi; eauto; fail);
try (unfold pperm_inject; intros; rewrite ZMap.gi; auto; fail);
try (eapply FlatMem.flatmem_empty_inj; fail).
+ rewrite ZMap.gi.
split; auto.
destruct (zle_lt 0 GlobalOracle.current_CPU_ID 8).
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
case_eq (zeq GlobalOracle.current_CPU_ID 7); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 6); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 5); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 4); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 3); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 2); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 1); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
case_eq (zeq GlobalOracle.current_CPU_ID 0); intros; subst;
[ rewrite e; rewrite ZMap.gss; auto | rewrite ZMap.gso; auto].
omega.
× unfold init_real_cidpool; simpl.
replace (8 - 1) with 7; auto.
simpl.
repeat (rewrite ZMap.gso; try (intros contra; subst; rewrite contra in o; try omega)).
rewrite ZMap.gi; auto.
+ unfold relate_AC_per_pd; simpl.
rewrite zeq_false; auto.
unfold thread_init_dproc.
simpl.
unfold thread_init_dproc_aux.
rewrite zeq_false; auto.
rewrite zeq_false; auto.
rewrite H1.
destruct (zlt_lt 8 i 1024); auto.
+ rewrite zeq_false; auto.
+ rewrite zeq_false; auto.
+ unfold relate_SyncChanPool_per_pd.
unfold init_shared_adt; simpl.
rewrite zeq_false; auto.
+ unfold relate_uctxt_per_pd; simpl.
rewrite zeq_false; eauto.
unfold thread_init_dproc.
simpl.
unfold thread_init_dproc_aux; simpl.
rewrite zeq_false; eauto.
rewrite zeq_false; eauto.
rewrite H1.
destruct (zlt_lt 8 i 1024); auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ rewrite ZMap.gi; auto; case_eq (zeq i vm_handling_cid); intros; auto.
+ constructor.
intros; simpl.
eapply dirty_ppage´_init.
intro contra.
rewrite ZMap.gi in contra.
inv contra. } }
× inv IHl.
rewrite ZMap.gso; auto.
generalize (per_data_re i); intros; auto.
+ constructor; simpl; intros; auto.
× eapply dirty_ppage´_init.
intros contra.
rewrite ZMap.gi in contra.
inv contra.
× rewrite ZMap.gi; auto.
× rewrite ZMap.gi; auto.
× unfold valid_AT_log_type_B; intros; simpl; inv Hdef.
× unfold valid_TCB_log_type_B; intros; simpl; inv Hdef.
× inversion multi_oracle_prop; auto.
× inv H0.
+ inv IHl.
constructor.
intros.
case_eq (zeq i a).
× intros; subst.
rewrite ZMap.gss in H0.
inversion H0.
unfold thread_init_dproc in H5.
unfold thread_init_dproc_aux in H5.
case_eq (zeq a main_thread).
{ intros; subst.
rewrite zeq_true in *; auto.
rewrite zeq_true in *; auto.
assert (match match init_log with
| nil ⇒ Some main_init_dproc
| _ :: _ ⇒ None
end with
| Some init_dproc_val ⇒ init_dproc_val
| None ⇒ main_init_dproc
end = main_init_dproc).
{ destruct init_log; auto. }
rewrite H5 in H2, H0; clear H5.
inv H0; simpl in ×.
rewrite ZMap.gi in H2.
elim H2; reflexivity. }
{ intros; subst.
rewrite zeq_false in *; auto.
rewrite zeq_false in *; auto.
case_eq (thread_init_dproc_iter a init_log); intros.
- inv H0.
rewrite H5 in H7.
generalize (thread_init_dproc_iter_preserve_fields _ _ _ H5).
intros.
blast H0.
rewrite H5 in H2; rewrite H17 in H2.
rewrite ZMap.gi in H2; elim H2; reflexivity.
- rewrite H5 in H0, H2.
simpl in H2.
rewrite ZMap.gi in H2; elim H2; reflexivity. }
× intros.
rewrite ZMap.gso in H0; auto.
case_eq (zeq j a); intros; subst.
{ rewrite ZMap.gss in H1.
inv H1.
unfold thread_init_dproc.
unfold thread_init_dproc_aux.
case_eq (zeq a main_thread).
{ intros; subst.
assert (match match init_log with
| nil ⇒ Some main_init_dproc
| _ :: _ ⇒ None
end with
| Some init_dproc_val ⇒ init_dproc_val
| None ⇒ main_init_dproc
end = main_init_dproc).
{ destruct init_log; auto. }
rewrite H5; clear H5.
simpl; rewrite ZMap.gi; auto. }
{ intros; subst.
case_eq (thread_init_dproc_iter a init_log); intros.
- generalize (thread_init_dproc_iter_preserve_fields _ _ _ H5).
intros.
blast H6.
rewrite H17.
rewrite ZMap.gi; reflexivity.
- simpl.
rewrite ZMap.gi; reflexivity. } }
{ rewrite ZMap.gso in H1; auto.
inv sh_mem_inv_re.
apply (pperm_disjoint i j pd pd´ H H0 H1 j0 H2). }
Qed.
End E2PBThreadGenLemmaINITMATCHFILE.