Library mcertikos.proc.CVIntroGenPassthrough
This file provide the contextual refinement proof between PKContextNew layer and PThreadIntro layer
Section Refinement.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma relate_SC_Log_Pool_gss:
∀ s hl ll l0,
relate_SC_Log_Pool s hl ll →
relate_SC_Log_Pool s
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + lock_TCB_range ≠ 0).
{
unfold lock_TCB_range, ID_TCB_range,ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_relate_SC_Log_Pool:
∀ s habd labd,
relate_SC_Log_Pool s (multi_log habd) (multi_log labd) →
relate_SC_Log_Pool s (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros s d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + lock_TCB_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + lock_TCB_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma tdqueue_init_exists :
∀ s mbi_adr adt adt´ ladt f,
tdqueue_init0_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_AbData s f adt ladt
→ ∃ ladt´,
tdqueue_init0_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_AbData s f adt´ ladt´.
Proof.
unfold tdqueue_init0_spec.
intros until f. exist_simpl.
- apply real_relate_SC_Log_Pool; eauto.
Qed.
Lemma tdqueue_init_match:
∀ s d d´ m i f,
tdqueue_init0_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold tdqueue_init0_spec; intros. subdestruct. inv H.
inv H0. econstructor; eauto.
Qed.
Lemma index2Z_eq´:
∀ i,
0 ≤ i < num_chan →
index2Z 1 i = Some (i + ID_AT_range).
Proof.
unfold index2Z.
unfold index_incrange, index_range.
intros.
unfold ID_TCB_range. rewrite zle_lt_true; trivial.
f_equal. omega.
Qed.
Require Import INVLemmaQLock.
Lemma acquire_lock_ABTCB_exist:
∀ s i habd habd´ labd f,
acquire_lock_ABTCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_ABTCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_ABTCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + ID_AT_range) (multi_log habd) = ZMap.get (i + ID_AT_range) (multi_log labd)).
{
inv multi_log_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
assert (Horacle: ZMap.get (i + ID_AT_range) (multi_oracle habd) = ZMap.get (i + ID_AT_range) (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog, <- Horacle.
subdestruct; inv HQ.
- refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
+ destruct (zeq r (i + ID_AT_range)); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
- refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
+ destruct (zeq r (i + ID_AT_range)); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_ABTCB_match:
∀ s i d d´ m f,
acquire_lock_ABTCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_ABTCB_spec; intros.
subdestruct; inv H.
- inv H0. econstructor; eauto.
- inv H0. econstructor; eauto.
Qed.
Lemma release_lock_ABTCB_exist:
∀ s i habd habd´ labd f,
release_lock_ABTCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_ABTCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_ABTCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + ID_AT_range) (multi_log habd) = ZMap.get (i + ID_AT_range) (multi_log labd)).
{
inv multi_log_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog.
subdestruct; inv HQ.
refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
- destruct (zeq r (i + ID_AT_range)); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_ABTCB_match:
∀ s i d d´ m f,
release_lock_ABTCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_ABTCB_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma enqueue_atomic_exist:
∀ s habd habd´ labd i z f,
enqueue_atomic_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, enqueue_atomic_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold enqueue_atomic_spec; intros.
revert H; subrewrite. subdestruct.
specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
intros [d0 [Hacq Hrel]]. rewrite Hacq.
specialize (enqueue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
intros [d1 [Henq Hrel1]]. rewrite Henq.
eapply release_lock_ABTCB_exist; eauto.
Qed.
Lemma enqueue_atomic_match:
∀ s d d´ m i z f,
enqueue_atomic_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold enqueue_atomic_spec; intros. subdestruct.
specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
specialize (enqueue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
eapply release_lock_ABTCB_match; eauto.
Qed.
Lemma enqueue_atomic_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem enqueue_atomic_spec)
(id ↦ gensem enqueue_atomic_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit enqueue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
assert (Hm: match_AbData s d1´ m2 ι) by (eapply enqueue_atomic_match; eauto).
match_external_states_simpl.
Qed.
Lemma dequeue_atomic_exist:
∀ s habd habd´ labd i z f,
dequeue_atomic_spec i habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, dequeue_atomic_spec i labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold dequeue_atomic_spec; intros.
revert H; subrewrite. subdestruct.
specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
intros [d0 [Hacq Hrel]]. rewrite Hacq.
specialize (dequeue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
intros [d1 [Henq Hrel1]]. rewrite Henq.
specialize (release_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct2 Hrel1).
intros [d2 [Hrls Hrel2]]. rewrite Hrls.
∃ d2. subst. inv HQ. eauto.
Qed.
Lemma dequeue_atomic_match:
∀ s d d´ m i z f,
dequeue_atomic_spec i d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold dequeue_atomic_spec; intros. subdestruct.
specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
specialize (dequeue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
eapply release_lock_ABTCB_match; eauto. inversion H. subst. eauto.
Qed.
Lemma dequeue_atomic_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem dequeue_atomic_spec)
(id ↦ gensem dequeue_atomic_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit dequeue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
assert (Hm: match_AbData s d1´ m2 ι) by (eapply dequeue_atomic_match; eauto).
match_external_states_simpl.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
Qed.
Lemma palloc_match:
∀ s d d´ m n i f,
palloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_spec; intros. inv H0.
subdestruct; inv H; subst; trivial.
- constructor; eauto.
- constructor; eauto.
- constructor; eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptAllocPDE0_match:
∀ s n v i d d´ m f,
ptAllocPDE0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptAllocPDE0_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- exploit palloc_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptInsert0_match:
∀ s n v pa pe d d´ m i f,
ptInsert0_spec n v pa pe d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptInsert0_spec; intros. subdestruct; inv H; trivial.
- exploit ptInsertPTE0_match; eauto.
- eapply ptAllocPDE0_match; eauto.
- exploit ptInsertPTE0_match; eauto.
eapply ptAllocPDE0_match; eauto.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv_match:
∀ s d d´ m i n v p f,
ptResv_spec n v p d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma ptResv2_match:
∀ s d d´ m i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv2_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma offer_shared_mem_match:
∀ s d d´ m i1 i2 v z f,
offer_shared_mem_spec i1 i2 v d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold offer_shared_mem_spec; intros. subdestruct; inv H; trivial.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
- inv H0. constructor; eauto.
Qed.
Lemma GetSharedBuffer_relate:
∀ l l´ s
(Hrel: relate_SC_Log s l l´),
GetSharedBuffer l´ = GetSharedBuffer l.
Proof.
induction l; simpl; intros. inv Hrel. trivial.
inv Hrel. inv Hrelate_event; simpl; eauto.
Qed.
Require Import CVIntroGenLemma.
Lemma index2Z_unique:
∀ i i´ ofs ofs´ z
(Hindex1: index2Z i ofs = Some z)
(Hindex2: index2Z i´ ofs´ = Some z),
i = i´.
Proof.
intros.
functional inversion Hindex1;
functional inversion Hindex2.
functional inversion H0;
functional inversion H4; trivial; subst; simpl in *; subst;
(inv H5; inv H1; unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in *; omega).
Qed.
Lemma lock_SC_range:
∀ ofs z
(Hindex: index2Z 2 ofs = Some z),
0 ≤ z - lock_TCB_range < 1040.
Proof.
intros. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. replace (lock_TCB_range + ofs - lock_TCB_range) with ofs by omega.
unfold ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. simpl in ×.
assert (Hrange: 0 ≤ z - lock_TCB_range < 1040).
{
eapply lock_SC_range; eauto.
}
pose proof (H1 _ Hrange) as Hrel.
replace (z - lock_TCB_range + lock_TCB_range) with z in Hrel by omega.
rewrite Hdestruct7 in Hrel. inv Hrel.
exploit page_copy_aux_exists; eauto.
intros Hpage. rewrite Hpage.
assert (Hrel: relate_SC_Log s (TEVENT (CPU_ID labd)
(TSHARED (OBUFFERE l0)) :: l)
(TEVENT (CPU_ID labd) (TSHARED (OBUFFERE l0)) :: l2)).
{
constructor; eauto. econstructor.
}
erewrite H_CalLock_relate_SC_log; eauto.
refine_split´; try trivial.
econstructor; simpl; eauto.
econstructor.
- intros. destruct (zeq r z); subst.
+ elim H2. eapply index2Z_unique; eauto.
+ repeat rewrite ZMap.gso; eauto.
- intros. destruct (zeq i0 (z - lock_TCB_range)); subst.
+ replace (z - lock_TCB_range + lock_TCB_range) with z by omega.
repeat rewrite ZMap.gss. econstructor. trivial.
+ assert (Hneq: i0 + lock_TCB_range ≠ z) by omega.
repeat rewrite ZMap.gso; auto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros.
subdestruct.
inv H. inv H0.
econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. simpl in ×.
assert (Hrange: 0 ≤ z - lock_TCB_range < 1040).
{
eapply lock_SC_range; eauto.
}
pose proof (H1 _ Hrange) as Hrel.
replace (z - lock_TCB_range + lock_TCB_range) with z in Hrel by omega.
rewrite Hdestruct7 in Hrel. inv Hrel.
erewrite GetSharedBuffer_relate; eauto. rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & Hback & Hinj). rewrite Hback.
refine_split´; try trivial.
econstructor; simpl; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_back_exist; eauto 1.
exploit page_copy_back_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
- eapply flatmem_store_match; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pcvintro_passthrough pabqueue_atomic.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply palloc_match; eauto).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply ptResv_match; eauto).
match_external_states_simpl.
- apply kctxt_new_sim.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply offer_shared_mem_match; eauto).
match_external_states_simpl.
- apply get_state0_sim.
- apply set_state0_sim.
- apply get_abtcb_CPU_ID_sim.
- apply set_abtcb_CPU_ID_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit tdqueue_init_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply tdqueue_init_match; eauto).
match_external_states_simpl.
- apply enqueue0_sim.
- apply dequeue0_sim.
- apply enqueue_atomic_sim.
- apply dequeue_atomic_sim.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma relate_SC_Log_Pool_gss:
∀ s hl ll l0,
relate_SC_Log_Pool s hl ll →
relate_SC_Log_Pool s
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + lock_TCB_range ≠ 0).
{
unfold lock_TCB_range, ID_TCB_range,ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_relate_SC_Log_Pool:
∀ s habd labd,
relate_SC_Log_Pool s (multi_log habd) (multi_log labd) →
relate_SC_Log_Pool s (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros s d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + lock_TCB_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + lock_TCB_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma tdqueue_init_exists :
∀ s mbi_adr adt adt´ ladt f,
tdqueue_init0_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_AbData s f adt ladt
→ ∃ ladt´,
tdqueue_init0_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_AbData s f adt´ ladt´.
Proof.
unfold tdqueue_init0_spec.
intros until f. exist_simpl.
- apply real_relate_SC_Log_Pool; eauto.
Qed.
Lemma tdqueue_init_match:
∀ s d d´ m i f,
tdqueue_init0_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold tdqueue_init0_spec; intros. subdestruct. inv H.
inv H0. econstructor; eauto.
Qed.
Lemma index2Z_eq´:
∀ i,
0 ≤ i < num_chan →
index2Z 1 i = Some (i + ID_AT_range).
Proof.
unfold index2Z.
unfold index_incrange, index_range.
intros.
unfold ID_TCB_range. rewrite zle_lt_true; trivial.
f_equal. omega.
Qed.
Require Import INVLemmaQLock.
Lemma acquire_lock_ABTCB_exist:
∀ s i habd habd´ labd f,
acquire_lock_ABTCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, acquire_lock_ABTCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold acquire_lock_ABTCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + ID_AT_range) (multi_log habd) = ZMap.get (i + ID_AT_range) (multi_log labd)).
{
inv multi_log_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
assert (Horacle: ZMap.get (i + ID_AT_range) (multi_oracle habd) = ZMap.get (i + ID_AT_range) (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog, <- Horacle.
subdestruct; inv HQ.
- refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
+ destruct (zeq r (i + ID_AT_range)); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
- refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
+ destruct (zeq r (i + ID_AT_range)); subst.
× repeat rewrite ZMap.gss. trivial.
× repeat rewrite ZMap.gso; eauto.
+ assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_ABTCB_match:
∀ s i d d´ m f,
acquire_lock_ABTCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_ABTCB_spec; intros.
subdestruct; inv H.
- inv H0. econstructor; eauto.
- inv H0. econstructor; eauto.
Qed.
Lemma release_lock_ABTCB_exist:
∀ s i habd habd´ labd f,
release_lock_ABTCB_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_ABTCB_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_ABTCB_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct_one.
subdestruct_one.
subdestruct_one.
subdestruct_one.
assert (Hlog: ZMap.get (i + ID_AT_range) (multi_log habd) = ZMap.get (i + ID_AT_range) (multi_log labd)).
{
inv multi_log_re. eapply (H ID_TCB i); auto.
omega. eapply index2Z_eq´; eauto.
}
rewrite <- Hlog.
subdestruct; inv HQ.
refine_split´; trivial.
constructor; eauto; simpl.
inv multi_log_re. constructor; intros.
- destruct (zeq r (i + ID_AT_range)); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- assert (Hneq: i + ID_AT_range ≠ i0 + lock_TCB_range).
{
eapply SC_neq0; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_ABTCB_match:
∀ s i d d´ m f,
release_lock_ABTCB_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_ABTCB_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma enqueue_atomic_exist:
∀ s habd habd´ labd i z f,
enqueue_atomic_spec i z habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, enqueue_atomic_spec i z labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold enqueue_atomic_spec; intros.
revert H; subrewrite. subdestruct.
specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
intros [d0 [Hacq Hrel]]. rewrite Hacq.
specialize (enqueue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
intros [d1 [Henq Hrel1]]. rewrite Henq.
eapply release_lock_ABTCB_exist; eauto.
Qed.
Lemma enqueue_atomic_match:
∀ s d d´ m i z f,
enqueue_atomic_spec i z d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold enqueue_atomic_spec; intros. subdestruct.
specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
specialize (enqueue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
eapply release_lock_ABTCB_match; eauto.
Qed.
Lemma enqueue_atomic_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem enqueue_atomic_spec)
(id ↦ gensem enqueue_atomic_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit enqueue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
assert (Hm: match_AbData s d1´ m2 ι) by (eapply enqueue_atomic_match; eauto).
match_external_states_simpl.
Qed.
Lemma dequeue_atomic_exist:
∀ s habd habd´ labd i z f,
dequeue_atomic_spec i habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, dequeue_atomic_spec i labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold dequeue_atomic_spec; intros.
revert H; subrewrite. subdestruct.
specialize (acquire_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct H0).
intros [d0 [Hacq Hrel]]. rewrite Hacq.
specialize (dequeue0_exist _ _ _ _ _ _ _ Hdestruct0 Hrel).
intros [d1 [Henq Hrel1]]. rewrite Henq.
specialize (release_lock_ABTCB_exist _ _ _ _ _ _ Hdestruct2 Hrel1).
intros [d2 [Hrls Hrel2]]. rewrite Hrls.
∃ d2. subst. inv HQ. eauto.
Qed.
Lemma dequeue_atomic_match:
∀ s d d´ m i z f,
dequeue_atomic_spec i d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold dequeue_atomic_spec; intros. subdestruct.
specialize (acquire_lock_ABTCB_match _ _ _ _ _ _ Hdestruct H0). intros Hm1.
specialize (dequeue0_match _ _ _ _ _ _ _ Hdestruct0 Hm1).
eapply release_lock_ABTCB_match; eauto. inversion H. subst. eauto.
Qed.
Lemma dequeue_atomic_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem dequeue_atomic_spec)
(id ↦ gensem dequeue_atomic_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit dequeue_atomic_exist; eauto 1; intros [labd´ [HP HM]].
assert (Hm: match_AbData s d1´ m2 ι) by (eapply dequeue_atomic_match; eauto).
match_external_states_simpl.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_SC_Log_Pool_gss. eauto.
Qed.
Lemma palloc_match:
∀ s d d´ m n i f,
palloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_spec; intros. inv H0.
subdestruct; inv H; subst; trivial.
- constructor; eauto.
- constructor; eauto.
- constructor; eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptAllocPDE0_match:
∀ s n v i d d´ m f,
ptAllocPDE0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptAllocPDE0_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- exploit palloc_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptInsert0_match:
∀ s n v pa pe d d´ m i f,
ptInsert0_spec n v pa pe d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptInsert0_spec; intros. subdestruct; inv H; trivial.
- exploit ptInsertPTE0_match; eauto.
- eapply ptAllocPDE0_match; eauto.
- exploit ptInsertPTE0_match; eauto.
eapply ptAllocPDE0_match; eauto.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv_match:
∀ s d d´ m i n v p f,
ptResv_spec n v p d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma ptResv2_match:
∀ s d d´ m i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv2_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma offer_shared_mem_match:
∀ s d d´ m i1 i2 v z f,
offer_shared_mem_spec i1 i2 v d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold offer_shared_mem_spec; intros. subdestruct; inv H; trivial.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
constructor; eauto.
- inv H0. constructor; eauto.
Qed.
Lemma GetSharedBuffer_relate:
∀ l l´ s
(Hrel: relate_SC_Log s l l´),
GetSharedBuffer l´ = GetSharedBuffer l.
Proof.
induction l; simpl; intros. inv Hrel. trivial.
inv Hrel. inv Hrelate_event; simpl; eauto.
Qed.
Require Import CVIntroGenLemma.
Lemma index2Z_unique:
∀ i i´ ofs ofs´ z
(Hindex1: index2Z i ofs = Some z)
(Hindex2: index2Z i´ ofs´ = Some z),
i = i´.
Proof.
intros.
functional inversion Hindex1;
functional inversion Hindex2.
functional inversion H0;
functional inversion H4; trivial; subst; simpl in *; subst;
(inv H5; inv H1; unfold lock_TCB_range, ID_SC_range, ID_TCB_range, ID_AT_range in *; omega).
Qed.
Lemma lock_SC_range:
∀ ofs z
(Hindex: index2Z 2 ofs = Some z),
0 ≤ z - lock_TCB_range < 1040.
Proof.
intros. functional inversion Hindex. subst.
functional inversion H0; subst. simpl in H1.
inv H1. replace (lock_TCB_range + ofs - lock_TCB_range) with ofs by omega.
unfold ID_SC_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. simpl in ×.
assert (Hrange: 0 ≤ z - lock_TCB_range < 1040).
{
eapply lock_SC_range; eauto.
}
pose proof (H1 _ Hrange) as Hrel.
replace (z - lock_TCB_range + lock_TCB_range) with z in Hrel by omega.
rewrite Hdestruct7 in Hrel. inv Hrel.
exploit page_copy_aux_exists; eauto.
intros Hpage. rewrite Hpage.
assert (Hrel: relate_SC_Log s (TEVENT (CPU_ID labd)
(TSHARED (OBUFFERE l0)) :: l)
(TEVENT (CPU_ID labd) (TSHARED (OBUFFERE l0)) :: l2)).
{
constructor; eauto. econstructor.
}
erewrite H_CalLock_relate_SC_log; eauto.
refine_split´; try trivial.
econstructor; simpl; eauto.
econstructor.
- intros. destruct (zeq r z); subst.
+ elim H2. eapply index2Z_unique; eauto.
+ repeat rewrite ZMap.gso; eauto.
- intros. destruct (zeq i0 (z - lock_TCB_range)); subst.
+ replace (z - lock_TCB_range + lock_TCB_range) with z by omega.
repeat rewrite ZMap.gss. econstructor. trivial.
+ assert (Hneq: i0 + lock_TCB_range ≠ z) by omega.
repeat rewrite ZMap.gso; auto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros.
subdestruct.
inv H. inv H0.
econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inversion H0.
revert H. subrewrite.
subdestruct. inv HQ.
pose proof multi_log_re as multi_log_re´.
inv multi_log_re. simpl in ×.
assert (Hrange: 0 ≤ z - lock_TCB_range < 1040).
{
eapply lock_SC_range; eauto.
}
pose proof (H1 _ Hrange) as Hrel.
replace (z - lock_TCB_range + lock_TCB_range) with z in Hrel by omega.
rewrite Hdestruct7 in Hrel. inv Hrel.
erewrite GetSharedBuffer_relate; eauto. rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros (lh´ & Hback & Hinj). rewrite Hback.
refine_split´; try trivial.
econstructor; simpl; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit page_copy_back_exist; eauto 1.
exploit page_copy_back_match; eauto 1.
intros.
destruct H0 as (labd´ & HM & HR).
match_external_states_simpl.
Qed.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
- eapply flatmem_store_match; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pcvintro_passthrough pabqueue_atomic.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply palloc_match; eauto).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply ptResv_match; eauto).
match_external_states_simpl.
- apply kctxt_new_sim.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply offer_shared_mem_match; eauto).
match_external_states_simpl.
- apply get_state0_sim.
- apply set_state0_sim.
- apply get_abtcb_CPU_ID_sim.
- apply set_abtcb_CPU_ID_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit tdqueue_init_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply tdqueue_init_match; eauto).
match_external_states_simpl.
- apply enqueue0_sim.
- apply dequeue0_sim.
- apply enqueue_atomic_sim.
- apply dequeue_atomic_sim.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_sim.
- apply trapin_sim.
- apply trapout_sim.
- apply hostin_sim.
- apply hostout_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End WITHMEM.
End Refinement.