Library mcertikos.ipc.PIPCIntro
This file defines the abstract data and the primitives for the PThread layer,
which will introduce the primtives of thread
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 PrimTMSemantics.
Require Import LAsm.
Require Import LoadStoreSem3high.
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 CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealProcModule.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import AbstractDataType.
Require Export ObjFlatMem.
Require Import INVLemmaInterrupt.
Require Import INVLemmaDriver.
Require Import DeviceStateDataType.
Require Import FutureTactic.
Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.
Require Import ObjTMVMXINIT.
Require Import ObjSyncIPC.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import INVLemmaIntel.
Require Import IntelPrimSemantics.
Require Import CalRealIntelModule.
Require Import INVLemmaThreadContainer.
Require Import INVLemmaProc.
Export PIPCIntroInvariant.
Opaque full_thread_list.
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 PrimTMSemantics.
Require Import LAsm.
Require Import LoadStoreSem3high.
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 CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealProcModule.
Require Import INVLemmaMemory.
Require Import INVLemmaThread.
Require Import AbstractDataType.
Require Export ObjFlatMem.
Require Import INVLemmaInterrupt.
Require Import INVLemmaDriver.
Require Import DeviceStateDataType.
Require Import FutureTactic.
Require Export ObjTMVMM.
Require Export ObjTMSCHED.
Require Export ObjTMINTELVIRT.
Require Export ObjTMIPCDEVPRIM.
Require Import ObjTMVMXINIT.
Require Import ObjSyncIPC.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Require Import INVLemmaIntel.
Require Import IntelPrimSemantics.
Require Import CalRealIntelModule.
Require Import INVLemmaThreadContainer.
Require Import INVLemmaProc.
Export PIPCIntroInvariant.
Opaque full_thread_list.
Section WITHMEM.
Local Open Scope Z_scope.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Local Open Scope Z_scope.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Global Instance pipcintro_data_ops : CompatDataOps RData :=
{
empty_data := thread_init_rdata current_thread;
high_level_invariant := high_level_invariant;
low_level_invariant := low_level_invariant;
kernel_mode adt := ikern adt = true ∧ ihost adt = true
}.
{
empty_data := thread_init_rdata current_thread;
high_level_invariant := high_level_invariant;
low_level_invariant := low_level_invariant;
kernel_mode adt := ikern adt = true ∧ ihost adt = true
}.
Global Instance pipcintro_data_prf : CompatData RData.
Proof.
constructor.
- apply low_level_invariant_incr.
- intros; apply init_data_low_level_invariant.
- apply init_data_pipcintro_high_level_invariant.
Qed.
End Property_Abstract_Data.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Proof.
constructor.
- apply low_level_invariant_incr.
- intros; apply init_data_low_level_invariant.
- apply init_data_pipcintro_high_level_invariant.
Qed.
End Property_Abstract_Data.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section INV.
Section SC_lock.
Lemma acquire_lock_SC_high_level_inv:
∀ d d´ i,
big2_acquire_lock_SC_spec i d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma acquire_lock_SC_low_level_inv:
∀ d d´ i n,
big2_acquire_lock_SC_spec i d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto.
- inv H0. constructor; simpl; eauto.
Qed.
Lemma acquire_lock_SC_kernel_mode:
∀ d d´ i,
big2_acquire_lock_SC_spec i d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
Qed.
Global Instance acquire_lock_SC_inv: PreservesInvariants big2_acquire_lock_SC_spec.
Proof.
preserves_invariants_simpl´.
- eapply acquire_lock_SC_low_level_inv; eassumption.
- eapply acquire_lock_SC_high_level_inv; eassumption.
- eapply acquire_lock_SC_kernel_mode; eassumption.
Qed.
Lemma release_lock_SC_high_level_inv:
∀ d d´ i,
big2_release_lock_SC_spec i d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
constructor; simpl; eauto; intros.
Qed.
Lemma release_lock_SC_low_level_inv:
∀ d d´ i n,
big2_release_lock_SC_spec i d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
constructor; simpl; eauto; intros.
Qed.
Lemma release_lock_SC_kernel_mode:
∀ d d´ i,
big2_release_lock_SC_spec i d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
auto.
Qed.
Global Instance release_lock_SC_inv: PreservesInvariants big2_release_lock_SC_spec.
Proof.
preserves_invariants_simpl´.
- eapply release_lock_SC_low_level_inv; eassumption.
- eapply release_lock_SC_high_level_inv; eassumption.
- eapply release_lock_SC_kernel_mode; eassumption.
Qed.
End SC_lock.
Section SEND.
Lemma page_copy_high_level_inv:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ high_level_invariant d
→ high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0.
constructor; simpl; intros; eauto.
Qed.
Lemma page_copy_low_level_inv:
∀ d d´ chid cound addr n,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ low_level_invariant n d
→ low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto 2.
Qed.
Lemma page_copy_kernel_mode:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ kernel_mode d
→ kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
Lemma ipc_send_body_high_level_inv:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_high_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2; simpl; intros.
Qed.
Lemma ipc_send_body_low_level_inv:
∀ fromid vaddr count d d´ n n´,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_low_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2.
Qed.
Lemma ipc_send_body_kernel_mode:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_kernel_mode; eauto.
Qed.
Global Instance ipc_send_body_inv: PreservesInvariants thread_ipc_send_body_spec.
Proof.
preserves_invariants_simpl´.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_low_level_inv; eassumption.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_high_level_inv; eassumption.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_kernel_mode; eassumption.
Qed.
Lemma big2_thread_sleep_high_level_inv:
∀ chid d d´,
big2_thread_sleep_spec chid d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big2_thread_sleep_low_level_inv:
∀ chid d d´ n,
big2_thread_sleep_spec chid d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big2_thread_sleep_kernel_mode:
∀ chid d d´,
big2_thread_sleep_spec chid d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- simpl; eauto.
- simpl; eauto.
Qed.
Lemma syncsendto_chan_pre_high_level_inv:
∀ chid d d´,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- exploit acquire_lock_SC_high_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- eapply acquire_lock_SC_high_level_inv; eauto.
eapply big2_thread_sleep_high_level_inv; eauto.
eapply acquire_lock_SC_high_level_inv; eauto.
Qed.
Lemma syncsendto_chan_pre_low_level_inv:
∀ chid d d´ n,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- exploit acquire_lock_SC_low_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- eapply acquire_lock_SC_low_level_inv; eauto.
eapply big2_thread_sleep_low_level_inv; eauto.
eapply acquire_lock_SC_low_level_inv; eauto.
Qed.
Lemma syncsendto_chan_pre_kernel_mode:
∀ chid d d´,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- simpl.
eapply acquire_lock_SC_kernel_mode; eauto.
- eapply acquire_lock_SC_kernel_mode; eauto.
eapply big2_thread_sleep_kernel_mode; eauto.
eapply acquire_lock_SC_kernel_mode; eauto.
Qed.
Global Instance syncsendto_chan_pre_inv: PreservesInvariants thread_syncsendto_chan_pre_spec.
Proof.
preserves_invariants_simpl´.
- eapply syncsendto_chan_pre_low_level_inv; eassumption.
- eapply syncsendto_chan_pre_high_level_inv; eassumption.
- eapply syncsendto_chan_pre_kernel_mode; eassumption.
Qed.
End SEND.
Section RECEIVE.
Lemma page_copy_back_high_level_inv:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ high_level_invariant d
→ high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0.
constructor; simpl; intros;
try eapply dirty_ppage´_gss_page_copy_back; eauto.
Qed.
Lemma page_copy_back_low_level_inv:
∀ d d´ chid cound addr n,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ low_level_invariant n d
→ low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto 2.
Qed.
Lemma page_copy_back_kernel_mode:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ kernel_mode d
→ kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
Lemma ipc_receive_body_high_level_inv:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_high_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2; simpl; intros.
Qed.
Lemma ipc_receive_body_low_level_inv:
∀ fromid vaddr count d d´ n n´,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_low_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2.
Qed.
Lemma ipc_receive_body_kernel_mode:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_kernel_mode; eauto.
Qed.
Lemma big_thread_wakeup_high_level_inv:
∀ chid d d´ r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big_thread_wakeup_low_level_inv:
∀ chid d d´ n r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big_thread_wakeup_kernel_mode:
∀ chid d d´ r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
Qed.
Lemma tryreceive_chan_high_level_inv:
∀ chanid vaddr count d d´ n,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_high_level_inv; eauto. intros.
exploit big_thread_wakeup_high_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- exploit ipc_receive_body_high_level_inv; eauto. intros.
exploit big_thread_wakeup_high_level_inv; eauto.
Qed.
Lemma tryreceive_chan_low_level_inv:
∀ chanid vaddr count d d´ n n´,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_low_level_inv; eauto. intros.
exploit big_thread_wakeup_low_level_inv; eauto.
intros Hlow. inv Hlow.
constructor; simpl; eauto; intros.
- exploit ipc_receive_body_low_level_inv; eauto. intros.
exploit big_thread_wakeup_low_level_inv; eauto.
Qed.
Lemma tryreceive_chan_kernel_mode:
∀ chanid vaddr count d d´ n,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_kernel_mode; eauto. intros.
exploit big_thread_wakeup_kernel_mode; eauto.
- exploit ipc_receive_body_kernel_mode; eauto. intros.
exploit big_thread_wakeup_kernel_mode; eauto.
Qed.
Global Instance tryreceive_chan_inv: PreservesInvariants thread_tryreceive_chan_spec.
Proof.
preserves_invariants_simpl´.
- eapply tryreceive_chan_low_level_inv; eassumption.
- eapply tryreceive_chan_high_level_inv; eassumption.
- eapply tryreceive_chan_kernel_mode; eassumption.
Qed.
End RECEIVE.
Global Instance cli_inv: PreservesInvariants thread_cli_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance sti_inv: PreservesInvariants thread_sti_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance cons_buf_read_inv: PreservesInvariants thread_cons_buf_read_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance serial_putc_inv: PreservesInvariants thread_serial_putc_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance serial_intr_disable_inv: PreservesInvariants thread_serial_intr_disable_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_disable_invariantdb.
generalize (serial_intr_disable_preserves_tf _ _ H); intro tmprw; rewrite <- tmprw; assumption.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_disable_invariantdb; rest.
- functional inversion H2; subst.
eauto 2 with serial_intr_disable_invariantdb.
Qed.
Global Instance serial_intr_enable_inv: PreservesInvariants thread_serial_intr_enable_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_enable_invariantdb.
generalize (serial_intr_enable_preserves_tf _ _ H); intro tmprw; rewrite <- tmprw; assumption.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_enable_invariantdb; rest.
- functional inversion H2; subst.
eauto 2 with serial_intr_enable_invariantdb.
Qed.
Section PALLOC.
Lemma palloc_high_level_inv:
∀ d d´ i n,
big2_palloc_spec i d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; subst; eauto;
inv H0; constructor; simpl; eauto; intros.
+ eapply alloc_thread_container_valid´; eauto.
+ subst; simpl;
intros; congruence.
+ eapply dirty_ppage´_gso_alloc; eauto.
Qed.
Lemma palloc_low_level_inv:
∀ d d´ i n n´,
big2_palloc_spec i d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; subst; eauto;
inv H0; constructor; eauto.
Qed.
Lemma palloc_kernel_mode:
∀ d d´ i n,
big2_palloc_spec i d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; simpl; eauto.
Qed.
Global Instance palloc_inv: PreservesInvariants big2_palloc_spec.
Proof.
preserves_invariants_simpl´.
- eapply palloc_low_level_inv; eassumption.
- eapply palloc_high_level_inv; eassumption.
- eapply palloc_kernel_mode; eassumption.
Qed.
End PALLOC.
Global Instance hostin_inv: PrimInvariants thread_hostin_spec.
Proof.
Thread_PrimInvariants_simpl_auto.
Qed.
Global Instance hostout_inv: PrimInvariants thread_hostout_spec.
Proof.
Thread_PrimInvariants_simpl_auto.
Qed.
Global Instance setPT_inv: PreservesInvariants thread_setPT_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Section PTINSERT.
Section PTINSERT_PTE.
Lemma big2_ptInsertPTE_high_level_inv:
∀ d d´ n vadr padr p,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0; constructor_gso_simpl_tac; intros.
- eapply PMap_valid_gso_valid; eauto.
- functional inversion H2. functional inversion H1.
eapply PMap_kern_gso; eauto.
Qed.
Lemma big2_ptInsertPTE_low_level_inv:
∀ d d´ n vadr padr p n´,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto.
Qed.
Lemma big2_ptInsertPTE_kernel_mode:
∀ d d´ n vadr padr p,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
End PTINSERT_PTE.
Section PTPALLOCPDE.
Lemma big2_palloc_inv_prop:
∀ n d d´ v,
big2_palloc_spec n d = Some (d´, v) →
ptpool d´ = ptpool d
∧ (v ≠ 0 →
ZMap.get v (pperm d´) = PGAlloc
∧ 0 < v < nps d´)
∧ pg d´ = true.
Proof.
unfold big2_palloc_spec. intros.
subdestruct; inv H; simpl; subst.
- repeat rewrite ZMap.gss. refine_split´; trivial.
destruct a0 as (? & ? & ?). intros.
refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Lemma big2_ptAllocPDE_high_level_inv:
∀ d d´ n vadr v,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_high_level_inv; eauto.
- exploit palloc_high_level_inv; eauto.
intros.
exploit big2_palloc_inv_prop; eauto. intros (HPT & Halloc & Hpg).
clear H11.
rewrite <- HPT in ×.
inv H1; constructor_gso_simpl_tac; try (intros; congruence); intros.
+ eapply PMap_valid_gso_pde_unp; eauto.
eapply real_init_PTE_defined.
+ functional inversion H3.
eapply PMap_kern_gso; eauto.
+ eapply dirty_ppage´_gss; eauto.
Qed.
Lemma big2_ptAllocPDE_low_level_inv:
∀ d d´ n vadr v n´,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_low_level_inv; eauto.
- exploit palloc_low_level_inv; eauto.
intros. inv H1. constructor; eauto.
Qed.
Lemma big2_ptAllocPDE_kernel_mode:
∀ d d´ n vadr v,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_kernel_mode; eauto.
- exploit palloc_kernel_mode; eauto.
Qed.
End PTPALLOCPDE.
Lemma big2_ptInsert_high_level_inv:
∀ d d´ n vadr padr p v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_high_level_inv; eassumption.
- eapply big2_ptAllocPDE_high_level_inv; eassumption.
- eapply big2_ptInsertPTE_high_level_inv; try eassumption.
eapply big2_ptAllocPDE_high_level_inv; eassumption.
Qed.
Lemma big2_ptInsert_low_level_inv:
∀ d d´ n vadr padr p n´ v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_low_level_inv; eassumption.
- eapply big2_ptAllocPDE_low_level_inv; eassumption.
- eapply big2_ptInsertPTE_low_level_inv; try eassumption.
eapply big2_ptAllocPDE_low_level_inv; eassumption.
Qed.
Lemma big2_ptInsert_kernel_mode:
∀ d d´ n vadr padr p v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_kernel_mode; eassumption.
- eapply big2_ptAllocPDE_kernel_mode; eassumption.
- eapply big2_ptInsertPTE_kernel_mode; try eassumption.
eapply big2_ptAllocPDE_kernel_mode; eassumption.
Qed.
End PTINSERT.
Section PTRESV.
Lemma big2_ptResv_high_level_inv:
∀ d d´ n vadr p v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto; clear H.
- eapply palloc_high_level_inv; eassumption.
- eapply big2_ptInsert_high_level_inv; try eassumption.
eapply palloc_high_level_inv; eassumption.
Qed.
Lemma big2_ptResv_low_level_inv:
∀ d d´ n vadr p n´ v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_low_level_inv; eassumption.
- eapply big2_ptInsert_low_level_inv; try eassumption.
eapply palloc_low_level_inv; eassumption.
Qed.
Lemma big2_ptResv_kernel_mode:
∀ d d´ n vadr p v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
eapply palloc_kernel_mode; eassumption.
eapply big2_ptInsert_kernel_mode; try eassumption.
eapply palloc_kernel_mode; eassumption.
Qed.
Global Instance big2_ptResv_inv: PreservesInvariants big2_ptResv_spec.
Proof.
preserves_invariants_simpl´.
- eapply big2_ptResv_low_level_inv; eassumption.
- eapply big2_ptResv_high_level_inv; eassumption.
- eapply big2_ptResv_kernel_mode; eassumption.
Qed.
End PTRESV.
Global Instance big2_proc_create_inv: PCreateInvariants big2_proc_create_spec.
Proof.
constructor; intros; inv H0;
unfold big2_proc_create_spec in *;
subdestruct; inv H; simpl; auto.
-
constructor; trivial; intros; simpl in ×.
-
assert (Hrdyq: 0 ≤ rdy_q_id (CPU_ID d) < num_chan).
{
unfold rdy_q_id. omega.
}
constructor; simpl; eauto 2; try congruence; intros.
exploit split_thread_container_valid; eauto.
simpl. omega.
Qed.
Global Instance sched_init_inv: PreservesInvariants big2_sched_init_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant.
- apply real_nps_range.
- apply thread_AC_init_container_valid.
- eapply real_pt_PMap_valid; eauto.
- apply real_pt_PMap_kern.
- omega.
- assumption.
- apply real_idpde_init.
- erewrite real_valid_cidpool; eauto.
omega.
Qed.
Local Opaque remove.
Section YIELD.
Global Instance thread_yield_inv: PreservesInvariants big2_thread_yield_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
End YIELD.
Global Instance thread_uctx_set_inv: PreservesInvariants thread_uctx_set_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
eapply uctxt_inject_neutral_gss; eauto.
eapply uctxt_inject_neutral0_gss; eauto.
eapply uctxt_inject_neutral0_Vint.
Qed.
Global Instance thread_proc_start_user_inv: TMStartUserInvariants thread_proc_start_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
- subst. constructor; auto; simpl in *; intros; congruence.
Qed.
Global Instance thread_proc_exit_user_inv: TMExitUserInvariants thread_proc_exit_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
simpl.
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
eapply uctxt_inject_neutral0_init.
- constructor; auto; simpl in *; intros.
inv H0.
Qed.
Global Instance thread_proc_start_user_inv2: TMStartUserInvariants2 thread_proc_start_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
- subst. constructor; auto; simpl in *; intros; congruence.
Qed.
Global Instance thread_proc_exit_user_inv2: TMExitUserInvariants2 thread_proc_exit_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
eapply uctxt_inject_neutral0_init.
- constructor; auto; simpl in *; intros.
inv H0.
Qed.
Global Instance proc_create_postinit_inv:
PreservesInvariants thread_proc_create_postinit_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Section INTELVMSUPPORT.
Section THREAD_INTERCEPT_INTWIN.
Lemma thread_vmx_set_intercept_intwin_high_inv:
∀ d d´ i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H.
functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_intercept_intwin_low_inv:
∀ d d´ n i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H;
functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_intercept_intwin_kernel_mode:
∀ d d´ i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_intercept_intwin_inv: PreservesInvariants thread_vmx_set_intercept_intwin_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_intercept_intwin_low_inv; eauto.
- eapply thread_vmx_set_intercept_intwin_high_inv; eauto.
- eapply thread_vmx_set_intercept_intwin_kernel_mode; eauto.
Qed.
End THREAD_INTERCEPT_INTWIN.
Section THREAD_SET_DESC1.
Lemma thread_vmx_set_desc1_high_inv:
∀ d d´ i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_desc1_low_inv:
∀ d d´ n i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
functional inversion H9.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_desc1_kernel_mode:
∀ d d´ i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_desc1_inv: PreservesInvariants thread_vmx_set_desc1_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_desc1_low_inv; eauto.
- eapply thread_vmx_set_desc1_high_inv; eauto.
- eapply thread_vmx_set_desc1_kernel_mode; eauto.
Qed.
End THREAD_SET_DESC1.
Section THREAD_SET_DESC2.
Lemma thread_vmx_set_desc2_high_inv:
∀ d d´ i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_desc2_low_inv:
∀ d d´ n i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
functional inversion H9.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_desc2_kernel_mode:
∀ d d´ i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_desc2_inv: PreservesInvariants thread_vmx_set_desc2_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_desc2_low_inv; eauto.
- eapply thread_vmx_set_desc2_high_inv; eauto.
- eapply thread_vmx_set_desc2_kernel_mode; eauto.
Qed.
End THREAD_SET_DESC2.
Section THREAD_INJECT_EVENT.
Lemma thread_vmx_inject_event_high_inv:
∀ d d´ i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_inject_event_low_inv:
∀ d d´ n i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_inject_event_kernel_mode:
∀ d d´ i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_inject_event_inv: PreservesInvariants thread_vmx_inject_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_inject_event_low_inv; eauto.
- eapply thread_vmx_inject_event_high_inv; eauto.
- eapply thread_vmx_inject_event_kernel_mode; eauto.
Qed.
End THREAD_INJECT_EVENT.
Section THREAD_SET_TSC_OFFSET.
Lemma thread_vmx_set_tsc_offset_high_inv:
∀ d d´ i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_tsc_offset_low_inv:
∀ d d´ n i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_tsc_offset_kernel_mode:
∀ d d´ i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_tsc_offset_inv: PreservesInvariants thread_vmx_set_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_tsc_offset_low_inv; eauto.
- eapply thread_vmx_set_tsc_offset_high_inv; eauto.
- eapply thread_vmx_set_tsc_offset_kernel_mode; eauto.
Qed.
End THREAD_SET_TSC_OFFSET.
Section THREAD_SET_REG.
Lemma thread_vmx_set_reg_high_inv:
∀ d d´ i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_reg_low_inv:
∀ d d´ n i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; eapply VMX_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_reg_kernel_mode:
∀ d d´ i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_reg_inv: PreservesInvariants thread_vmx_set_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_reg_low_inv; eauto.
- eapply thread_vmx_set_reg_high_inv; eauto.
- eapply thread_vmx_set_reg_kernel_mode; eauto.
Qed.
End THREAD_SET_REG.
Section THREAD_SET_MMAP.
Lemma thread_vmx_set_mmap_high_inv:
∀ d d´ i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros.
inv H0; functional inversion H; functional inversion H0; functional inversion H5; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_mmap_low_inv:
∀ d d´ n i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
inv H0; functional inversion H; functional inversion H0; functional inversion H5; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_mmap_kernel_mode:
∀ d d´ i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H;
functional inversion H1; functional inversion H6; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_mmap_inv: PreservesInvariants thread_vmx_set_mmap_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_mmap_low_inv; eauto.
- eapply thread_vmx_set_mmap_high_inv; eauto.
- eapply thread_vmx_set_mmap_kernel_mode; eauto.
Qed.
End THREAD_SET_MMAP.
Global Instance thread_vmx_run_inv: VMXEnterInvariants thread_vm_run_spec.
Proof.
constructor; intros;
unfold thread_vm_run_spec in *;
unfold ObjVMX.vm_run_spec in *;
subdestruct; inv H; simpl; auto.
-
inv H1. constructor; trivial; intros; simpl in ×.
+ unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
× rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
× rewrite ZMap.gso; eauto.
+ unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
× rewrite ZMap.gss.
eapply VMX_inject_neutral_gss_enter; eauto.
× rewrite ZMap.gso; eauto.
-
inv H0. constructor; simpl; eauto 2; try congruence; intros.
Qed.
Global Instance thread_vmx_return_from_guest_inv: VMXReturnInvariants thread_vmx_return_from_guest_spec.
Proof.
constructor; intros;
unfold thread_vmx_return_from_guest_spec in *;
unfold ObjVMX.vmx_return_from_guest_spec in *;
subdestruct; inv H; simpl; auto.
-
inv H0. constructor; trivial; intros; simpl in ×.
unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; repeat eapply VMX_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
-
inv H0. constructor; simpl; eauto 2; try congruence; intros.
Qed.
Global Instance thread_vmx_init_inv: VMCSSetDefaultsInvariants thread_vmx_init_spec.
Proof.
constructor; intros; functional inversion H.
-
functional inversion H7; simpl; auto; simpl in ×.
inv H6; constructor; trivial; intros; simpl in *; eauto.
+ eapply real_vmcs_inject_neutral; eauto.
+ eapply real_vmx_inject_neutral; eauto.
-
functional inversion H1; simpl; auto; simpl in ×.
inv H0. constructor; simpl; try congruence; intros; eauto.
-
functional inversion H1; simpl; auto.
Qed.
End INTELVMSUPPORT.
End INV.
Definition exec_loadex {F V} := exec_loadex3high (F := F) (V := V).
Definition exec_storeex {F V} := exec_storeex3high (flatmem_store:= flatmem_store) (F := F) (V := V).
Global Instance flatmem_store_inv: FlatmemStoreInvariant (flatmem_store:= flatmem_store).
Proof.
split; inversion 1; intros.
- functional inversion H0. split; trivial.
- functional inversion H1.
split; simpl; try (eapply dirty_ppage´_store_unmapped´; try reflexivity; try eassumption); trivial.
Qed.
Global Instance trapinfo_set_inv: TrapinfoSetInvariant.
Proof.
split; inversion 1; intros; constructor; auto.
Qed.
Definition pipcintro_fresh : compatlayer (cdata RData) :=
syncsendto_chan_pre ↦ gensem thread_syncsendto_chan_pre_spec
⊕ tryreceive_chan ↦ gensem thread_tryreceive_chan_spec.
Definition pipcintro_passthrough : compatlayer (cdata RData) :=
vmxinfo_get ↦ gensem thread_vmxinfo_get_spec
⊕ palloc ↦ gensem big2_palloc_spec
⊕ set_pt ↦ gensem thread_setPT_spec
⊕ pt_read ↦ gensem thread_ptRead_spec
⊕ pt_resv ↦ gensem big2_ptResv_spec
⊕ thread_yield ↦ gensem big2_thread_yield_spec
⊕ sched_init ↦ gensem big2_sched_init_spec
⊕ uctx_get ↦ gensem thread_uctx_get_spec
⊕ uctx_set ↦ gensem thread_uctx_set_spec
⊕ proc_create ↦ proc_create_compatsem big2_proc_create_spec
⊕ container_get_nchildren ↦ gensem thread_container_get_nchildren_spec
⊕ container_get_quota ↦ gensem thread_container_get_quota_spec
⊕ container_get_usage ↦ gensem thread_container_get_usage_spec
⊕ container_can_consume ↦ gensem thread_container_can_consume_spec
⊕ get_CPU_ID ↦ gensem thread_get_CPU_ID_spec
⊕ get_curid ↦ gensem thread_get_curid_spec
⊕ acquire_lock_CHAN ↦ gensem big2_acquire_lock_SC_spec
⊕ release_lock_CHAN ↦ gensem big2_release_lock_SC_spec
⊕ ipc_send_body ↦ gensem thread_ipc_send_body_spec
⊕ rdmsr ↦ gensem thread_rdmsr_spec
⊕ wrmsr ↦ gensem thread_wrmsr_spec
⊕ vmx_set_intercept_intwin ↦ gensem thread_vmx_set_intercept_intwin_spec
⊕ vmx_set_desc1 ↦ gensem thread_vmx_set_desc1_spec
⊕ vmx_set_desc2 ↦ gensem thread_vmx_set_desc2_spec
⊕ vmx_inject_event ↦ gensem thread_vmx_inject_event_spec
⊕ vmx_set_tsc_offset ↦ gensem thread_vmx_set_tsc_offset_spec
⊕ vmx_get_tsc_offset ↦ gensem thread_vmx_get_tsc_offset_spec
⊕ vmx_get_exit_reason ↦ gensem thread_vmx_get_exit_reason_spec
⊕ vmx_get_exit_fault_addr ↦ gensem thread_vmx_get_exit_fault_addr_spec
⊕ vmx_get_exit_qualification ↦ gensem thread_vmx_get_exit_qualification_spec
⊕ vmx_check_pending_event ↦ gensem thread_vmx_check_pending_event_spec
⊕ vmx_check_int_shadow ↦ gensem thread_vmx_check_int_shadow_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ vmx_get_io_width ↦ gensem thread_vmx_get_io_width_spec
⊕ vmx_get_io_write ↦ gensem thread_vmx_get_io_write_spec
⊕ vmx_get_exit_io_rep ↦ gensem thread_vmx_get_exit_io_rep_spec
⊕ vmx_get_exit_io_str ↦ gensem thread_vmx_get_exit_io_str_spec
⊕ vmx_get_exit_io_port ↦ gensem thread_vmx_get_exit_io_port_spec
⊕ vmx_set_mmap ↦ gensem thread_vmx_set_mmap_spec
⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm
⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec
⊕ vmx_init ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec
⊕ cli ↦ gensem thread_cli_spec
⊕ sti ↦ gensem thread_sti_spec
⊕ serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ serial_putc ↦ gensem thread_serial_putc_spec
⊕ cons_buf_read ↦ gensem thread_cons_buf_read_spec
⊕ host_in ↦ primcall_general_compatsem thread_hostin_spec
⊕ host_out ↦ primcall_general_compatsem thread_hostout_spec
⊕ proc_create_postinit ↦ gensem thread_proc_create_postinit_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec
⊕ proc_start_user ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec
⊕ proc_exit_user ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec
⊕ proc_start_user2 ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec
⊕ proc_exit_user2 ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec
⊕ accessors ↦ {| exec_load := @exec_loadex; exec_store := @exec_storeex |}.
Definition pipcintro : compatlayer (cdata RData) := pipcintro_fresh ⊕ pipcintro_passthrough.
End WITHMEM.
Section SC_lock.
Lemma acquire_lock_SC_high_level_inv:
∀ d d´ i,
big2_acquire_lock_SC_spec i d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma acquire_lock_SC_low_level_inv:
∀ d d´ i n,
big2_acquire_lock_SC_spec i d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto.
- inv H0. constructor; simpl; eauto.
Qed.
Lemma acquire_lock_SC_kernel_mode:
∀ d d´ i,
big2_acquire_lock_SC_spec i d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
unfold big2_acquire_lock_SC_spec; intros.
subdestruct; inv H; eauto.
Qed.
Global Instance acquire_lock_SC_inv: PreservesInvariants big2_acquire_lock_SC_spec.
Proof.
preserves_invariants_simpl´.
- eapply acquire_lock_SC_low_level_inv; eassumption.
- eapply acquire_lock_SC_high_level_inv; eassumption.
- eapply acquire_lock_SC_kernel_mode; eassumption.
Qed.
Lemma release_lock_SC_high_level_inv:
∀ d d´ i,
big2_release_lock_SC_spec i d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
constructor; simpl; eauto; intros.
Qed.
Lemma release_lock_SC_low_level_inv:
∀ d d´ i n,
big2_release_lock_SC_spec i d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
constructor; simpl; eauto; intros.
Qed.
Lemma release_lock_SC_kernel_mode:
∀ d d´ i,
big2_release_lock_SC_spec i d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros.
unfold big2_release_lock_SC_spec in *;
unfold ObjBigThread.big_release_lock_SC_spec in *; subdestruct; inv H.
inv H0.
auto.
Qed.
Global Instance release_lock_SC_inv: PreservesInvariants big2_release_lock_SC_spec.
Proof.
preserves_invariants_simpl´.
- eapply release_lock_SC_low_level_inv; eassumption.
- eapply release_lock_SC_high_level_inv; eassumption.
- eapply release_lock_SC_kernel_mode; eassumption.
Qed.
End SC_lock.
Section SEND.
Lemma page_copy_high_level_inv:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ high_level_invariant d
→ high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0.
constructor; simpl; intros; eauto.
Qed.
Lemma page_copy_low_level_inv:
∀ d d´ chid cound addr n,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ low_level_invariant n d
→ low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto 2.
Qed.
Lemma page_copy_kernel_mode:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_spec chid cound addr d = Some d´
→ kernel_mode d
→ kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
Lemma ipc_send_body_high_level_inv:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_high_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2; simpl; intros.
Qed.
Lemma ipc_send_body_low_level_inv:
∀ fromid vaddr count d d´ n n´,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_low_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2.
Qed.
Lemma ipc_send_body_kernel_mode:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_send_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_kernel_mode; eauto.
Qed.
Global Instance ipc_send_body_inv: PreservesInvariants thread_ipc_send_body_spec.
Proof.
preserves_invariants_simpl´.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_low_level_inv; eassumption.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_high_level_inv; eassumption.
- unfold thread_ipc_send_body_spec in H2; subdestruct.
eapply ipc_send_body_kernel_mode; eassumption.
Qed.
Lemma big2_thread_sleep_high_level_inv:
∀ chid d d´,
big2_thread_sleep_spec chid d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big2_thread_sleep_low_level_inv:
∀ chid d d´ n,
big2_thread_sleep_spec chid d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big2_thread_sleep_kernel_mode:
∀ chid d d´,
big2_thread_sleep_spec chid d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold big2_thread_sleep_spec in ×. subdestruct; inv H.
- simpl; eauto.
- simpl; eauto.
Qed.
Lemma syncsendto_chan_pre_high_level_inv:
∀ chid d d´,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- exploit acquire_lock_SC_high_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- eapply acquire_lock_SC_high_level_inv; eauto.
eapply big2_thread_sleep_high_level_inv; eauto.
eapply acquire_lock_SC_high_level_inv; eauto.
Qed.
Lemma syncsendto_chan_pre_low_level_inv:
∀ chid d d´ n,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- exploit acquire_lock_SC_low_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- eapply acquire_lock_SC_low_level_inv; eauto.
eapply big2_thread_sleep_low_level_inv; eauto.
eapply acquire_lock_SC_low_level_inv; eauto.
Qed.
Lemma syncsendto_chan_pre_kernel_mode:
∀ chid d d´,
thread_syncsendto_chan_pre_spec chid d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold thread_syncsendto_chan_pre_spec in ×. subdestruct; inv H.
- simpl.
eapply acquire_lock_SC_kernel_mode; eauto.
- eapply acquire_lock_SC_kernel_mode; eauto.
eapply big2_thread_sleep_kernel_mode; eauto.
eapply acquire_lock_SC_kernel_mode; eauto.
Qed.
Global Instance syncsendto_chan_pre_inv: PreservesInvariants thread_syncsendto_chan_pre_spec.
Proof.
preserves_invariants_simpl´.
- eapply syncsendto_chan_pre_low_level_inv; eassumption.
- eapply syncsendto_chan_pre_high_level_inv; eassumption.
- eapply syncsendto_chan_pre_kernel_mode; eassumption.
Qed.
End SEND.
Section RECEIVE.
Lemma page_copy_back_high_level_inv:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ high_level_invariant d
→ high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0.
constructor; simpl; intros;
try eapply dirty_ppage´_gss_page_copy_back; eauto.
Qed.
Lemma page_copy_back_low_level_inv:
∀ d d´ chid cound addr n,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ low_level_invariant n d
→ low_level_invariant n d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto 2.
Qed.
Lemma page_copy_back_kernel_mode:
∀ d d´ chid cound addr,
ObjBigThread.big_page_copy_back_spec chid cound addr d = Some d´
→ kernel_mode d
→ kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
Lemma ipc_receive_body_high_level_inv:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_high_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2; simpl; intros.
Qed.
Lemma ipc_receive_body_low_level_inv:
∀ fromid vaddr count d d´ n n´,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_low_level_inv; eauto.
intros Hh. inv Hh. constructor; eauto 2.
Qed.
Lemma ipc_receive_body_kernel_mode:
∀ fromid vaddr count d d´ n,
ObjBigThread.big_ipc_receive_body_spec fromid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
exploit page_copy_back_kernel_mode; eauto.
Qed.
Lemma big_thread_wakeup_high_level_inv:
∀ chid d d´ r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big_thread_wakeup_low_level_inv:
∀ chid d d´ n r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
- inv H0. constructor; simpl; eauto; intros.
Qed.
Lemma big_thread_wakeup_kernel_mode:
∀ chid d d´ r,
big2_thread_wakeup_spec chid d = Some (d´, r) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold big2_thread_wakeup_spec in ×. subdestruct; inv H; eauto.
Qed.
Lemma tryreceive_chan_high_level_inv:
∀ chanid vaddr count d d´ n,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_high_level_inv; eauto. intros.
exploit big_thread_wakeup_high_level_inv; eauto.
intros Hhigh. inv Hhigh.
constructor; simpl; eauto; intros.
- exploit ipc_receive_body_high_level_inv; eauto. intros.
exploit big_thread_wakeup_high_level_inv; eauto.
Qed.
Lemma tryreceive_chan_low_level_inv:
∀ chanid vaddr count d d´ n n´,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_low_level_inv; eauto. intros.
exploit big_thread_wakeup_low_level_inv; eauto.
intros Hlow. inv Hlow.
constructor; simpl; eauto; intros.
- exploit ipc_receive_body_low_level_inv; eauto. intros.
exploit big_thread_wakeup_low_level_inv; eauto.
Qed.
Lemma tryreceive_chan_kernel_mode:
∀ chanid vaddr count d d´ n,
thread_tryreceive_chan_spec chanid vaddr count d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. unfold thread_tryreceive_chan_spec in ×.
unfold thread_ipc_receive_body_spec in ×.
subdestruct; inv H; eauto.
- exploit ipc_receive_body_kernel_mode; eauto. intros.
exploit big_thread_wakeup_kernel_mode; eauto.
- exploit ipc_receive_body_kernel_mode; eauto. intros.
exploit big_thread_wakeup_kernel_mode; eauto.
Qed.
Global Instance tryreceive_chan_inv: PreservesInvariants thread_tryreceive_chan_spec.
Proof.
preserves_invariants_simpl´.
- eapply tryreceive_chan_low_level_inv; eassumption.
- eapply tryreceive_chan_high_level_inv; eassumption.
- eapply tryreceive_chan_kernel_mode; eassumption.
Qed.
End RECEIVE.
Global Instance cli_inv: PreservesInvariants thread_cli_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance sti_inv: PreservesInvariants thread_sti_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance cons_buf_read_inv: PreservesInvariants thread_cons_buf_read_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance serial_putc_inv: PreservesInvariants thread_serial_putc_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Global Instance serial_intr_disable_inv: PreservesInvariants thread_serial_intr_disable_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_disable_invariantdb.
generalize (serial_intr_disable_preserves_tf _ _ H); intro tmprw; rewrite <- tmprw; assumption.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_disable_invariantdb; rest.
- functional inversion H2; subst.
eauto 2 with serial_intr_disable_invariantdb.
Qed.
Global Instance serial_intr_enable_inv: PreservesInvariants thread_serial_intr_enable_spec.
Proof.
constructor; simpl; intros; inv_generic_sem H.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_enable_invariantdb.
generalize (serial_intr_enable_preserves_tf _ _ H); intro tmprw; rewrite <- tmprw; assumption.
- functional inversion H2; subst.
inversion H0; econstructor; eauto 2 with serial_intr_enable_invariantdb; rest.
- functional inversion H2; subst.
eauto 2 with serial_intr_enable_invariantdb.
Qed.
Section PALLOC.
Lemma palloc_high_level_inv:
∀ d d´ i n,
big2_palloc_spec i d = Some (d´, n) →
high_level_invariant d →
high_level_invariant d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; subst; eauto;
inv H0; constructor; simpl; eauto; intros.
+ eapply alloc_thread_container_valid´; eauto.
+ subst; simpl;
intros; congruence.
+ eapply dirty_ppage´_gso_alloc; eauto.
Qed.
Lemma palloc_low_level_inv:
∀ d d´ i n n´,
big2_palloc_spec i d = Some (d´, n) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; subst; eauto;
inv H0; constructor; eauto.
Qed.
Lemma palloc_kernel_mode:
∀ d d´ i n,
big2_palloc_spec i d = Some (d´, n) →
kernel_mode d →
kernel_mode d´.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; simpl; eauto.
Qed.
Global Instance palloc_inv: PreservesInvariants big2_palloc_spec.
Proof.
preserves_invariants_simpl´.
- eapply palloc_low_level_inv; eassumption.
- eapply palloc_high_level_inv; eassumption.
- eapply palloc_kernel_mode; eassumption.
Qed.
End PALLOC.
Global Instance hostin_inv: PrimInvariants thread_hostin_spec.
Proof.
Thread_PrimInvariants_simpl_auto.
Qed.
Global Instance hostout_inv: PrimInvariants thread_hostout_spec.
Proof.
Thread_PrimInvariants_simpl_auto.
Qed.
Global Instance setPT_inv: PreservesInvariants thread_setPT_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Section PTINSERT.
Section PTINSERT_PTE.
Lemma big2_ptInsertPTE_high_level_inv:
∀ d d´ n vadr padr p,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0; constructor_gso_simpl_tac; intros.
- eapply PMap_valid_gso_valid; eauto.
- functional inversion H2. functional inversion H1.
eapply PMap_kern_gso; eauto.
Qed.
Lemma big2_ptInsertPTE_low_level_inv:
∀ d d´ n vadr padr p n´,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
inv H0. constructor; eauto.
Qed.
Lemma big2_ptInsertPTE_kernel_mode:
∀ d d´ n vadr padr p,
big2_ptInsertPTE0_spec n vadr padr p d = Some d´ →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
Qed.
End PTINSERT_PTE.
Section PTPALLOCPDE.
Lemma big2_palloc_inv_prop:
∀ n d d´ v,
big2_palloc_spec n d = Some (d´, v) →
ptpool d´ = ptpool d
∧ (v ≠ 0 →
ZMap.get v (pperm d´) = PGAlloc
∧ 0 < v < nps d´)
∧ pg d´ = true.
Proof.
unfold big2_palloc_spec. intros.
subdestruct; inv H; simpl; subst.
- repeat rewrite ZMap.gss. refine_split´; trivial.
destruct a0 as (? & ? & ?). intros.
refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Lemma big2_ptAllocPDE_high_level_inv:
∀ d d´ n vadr v,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_high_level_inv; eauto.
- exploit palloc_high_level_inv; eauto.
intros.
exploit big2_palloc_inv_prop; eauto. intros (HPT & Halloc & Hpg).
clear H11.
rewrite <- HPT in ×.
inv H1; constructor_gso_simpl_tac; try (intros; congruence); intros.
+ eapply PMap_valid_gso_pde_unp; eauto.
eapply real_init_PTE_defined.
+ functional inversion H3.
eapply PMap_kern_gso; eauto.
+ eapply dirty_ppage´_gss; eauto.
Qed.
Lemma big2_ptAllocPDE_low_level_inv:
∀ d d´ n vadr v n´,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_low_level_inv; eauto.
- exploit palloc_low_level_inv; eauto.
intros. inv H1. constructor; eauto.
Qed.
Lemma big2_ptAllocPDE_kernel_mode:
∀ d d´ n vadr v,
big2_ptAllocPDE_spec n vadr d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_kernel_mode; eauto.
- exploit palloc_kernel_mode; eauto.
Qed.
End PTPALLOCPDE.
Lemma big2_ptInsert_high_level_inv:
∀ d d´ n vadr padr p v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_high_level_inv; eassumption.
- eapply big2_ptAllocPDE_high_level_inv; eassumption.
- eapply big2_ptInsertPTE_high_level_inv; try eassumption.
eapply big2_ptAllocPDE_high_level_inv; eassumption.
Qed.
Lemma big2_ptInsert_low_level_inv:
∀ d d´ n vadr padr p n´ v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_low_level_inv; eassumption.
- eapply big2_ptAllocPDE_low_level_inv; eassumption.
- eapply big2_ptInsertPTE_low_level_inv; try eassumption.
eapply big2_ptAllocPDE_low_level_inv; eassumption.
Qed.
Lemma big2_ptInsert_kernel_mode:
∀ d d´ n vadr padr p v,
big2_ptInsert_spec n vadr padr p d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply big2_ptInsertPTE_kernel_mode; eassumption.
- eapply big2_ptAllocPDE_kernel_mode; eassumption.
- eapply big2_ptInsertPTE_kernel_mode; try eassumption.
eapply big2_ptAllocPDE_kernel_mode; eassumption.
Qed.
End PTINSERT.
Section PTRESV.
Lemma big2_ptResv_high_level_inv:
∀ d d´ n vadr p v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. functional inversion H; subst; eauto; clear H.
- eapply palloc_high_level_inv; eassumption.
- eapply big2_ptInsert_high_level_inv; try eassumption.
eapply palloc_high_level_inv; eassumption.
Qed.
Lemma big2_ptResv_low_level_inv:
∀ d d´ n vadr p n´ v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
low_level_invariant n´ d →
low_level_invariant n´ d´.
Proof.
intros. functional inversion H; subst; eauto.
- eapply palloc_low_level_inv; eassumption.
- eapply big2_ptInsert_low_level_inv; try eassumption.
eapply palloc_low_level_inv; eassumption.
Qed.
Lemma big2_ptResv_kernel_mode:
∀ d d´ n vadr p v,
big2_ptResv_spec n vadr p d = Some (d´, v) →
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; subst; eauto.
eapply palloc_kernel_mode; eassumption.
eapply big2_ptInsert_kernel_mode; try eassumption.
eapply palloc_kernel_mode; eassumption.
Qed.
Global Instance big2_ptResv_inv: PreservesInvariants big2_ptResv_spec.
Proof.
preserves_invariants_simpl´.
- eapply big2_ptResv_low_level_inv; eassumption.
- eapply big2_ptResv_high_level_inv; eassumption.
- eapply big2_ptResv_kernel_mode; eassumption.
Qed.
End PTRESV.
Global Instance big2_proc_create_inv: PCreateInvariants big2_proc_create_spec.
Proof.
constructor; intros; inv H0;
unfold big2_proc_create_spec in *;
subdestruct; inv H; simpl; auto.
-
constructor; trivial; intros; simpl in ×.
-
assert (Hrdyq: 0 ≤ rdy_q_id (CPU_ID d) < num_chan).
{
unfold rdy_q_id. omega.
}
constructor; simpl; eauto 2; try congruence; intros.
exploit split_thread_container_valid; eauto.
simpl. omega.
Qed.
Global Instance sched_init_inv: PreservesInvariants big2_sched_init_spec.
Proof.
preserves_invariants_simpl low_level_invariant high_level_invariant.
- apply real_nps_range.
- apply thread_AC_init_container_valid.
- eapply real_pt_PMap_valid; eauto.
- apply real_pt_PMap_kern.
- omega.
- assumption.
- apply real_idpde_init.
- erewrite real_valid_cidpool; eauto.
omega.
Qed.
Local Opaque remove.
Section YIELD.
Global Instance thread_yield_inv: PreservesInvariants big2_thread_yield_spec.
Proof.
preserves_invariants_simpl_auto.
Qed.
End YIELD.
Global Instance thread_uctx_set_inv: PreservesInvariants thread_uctx_set_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
eapply uctxt_inject_neutral_gss; eauto.
eapply uctxt_inject_neutral0_gss; eauto.
eapply uctxt_inject_neutral0_Vint.
Qed.
Global Instance thread_proc_start_user_inv: TMStartUserInvariants thread_proc_start_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
- subst. constructor; auto; simpl in *; intros; congruence.
Qed.
Global Instance thread_proc_exit_user_inv: TMExitUserInvariants thread_proc_exit_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
simpl.
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
eapply uctxt_inject_neutral0_init.
- constructor; auto; simpl in *; intros.
inv H0.
Qed.
Global Instance thread_proc_start_user_inv2: TMStartUserInvariants2 thread_proc_start_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
- subst. constructor; auto; simpl in *; intros; congruence.
Qed.
Global Instance thread_proc_exit_user_inv2: TMExitUserInvariants2 thread_proc_exit_user_spec.
Proof.
constructor; intros; functional inversion H; functional inversion H1; inv H0.
- constructor; trivial.
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
eapply uctxt_inject_neutral0_init.
- constructor; auto; simpl in *; intros.
inv H0.
Qed.
Global Instance proc_create_postinit_inv:
PreservesInvariants thread_proc_create_postinit_spec.
Proof.
preserves_invariants_nested low_level_invariant high_level_invariant; eauto 2.
Qed.
Section INTELVMSUPPORT.
Section THREAD_INTERCEPT_INTWIN.
Lemma thread_vmx_set_intercept_intwin_high_inv:
∀ d d´ i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H.
functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_intercept_intwin_low_inv:
∀ d d´ n i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H;
functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_intercept_intwin_kernel_mode:
∀ d d´ i,
thread_vmx_set_intercept_intwin_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_intercept_intwin_inv: PreservesInvariants thread_vmx_set_intercept_intwin_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_intercept_intwin_low_inv; eauto.
- eapply thread_vmx_set_intercept_intwin_high_inv; eauto.
- eapply thread_vmx_set_intercept_intwin_kernel_mode; eauto.
Qed.
End THREAD_INTERCEPT_INTWIN.
Section THREAD_SET_DESC1.
Lemma thread_vmx_set_desc1_high_inv:
∀ d d´ i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_desc1_low_inv:
∀ d d´ n i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
functional inversion H9.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_desc1_kernel_mode:
∀ d d´ i i0 i1,
thread_vmx_set_desc1_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_desc1_inv: PreservesInvariants thread_vmx_set_desc1_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_desc1_low_inv; eauto.
- eapply thread_vmx_set_desc1_high_inv; eauto.
- eapply thread_vmx_set_desc1_kernel_mode; eauto.
Qed.
End THREAD_SET_DESC1.
Section THREAD_SET_DESC2.
Lemma thread_vmx_set_desc2_high_inv:
∀ d d´ i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_desc2_low_inv:
∀ d d´ n i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
functional inversion H9.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_desc2_kernel_mode:
∀ d d´ i i0 i1,
thread_vmx_set_desc2_spec i i0 i1 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_desc2_inv: PreservesInvariants thread_vmx_set_desc2_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_desc2_low_inv; eauto.
- eapply thread_vmx_set_desc2_high_inv; eauto.
- eapply thread_vmx_set_desc2_kernel_mode; eauto.
Qed.
End THREAD_SET_DESC2.
Section THREAD_INJECT_EVENT.
Lemma thread_vmx_inject_event_high_inv:
∀ d d´ i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_inject_event_low_inv:
∀ d d´ n i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_inject_event_kernel_mode:
∀ d d´ i i0 i1 i2,
thread_vmx_inject_event_spec i i0 i1 i2 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_inject_event_inv: PreservesInvariants thread_vmx_inject_event_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_inject_event_low_inv; eauto.
- eapply thread_vmx_inject_event_high_inv; eauto.
- eapply thread_vmx_inject_event_kernel_mode; eauto.
Qed.
End THREAD_INJECT_EVENT.
Section THREAD_SET_TSC_OFFSET.
Lemma thread_vmx_set_tsc_offset_high_inv:
∀ d d´ i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_tsc_offset_low_inv:
∀ d d´ n i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss.
repeat eapply VMCS_inject_neutral_gss_Vint_same; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_tsc_offset_kernel_mode:
∀ d d´ i,
thread_vmx_set_tsc_offset_spec i d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_tsc_offset_inv: PreservesInvariants thread_vmx_set_tsc_offset_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_tsc_offset_low_inv; eauto.
- eapply thread_vmx_set_tsc_offset_high_inv; eauto.
- eapply thread_vmx_set_tsc_offset_kernel_mode; eauto.
Qed.
End THREAD_SET_TSC_OFFSET.
Section THREAD_SET_REG.
Lemma thread_vmx_set_reg_high_inv:
∀ d d´ i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_reg_low_inv:
∀ d d´ n i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros. inv H0; functional inversion H; functional inversion H0; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
- unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; eapply VMX_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
- unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; eapply VMCS_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma thread_vmx_set_reg_kernel_mode:
∀ d d´ i i0,
thread_vmx_set_reg_spec i i0 d = Some d´→
kernel_mode d →
kernel_mode d´.
Proof.
intros. functional inversion H; functional inversion H1; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_reg_inv: PreservesInvariants thread_vmx_set_reg_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_reg_low_inv; eauto.
- eapply thread_vmx_set_reg_high_inv; eauto.
- eapply thread_vmx_set_reg_kernel_mode; eauto.
Qed.
End THREAD_SET_REG.
Section THREAD_SET_MMAP.
Lemma thread_vmx_set_mmap_high_inv:
∀ d d´ i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
high_level_invariant d →
high_level_invariant d´.
Proof.
intros.
inv H0; functional inversion H; functional inversion H0; functional inversion H5; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_mmap_low_inv:
∀ d d´ n i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
low_level_invariant n d →
low_level_invariant n d´.
Proof.
intros.
inv H0; functional inversion H; functional inversion H0; functional inversion H5; subst; simpl;
constructor; simpl; intros; try congruence; eauto 2.
Qed.
Lemma thread_vmx_set_mmap_kernel_mode:
∀ d d´ i i0 i1 v,
thread_vmx_set_mmap_spec i i0 i1 d = Some (d´, v)→
kernel_mode d →
kernel_mode d´.
Proof.
intros; functional inversion H;
functional inversion H1; functional inversion H6; subst; constructor; trivial.
Qed.
Global Instance thread_vmx_set_mmap_inv: PreservesInvariants thread_vmx_set_mmap_spec.
Proof.
preserves_invariants_simpl´.
- eapply thread_vmx_set_mmap_low_inv; eauto.
- eapply thread_vmx_set_mmap_high_inv; eauto.
- eapply thread_vmx_set_mmap_kernel_mode; eauto.
Qed.
End THREAD_SET_MMAP.
Global Instance thread_vmx_run_inv: VMXEnterInvariants thread_vm_run_spec.
Proof.
constructor; intros;
unfold thread_vm_run_spec in *;
unfold ObjVMX.vm_run_spec in *;
subdestruct; inv H; simpl; auto.
-
inv H1. constructor; trivial; intros; simpl in ×.
+ unfold VMCSPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
× rewrite ZMap.gss.
eapply VMCS_inject_neutral_gss_Vint; eauto.
× rewrite ZMap.gso; eauto.
+ unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
× rewrite ZMap.gss.
eapply VMX_inject_neutral_gss_enter; eauto.
× rewrite ZMap.gso; eauto.
-
inv H0. constructor; simpl; eauto 2; try congruence; intros.
Qed.
Global Instance thread_vmx_return_from_guest_inv: VMXReturnInvariants thread_vmx_return_from_guest_spec.
Proof.
constructor; intros;
unfold thread_vmx_return_from_guest_spec in *;
unfold ObjVMX.vmx_return_from_guest_spec in *;
subdestruct; inv H; simpl; auto.
-
inv H0. constructor; trivial; intros; simpl in ×.
unfold VMXPool_inject_neutral; intros.
case_eq (zeq vmid (CPU_ID d)); intros; subst.
+ rewrite ZMap.gss; repeat eapply VMX_inject_neutral_gss_Vint; eauto.
+ rewrite ZMap.gso; eauto.
-
inv H0. constructor; simpl; eauto 2; try congruence; intros.
Qed.
Global Instance thread_vmx_init_inv: VMCSSetDefaultsInvariants thread_vmx_init_spec.
Proof.
constructor; intros; functional inversion H.
-
functional inversion H7; simpl; auto; simpl in ×.
inv H6; constructor; trivial; intros; simpl in *; eauto.
+ eapply real_vmcs_inject_neutral; eauto.
+ eapply real_vmx_inject_neutral; eauto.
-
functional inversion H1; simpl; auto; simpl in ×.
inv H0. constructor; simpl; try congruence; intros; eauto.
-
functional inversion H1; simpl; auto.
Qed.
End INTELVMSUPPORT.
End INV.
Definition exec_loadex {F V} := exec_loadex3high (F := F) (V := V).
Definition exec_storeex {F V} := exec_storeex3high (flatmem_store:= flatmem_store) (F := F) (V := V).
Global Instance flatmem_store_inv: FlatmemStoreInvariant (flatmem_store:= flatmem_store).
Proof.
split; inversion 1; intros.
- functional inversion H0. split; trivial.
- functional inversion H1.
split; simpl; try (eapply dirty_ppage´_store_unmapped´; try reflexivity; try eassumption); trivial.
Qed.
Global Instance trapinfo_set_inv: TrapinfoSetInvariant.
Proof.
split; inversion 1; intros; constructor; auto.
Qed.
Definition pipcintro_fresh : compatlayer (cdata RData) :=
syncsendto_chan_pre ↦ gensem thread_syncsendto_chan_pre_spec
⊕ tryreceive_chan ↦ gensem thread_tryreceive_chan_spec.
Definition pipcintro_passthrough : compatlayer (cdata RData) :=
vmxinfo_get ↦ gensem thread_vmxinfo_get_spec
⊕ palloc ↦ gensem big2_palloc_spec
⊕ set_pt ↦ gensem thread_setPT_spec
⊕ pt_read ↦ gensem thread_ptRead_spec
⊕ pt_resv ↦ gensem big2_ptResv_spec
⊕ thread_yield ↦ gensem big2_thread_yield_spec
⊕ sched_init ↦ gensem big2_sched_init_spec
⊕ uctx_get ↦ gensem thread_uctx_get_spec
⊕ uctx_set ↦ gensem thread_uctx_set_spec
⊕ proc_create ↦ proc_create_compatsem big2_proc_create_spec
⊕ container_get_nchildren ↦ gensem thread_container_get_nchildren_spec
⊕ container_get_quota ↦ gensem thread_container_get_quota_spec
⊕ container_get_usage ↦ gensem thread_container_get_usage_spec
⊕ container_can_consume ↦ gensem thread_container_can_consume_spec
⊕ get_CPU_ID ↦ gensem thread_get_CPU_ID_spec
⊕ get_curid ↦ gensem thread_get_curid_spec
⊕ acquire_lock_CHAN ↦ gensem big2_acquire_lock_SC_spec
⊕ release_lock_CHAN ↦ gensem big2_release_lock_SC_spec
⊕ ipc_send_body ↦ gensem thread_ipc_send_body_spec
⊕ rdmsr ↦ gensem thread_rdmsr_spec
⊕ wrmsr ↦ gensem thread_wrmsr_spec
⊕ vmx_set_intercept_intwin ↦ gensem thread_vmx_set_intercept_intwin_spec
⊕ vmx_set_desc1 ↦ gensem thread_vmx_set_desc1_spec
⊕ vmx_set_desc2 ↦ gensem thread_vmx_set_desc2_spec
⊕ vmx_inject_event ↦ gensem thread_vmx_inject_event_spec
⊕ vmx_set_tsc_offset ↦ gensem thread_vmx_set_tsc_offset_spec
⊕ vmx_get_tsc_offset ↦ gensem thread_vmx_get_tsc_offset_spec
⊕ vmx_get_exit_reason ↦ gensem thread_vmx_get_exit_reason_spec
⊕ vmx_get_exit_fault_addr ↦ gensem thread_vmx_get_exit_fault_addr_spec
⊕ vmx_get_exit_qualification ↦ gensem thread_vmx_get_exit_qualification_spec
⊕ vmx_check_pending_event ↦ gensem thread_vmx_check_pending_event_spec
⊕ vmx_check_int_shadow ↦ gensem thread_vmx_check_int_shadow_spec
⊕ vmx_get_reg ↦ gensem thread_vmx_get_reg_spec
⊕ vmx_set_reg ↦ gensem thread_vmx_set_reg_spec
⊕ vmx_get_next_eip ↦ gensem thread_vmx_get_next_eip_spec
⊕ vmx_get_io_width ↦ gensem thread_vmx_get_io_width_spec
⊕ vmx_get_io_write ↦ gensem thread_vmx_get_io_write_spec
⊕ vmx_get_exit_io_rep ↦ gensem thread_vmx_get_exit_io_rep_spec
⊕ vmx_get_exit_io_str ↦ gensem thread_vmx_get_exit_io_str_spec
⊕ vmx_get_exit_io_port ↦ gensem thread_vmx_get_exit_io_port_spec
⊕ vmx_set_mmap ↦ gensem thread_vmx_set_mmap_spec
⊕ vmx_run_vm ↦ primcall_vmx_enter_compatsem thread_vm_run_spec vmx_run_vm
⊕ vmx_return_from_guest ↦ primcall_vmx_return_compatsem thread_vmx_return_from_guest_spec
⊕ vmx_init ↦ vmcs_set_defaults_compatsem thread_vmx_init_spec
⊕ cli ↦ gensem thread_cli_spec
⊕ sti ↦ gensem thread_sti_spec
⊕ serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ serial_putc ↦ gensem thread_serial_putc_spec
⊕ cons_buf_read ↦ gensem thread_cons_buf_read_spec
⊕ host_in ↦ primcall_general_compatsem thread_hostin_spec
⊕ host_out ↦ primcall_general_compatsem thread_hostout_spec
⊕ proc_create_postinit ↦ gensem thread_proc_create_postinit_spec
⊕ trap_get ↦ primcall_trap_info_get_compatsem thread_trap_info_get_spec
⊕ trap_set ↦ primcall_trap_info_ret_compatsem thread_trap_info_ret_spec
⊕ proc_start_user ↦ primcall_start_user_tm_compatsem thread_proc_start_user_spec
⊕ proc_exit_user ↦ primcall_exit_user_tm_compatsem thread_proc_exit_user_spec
⊕ proc_start_user2 ↦ primcall_start_user_tm_compatsem2 thread_proc_start_user_spec
⊕ proc_exit_user2 ↦ primcall_exit_user_tm_compatsem2 thread_proc_exit_user_spec
⊕ accessors ↦ {| exec_load := @exec_loadex; exec_store := @exec_storeex |}.
Definition pipcintro : compatlayer (cdata RData) := pipcintro_fresh ⊕ pipcintro_passthrough.
End WITHMEM.