Library mcertikos.multithread.lowrefins.E2PBThreadGenDef
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 LRegSet.
Require Import INVLemmaProc.
Opaque full_thread_list.
Section E2PBTHREADGENDEFFILE.
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)}.
Definition Hthread_sched_sem_hyp (rs : regset) (s: stencil) (m : mem) (a a´ : RData) (des_rs´ : regset) :=
((let rs0 := undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (map preg_of Conventions1.destroyed_at_call) rs) in
primcall_thread_schedule_sem (prim_ident := thread_yield) big_thread_yield_spec s rs (m, a)
(((((rs0 # ESP <- (des_rs´ ESP)) # EDI <- (des_rs´ EDI)) # ESI <- (des_rs´ ESI))
# EBX <- (des_rs´ EBX)) # EBP <- (des_rs´ EBP)) # PC <- (des_rs´ RA) (m, a´)) →
primcall_thread_schedule_sem (prim_ident := thread_yield) big_thread_yield_spec s rs (m, a)
(((((((((((((((((((des_rs´ # ST0 <- Vundef) # EAX <- Vundef) # ECX <- Vundef)
# EDX <- Vundef) # XMM0 <- Vundef) # XMM1 <- Vundef) # XMM2 <- Vundef)
# XMM3 <- Vundef) # XMM4 <- Vundef) # XMM5 <- Vundef) # XMM6 <- Vundef)
# XMM7 <- Vundef) # ZF <- Vundef) # CF <- Vundef) # PF <- Vundef) # SF <- Vundef)
# OF <- Vundef) # EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef (m, a´)).
Definition Hthread_trans_sem_hyp (rs : regset) (s: stencil) (m : mem) (a a´ : RData) (des_rs´ : regset) :=
((let rs0 := undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: IR EDX :: IR ECX :: IR EAX :: RA :: nil)
(undef_regs (map preg_of Conventions1.destroyed_at_call) rs) in
primcall_thread_transfer_sem big_thread_sleep_spec s rs (m, a)
(((((rs0 # ESP <- (des_rs´ ESP)) # EDI <- (des_rs´ EDI)) # ESI <- (des_rs´ ESI))
# EBX <- (des_rs´ EBX)) # EBP <- (des_rs´ EBP)) # PC <- (des_rs´ RA) (m, a´)) →
primcall_thread_transfer_sem big_thread_sleep_spec s rs (m, a)
(((((((((((((((((((des_rs´ # ST0 <- Vundef) # EAX <- Vundef) # ECX <- Vundef)
# EDX <- Vundef) # XMM0 <- Vundef) # XMM1 <- Vundef) # XMM2 <- Vundef)
# XMM3 <- Vundef) # XMM4 <- Vundef) # XMM5 <- Vundef) # XMM6 <- Vundef)
# XMM7 <- Vundef) # ZF <- Vundef) # CF <- Vundef) # PF <- Vundef) # SF <- Vundef)
# OF <- Vundef) # EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef (m, a´)).
Ltac Lregset_simpl_tac:=
repeat match goal with
| |- context [undef_regs (map _ _) (Lregset_fold _)] ⇒
rewrite Lregset_fold_destroyed
| |- context[(Lregset_fold _) _] ⇒
rewrite Lregset_fold_get; simpl
| |- context [nextinstr (Lregset_fold _)] ⇒
rewrite Lregset_fold_nextinstr
| |- context [nextinstr_nf (Lregset_fold _)] ⇒
rewrite Lregset_fold_nextinstr_nf
| |- context[(Lregset_fold _) # RA <- _ ] ⇒
rewrite Lregset_fold_ra
| |- context[(Lregset_fold _) # PC <- _ ] ⇒
rewrite Lregset_fold_pc
| |- context[(Lregset_fold _) # ST0 <- _ ] ⇒
rewrite Lregset_fold_st0
| |- context[(Lregset_fold _) # (FR ?i) <- _ ] ⇒
match i with
| XMM0 ⇒ rewrite Lregset_fold_xmm0
| XMM1 ⇒ rewrite Lregset_fold_xmm1
| XMM2 ⇒ rewrite Lregset_fold_xmm2
| XMM3 ⇒ rewrite Lregset_fold_xmm3
| XMM4 ⇒ rewrite Lregset_fold_xmm4
| XMM5 ⇒ rewrite Lregset_fold_xmm5
| XMM6 ⇒ rewrite Lregset_fold_xmm6
| XMM7 ⇒ rewrite Lregset_fold_xmm7
end
| |- context[(Lregset_fold _) # (IR ?i) <- _ ] ⇒
match i with
| EAX ⇒ rewrite Lregset_fold_eax
| EDX ⇒ rewrite Lregset_fold_edx
| ESP ⇒ rewrite Lregset_fold_esp
| ECX ⇒ rewrite Lregset_fold_ecx
| EDI ⇒ rewrite Lregset_fold_edi
| ESI ⇒ rewrite Lregset_fold_esi
| EBX ⇒ rewrite Lregset_fold_ebx
| EBP ⇒ rewrite Lregset_fold_ebp
end
| |- context[(Lregset_fold _) # (CR ?i) <- _ ] ⇒
match i with
| ZF ⇒ rewrite Lregset_fold_zf
| CF ⇒ rewrite Lregset_fold_cf
| PF ⇒ rewrite Lregset_fold_pf
| SF ⇒ rewrite Lregset_fold_sf
| OF ⇒ rewrite Lregset_fold_of
end
end.
Lemma Hthread_sched_sem_hyp_correct:
∀ s m a a´ rs rs´,
Hthread_sched_sem_hyp rs s m a a´ rs´.
Proof.
unfold Hthread_sched_sem_hyp. intros.
rewrite (Lregset_rewrite rs) in ×.
rewrite (Lregset_rewrite rs´).
revert H.
Lregset_simpl_tac. intros.
inv H; subst; econstructor; eauto.
Qed.
Lemma Hthread_trans_sem_hyp_correct:
∀ s m a a´ rs rs´,
Hthread_trans_sem_hyp rs s m a a´ rs´.
Proof.
unfold Hthread_trans_sem_hyp. intros.
rewrite (Lregset_rewrite rs) in ×.
rewrite (Lregset_rewrite rs´).
revert H.
Lregset_simpl_tac. intros.
inv H; subst; econstructor; eauto.
Qed.
Definition Hthread_sched_trans_common_cond
(ge: genv) (source_kctxt : KContextPool) (l : Log) (ev : LogEvent) (dp : ZMap.t (option privData))
(d d´ : privData) (a : RData) (s : stencil) (id : positive) (b : block) (sg : signature)
(rsm : ZMap.t EAsmCommon.ThreadState) (rs des_rs´ : regset) :=
relate_RData source_kctxt (uRData l) dp a ∧
(∀ i : Z, In i full_thread_list → total_machine_regset i rsm) ∧
(∀ i : Z, i ≠ (proc_id (uRData l)) →
∀ rs0 : regset, match_estate_regset ge i rsm l rs0 →
match_estate_kctxt rs0 (ZMap.get i (kctxt a))) ∧
stencil_matches s ge ∧
Genv.find_funct_ptr ge b = Some (External (EF_external id sg)) ∧
find_symbol s id = Some b ∧
ZMap.get (proc_id (uRData l)) dp = Some d ∧
ZMap.get (proc_id (uRData l)) rsm = EAsmCommon.Running rs ∧
ZMap.get (proc_id (uRData (ev :: l))) dp = Some d´ ∧
(ZMap.get (proc_id (uRData (ev::l))) rsm = EAsmCommon.Available ∧
initial_thread_kctxt ge (proc_id (uRData (ev :: l))) (ev :: l) = Some des_rs´ ∨
ZMap.get (proc_id (uRData (ev :: l))) rsm = EAsmCommon.Running des_rs´).
Definition single_dirty_ppage´ (pperm: PPermT) (hp: flatmem) :=
∀ i, ZMap.get i pperm = PGUndef →
∀ adr,
ZMap.get adr hp = ZMap.get adr (FlatMem.free_page i hp).
Lemma abs_rel_flatmem_free_page_prop1:
∀ res i res´ hm,
ZMap.get res hm = ZMap.get res (FlatMem.free_page i hm) →
ZMap.get res (FlatMem.free_page res´ hm) =
ZMap.get res (FlatMem.free_page i (FlatMem.free_page res´ hm)).
Proof.
intros. destruct (zeq res´ (PageI res)); subst.
- rewrite FlatMem.free_page_gss.
destruct (zeq i (PageI res)); subst.
+ rewrite FlatMem.free_page_gss. trivial.
+ rewrite FlatMem.free_page_gso.
rewrite FlatMem.free_page_gss. trivial. assumption.
- rewrite FlatMem.free_page_gso.
destruct (zeq i (PageI res)); subst.
+ rewrite FlatMem.free_page_gss in ×. trivial.
+ rewrite FlatMem.free_page_gso.
rewrite FlatMem.free_page_gso.
reflexivity. assumption. assumption.
+ assumption.
Qed.
Lemma abs_rel_flatmem_free_page_prop2:
∀ hm lm res,
FlatMem.flatmem_inj hm lm →
(∀ i, ZMap.get i hm = ZMap.get i (FlatMem.free_page res hm)) →
FlatMem.flatmem_inj hm (FlatMem.free_page res lm).
Proof.
intros. unfold FlatMem.flatmem_inj in ×.
intros. rewrite H0. destruct (zeq res (PageI addr)); subst.
- repeat rewrite FlatMem.free_page_gss.
constructor.
- repeat rewrite FlatMem.free_page_gso; auto.
Qed.
Lemma PageI_rewrite:
∀ v ofs,
(v × 4096 + ofs mod 4096) / 4096 = v.
Proof.
intros. rewrite Zplus_comm.
rewrite Z_div_plus_full.
- rewrite Zdiv_small. trivial.
xomega.
- xomega.
Qed.
Lemma chunk_PageI:
∀ chunk ofs v z,
ofs mod 4096 ≤ 4096 - chunk →
0 ≤ z < chunk →
v = PageI (v × 4096 + ofs mod 4096 + z).
Proof.
intros.
unfold PageI.
replace (v × 4096 + ofs mod 4096 + z) with
((ofs mod 4096 + z) + v × 4096).
rewrite Z_div_plus_full.
rewrite Zdiv_small. trivial.
xomega. xomega. xomega.
Qed.
Lemma abs_rel_palloc_mem_related_prop:
∀ v ofs TY hi_m lo_m,
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
(∀ id : ZIndexed.t,
ZMap.get id hi_m = ZMap.get id (FlatMem.free_page ((v × 4096 + ofs mod 4096) / 4096) hi_m)) →
(∀ id : ZIndexed.t,
ZMap.get id lo_m = ZMap.get id (FlatMem.free_page ((v × 4096 + ofs mod 4096) / 4096) lo_m)) →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) = FlatMem.load TY lo_m (v × 4096 + ofs mod 4096).
Proof.
intros. eapply FlatMem.load_rep.
Focus 2. trivial.
Focus 2. trivial.
intros. rewrite H1. rewrite H2.
rewrite PageI_rewrite.
set (adr := v × 4096 + ofs mod 4096 + z) in ×.
assert (Hv: v = PageI adr).
{
eapply chunk_PageI; eauto.
}
rewrite Hv. repeat rewrite FlatMem.free_page_gss; trivial.
Qed.
Lemma load_free_page_other:
∀ TY v ofs res m,
res ≠ v →
ofs mod 4096 ≤ 4096 - size_chunk TY →
FlatMem.load TY (FlatMem.free_page res m) (v × 4096 + ofs mod 4096) =
FlatMem.load TY m (v × 4096 + ofs mod 4096).
Proof.
unfold FlatMem.load, FlatMem.free_page. intros.
f_equal. eapply FlatMem.getN_setN_outside.
destruct (zlt res v).
- right.
rewrite length_list_repeat.
rewrite Z2Nat.id; [| omega].
xomega.
- left. unfold size_chunk_nat.
rewrite Z2Nat.id.
xomega.
unfold size_chunk.
destruct TY; xomega.
Qed.
Lemma abs_rel_free_page_mem_related_prop1:
∀ v ofs TY hi_m lo_m res,
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) = FlatMem.load TY lo_m (v × 4096 + ofs mod 4096) →
FlatMem.load TY (FlatMem.free_page res hi_m) (v × 4096 + ofs mod 4096) =
FlatMem.load TY (FlatMem.free_page res lo_m) (v × 4096 + ofs mod 4096).
Proof.
intros.
destruct (zeq res v); subst.
- eapply FlatMem.load_rep.
Focus 2. trivial.
Focus 2. trivial.
intros.
set (adr := v × 4096 + ofs mod 4096 + z) in ×.
assert (Hv: v = PageI adr).
{
eapply chunk_PageI; eauto.
}
rewrite Hv. repeat rewrite FlatMem.free_page_gss; trivial.
- repeat erewrite load_free_page_other; auto.
Qed.
Lemma abs_rel_free_page_mem_related_prop2:
∀ (v ofs : Z) (TY : memory_chunk) hi_m lo_m hi_pperm res,
ZMap.get res hi_pperm = PGUndef →
(∀ id : ZIndexed.t, ZMap.get id hi_m = ZMap.get id (FlatMem.free_page res hi_m)) →
(∀ id : ZIndexed.t, ZMap.get id lo_m = ZMap.get id (FlatMem.free_page res lo_m)) →
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) hi_pperm = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) = FlatMem.load TY lo_m (v × 4096 + ofs mod 4096) →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) =
FlatMem.load TY (FlatMem.free_page res lo_m) (v × 4096 + ofs mod 4096).
Proof.
intros.
destruct (zeq res v); subst.
- eapply FlatMem.load_rep.
Focus 2. trivial.
Focus 2. trivial.
intros.
set (adr := v × 4096 + ofs mod 4096 + z) in ×.
assert (Hv: v = PageI adr).
{
eapply chunk_PageI; eauto.
}
rewrite Hv.
rewrite H0. rewrite Hv.
repeat rewrite FlatMem.free_page_gss; trivial.
- repeat erewrite load_free_page_other; auto.
Qed.
Lemma abs_rel_flatmem_store_other_related_prop:
∀ v ofs TY value hi_pperm hi_m lo_m,
(∀ (v0 ofs0 : Z) (TY0 : memory_chunk),
ZMap.get ((v0 × 4096 + ofs0 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs0 mod 4096 ≤ 4096 - size_chunk TY0 → (align_chunk TY0 | ofs0 mod 4096) →
FlatMem.load TY0 hi_m (v0 × 4096 + ofs0 mod 4096) =
FlatMem.load TY0 lo_m (v0 × 4096 + ofs0 mod 4096)) →
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
ZMap.get (PageI (v × 4096 + ofs mod 4096)) hi_pperm = PGUndef →
∀ (v1 ofs1 : Z) (TY1 : memory_chunk),
ZMap.get ((v1 × 4096 + ofs1 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs1 mod 4096 ≤ 4096 - size_chunk TY1 → (align_chunk TY1 | ofs1 mod 4096) →
FlatMem.load TY1 hi_m (v1 × 4096 + ofs1 mod 4096) =
FlatMem.load TY1 (FlatMem.store TY lo_m (v × 4096 + ofs mod 4096) value) (v1 × 4096 + ofs1 mod 4096).
Proof.
intros.
destruct (zeq v v1); subst.
- unfold PageI in H2.
rewrite PageI_rewrite in ×. congruence.
- symmetry.
erewrite FlatMem.load_store_other.
Focus 2. trivial.
symmetry.
eapply H; eauto.
destruct (zlt v v1).
+ right. xomega.
+ left. xomega.
Qed.
Lemma rev_if_be_eq:
∀ i,
rev_if_be (i :: nil) = i :: nil.
Proof.
intros. unfold rev_if_be.
destruct (Archi.big_endian); trivial.
Qed.
Lemma decode_byte_eq:
∀ i,
decode_int (i :: nil) = Byte.unsigned i.
Proof.
intros. unfold decode_int.
rewrite rev_if_be_eq. simpl. rewrite Z.add_0_r.
trivial.
Qed.
Lemma byte_range´:
∀ i,
0 ≤ Byte.unsigned i < 256.
Proof.
intros. specialize (Byte.unsigned_range i).
unfold Byte.modulus. rewrite two_power_nat_equiv.
unfold Byte.wordsize. unfold Wordsize_8.wordsize.
change (2 ^ Z.of_nat 8) with (256).
trivial.
Qed.
Lemma byte_range:
∀ i,
Int.unsigned (Int.repr (Byte.unsigned i)) = Byte.unsigned i.
Proof.
intros.
rewrite Int.unsigned_repr. trivial.
specialize (byte_range´ i). intros.
rewrite int_max. omega.
Qed.
Lemma byte_mod:
∀ i,
Byte.unsigned i mod two_p (Z.of_nat 1 × 8) = Byte.unsigned i.
Proof.
intros. simpl. rewrite two_power_pos_equiv.
simpl.
change (Z.pow_pos 2 8) with 256.
rewrite Zmod_small; trivial.
eapply byte_range´.
Qed.
Lemma IntByte:
∀ i i0,
Vint (Int.zero_ext 8 (Int.repr (decode_int (i :: nil)))) =
Vint (Int.zero_ext 8 (Int.repr (decode_int (i0 :: nil)))) → i = i0.
Proof.
intros. inv H.
assert (Heq: Int.unsigned (Int.zero_ext 8 (Int.repr (decode_int (i :: nil))))
= Int.unsigned (Int.zero_ext 8 (Int.repr (decode_int (i0 :: nil))))).
{
unfold Int.unsigned. destruct (Int.zero_ext 8 (Int.repr (decode_int (i :: nil)))).
destruct (Int.zero_ext 8 (Int.repr (decode_int (i0 :: nil)))).
simpl. trivial.
}
clear H1.
repeat rewrite <- decode_encode_int_1 in Heq.
repeat rewrite decode_byte_eq in Heq.
repeat rewrite byte_range in Heq.
repeat rewrite decode_encode_int in Heq.
repeat rewrite byte_mod in Heq.
repeat rewrite byte_range in Heq.
rewrite <- Byte.repr_unsigned with i.
rewrite <- Byte.repr_unsigned with i0.
rewrite Heq. trivial.
Qed.
Lemma load_get:
∀ hi_m lo_m hi_pperm,
(∀ (v0 ofs0 : Z) (TY0 : memory_chunk),
ZMap.get ((v0 × 4096 + ofs0 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs0 mod 4096 ≤ 4096 - size_chunk TY0 →
(align_chunk TY0 | ofs0 mod 4096) →
FlatMem.load TY0 hi_m (v0 × 4096 + ofs0 mod 4096) =
FlatMem.load TY0 lo_m (v0 × 4096 + ofs0 mod 4096)) →
(∀ v1 ofs1 TY1,
ZMap.get ((v1 × 4096 + ofs1 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs1 mod 4096 ≤ 4096 - size_chunk TY1 →
(align_chunk TY1 | ofs1 mod 4096) →
(∀ z, 0 ≤ z < size_chunk TY1 →
ZMap.get (v1 × 4096 + ofs1 mod 4096 + z) hi_m =
ZMap.get (v1 × 4096 + ofs1 mod 4096 + z) lo_m)).
Proof.
intros.
specialize (H v1 (ofs1 + z) Mint8unsigned).
assert (Hofs: (ofs1 + z) mod 4096 = ofs1 mod 4096 + z).
{
rewrite Zplus_mod.
assert (Hz: z mod 4096 = z).
{
rewrite Zmod_small; trivial.
destruct TY1; simpl in H3; omega.
}
rewrite Hz.
apply Zmod_small; trivial.
clear H H0 H2 Hz.
destruct TY1; simpl in H1, H3; xomega.
}
rewrite Hofs in ×.
assert (Haddr: v1 × 4096 + (ofs1 mod 4096 + z) =
v1 × 4096 + ofs1 mod 4096 + z) by omega.
rewrite Haddr in ×.
clear Hofs Haddr.
exploit H; eauto.
- simpl. rewrite PageI_rewrite in H0.
exploit (chunk_PageI (size_chunk TY1) ofs1 v1); eauto.
unfold PageI. intros Hv1. rewrite <- Hv1. clear Hv1. trivial.
- simpl. clear H0 H2 H.
destruct TY1; simpl in *; omega.
- simpl. ∃ (ofs1 mod 4096 + z). omega.
- clear H H0 H1 H2 H3. intros Hload.
unfold FlatMem.load in ×. simpl in ×.
destruct (ZMap.get (v1 × 4096 + ofs1 mod 4096 + z) hi_m); simpl in ×.
+ simpl in ×.
destruct (ZMap.get (v1 × 4096 + ofs1 mod 4096 + z) lo_m); trivial.
simpl in ×. inv Hload.
+ simpl in ×.
destruct (ZMap.get (v1 × 4096 + ofs1 mod 4096 + z) lo_m); trivial.
× simpl in ×. inv Hload.
× simpl in ×. unfold decode_val in ×. simpl in ×.
eapply IntByte in Hload. subst. trivial.
Qed.
Lemma chunk_nat:
∀ TY,
Z.of_nat (size_chunk_nat TY) = size_chunk TY.
Proof.
unfold size_chunk_nat. intros.
rewrite Z2Nat.id. trivial.
destruct TY; simpl; omega.
Qed.
Lemma setN_same:
∀ vl c c´ p q,
p ≤ q < p + Z_of_nat (length vl) →
ZMap.get q (FlatMem.setN vl p c) = ZMap.get q (FlatMem.setN vl p c´).
Proof.
induction vl; intros; simpl.
- simpl in H. omega.
- simpl length in H. rewrite inj_S in H.
destruct (zeq q p).
+ subst.
repeat rewrite FlatMem.setN_outside.
repeat rewrite ZMap.gss. trivial.
left; omega.
left; omega.
+ eapply IHvl.
omega.
Qed.
Lemma abs_rel_flatmem_store_mine_related_prop:
∀ v ofs TY value hi_pperm hi_m lo_m,
(∀ (v0 ofs0 : Z) (TY0 : memory_chunk),
ZMap.get ((v0 × 4096 + ofs0 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs0 mod 4096 ≤ 4096 - size_chunk TY0 → (align_chunk TY0 | ofs0 mod 4096) →
FlatMem.load TY0 hi_m (v0 × 4096 + ofs0 mod 4096) =
FlatMem.load TY0 lo_m (v0 × 4096 + ofs0 mod 4096)) →
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
ZMap.get (PageI (v × 4096 + ofs mod 4096)) hi_pperm = PGAlloc →
∀ (v1 ofs1 : Z) (TY1 : memory_chunk),
ZMap.get ((v1 × 4096 + ofs1 mod 4096) / 4096) hi_pperm = PGAlloc →
ofs1 mod 4096 ≤ 4096 - size_chunk TY1 → (align_chunk TY1 | ofs1 mod 4096) →
FlatMem.load TY1 (FlatMem.store TY hi_m (v × 4096 + ofs mod 4096) value) (v1 × 4096 + ofs1 mod 4096) =
FlatMem.load TY1 (FlatMem.store TY lo_m (v × 4096 + ofs mod 4096) value) (v1 × 4096 + ofs1 mod 4096).
Proof.
intros.
eapply FlatMem.load_rep.
Focus 2. trivial.
Focus 2. trivial. intros.
exploit load_get; eauto.
intros Hload. unfold FlatMem.store.
destruct (zle_lt (v × 4096 + ofs mod 4096) (v1 × 4096 + ofs1 mod 4096 + z)
(v × 4096 + ofs mod 4096 + size_chunk TY)).
- eapply setN_same; eauto.
rewrite encode_val_length.
erewrite chunk_nat. trivial.
- assert (Hr:
v1 × 4096 + ofs1 mod 4096 + z < v × 4096 + ofs mod 4096 ∨
v1 × 4096 + ofs1 mod 4096 + z ≥
v × 4096 + ofs mod 4096 + Z.of_nat (length (encode_val TY value))).
{
rewrite encode_val_length.
erewrite chunk_nat.
destruct o.
- left. omega.
- right; trivial.
}
repeat rewrite FlatMem.setN_outside; eauto.
Qed.
Class E2PBThreadGenProp (s_oracle_prf : SingleOracle) :=
{
abs_rel_proc_create_prop:
∀ (ge : genv) kctxt_pool l dp a d b b´ b_uc uc_ofs q sd´ d´ a´ res res´ largs elf_id,
relate_RData kctxt_pool (uRData l) dp a →
ZMap.get (proc_id (uRData l)) dp = Some d →
single_big_proc_create_spec ((uRData l), d) b b´ b_uc uc_ofs (Int.unsigned q) = Some ((sd´, d´), res) →
big_proc_create_spec a b b´ b_uc uc_ofs (Int.unsigned q) = Some (a´, res´) →
res = res´ →
largs = (Lint elf_id :: Lptr b_uc uc_ofs :: Lint q::nil) →
thread_init_dproc res = cal_init_dproc nomain_init_priv_adt (proc_id (uRData l)) (Int.unsigned q) b_uc uc_ofs ∧
kctxt a´ = do_init ge (Some (LEvent (proc_id (uRData l)) (LogPrim proc_create largs res´ (snap_func d)))) l (kctxt a);
Hthread_sched_match_prop:
∀ (ge :genv) (source_kctxt : KContextPool) (l : Log) (dp : ZMap.t (option privData))
(d d´ : privData) (a : RData) (a´ : RData) (s : stencil) (b : block) (sg : signature)
(rsm : ZMap.t EAsmCommon.ThreadState) (rs des_rs´ : regset) (m : mem) (yield_ev : LogEvent),
state_checks thread_yield nil l dp →
yield_ev = LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m)) →
Hthread_sched_trans_common_cond ge source_kctxt l yield_ev dp d d´ a s thread_yield b sg rsm rs des_rs´ →
(∀ v r, ZtoPreg v = Some r → Val.has_type (des_rs´#r) AST.Tint) ∧
(∀ v r, ZtoPreg v = Some r →
val_inject (Mem.flat_inj (Mem.nextblock m)) (des_rs´#r) (des_rs´#r)) ∧
ZMap.get (proc_id (uRData (yield_ev::l))) (kctxt a) = des_rs´ ∧
(ZMap.get (proc_id (uRData (yield_ev::l))) rsm = EAsmCommon.Running des_rs´ →
∃ pc, initial_thread_pc (spl_data := single_data) ge (proc_id (uRData (yield_ev::l))) l = Some pc);
Hthread_trans_match_prop:
∀ (ge :genv) (source_kctxt : KContextPool) (l : Log) (dp : ZMap.t (option privData))
(d d´ : privData) (a : RData) (a´ : RData) (s : stencil) (b : block) (sg : signature)
(rsm : ZMap.t EAsmCommon.ThreadState) (rs des_rs´ : regset) (m : mem) (sleep_ev : LogEvent) (i0 : int),
extcall_arguments rs m {| sig_args := Tint :: nil;
sig_res := None;
sig_cc := cc_default |} (Vint i0 :: nil) →
state_checks thread_sleep (Lint i0 :: nil) l dp →
sleep_ev = LEvent (proc_id (uRData l)) (LogSleep (Int.unsigned i0) (Mem.nextblock m)
(sync_chpool_check thread_sleep (Lint i0 :: nil) (uRData l) d)) →
Hthread_sched_trans_common_cond ge source_kctxt l sleep_ev dp d d´ a s thread_sleep b sg rsm rs des_rs´ →
(∀ v r, ZtoPreg v = Some r → Val.has_type (des_rs´#r) AST.Tint) ∧
(∀ v r, ZtoPreg v = Some r →
val_inject (Mem.flat_inj (Mem.nextblock m)) (des_rs´#r) (des_rs´#r)) ∧
ZMap.get (proc_id (uRData (sleep_ev::l))) (kctxt a) = des_rs´ ∧
(ZMap.get (proc_id (uRData (sleep_ev::l))) rsm = EAsmCommon.Running des_rs´ →
∃ pc, initial_thread_pc (spl_data := single_data) ge (proc_id (uRData (sleep_ev::l))) l = Some pc)
}.
Section BasicProps.
Lemma ucxt_create_satisfy_low_level_inv:
∀ id a n,
0 ≤ id < 1024 →
uctxt_inject_neutral (AbstractDataType.uctxt a) n →
uctxt_inject_neutral (ZMap.set id (uctxt (thread_init_dproc id)) (AbstractDataType.uctxt a)) n.
Proof.
intros.
unfold thread_init_dproc.
unfold thread_init_dproc_aux.
case_eq (zeq id main_thread).
{ intros; subst.
assert (match
match init_log with
| nil ⇒ Some main_init_dproc
| _ :: _ ⇒ None
end
with
| Some init_dproc_val ⇒ init_dproc_val
| None ⇒ main_init_dproc
end = main_init_dproc).
{ destruct init_log; auto. }
rewrite H2; clear H2.
simpl.
eapply INVLemmaProc.uctxt_inject_neutral_gss; eauto.
intros.
unfold uctxt_inject_neutral in H0.
rewrite ZMap.gi; split; constructor. }
{ intros.
case_eq (thread_init_dproc_iter id init_log); intros.
exploit thread_init_iter_uctxt_val; eauto.
intros.
rewrite H3.
simpl.
assert (uctxt_inject_neutral (ZMap.init (ZMap.init Vundef)) n).
{ unfold uctxt_inject_neutral.
intros.
rewrite ZMap.gi.
rewrite ZMap.gi.
split; constructor. }
eapply uctxt_inject_neutral_gss; eauto.
repeat eapply uctxt_inject_neutral0_gss;
try eapply uctxt_inject_neutral0_Vint.
intros.
rewrite ZMap.gi.
split; constructor.
- simpl.
eapply INVLemmaProc.uctxt_inject_neutral_gss; eauto.
intros.
unfold uctxt_inject_neutral in H0.
rewrite ZMap.gi; split; constructor. }
Qed.
Lemma single_big_palloc_exists_log :
∀ adt adt´ n res,
single_big_palloc_spec n adt = Some (adt´, res) →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
intros.
unfold single_big_palloc_spec in *; subdestruct; inv H; simpl; destruct adt; simpl in *;
unfold single_big_palloc_spec_share in *; subdestruct; simpl in *;
inv Hdestruct7; refine_split´; tauto.
Qed.
Lemma single_big_palloc_preserves_cused´:
∀ tid (adt adt´ : @PData (@single_data oracle_ops big_ops)) n res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_palloc_spec n adt = Some (adt´, res) →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt)) =
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
unfold B_GetContainerUsed´.
generalize (single_big_palloc_exists_log _ _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
rewrite H1, H2.
eapply single_big_palloc_preserves_cused; eauto.
Qed.
Lemma single_big_ptResv_exists_log :
∀ adt adt´ n vadr perm res,
single_big_ptResv_spec n vadr perm adt = Some (adt´, res) →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
intros.
unfold single_big_ptResv_spec in *; subdestruct; inv H; simpl; destruct adt; simpl in ×.
- eapply single_big_palloc_exists_log in Hdestruct0; simpl in Hdestruct0; auto.
- eapply single_big_palloc_exists_log in Hdestruct0.
destruct Hdestruct0 as (l & l´ & Htemp1 & Htemp2).
∃ l; simpl in ×.
unfold single_big_ptInsert_spec in H1; subdestruct; inv H1.
+ functional inversion Hdestruct9; inv H; simpl; esplit; eauto.
+ functional inversion Hdestruct9; inv H; simpl.
× eapply single_big_palloc_exists_log in H8.
destruct H8 as (l0 & l0´ & H8 & H10).
esplit; eauto.
× eapply single_big_palloc_exists_log in H8.
destruct H8 as (l0 & l0´ & H8 & H10).
esplit; eauto.
+ functional inversion Hdestruct9; subst.
× functional inversion Hdestruct12; subst; simpl in ×.
eapply single_big_palloc_exists_log in H8.
destruct H8 as (l0 & l0´ & H8 & Htemp).
esplit; eauto.
× functional inversion Hdestruct12; subst; simpl in ×.
eapply single_big_palloc_exists_log in H8.
destruct H8 as (l0 & l0´ & H8 & Htemp).
esplit; eauto.
Qed.
Lemma single_big_ptResv_preserves_cused´:
∀ tid (adt adt´ : @PData (@single_data oracle_ops big_ops)) n vadr perm res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_ptResv_spec n vadr perm adt = Some (adt´, res) →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt))
= B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_ptResv_exists_log _ _ _ _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
unfold B_GetContainerUsed´.
rewrite H1, H2.
eapply single_big_ptResv_preserves_cused; eauto.
Qed.
Lemma single_big_acquire_lock_SC_exists_log :
∀ adt adt´ lock_id,
single_big_acquire_lock_SC_spec lock_id adt = Some adt´ →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
unfold single_big_acquire_lock_SC_spec in H; subdestruct;
unfold single_big_acquire_lock_SC_spec_share in Hdestruct1; subdestruct; simpl in *; inv H; inv Hdestruct1; simpl in ×.
- refine_split´; eauto.
- refine_split´; eauto.
Qed.
Lemma single_big_acquire_lock_SC_preserves_cused´:
∀ tid lock_id (adt adt´ : @PData (@single_data oracle_ops big_ops)),
valid_big_oracle (big_oracle (fst adt)) →
single_big_acquire_lock_SC_spec lock_id adt = Some adt´ →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt))
= B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_acquire_lock_SC_exists_log _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
unfold B_GetContainerUsed´.
rewrite H1, H2.
eapply single_big_acquire_lock_SC_preserves_cused; eauto.
Qed.
Lemma single_big_release_lock_SC_exists_log :
∀ adt adt´ lock_id,
single_big_release_lock_SC_spec lock_id adt = Some adt´ →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
unfold single_big_release_lock_SC_spec in H; subdestruct;
unfold single_big_release_lock_SC_spec_share in Hdestruct1; subdestruct; simpl in *; inv H; inv Hdestruct1; simpl in ×.
refine_split´; eauto.
Qed.
Lemma single_big_release_lock_SC_preserves_cused:
∀ tid lock_id (adt adt´ : @PData (@single_data oracle_ops big_ops)),
valid_big_oracle (big_oracle (fst adt)) →
single_big_release_lock_SC_spec lock_id adt = Some adt´ →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt))
= B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_release_lock_SC_exists_log _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
unfold B_GetContainerUsed´.
rewrite H1, H2.
eapply single_big_release_lock_SC_preserves_cused; eauto.
Qed.
Lemma single_big_thread_wakeup_exists_log :
∀ adt adt´ sc res,
single_big_thread_wakeup_spec sc adt = Some (adt´, res) →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
unfold single_big_thread_wakeup_spec in H; subdestruct.
unfold single_big_thread_wakeup_spec_share in Hdestruct2; subdestruct; simpl in *; inv H; inv Hdestruct2; simpl in ×.
- refine_split´; eauto.
- refine_split´; eauto.
- refine_split´; eauto.
Qed.
Lemma single_big_thread_wakeup_preserves_cused:
∀ tid sc (adt adt´ : @PData (@single_data oracle_ops big_ops)) res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_thread_wakeup_spec sc adt = Some (adt´, res) →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt))
= B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_thread_wakeup_exists_log _ _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
unfold B_GetContainerUsed´.
rewrite H1, H2.
eapply single_big_thread_wakeup_preserves_cused; eauto.
Qed.
Lemma single_big_proc_create_exists_log :
∀ adt adt´ b b´ buc ofs_uc q res,
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
∃ l l´, big_log (fst adt) = BigDef l ∧ big_log (fst adt´) = BigDef l´.
Proof.
intros.
functional inversion H; inv H0.
functional inversion H11; subst.
simpl in ×.
refine_split´; eauto.
Qed.
Lemma single_big_proc_create_preserves_cused´:
∀ (adt adt´ : @PData (@single_data oracle_ops big_ops)) b b´ buc ofs_uc q res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
B_GetContainerUsed´ (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) (CPU_ID (fst adt)) (big_log (fst adt)) =
B_GetContainerUsed´ (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_proc_create_exists_log _ _ _ _ _ _ _ _ H0); intros.
destruct H1 as (l & l´ & H1 & H2).
unfold B_GetContainerUsed´.
rewrite H1, H2.
eapply single_big_proc_create_preserves_cused; eauto.
Qed.
Lemma single_big_proc_create_preserves_cused_snd´:
∀ tid (adt adt´ : @PData (@single_data oracle_ops big_ops)) b b´ buc ofs_uc q res,
valid_big_oracle (big_oracle (fst adt)) →
single_big_proc_create_spec adt b b´ buc ofs_uc q = Some (adt´, res) →
tid ≠ res →
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt)) =
B_GetContainerUsed´ tid (CPU_ID (fst adt)) (big_log (fst adt´)).
Proof.
intros.
generalize (single_big_proc_create_exists_log _ _ _ _ _ _ _ _ H0); intros.
destruct H2 as (l & l´ & H2 & H3).
unfold B_GetContainerUsed´.
rewrite H2, H3.
eapply single_big_proc_create_preserves_cused_snd; eauto.
Qed.
End BasicProps.
Section FlatMemRelated.
Lemma single_dirty_ppage´_init:
single_dirty_ppage´ (ZMap.init PGUndef) FlatMem.empty_flatmem.
Proof.
unfold single_dirty_ppage´; intros; unfold FlatMem.empty_flatmem.
destruct (zeq (PageI adr) i); subst.
rewrite ZMap.gi; rewrite FlatMem.free_page_gss; auto.
rewrite FlatMem.free_page_gso; auto.
Qed.
Lemma single_dirty_ppage´_gso:
∀ pp h,
single_dirty_ppage´ pp h →
∀ n,
single_dirty_ppage´ (ZMap.set n PGAlloc pp) h.
Proof.
unfold single_dirty_ppage´; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss in H0. contradict H0; auto.
intro contra; inv contra.
- rewrite ZMap.gso in H0; auto.
Qed.
Lemma single_dirty_ppage´_store_unmapped´:
∀ pp h,
single_dirty_ppage´ pp h →
∀ i,
ZMap.get (PageI i) pp = PGAlloc →
∀ v h´ chunk,
FlatMem.store chunk h i v = h´ →
i mod PgSize ≤ PgSize - size_chunk chunk →
single_dirty_ppage´ pp h´.
Proof.
unfold single_dirty_ppage´ in ×. intros. subst.
destruct (zeq i0 (PageI adr)); subst.
- rewrite FlatMem.free_page_gss.
unfold FlatMem.store.
erewrite FlatMem.setN_other.
+ erewrite H; try apply H3.
rewrite FlatMem.free_page_gss.
reflexivity.
+ rewrite encode_val_length. rewrite <- size_chunk_conv.
red; intros; subst.
assert (HW: PageI adr = PageI i).
{
unfold PageI.
assert (HW: ∃ a, adr = i + a
∧ 0 ≤ a < size_chunk chunk).
{
∃ (adr - i).
unfold ZIndexed.t in ×.
split.
Transparent Z.sub.
omega.
omega.
Opaque Z.sub.
}
destruct HW as (a & Heq & Hrange); subst.
assert (HW: ∃ b c, i = b × PgSize + c
∧ 0 ≤ c ≤ PgSize - size_chunk chunk).
{
rewrite (Z_div_mod_eq i PgSize); [|omega].
rewrite (Zmult_comm PgSize (i/ PgSize)).
esplit; esplit; split. reflexivity.
exploit (Z_mod_lt i PgSize). omega.
intros (HP & _).
split; try assumption.
}
destruct HW as (b & c & Heq & Hrange´). rewrite Heq.
replace (b × PgSize + c + a) with (b × PgSize + (c + a)) by omega.
repeat rewrite Z_div_plus_full_l; try omega.
Transparent Z.sub.
repeat rewrite Zdiv_small; omega.
Opaque Z.sub.
}
congruence.
- rewrite FlatMem.free_page_gso; trivial.
Qed.
Lemma single_dirty_ppage´_store_unmapped:
∀ pp h,
single_dirty_ppage´ pp h →
∀ i,
ZMap.get (PageI (i × 4)) pp = PGAlloc →
∀ v h´,
FlatMem.store Mint32 h (i × 4) v = h´ →
single_dirty_ppage´ pp h´.
Proof.
intros. eapply single_dirty_ppage´_store_unmapped´; try eassumption.
clear. simpl.
change 4096 with (1024 × 4).
rewrite Zmult_mod_distr_r.
apply mod_chunk.
Qed.
Lemma single_dirty_ppage´_gss:
∀ pp h,
single_dirty_ppage´ pp h →
∀ p n,
single_dirty_ppage´ (ZMap.set n p pp) (FlatMem.free_page n h).
Proof.
unfold single_dirty_ppage´; intros.
destruct (zeq i n); subst.
- destruct (zeq n (PageI adr)); subst.
+ repeat rewrite FlatMem.free_page_gss.
reflexivity.
+ repeat rewrite FlatMem.free_page_gso; auto.
- rewrite ZMap.gso in H0; [|assumption].
destruct (zeq n (PageI adr)); subst.
+ repeat rewrite FlatMem.free_page_gss.
rewrite FlatMem.free_page_gso; auto.
rewrite FlatMem.free_page_gss.
reflexivity.
+ destruct (zeq i (PageI adr)); subst.
× rewrite FlatMem.free_page_gso.
rewrite FlatMem.free_page_gss.
erewrite H; [| eassumption].
rewrite FlatMem.free_page_gss.
reflexivity. auto.
× repeat rewrite FlatMem.free_page_gso; auto.
Qed.
Lemma single_dirty_ppage´_gso_alloc:
∀ pp h,
single_dirty_ppage´ pp h →
∀ n,
single_dirty_ppage´ (ZMap.set n PGAlloc pp) h.
Proof.
intros. apply single_dirty_ppage´_gso; try assumption.
Qed.
Lemma single_dirty_ppage´_gss_copy_plus:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(4 | to) →
PageI to = PageI (to + (Z.of_nat (n + 1)) × 4 - 4) →
single_dirty_ppage´ pp h →
flatmem_copy_aux (n + 1) from to h = Some h´ →
single_dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply single_dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
- simpl; intros. subdestruct.
eapply (IHn (FlatMem.store Mint32 h to (Vint i)));
try eapply H3.
+ erewrite PageI_range; eauto.
eapply to_range.
+ apply to_add_divide; eauto.
+ eapply PageI_eq; eauto.
+ eapply single_dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma single_dirty_ppage´_gss_copy´:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
single_dirty_ppage´ pp h →
flatmem_copy_aux n from to h = Some h´ →
single_dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply single_dirty_ppage´_gss_copy_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma single_dirty_ppage´_gss_page_copy_back_plus:
∀ n h h´ pp to l,
ZMap.get (PageI to) pp = PGAlloc →
(4 | to) →
PageI to = PageI (to + (Z.of_nat (n + 1)) × 4 - 4) →
single_dirty_ppage´ pp h →
page_copy_back_aux (n + 1) to l h = Some h´ →
single_dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply single_dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
- simpl; intros. subdestruct.
eapply (IHn (FlatMem.store Mint32 h to (Vint i)));
try eapply H3.
+ erewrite PageI_range; eauto.
eapply to_range.
+ apply to_add_divide; eauto.
+ eapply PageI_eq; eauto.
+ eapply single_dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma single_dirty_ppage´_gss_page_copy_back´:
∀ n h h´ pp to l,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
single_dirty_ppage´ pp h →
page_copy_back_aux n to l h = Some h´ →
single_dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply single_dirty_ppage´_gss_page_copy_back_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma single_dirty_ppage´_gss_copy:
∀ n h h´ pp from to,
flatmem_copy_aux (Z.to_nat n) from to h = Some h´ →
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
0 ≤ n ≤ one_k →
single_dirty_ppage´ pp h →
single_dirty_ppage´ pp h´.
Proof.
intros.
eapply single_dirty_ppage´_gss_copy´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma single_dirty_ppage´_gss_page_copy_back:
∀ n h h´ pp to l,
page_copy_back_aux (Z.to_nat n) to l h = Some h´ →
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
0 ≤ n ≤ one_k →
single_dirty_ppage´ pp h →
single_dirty_ppage´ pp h´.
Proof.
intros.
eapply single_dirty_ppage´_gss_page_copy_back´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
End FlatMemRelated.
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 snap_rev_func_snap_func_eq_pd:
∀ pd, snap_rev_func (snap_func pd) = pd.
Proof.
intros.
destruct pd; simpl.
unfold snap_rev_func; simpl.
unfold snap_func; simpl.
auto.
Qed.
Lemma ptRead_related:
∀ kctxt_val sd pd a n vadr res,
relate_RData_per_pd (proc_id sd) kctxt_val sd pd a →
ObjPHBThreadVMM.single_ptRead_spec n vadr (sd, pd) = Some res →
∃ res´,
ptRead_spec n vadr a = Some res´ ∧ res = res´.
Proof.
intros.
unfold ObjPHBThreadVMM.single_ptRead_spec in H0.
unfold ObjPHBThreadVMM.single_getPDE_spec in H0.
unfold ObjPHBThreadVMM.single_getPTE_spec in H0; simpl in H0.
inv H.
clear AC_re.
Transparent update uRData proc_id.
rewrite zeq_true in *; eauto.
subdestruct; simpl in *; unfold ptRead_spec; unfold getPDE_spec; unfold getPTE_spec; subst;
rewrite <- ikern_re, <- ihost_re, <- ipt_re, <- ptp_re;
rewrite <- init_re, Hdestruct6, Hdestruct8;
try (rewrite zeq_true; eauto; fail);
try (rewrite zeq_false; auto; rewrite zlt_lt_true; auto; rewrite Hdestruct7, Hdestruct11; esplit; eauto).
Opaque update uRData proc_id.
Qed.
Lemma get_kernel_pa_spec_imples_ptRead_spec:
∀ sd d curid vaddr rbuffpa,
curid = ZMap.get (CPU_ID sd) (cid sd) →
single_get_kernel_pa_spec curid vaddr (sd, d) = Some rbuffpa →
∃ paddr,
single_ptRead_spec (ZMap.get (CPU_ID sd) (cid sd)) vaddr (sd, d) = Some paddr ∧
(paddr / 4096 × 4096 + vaddr mod 4096) = rbuffpa.
Proof.
intros.
functional inversion H0; subst.
rewrite H3.
eexists; eauto.
Qed.
Lemma get_kernel_pa_spec_related:
∀ kctxt_pool sd a d dp curid vaddr rbuffpa,
relate_RData kctxt_pool sd dp a →
ZMap.get (proc_id sd) dp = Some d →
curid = ZMap.get (CPU_ID sd) (cid sd) →
single_get_kernel_pa_spec curid vaddr (sd, d) = Some rbuffpa →
∃ rbuffpa´,
get_kernel_pa_spec curid vaddr a = Some rbuffpa´ ∧
rbuffpa = rbuffpa´.
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; intro Hrelated.
inv H; simpl in ×.
functional inversion H2; subst; simpl in ×.
unfold get_kernel_pa_spec.
rewrite <- sh_pg_re.
rewrite H1.
generalize (per_data_re (ZMap.get (CPU_ID sd) (cid sd))); intros.
rewrite H0 in H.
exploit ptRead_related; simpl; eauto.
intros.
destruct H5 as (res´ & H5a & H5b).
subst.
rewrite H5a.
rewrite H4.
eexists; eauto.
Qed.
Lemma page_copy_back_exists:
∀ count addr b HH LH HH´,
page_copy_back_aux count addr b HH = Some HH´ →
∃ LH´, page_copy_back_aux count addr b LH = Some LH´.
Proof.
induction count; intros; subst.
- simpl.
esplit; eauto.
- simpl in H.
subdestruct; try (inv H).
eapply IHcount in H1; eauto.
Qed.
Lemma page_copy_in_same_page:
∀ val1 val2 index,
(4096 | val1 × 4096 + val2) →
0 ≤ val2 < 4096 →
0 ≤ index < 4096 →
(PageI (val1 × 4096 + val2)) =
(PageI (val1 × 4096 + val2 + index)).
Proof.
Transparent Z.sub Z.mul Z.div Z.add.
intros.
unfold Zdivide in H.
destruct H as (val3 & H).
rewrite H; clear H.
unfold PageI.
replace (val3 × 4096 / 4096) with val3 by xomega.
replace ((val3 × 4096 + index) / 4096) with (val3 + index / 4096) by xomega.
assert (index / 4096 = 0) by xomega.
rewrite H.
ring.
Qed.
Lemma page_copy_vaddr_val:
∀ val1 val2,
0 ≤ val2 < 4096 →
(4096 | val1 × 4096 + val2) →
val2 = 0.
Proof.
intros.
unfold Zdivide in H0.
destruct H0 as (val3 & H0).
assert (val2 = val1 × 4096 - val3 × 4096) by omega.
clear H0.
replace (val1 × 4096 - val3 × 4096) with ((val1 - val3) × 4096) in H1 by ring.
remember (val1 - val3) as val4.
clear Heqval4.
rewrite H1 in H.
assert (val4 = 0) by omega.
rewrite H0 in H1.
omega.
Qed.
Lemma size_chunk_range_prop:
∀ val1 val2,
(4096 | val1 × 4096 + val2) →
(4 | val2).
Proof.
unfold Zdivide.
intros.
destruct H as (val3 & H).
assert (val2 = (val3 - val1) × 4096) by omega.
subst.
∃ ((val3 - val1) × 1024).
ring.
Qed.
Lemma mod_mod_eq:
∀ val1, (val1 mod 4096) mod 4096 = val1 mod 4096.
Proof. intros; xomega. Qed.
Lemma vaddr_mod:
∀ vaddr count,
vaddr mod 4096 ≤ 4096 - 4 × Z.succ (Z.of_nat count) →
(((vaddr + 4) mod 4096 = vaddr mod 4096 + 4
∧ vaddr mod 4096 < 4092)
∨ vaddr mod 4096 = 4092).
Proof.
intros. rewrite Zplus_mod. change (4 mod 4096) with 4.
destruct (zeq (vaddr mod 4096) 4092).
- rewrite e. right; trivial.
- left.
assert (Hr: 0 ≤ vaddr mod 4096 + 4 < 4096).
{
exploit (Z_mod_lt vaddr 4096). omega.
intros. omega.
}
rewrite (Zmod_small (vaddr mod 4096 + 4)); trivial.
split; omega.
Qed.
Lemma PageI_add:
∀ init_addr paddr vaddr,
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
vaddr mod 4096 < 4092 →
PageI (init_addr + 4) = PageI init_addr.
Proof.
intros. unfold PageI.
rewrite H.
replace (paddr / 4096 × 4096 + vaddr mod 4096 + 4)
with (paddr / 4096 × 4096 + (vaddr mod 4096 + 4)) by omega.
repeat rewrite Z_div_plus_full_l; try omega.
assert (Hles: vaddr mod 4096 + 4 < 4096) by omega.
exploit (Z_mod_lt vaddr 4096). omega. intros.
rewrite (Zdiv_small (vaddr mod 4096 + 4)); try omega.
rewrite (Zdiv_small (vaddr mod 4096)); try omega.
Qed.
Lemma page_copy_aux_related´:
∀ HH LH ppermT count init_addr paddr vaddr b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ 4 × (Z.of_nat count) + vaddr mod 4096 ≤ 4096 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
vaddr mod 4096 ≤ 4096 - (size_chunk Mint32) × (Z.of_nat count) →
(align_chunk Mint32 | vaddr mod 4096) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_aux count init_addr HH = Some b →
∃ b´ : list int,
page_copy_aux count init_addr LH = Some b´ ∧ b = b´.
Proof.
induction count; intros.
- eauto.
- simpl in H5. simpl. subdestruct.
change (size_chunk Mint32) with 4 in ×.
assert (Hload: Vint i = FlatMem.load Mint32 LH init_addr).
{
rewrite <- Hdestruct.
subst init_addr.
exploit H; eauto.
rewrite Nat2Z.inj_succ in H2.
change (size_chunk Mint32) with 4 in ×.
omega.
}
change (align_chunk Mint32) with 4 in ×.
rewrite <- Hload.
rewrite Nat2Z.inj_succ in ×.
exploit vaddr_mod; eauto. intros Hvaddr´.
destruct Hvaddr´ as [(Hvaddr & Hless)| Hvaddr´].
{
exploit (IHcount (init_addr + 4) paddr (vaddr + 4)); eauto.
+ omega.
+ rewrite Hvaddr. omega.
+ omega.
+ simpl. rewrite Hvaddr.
destruct H3 as (x & Hx).
∃ (x + 1). omega.
+ exploit PageI_add; eauto. intros Hpage.
rewrite Hpage. trivial.
+ intros (b´ & Hcopy & ?); subst.
rewrite Hcopy. eauto.
}
{
rewrite Hvaddr´ in H0.
assert (Hcount: count = O).
{
destruct count; trivial.
rewrite Nat2Z.inj_succ in ×.
omega.
}
rewrite Hcount in ×. inv Hdestruct0. inv H5.
simpl. eauto.
}
Qed.
Lemma init_mod:
∀ init_addr paddr vaddr,
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
(4096 | init_addr) →
vaddr mod 4096 = 0.
Proof.
intros. rewrite H in H0.
apply Zdivide_mod in H0.
replace (paddr / 4096 × 4096 + vaddr mod 4096) with
(vaddr mod 4096 + paddr / 4096 × 4096) in H0 by omega.
rewrite Z_mod_plus_full in H0. rewrite Zmod_mod in H0. trivial.
Qed.
Lemma page_copy_aux_related´´:
∀ HH LH ppermT init_addr paddr vaddr count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_aux (Z.to_nat count) init_addr HH = Some b →
∃ b´ : list int,
page_copy_aux (Z.to_nat count) init_addr LH = Some b´ ∧ b = b´.
Proof.
intros.
assert (Hcount: Z.of_nat (Z.to_nat count) = count).
{
rewrite Z2Nat.id; omega.
}
exploit init_mod; eauto. intros Hvaddr.
eapply page_copy_aux_related´; eauto.
- rewrite Hcount; trivial. omega.
- rewrite Hcount. change (size_chunk Mint32) with 4. omega.
- rewrite Hvaddr. simpl. ∃ 0. trivial.
Qed.
Lemma page_copy_back_aux_mine_related´:
∀ count HH LH ppermT init_addr paddr vaddr HH´ LH´ b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ 4 × (Z.of_nat count) + vaddr mod 4096 ≤ 4096 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
vaddr mod 4096 ≤ 4096 - (size_chunk Mint32) × (Z.of_nat count) →
(align_chunk Mint32 | vaddr mod 4096) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_back_aux count init_addr b HH = Some HH´ →
page_copy_back_aux count init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH´ (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
induction count.
- intros. simpl in H6, H5. inv H5. inv H6. eauto.
- intros. simpl in H6, H5. destruct b; contra_inv.
change (size_chunk Mint32) with 4 in ×.
change (align_chunk Mint32) with 4 in ×.
rewrite Nat2Z.inj_succ in ×.
exploit vaddr_mod; eauto. intros Hvaddr´.
destruct Hvaddr´ as [(Hvaddr & Hless)| Hvaddr´].
{
eapply IHcount.
Focus 7. eapply H5.
Focus 7. eapply H6.
subst init_addr.
eapply abs_rel_flatmem_store_mine_related_prop; eauto.
+ change (size_chunk Mint32) with 4 in ×. omega.
+ instantiate (1:= vaddr + 4).
rewrite Hvaddr. omega.
+ instantiate (1:= paddr). omega.
+ rewrite Hvaddr. omega.
+ rewrite Hvaddr.
destruct H3 as (x & Hx).
∃ (x + 1). omega.
+ exploit PageI_add; eauto. intros Hpage.
rewrite Hpage. trivial.
+ eauto.
+ eauto.
+ eauto.
}
{
rewrite Hvaddr´ in H0.
assert (Hcount: count = O).
{
destruct count; trivial.
rewrite Nat2Z.inj_succ in ×.
omega.
}
rewrite Hcount in ×. inv H5. inv H6.
eapply abs_rel_flatmem_store_mine_related_prop; eauto.
}
Qed.
Lemma page_copy_back_aux_mine_related´´:
∀ HH LH ppermT init_addr paddr vaddr HH´ LH´ count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_back_aux (Z.to_nat count) init_addr b HH = Some HH´ →
page_copy_back_aux (Z.to_nat count) init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH´ (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
intros.
assert (Hcount: Z.of_nat (Z.to_nat count) = count).
{
rewrite Z2Nat.id; omega.
}
exploit init_mod; eauto. intros Hvaddr.
eapply page_copy_back_aux_mine_related´; eauto.
- rewrite Hcount; trivial. omega.
- rewrite Hcount. change (size_chunk Mint32) with 4. omega.
- rewrite Hvaddr. simpl. ∃ 0. trivial.
Qed.
Lemma store_others_related:
∀ (v ofs : Z) (TY : memory_chunk) hi_m lo_m hi_pperm addr paddr vaddr v´,
addr = paddr × 4096 + vaddr mod 4096 →
ZMap.get (PageI addr) hi_pperm = PGUndef →
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) hi_pperm = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY → (align_chunk TY | ofs mod 4096) →
vaddr mod 4096 ≤ 4092 →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) = FlatMem.load TY lo_m (v × 4096 + ofs mod 4096) →
FlatMem.load TY hi_m (v × 4096 + ofs mod 4096) =
FlatMem.load TY (FlatMem.store Mint32 lo_m addr v´) (v × 4096 + ofs mod 4096).
Proof.
intros.
destruct (zeq paddr v); subst.
- unfold PageI in ×.
rewrite PageI_rewrite in ×. congruence.
- symmetry.
erewrite FlatMem.load_store_other.
Focus 2. trivial. auto.
destruct (zlt v paddr).
+ left. xomega.
+ right. simpl. xomega.
Qed.
Lemma page_copy_back_aux_others_related´:
∀ count HH LH ppermT init_addr paddr vaddr LH´ b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ 4 × (Z.of_nat count) + vaddr mod 4096 ≤ 4096 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
vaddr mod 4096 ≤ 4096 - (size_chunk Mint32) × (Z.of_nat count) →
ZMap.get (PageI init_addr) ppermT = PGUndef →
page_copy_back_aux count init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
induction count; intros.
- simpl in H4. inv H4. eauto.
- simpl in H4. destruct b; contra_inv.
change (size_chunk Mint32) with 4 in ×.
change (align_chunk Mint32) with 4 in ×.
rewrite Nat2Z.inj_succ in ×.
exploit vaddr_mod; eauto. intros Hvaddr´.
destruct Hvaddr´ as [(Hvaddr & Hless)| Hvaddr´].
{
eapply IHcount.
Focus 6. eapply H4.
+ instantiate (1:= ppermT). intros.
eapply store_others_related; eauto.
omega.
+ instantiate (1:= vaddr + 4).
rewrite Hvaddr. omega.
+ instantiate (1:= paddr). omega.
+ rewrite Hvaddr. omega.
+ exploit PageI_add; eauto. intros Hpage.
rewrite Hpage. trivial.
+ eauto.
+ eauto.
+ eauto.
}
{
rewrite Hvaddr´ in H0.
assert (Hcount: count = O).
{
destruct count; trivial.
rewrite Nat2Z.inj_succ in ×.
omega.
}
rewrite Hcount in ×. inv H4.
eapply store_others_related; eauto.
}
Qed.
Lemma page_copy_back_aux_others_related´´:
∀ HH LH ppermT init_addr paddr vaddr LH´ count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
init_addr = paddr / 4096 × 4096 + vaddr mod 4096 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGUndef →
page_copy_back_aux (Z.to_nat count) init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
intros.
assert (Hcount: Z.of_nat (Z.to_nat count) = count).
{
rewrite Z2Nat.id; omega.
}
exploit init_mod; eauto. intros Hvaddr.
eapply page_copy_back_aux_others_related´; eauto.
- rewrite Hcount; trivial. omega.
- rewrite Hcount. change (size_chunk Mint32) with 4. omega.
Qed.
Lemma address_rewrite:
∀ init_addr,
(4096 | init_addr) → ∃ vaddr paddr, init_addr = paddr / 4096 × 4096 + vaddr mod 4096.
Proof.
intros.
unfold Zdivide in H; destruct H as (val & H).
subst.
∃ 0.
assert (0 mod 4096 = 0).
{ xomega. }
rewrite H; clear H.
∃ (val × 4096).
xomega.
Qed.
Lemma page_copy_aux_related:
∀ HH LH ppermT init_addr count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_aux (Z.to_nat count) init_addr HH = Some b →
∃ b´ : list int,
page_copy_aux (Z.to_nat count) init_addr LH = Some b´ ∧ b = b´.
Proof.
intros.
exploit address_rewrite; eauto.
intros Hinit_val.
destruct Hinit_val as (vaddr & paddr & Hinit_val).
eauto using page_copy_aux_related´´.
Qed.
Lemma page_copy_back_aux_mine_related:
∀ HH LH ppermT init_addr HH´ LH´ count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGAlloc →
page_copy_back_aux (Z.to_nat count) init_addr b HH = Some HH´ →
page_copy_back_aux (Z.to_nat count) init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH´ (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
intros.
exploit address_rewrite; eauto.
intros Hinit_val.
destruct Hinit_val as (vaddr & paddr & Hinit_val).
eauto using page_copy_back_aux_mine_related´´.
Qed.
Lemma page_copy_back_aux_others_related:
∀ HH LH ppermT init_addr LH´ count b,
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH (v × 4096 + ofs mod 4096)) →
0 ≤ count ≤ 1024 →
(4096 | init_addr) →
ZMap.get (PageI init_addr) ppermT = PGUndef →
page_copy_back_aux (Z.to_nat count) init_addr b LH = Some LH´ →
(∀ (v ofs : Z) (TY : memory_chunk),
ZMap.get ((v × 4096 + ofs mod 4096) / 4096) ppermT = PGAlloc →
ofs mod 4096 ≤ 4096 - size_chunk TY →
(align_chunk TY | ofs mod 4096) →
FlatMem.load TY HH (v × 4096 + ofs mod 4096) = FlatMem.load TY LH´ (v × 4096 + ofs mod 4096)).
Proof.
intros.
exploit address_rewrite; eauto.
intros Hinit_val.
destruct Hinit_val as (vaddr & paddr & Hinit_val).
eauto using page_copy_back_aux_others_related´´.
Qed.
End E2PBTHREADGENDEFFILE.
Ltac per_data_auto :=
constructor; simpl; [auto | auto | auto | auto | auto | auto | auto | auto | auto |
auto | auto | auto | auto | auto | auto | | auto | |
| auto | auto | auto | auto | auto | auto | auto | auto |
auto | auto | auto | | auto | auto | auto | | ].
Ltac per_data_auto_simpl :=
constructor; simpl; [auto | auto | auto | auto | auto | auto | auto | auto | auto |
auto | auto | auto | auto | auto | auto | | | |
| | | | | auto | auto | auto | auto |
auto | auto | auto | | | | | | ].
Ltac per_data_auto_simpl´ :=
constructor; simpl; [auto | auto | auto | auto | auto | auto | auto | auto | auto |
auto | auto | auto | | auto | auto | | | |
| | | | | auto | auto | auto | auto |
auto | auto | auto | | | | | | ].