Library mcertikos.multithread.lowrefins.E2PBThreadGenLemma
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 E2PBTHREADGENLEMMAFILE.
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 PDX Zdivide_dec zle Z.mul Z.add Z.sub Z.div.
Opaque CalRealPT.real_pt CalRealProcModule.real_syncchpool.
Opaque compatlayer_ops.
Opaque update.
Opaque uRData.
Opaque proc_id.
Opaque full_thread_list.
Lemma ipc_receive_body_related:
∀ kctxt_pool sd sd´ a d d´ dp chid vaddr rcount res,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
ObjPHBThreadIPC.single_big_ipc_receive_body_spec chid vaddr rcount (sd, d) = Some ((sd´, d´), res) →
∃ a´ res´,
big_ipc_receive_body_spec chid vaddr rcount a = Some (a´, res´) ∧
relate_RData kctxt_pool sd´ (ZMap.set (proc_id sd´) (Some d´) dp) a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´) ∧ res = res´.
Proof.
Opaque Z.add Z.sub Z.div Z.mul.
Opaque OracleInstances.SerialEnv.
Opaque cons_buf list_eq_dec Zlength serial_exists.
intros.
Transparent uRData proc_id update.
generalize H; intros Hrelated.
inv H; simpl in ×.
functional inversion H1; subst; simpl in ×.
destruct adt1; subst; simpl in ×.
unfold big_ipc_receive_body_spec.
generalize (per_data_re (ZMap.get (CPU_ID sd) (cid sd))).
rewrite H0.
intros.
inv H; subst; simpl in ×.
rewrite zeq_true in ×.
unfold sh_adt, pv_adt, curid in ×.
unfold sh_adt in H12.
clear sh_adt pv_adt curid.
rewrite <- pg_re, <- ikern_re, <- ihost_re, <- ipt_re.
unfold relate_SyncChanPool_per_pd in syncchpool_re.
rewrite H9 in ×.
rewrite H4 in ×.
simpl in syncchpool_re; rewrite zeq_true in syncchpool_re.
rewrite <- syncchpool_re.
rewrite H5, H6, H7, H8, H11, H10.
rewrite <- cid_re.
functional inversion H12; simpl in *; subst.
unfold sh_adt0, pv_adt0, index in ×.
clear index pv_adt0 sh_adt0.
inv H.
unfold big_page_copy_back_spec.
rewrite <- ikern_re, <- ihost_re, <- ipt_re.
rewrite H3, H5, H6, H7.
rewrite H17, H18, H16.
assert (Hpperm: ZMap.get (PageI (vaddr)) (AbstractDataType.pperm a) = PGAlloc).
{ unfold pperm_inject in pperm_re.
generalize (pperm_re (PageI (vaddr))).
rewrite H19.
intros.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
subdestruct; inv H.
reflexivity.
}
rewrite Hpperm.
rewrite <- big_log_re.
rewrite <- lock_re.
rewrite H20, H21, H22, H23.
rewrite <- CPU_ID_re; rewrite zeq_true.
assert (Hcopy_back_exists:
∃ h´, page_copy_back_aux (Z.to_nat (Z.min (Int.unsigned scount) rcount))
vaddr b (AbstractDataType.HP a) = Some h´).
{
eauto using page_copy_back_exists.
}
destruct Hcopy_back_exists as (h´ & Hcopy_back_exists).
rewrite Hcopy_back_exists.
assert (Hcopy_back_preserve_freepage:
∀ res i : ZIndexed.t,
ZMap.get i (pperm d) = PGUndef → ZMap.get res h = ZMap.get res (FlatMem.free_page i h)).
{ assert (single_dirty_ppage´ (pperm d) (HP d)).
{ intros; eauto.
unfold single_dirty_ppage´.
intros.
inv inv_re.
eapply dirty_page_per_thread_inv; eauto. }
intros.
generalize (single_dirty_ppage´_gss_page_copy_back (Z.min (Int.unsigned scount) rcount) (HP d) h
(pperm d) vaddr b H25 H19 _x2).
intros.
unfold single_dirty_ppage´ in H26.
eapply H26; eauto. }
refine_split´; try eauto.
constructor; simpl; auto.
- rewrite H9; auto.
- rewrite H9; auto.
- intros.
case_eq (zeq i (ZMap.get (CPU_ID s) (cid s))); intros; subst.
+ rewrite ZMap.gss.
constructor; auto.
× simpl; rewrite H9; auto.
× simpl; rewrite H9; auto.
× simpl; intros.
exploit page_copy_back_aux_mine_related; eauto.
× simpl; rewrite zeq_true; auto.
× simpl; rewrite zeq_true; auto.
× simpl; rewrite zeq_true; auto.
× simpl; rewrite H9; rewrite zeq_true; auto.
× simpl; rewrite H9; auto.
× simpl; rewrite zeq_true; auto.
× simpl; rewrite zeq_true; auto.
× simpl; rewrite zeq_true; auto.
× unfold relate_SyncChanPool_per_pd.
rewrite H9.
rewrite H4.
simpl; rewrite zeq_true.
rewrite syncchpool_re.
auto.
× inv inv_re.
constructor; simpl; auto.
+ rewrite ZMap.gso; try auto.
repeat match goal with
| [H: context[if _ then _ else _] |- _] ⇒ clear H
end.
generalize (per_data_re i).
intros.
subdestruct.
× inv H2; simpl in ×.
per_data_auto.
{ assert (Hpperm_val: ZMap.get (PageI vaddr) (pperm p) = PGUndef).
{ inv sh_mem_inv_re.
exploit (pperm_disjoint (ZMap.get (CPU_ID s) (cid s)) i); eauto.
rewrite H19.
intro contra; inv contra. }
simpl; intros.
exploit page_copy_back_aux_others_related; eauto. }
{ unfold relate_AC_per_pd in ×.
simpl in ×.
rewrite H9 in ×.
auto. }
{ auto. }
{ auto. }
{ unfold relate_SyncChanPool_per_pd in *; simpl.
rewrite H9.
rewrite H4.
rewrite zeq_false; auto. }
{ auto. }
{ inv inv_re0; constructor; simpl in ×.
auto. }
× constructor; auto.
- inv sh_shared_inv_re.
constructor; simpl; intros; auto.
+ assert (single_dirty_ppage´ (AbstractDataType.pperm a) (AbstractDataType.HP a)).
{ intros; eauto.
unfold single_dirty_ppage´.
intros.
eapply dirty_page_shared_inv; eauto. }
generalize (single_dirty_ppage´_gss_page_copy_back (Z.min (Int.unsigned scount) rcount)
(AbstractDataType.HP a) h´
(AbstractDataType.pperm a) vaddr b
Hcopy_back_exists Hpperm _x2 _x1 H2).
intros.
unfold single_dirty_ppage´ in H26.
eapply H26; eauto.
+ rewrite H4 in H.
inv H.
+ eapply valid_B_Cal_AT_log_inv; eauto.
- generalize sh_mem_inv_re.
generalize H0.
clear.
intros.
inv sh_mem_inv_re.
constructor; simpl; auto.
intros.
intros.
case_eq (zeq i (ZMap.get (CPU_ID s) (cid s))).
+ generalize (pperm_disjoint i j d pd´ H).
intros; subst.
rewrite ZMap.gss in H1.
rewrite ZMap.gso in H2; try auto.
inv H1.
simpl in ×.
eapply H4; eauto.
+ intros; subst.
rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID s) (cid s))).
× generalize (pperm_disjoint i j pd d H).
intros; subst; simpl.
rewrite ZMap.gss in H2.
inv H2; simpl in ×.
eapply H5; eauto.
× intros.
generalize (pperm_disjoint i j pd pd´ H).
rewrite ZMap.gso in H2; eauto.
Qed.
Lemma cons_intr_aux_related :
∀ kctxt_val sd sd´ a d d´,
proc_id sd = dev_handling_cid →
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_cons_intr_aux (sd, d) = Some (sd´, d´) →
∃ a´,
cons_intr_aux a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
Opaque Z.add Z.sub Z.div Z.mul.
Opaque OracleInstances.SerialEnv.
Opaque cons_buf list_eq_dec Zlength serial_exists.
intros.
Transparent uRData proc_id update.
inv H0; simpl in *; rewrite zeq_true in ×.
rewrite <- H in *; rewrite zeq_true in ×.
functional inversion H1; subst; simpl in ×.
- unfold cons_intr_aux.
rewrite <- ikern_re, <- ihost_re, <- init_re, <- in_intr_re, <- drv_serial_re, <- com1_re, <- console_re.
rewrite H3, H4, H5, H6.
rewrite _x; rewrite zeq_true.
rewrite H8; rewrite <- _x.
rewrite H9, H10, H11.
simpl; esplit; split; [ reflexivity | ].
split; eauto.
constructor; simpl; auto; try (rewrite zeq_true; auto; fail); try (rewrite <- H; rewrite zeq_true; auto).
simpl.
rewrite <- com1_re; rewrite H8; auto.
+ inv inv_re.
constructor; simpl; intros; auto.
- unfold cons_intr_aux.
rewrite <- ikern_re, <- ihost_re, <- init_re, <- in_intr_re, <- drv_serial_re, <- com1_re, <- console_re.
rewrite H3, H4, H5, H6.
rewrite _x; rewrite zeq_true.
rewrite H8; rewrite <- _x.
rewrite H9, H10, H11.
simpl; esplit; split; [ reflexivity | ].
split; eauto.
constructor; simpl; auto; try (rewrite zeq_true; auto; fail); try (rewrite <- H; rewrite zeq_true; auto).
simpl.
rewrite <- com1_re; rewrite H8; auto.
+ inv inv_re.
constructor; simpl; intros; auto.
Opaque uRData proc_id update.
Qed.
Lemma serial_enable_aux_related:
∀ n kctxt_val sd sd´ a d d´,
proc_id sd = dev_handling_cid →
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_serial_intr_enable n (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_enable_aux n a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
induction n; intros.
- simpl; intros; simpl in H1; inv H1.
∃ a; auto.
- simpl in ×.
assert (SerialIrq_eq: SerialIrq (s (com1 d)) = SerialIrq (s (AbstractDataType.com1 a))).
{ inv H0.
rewrite <- H in com1_re.
rewrite zeq_true in com1_re.
rewrite <- com1_re; auto. }
case_eq (SerialIrq (s (com1 d))); intros.
+ rewrite <- SerialIrq_eq.
rewrite H2 in H1; rewrite H2.
subdestruct; try (inv H0; fail).
destruct p.
exploit cons_intr_aux_related; eauto; intros Hrelated.
destruct Hrelated as (a´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e).
rewrite Hrelated_a; subst.
rewrite Hrelated_d.
rewrite Hrelated_e.
eapply IHn; eauto.
+ rewrite <- SerialIrq_eq.
rewrite H2 in H1.
rewrite H2.
inv H1.
refine_split´; eauto.
Qed.
Lemma serial_disable_aux_true_related:
∀ n kctxt_val sd sd´ a d d´,
proc_id sd = dev_handling_cid →
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_serial_intr_disable n true (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_disable_aux n true a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
induction n; intros.
- simpl in H1; inv H1; ∃ a; auto.
- assert (relate_RData_per_pd (proc_id sd) kctxt_val sd
(d {pv_com1: ObjPHBThreadDEV.single_serial_intr (com1 d)})
(a {com1 : serial_intr (AbstractDataType.com1 a)})).
{ unfold ObjPHBThreadDEV.single_serial_intr; simpl.
unfold ObjPHBThreadDEV.single_serial_trans_env; simpl.
unfold serial_intr.
unfold ObjSerialDevice.serial_trans_env; simpl.
inv H0.
constructor; simpl; auto.
rewrite H; rewrite zeq_true; rewrite H in com1_re; rewrite zeq_true in com1_re.
rewrite <- com1_re; auto.
inv inv_re.
constructor; simpl; intros; auto. }
simpl in ×.
assert (SerialIrq_eq: SerialIrq (ObjPHBThreadDEV.single_serial_trans_env
(OracleInstances.SerialEnv (l1 (com1 d))) (s (com1 d))) =
SerialIrq (ObjSerialDevice.serial_trans_env
(OracleInstances.SerialEnv (l1 (AbstractDataType.com1 a)))
(s (AbstractDataType.com1 a)))).
{ unfold ObjPHBThreadDEV.single_serial_trans_env.
unfold ObjSerialDevice.serial_trans_env.
inv H0.
rewrite H in *; rewrite zeq_true in ×.
rewritesb; simpl; auto. }
case_eq (SerialIrq (ObjPHBThreadDEV.single_serial_trans_env
(OracleInstances.SerialEnv (l1 (com1 d))) (s (com1 d)))); intros.
+ rewrite <- SerialIrq_eq.
rewrite H3.
rewrite H3 in H1.
generalize H1; intros Htemp.
eapply IHn in Htemp; simpl in Htemp; eauto.
simpl in Htemp; eauto.
+ rewrite <- SerialIrq_eq.
rewrite H3.
rewrite H3 in H1.
inv H1.
∃ a; split; auto.
Qed.
Lemma serial_disable_aux_false_related:
∀ n kctxt_val sd sd´ a d d´,
proc_id sd = dev_handling_cid →
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_serial_intr_disable n false (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_disable_aux n false a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
induction n; intros.
- simpl in H1; inv H1; ∃ a; auto.
- assert (relate_RData_per_pd (proc_id sd) kctxt_val sd
(d {pv_com1: ObjPHBThreadDEV.single_serial_intr (com1 d)})
(a {com1 : serial_intr (AbstractDataType.com1 a)})).
{ unfold ObjPHBThreadDEV.single_serial_intr; simpl.
unfold ObjPHBThreadDEV.single_serial_trans_env; simpl.
unfold serial_intr.
unfold ObjSerialDevice.serial_trans_env; simpl.
inv H0.
constructor; simpl; auto.
rewrite H; rewrite zeq_true; rewrite H in com1_re; rewrite zeq_true in com1_re.
rewrite <- com1_re; auto.
inv inv_re.
constructor; simpl; intros; auto. }
simpl in ×.
assert (SerialIrq_eq: SerialIrq (ObjPHBThreadDEV.single_serial_trans_env
(OracleInstances.SerialEnv (l1 (com1 d))) (s (com1 d))) =
SerialIrq (ObjSerialDevice.serial_trans_env
(OracleInstances.SerialEnv (l1 (AbstractDataType.com1 a)))
(s (AbstractDataType.com1 a)))).
{ unfold ObjPHBThreadDEV.single_serial_trans_env.
unfold ObjSerialDevice.serial_trans_env.
inv H0.
rewrite H in *; rewrite zeq_true in ×.
rewritesb; simpl; auto. }
case_eq (SerialIrq (ObjPHBThreadDEV.single_serial_trans_env
(OracleInstances.SerialEnv (l1 (com1 d))) (s (com1 d)))); intros.
+ rewrite <- SerialIrq_eq.
rewrite H3.
rewrite H3 in H1.
subdestruct.
destruct p; subst.
exploit cons_intr_aux_related; eauto; intros Hrelated.
destruct Hrelated as (a´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e); subst.
rewrite Hrelated_a.
generalize Hrelated_b; intros Htemp.
eapply IHn in Htemp; eauto; simpl in Htemp; eauto.
simpl in Hrelated_d; rewrite Hrelated_d.
simpl in Hrelated_e.
rewrite Hrelated_e; eauto.
+ rewrite <- SerialIrq_eq.
rewrite H3.
rewrite H3 in H1.
inv H1; ∃ a; split; auto.
Qed.
Section SERIALINTRDISABLERELATED.
Opaque ObjPHBThreadDEV.single_serial_intr_disable.
Opaque serial_intr_disable_aux.
Lemma serial_intr_disable_related_mine:
∀ kctxt_val sd sd´ a d d´,
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_serial_intr_disable_spec (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_disable_spec a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
intros.
assert (in_intr_related:
relate_RData_per_pd (proc_id sd) kctxt_val sd (d {pv_in_intr: true})
a {in_intr: true}).
{ inv H; constructor; simpl in *; auto; try (rewrite zeq_true; auto).
inv inv_re.
constructor; simpl; intros; auto. }
unfold serial_intr_disable_spec; unfold ObjPHBThreadDEV.single_serial_intr_disable_spec in H0.
Transparent uRData proc_id update.
inv H0.
subdestruct; simpl in *; inv H;
inv H2; subst; simpl in *; rewrite e in *; rewrite zeq_true in *;
rewrite <- ikern_re, <- ihost_re, <- init_re, <- intr_flag_re, <- in_intr_re, <- ioapic_re;
rewrite Hdestruct0, Hdestruct1, Hdestruct2, Hdestruct3, Hdestruct4, Hdestruct5;
try (rewrite Hdestruct10); simpl;
destruct p; simpl in *; rewrite <- e in in_intr_related;
try (exploit serial_disable_aux_true_related; eauto; simpl; auto; try exact in_intr_related;
intros Hrelated; destruct Hrelated
as (a´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e); subst;
rewrite Hrelated_a; refine_split´; eauto); try (inv H2; auto);
try (inv Hrelated_b; constructor; simpl in *; auto;
try (rewrite <- e; rewrite Hrelated_d; auto);
try (rewrite zeq_true; auto));
try (rewrite Hdestruct2 in cid_re0, cid_re;
rewrite cid_re; rewrite cid_re0; rewrite <- Hrelated_e; rewrite zeq_true; auto;
rewrite cid_re in ioapic_re0; rewrite cid_re0 in ioapic_re0; rewrite <- Hrelated_e in ioapic_re0;
rewrite zeq_true in ioapic_re0; auto;
rewrite ioapic_re0; auto);
try (inv inv_re0; constructor; simpl; intros; auto).
exploit serial_disable_aux_false_related; eauto; simpl; auto; try exact in_intr_related.
intros Hrelated; destruct Hrelated as (a´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e); subst.
rewrite Hrelated_a; refine_split´; eauto.
inv Hrelated_b; constructor; simpl in *; auto; try (rewrite <- e; rewrite Hrelated_d; auto);
try (rewrite zeq_true; auto); try (rewrite e; rewrite zeq_true; auto);
try (rewrite e in ioapic_re0; rewrite zeq_true in ioapic_re0; rewrite <- ioapic_re0; auto);
try (inv inv_re0; constructor; simpl; intros; auto).
Qed.
Lemma serial_intr_disable_cid:
∀ sd sd´ d d´,
ObjPHBThreadDEV.single_serial_intr_disable_spec (sd, d) = Some (sd´, d´) →
proc_id sd = dev_handling_cid.
Proof.
intros; subst; simpl in *; functional inversion H; simpl in *; auto.
Qed.
Lemma serial_intr_disable_related_others:
∀ i kctxt_val sd a d d´ other_d a´,
i ≠ proc_id sd →
relate_RData_per_pd i kctxt_val sd other_d a →
ObjPHBThreadDEV.single_serial_intr_disable_spec (sd, d) = Some (sd, d´) →
serial_intr_disable_spec a = Some a´ →
kctxt a = kctxt a´ →
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´) →
relate_RData_per_pd i kctxt_val sd other_d a´.
Proof.
intros; subst.
exploit INVLemmaInterrupt.serial_intr_disable_preserves_all; eauto; simpl.
intros Hpre; blast Hpre.
assert (ZMap.get (CPU_ID sd) (cid sd) = dev_handling_cid).
{ exploit serial_intr_disable_cid; eauto. }
inv H0; simpl in ×.
constructor; simpl in *; rewritesb.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ rewrite CPU_ID_re.
rewrite CPU_ID_re in cid_re.
auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ unfold relate_AC_per_pd in *; simpl; auto.
rewrite <- H15; auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ rewrite zeq_false; auto; rewrite zeq_false in intr_flag_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in in_intr_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in com1_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in console_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in console_concrete_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in ioapic_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in lapic_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in curr_intr_num_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in drv_serial_re; auto.
+ unfold relate_SyncChanPool_per_pd; unfold relate_SyncChanPool_per_pd in syncchpool_re.
destruct (init sd).
destruct (BigLogThreadConfigFunction.B_inLock (CPU_ID sd) (big_log sd)); auto.
simpl; rewrite zeq_false; auto.
case_eq (zeq i main_thread).
× intros; subst.
rewrite zeq_true in syncchpool_re; auto.
× intros; rewrite zeq_false in syncchpool_re; auto.
+ unfold relate_uctxt_per_pd in uctxt_re.
unfold relate_uctxt_per_pd.
rewrite <- Hpre33.
auto.
+ rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re; auto.
+ inv inv_re; constructor; intros; auto.
Qed.
Lemma serial_intr_disable_related:
∀ kctxt_pool sd sd´ a d d´ dp,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
ObjPHBThreadDEV.single_serial_intr_disable_spec (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_disable_spec a = Some a´ ∧
relate_RData kctxt_pool sd´ (ZMap.set (proc_id sd´) (Some d´) dp) a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
intros.
generalize (per_data_re _ _ _ _ H (proc_id sd)); intros Hper_data_rel.
rewrite H0 in Hper_data_rel.
exploit serial_intr_disable_related_mine; eauto; intros Hrel_m.
destruct Hrel_m as (a´ & Hrel_ma & Hrel_mb & Hrel_mc & Hrel_md & Hrel_me); subst.
∃ a´; refine_split; auto.
constructor; simpl; try (inv Hrel_mb; simpl; auto; fail).
- inv H; auto.
- intros.
inv H.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst; [rewrite ZMap.gss; auto |].
rewrite ZMap.gso; auto.
clear sh_cid_re.
subdestruct; auto.
generalize serial_intr_disable_related_others; eauto.
simpl; auto.
inv Hrel; constructor; simpl; auto.
- inv H.
inv sh_shared_inv_re.
exploit INVLemmaInterrupt.serial_intr_disable_preserves_all; eauto.
intros.
blast H.
constructor.
+ rewrite <- H43, <- H51; auto.
+ auto.
+ rewrite <- H42; auto.
+ rewrite <- H68; auto.
+ rewrite <- H66; auto.
+ rewrite <- H20; auto.
+ rewrite <- H68; auto.
+ auto.
+ auto.
+ auto.
+ rewrite <- H42, <- H84; auto.
- assert (Hpperm: pperm d = pperm d´).
{ exploit INVLemmaSingleInterrupt.single_serial_intr_disable_preserves_all; eauto.
intros Htemp; blast Htemp; simpl in *; auto. }
inv H.
inv sh_mem_inv_re.
intros.
constructor; try rewritesb; auto.
intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss in H2; rewrite ZMap.gso in H3; auto.
inv H2.
unfold proc_id in H0; simpl in ×.
rewrite <- Hpperm in H4.
apply (pperm_disjoint (ZMap.get (CPU_ID sd´) (cid sd´)) j d pd´ H H0 H3 j0 H4).
+ rewrite ZMap.gso in H2; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H3.
inv H3.
unfold proc_id in H0; simpl in ×.
rewrite <- Hpperm.
apply (pperm_disjoint i (ZMap.get (CPU_ID sd´) (cid sd´)) pd d n H2 H0 j0 H4).
× rewrite ZMap.gso in H3; auto.
apply (pperm_disjoint i j pd pd´ H H2 H3 j0 H4).
Qed.
Transparent ObjPHBThreadDEV.single_serial_intr_disable.
Transparent serial_intr_disable_aux.
End SERIALINTRDISABLERELATED.
Section SERIALINTRENABLERELATED.
Opaque serial_intr_enable_aux.
Opaque ObjPHBThreadDEV.single_serial_intr_enable.
Lemma serial_intr_enable_related_mine:
∀ kctxt_val sd sd´ a d d´,
relate_RData_per_pd (proc_id sd) kctxt_val sd d a →
ObjPHBThreadDEV.single_serial_intr_enable_spec (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_enable_spec a = Some a´ ∧
relate_RData_per_pd (proc_id sd´) kctxt_val sd´ d´ a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
intros.
assert (in_intr_related:
relate_RData_per_pd (proc_id sd) kctxt_val sd (d {pv_in_intr: true})
a {in_intr: true}).
{ inv H; constructor; simpl in *; auto; try (rewrite zeq_true; auto).
inv inv_re; constructor; simpl; auto. }
functional inversion H0.
simpl in *; destruct abd´; simpl in ×.
unfold serial_intr_enable_spec.
Transparent uRData proc_id update.
subdestruct; simpl in *; inv H0;
inv H; rewrite zeq_true in *; subst; simpl in *; rewrite _x in *; rewrite zeq_true in *;
rewrite <- ikern_re, <- ihost_re, <- init_re, <- intr_flag_re, <- in_intr_re, <- ioapic_re.
rewrite H4, H5, H6, H7, H8, Hdestruct4, Hdestruct; rewrite <- _x in in_intr_related; subst.
simpl; inv H10; auto.
simpl; exploit serial_enable_aux_related; eauto; simpl in *; auto; try exact in_intr_related;
intros Htemp; destruct Htemp as (a´ & Hrelated_a & Hrelated_b & Hrelated_c & Hrelated_d & Hrelated_e);
subst.
rewrite Hrelated_a; simpl in Hrelated_d, Hrelated_e; refine_split´; eauto;
inv Hrelated_b; constructor; simpl in *; auto; try (rewrite _x); try (rewrite zeq_true; auto);
try (rewrite Hrelated_d; auto).
rewrite _x in ioapic_re0; rewrite zeq_true in ioapic_re0; rewrite ioapic_re0; auto.
inv inv_re0; constructor; intros; simpl; auto.
Opaque uRData proc_id update.
Qed.
Lemma serial_intr_enable_cid:
∀ sd sd´ d d´,
ObjPHBThreadDEV.single_serial_intr_enable_spec (sd, d) = Some (sd´, d´) →
proc_id sd = dev_handling_cid.
Proof.
intros; subst; simpl in *; functional inversion H; simpl in *; auto.
Qed.
Lemma serial_intr_enable_related_others:
∀ i kctxt_val sd sd´ a d d´ other_d a´,
i ≠ proc_id sd →
relate_RData_per_pd i kctxt_val sd other_d a →
ObjPHBThreadDEV.single_serial_intr_enable_spec (sd, d) = Some (sd´, d´) →
serial_intr_enable_spec a = Some a´ →
sd = sd´ →
kctxt a = kctxt a´ →
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´) →
relate_RData_per_pd i kctxt_val sd other_d a´.
Proof.
intros; subst.
exploit INVLemmaInterrupt.serial_intr_enable_preserves_all; eauto; simpl.
intros Hpre; blast Hpre.
assert (ZMap.get (CPU_ID sd´) (cid sd´) = dev_handling_cid).
{ exploit serial_intr_enable_cid; eauto. }
inv H0; simpl in ×.
constructor; simpl in *; rewritesb.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ rewrite <- CPU_ID_re in cid_re.
auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ unfold relate_AC_per_pd in *; simpl; auto.
rewrite <- H15; auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ auto.
+ rewrite zeq_false; auto; rewrite zeq_false in intr_flag_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in in_intr_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in com1_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in console_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in console_concrete_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in ioapic_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in lapic_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in curr_intr_num_re; auto.
+ rewrite zeq_false; auto; rewrite zeq_false in drv_serial_re; auto.
+ unfold relate_SyncChanPool_per_pd; unfold relate_SyncChanPool_per_pd in syncchpool_re.
rewrite <- H38.
auto.
+ unfold relate_uctxt_per_pd in *; simpl; auto.
rewrite <- H12.
auto.
+ rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re; auto.
+ rewrite CPU_ID_re; auto.
+ inv inv_re; constructor; simpl; intros.
auto.
Qed.
Lemma serial_intr_enable_related:
∀ kctxt_pool sd sd´ a d d´ dp,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
ObjPHBThreadDEV.single_serial_intr_enable_spec (sd, d) = Some (sd´, d´) →
∃ a´,
serial_intr_enable_spec a = Some a´ ∧
relate_RData kctxt_pool sd´ (ZMap.set (proc_id sd´) (Some d´) dp) a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
intros.
generalize (per_data_re _ _ _ _ H (proc_id sd)); intros Hper_data_rel.
rewrite H0 in Hper_data_rel.
exploit serial_intr_enable_related_mine; eauto; intros Hrel_m.
destruct Hrel_m as (a´ & Hrel_ma & Hrel_mb & Hrel_mc & Hrel_md & Hrel_me); subst.
∃ a´; refine_split; auto.
constructor; simpl; try (inv Hrel_mb; simpl; auto; fail).
- rewrite <- Hrel_md.
inv H; simpl; auto.
- intros.
inv H.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst; [rewrite ZMap.gss; auto |].
clear sh_cid_re.
subdestruct.
+ rewrite ZMap.gso; auto.
rewrite Hdestruct.
exploit serial_intr_enable_related_others; eauto; simpl; assumption.
+ simpl.
rewrite ZMap.gso; auto.
rewrite Hdestruct.
constructor.
- inv H.
inv sh_shared_inv_re.
exploit INVLemmaInterrupt.serial_intr_enable_preserves_all; eauto.
intros.
blast H.
constructor.
+ rewrite <- H43, <- H51; auto.
+ auto.
+ rewrite <- H42; auto.
+ rewrite <- H68; auto.
+ rewrite <- H66; auto.
+ rewrite <- H20; auto.
+ rewrite <- H68; auto.
+ auto.
+ auto.
+ auto.
+ rewrite <- H42, <- H81.
auto.
- assert (Hpperm: pperm d = pperm d´).
{ exploit INVLemmaSingleInterrupt.single_serial_intr_enable_preserves_all; eauto.
intros Htemp; blast Htemp; simpl in *; auto. }
inv H.
inv sh_mem_inv_re.
intros.
constructor; try rewritesb; auto.
intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss in H2; rewrite ZMap.gso in H3; auto.
inv H2.
Transparent proc_id.
unfold proc_id in H0; simpl in ×.
rewrite <- Hpperm in H4.
apply (pperm_disjoint (ZMap.get (CPU_ID sd´) (cid sd´)) j d pd´ H H0 H3 j0 H4).
+ rewrite ZMap.gso in H2; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H3.
inv H3.
unfold proc_id in H0; simpl in ×.
rewrite <- Hpperm.
apply (pperm_disjoint i (ZMap.get (CPU_ID sd´) (cid sd´)) pd d n H2 H0 j0 H4).
× rewrite ZMap.gso in H3; auto.
apply (pperm_disjoint i j pd pd´ H H2 H3 j0 H4).
Opaque proc_id.
Qed.
Transparent ObjPHBThreadDEV.single_serial_intr_enable.
Transparent serial_intr_enable_aux.
End SERIALINTRENABLERELATED.
Lemma serial_putc_related:
∀ kctxt_pool sd sd´ a d d´ dp c,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
ObjPHBThreadDEV.single_serial_putc_spec c (sd, d) = Some (sd´, d´) →
∃ a´,
serial_putc_spec c a = Some a´ ∧
relate_RData kctxt_pool sd´ (ZMap.set (proc_id sd´) (Some d´) dp) a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´).
Proof.
intros.
generalize (per_data_re _ _ _ _ H (proc_id sd)); intros Hper_data_rel.
rewrite H0 in Hper_data_rel.
inv Hper_data_rel; simpl.
Transparent uRData proc_id update.
functional inversion H1; inv H1; simpl in *; rewrite <- _x in *; rewrite zeq_true in *;
unfold serial_putc_spec; rewrite <- ikern_re, <- init_re, <- ihost_re, <- drv_serial_re, <- com1_re;
rewrite H5, H6, H7; try (rewrite _x0; rewrite zeq_true; rewrite H9; simpl; esplit; eauto);
try (rewrite zeq_false); auto.
- refine_split´; eauto.
inv H; constructor; simpl in *; eauto.
intros.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss; auto.
constructor; simpl; try (rewrite zeq_true); try (rewrite <- _x; rewrite zeq_true); auto.
inv inv_re; constructor; simpl; intros; auto.
+ rewrite ZMap.gso; auto.
case_eq (ZMap.get i dp); intros; auto.
× rewrite H1 in Hrel.
clear AC_re.
clear H8.
clear ept_re vmcs_re vmx_re.
subdestruct; auto.
inv Hrel; constructor; simpl in *; auto.
rewrite <- _x; rewrite zeq_false; auto.
inv inv_re0; constructor; simpl; auto.
× constructor.
+ inv sh_shared_inv_re.
constructor; simpl; auto.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). }
- refine_split´; eauto.
inv H; constructor; simpl in *; eauto.
intros.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss; auto.
constructor; simpl; try (rewrite zeq_true); try (rewrite <- _x; rewrite zeq_true); auto.
inv inv_re; constructor; simpl; intros; auto.
+ rewrite ZMap.gso; auto.
case_eq (ZMap.get i dp); intros; auto.
× rewrite H1 in Hrel.
clear AC_re.
clear ept_re vmcs_re vmx_re.
subdestruct; auto.
inv Hrel; constructor; simpl in *; auto.
rewrite <- _x; rewrite zeq_false; auto.
inv inv_re0; constructor; simpl; auto.
× constructor.
+ inv sh_shared_inv_re.
constructor; simpl; auto.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). }
- destruct _x12; try contradiction.
refine_split´; eauto.
inv H; constructor; simpl in *; eauto.
intros.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss; auto.
constructor; simpl; try (rewrite zeq_true); try (rewrite <- _x; rewrite zeq_true); auto.
inv inv_re; constructor; simpl; intros; auto.
+ rewrite ZMap.gso; auto.
case_eq (ZMap.get i dp); intros; auto.
× rewrite H1 in Hrel.
clear H8.
clear AC_re.
clear ept_re vmcs_re vmx_re.
subdestruct; auto.
inv Hrel; constructor; simpl in *; auto.
rewrite <- _x; rewrite zeq_false; auto.
inv inv_re0; constructor; simpl; auto.
× constructor.
+ inv sh_shared_inv_re.
constructor; simpl; auto.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). }
- destruct _x12; try contradiction.
rewrite H12.
refine_split´; eauto.
inv H; constructor; simpl in *; eauto.
intros.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss; auto.
constructor; simpl; try (rewrite zeq_true); try (rewrite <- _x; rewrite zeq_true); auto.
inv inv_re; constructor; simpl; intros; auto.
+ rewrite ZMap.gso; auto.
case_eq (ZMap.get i dp); intros; auto.
× rewrite H1 in Hrel.
clear H8.
clear AC_re.
clear ept_re vmcs_re vmx_re.
subdestruct; auto.
inv Hrel; constructor; simpl in *; auto.
rewrite <- _x; rewrite zeq_false; auto.
inv inv_re0; constructor; simpl; auto.
× constructor.
+ inv sh_shared_inv_re.
constructor; simpl; auto.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H1; rewrite ZMap.gso in H2; auto; simpl in ×.
inv H1.
simpl in H3.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H1; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
{ rewrite ZMap.gss in H2.
inv H2.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H2; auto.
apply (pperm_disjoint i j pd pd´ H H1 H2 j0 H3). }
- refine_split´; eauto.
eapply relate_RData_gss; auto.
Opaque uRData proc_id update.
Qed.
Lemma cons_buf_read_related:
∀ kctxt_pool sd sd´ a d d´ dp res,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
ObjPHBThreadDEV.single_cons_buf_read_spec (sd, d) = Some ((sd´, d´), res) →
∃ a´ res´,
cons_buf_read_spec a = Some (a´, res´) ∧
relate_RData kctxt_pool sd´ (ZMap.set (proc_id sd´) (Some d´) dp) a´ ∧
sd = sd´ ∧ kctxt a = kctxt a´ ∧
ZMap.get (AbstractDataType.CPU_ID a) (AbstractDataType.cid a) =
ZMap.get (AbstractDataType.CPU_ID a´) (AbstractDataType.cid a´) ∧ res = res´.
Proof.
intros.
generalize (per_data_re _ _ _ _ H (proc_id sd)); intros Hper_data_rel.
rewrite H0 in Hper_data_rel.
inv Hper_data_rel; simpl.
Transparent uRData proc_id update.
functional inversion H1; substx; unfold cons_buf_read_spec; simpl in *;
rewrite <- _x in *; simpl in *; rewrite zeq_true in *; auto;
rewrite <- ikern_re, <- ihost_re, <- console_re, <- init_re;
rewrite H6, H7, H8, H9; refine_split; eauto.
- eapply relate_RData_gss; auto.
- inv H; constructor; simpl in *; eauto.
intros.
generalize (per_data_re i); intros Hrel.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
+ rewrite ZMap.gss; auto.
constructor; simpl; try (rewrite zeq_true); try (rewrite <- _x; rewrite zeq_true); auto.
inv inv_re; constructor; simpl; auto.
+ rewrite ZMap.gso; auto.
case_eq (ZMap.get i dp); intros; auto.
× rewrite H2 in Hrel.
clear AC_re.
clear ept_re vmcs_re vmx_re.
subdestruct; auto.
inv Hrel; constructor; simpl in *; auto.
rewrite <- _x; rewrite zeq_false; auto.
inv inv_re0; constructor; simpl; auto.
× constructor.
+ inv sh_shared_inv_re.
constructor; simpl; auto.
+ inv sh_mem_inv_re.
constructor; simpl; intros.
case_eq (zeq i (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
× rewrite ZMap.gss in H2; rewrite ZMap.gso in H3; auto; simpl in ×.
inv H2.
simpl in H4.
eapply pperm_disjoint; eauto.
× rewrite ZMap.gso in H2; auto.
case_eq (zeq j (ZMap.get (CPU_ID sd´) (cid sd´))); intros; subst.
{ rewrite ZMap.gss in H3.
inv H3.
simpl.
eapply pperm_disjoint; eauto. }
{ rewrite ZMap.gso in H3; auto.
apply (pperm_disjoint i j pd pd´ H H2 H3 j0 H4). }
Opaque uRData proc_id update.
Qed.
End E2PBTHREADGENLEMMAFILE.