Library mcertikos.objects.ObjFlatMem
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import LogReplay.
Section OBJ_FLATMEM.
Local Open Scope Z_scope.
primitve: store to the heap
Function flatmem_store´ (adt: RData) (chunk: memory_chunk) (addr: Z) (v: val): option RData :=
Some adt {HP: FlatMem.store chunk (HP adt) addr v}.
Function flatmem_store (adt: RData) (chunk: memory_chunk) (addr: Z) (v: val): option RData :=
match ZMap.get (PageI addr) (pperm adt) with
| PGAlloc ⇒ Some adt {HP: FlatMem.store chunk (HP adt) addr v}
| _ ⇒ None
end.
Some adt {HP: FlatMem.store chunk (HP adt) addr v}.
Function flatmem_store (adt: RData) (chunk: memory_chunk) (addr: Z) (v: val): option RData :=
match ZMap.get (PageI addr) (pperm adt) with
| PGAlloc ⇒ Some adt {HP: FlatMem.store chunk (HP adt) addr v}
| _ ⇒ None
end.
primitve: store to the heap
Function fstore´_spec (addr v: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store´ adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fstore0_spec (addr v: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fstore_spec (addr v: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fload´_spec (addr: Z) (adt: RData): option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
match FlatMem.load Mint32 (HP adt) (addr × 4) with
| Vint n ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function fload_spec (addr: Z) (adt: RData): option Z :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 addr adr_low then
match (ZMap.get (PageI (addr × 4)) (pperm adt),
FlatMem.load Mint32 (HP adt) (addr × 4)) with
| (PGAlloc, Vint n) ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Fixpoint flatmem_copy_aux (n: nat) (from to: Z) (h: flatmem) :=
match n with
| O ⇒ Some h
| S n´ ⇒
match FlatMem.load Mint32 h from with
| Vint v ⇒
flatmem_copy_aux n´ (from + 4) (to + 4) (FlatMem.store Mint32 h to (Vint v))
| _ ⇒ None
end
end.
Fixpoint page_copy_aux (n: nat) (from: Z) (h: flatmem) :=
match n with
| O ⇒ Some nil
| S n´ ⇒
match FlatMem.load Mint32 h from with
| Vint v ⇒
match page_copy_aux n´ (from + 4) h with
| Some l ⇒ Some (v :: l)
| _ ⇒ None
end
| _ ⇒ None
end
end.
Fixpoint page_copy_back_aux (n: nat) (to: Z) (l: PageBuffer) (h: flatmem) :=
match n with
| O ⇒ Some h
| S n´ ⇒
match l with
| v :: l´ ⇒
page_copy_back_aux n´ (to + 4) l´ (FlatMem.store Mint32 h to (Vint v))
| _ ⇒ None
end
end.
Section COPY_INV.
Lemma PageI_monotonic:
∀ a b,
a ≤ b →
PageI a ≤ PageI b.
Proof.
unfold PageI.
intros. eapply Z_div_le; eauto.
omega.
Qed.
Lemma PageI_range:
∀ a b c,
a ≤ b ≤ c→
PageI a = PageI c →
PageI b = PageI a.
Proof.
intros.
assert (HR1: PageI a ≤ PageI b) by (eapply PageI_monotonic; try omega).
assert (HR2: PageI b ≤ PageI c) by (eapply PageI_monotonic; try omega).
omega.
Qed.
Lemma to_range:
∀ to n,
to ≤ to + 4 ≤ to + Z.of_nat (S (n + 1)) × 4 - 4.
Proof.
intros.
erewrite Nat2Z.inj_succ.
replace ((n + 1)%nat) with (S n) by omega.
erewrite Nat2Z.inj_succ.
pose proof (Nat2Z.is_nonneg n).
omega.
Qed.
Lemma to_mod_le:
∀ to,
(4 | to) →
to mod 4096 ≤ 4092.
Proof.
intros.
destruct H as (i & He).
subst.
change 4096 with (4 × 1024) in ×.
replace (i × 4) with (4 × i) by omega.
rewrite Zmult_mod_distr_l in ×.
assert (i mod 1024 < 1024).
{
eapply Z_mod_lt. omega.
}
omega.
Qed.
Lemma to_add_divide:
∀ to,
(4 | to) →
(4 | to + 4).
Proof.
intros.
destruct H as (i & He).
subst.
∃ (i + 1). omega.
Qed.
Lemma PageI_eq:
∀ to n,
PageI to = PageI (to + Z.of_nat (S (n + 1)) × 4 - 4) →
PageI (to + 4) = PageI (to + 4 + Z.of_nat (n + 1) × 4 - 4).
Proof.
intros.
rewrite Nat2Z.inj_succ in H.
replace ((n + 1)%nat) with (S n) in × by omega.
rewrite Nat2Z.inj_succ in ×.
pose proof (Nat2Z.is_nonneg n).
erewrite (PageI_range to (to + 4 + Z.succ (Z.of_nat n) × 4 - 4)); eauto.
erewrite (PageI_range to (to + 4)); eauto.
omega.
omega.
Qed.
Lemma 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) →
dirty_ppage pp h →
flatmem_copy_aux (n + 1) from to h = Some h´ →
dirty_ppage pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply dirty_ppage_store_unmaped´; 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 dirty_ppage_store_unmaped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma 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) →
dirty_ppage pp h →
page_copy_back_aux (n + 1) to l h = Some h´ →
dirty_ppage pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply dirty_ppage_store_unmaped´; 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 dirty_ppage_store_unmaped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma PageI_divide´:
∀ to n,
(4096 | to) →
1 ≤ n ≤ 1024 →
PageI to = PageI (to + n × 4 - 4).
Proof.
intros. destruct H as (i & He). subst.
unfold PageI.
assert (4096 > 0) by omega.
replace (i × 4096 + n × 4 - 4)
with (n × 4 - 4 + i × 4096) by omega.
rewrite Z_div_plus; trivial.
rewrite Z_div_mult; trivial.
rewrite Zdiv_small; trivial.
omega.
Qed.
Lemma PageI_divide:
∀ to n,
(4096 | to) →
Z.of_nat (n + 1) ≤ 1024 →
PageI to = PageI (to + Z.of_nat (n + 1) × 4 - 4).
Proof.
intros. eapply PageI_divide´; eauto.
replace ((n + 1)%nat) with (S n) in × by omega.
rewrite Nat2Z.inj_succ in ×.
pose proof (Nat2Z.is_nonneg n).
omega.
Qed.
Lemma dirty_ppage_gss_copy´:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
dirty_ppage pp h →
flatmem_copy_aux n from to h = Some h´ →
dirty_ppage pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage_gss_copy_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage pp h →
page_copy_back_aux n to l h = Some h´ →
dirty_ppage pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage_gss_page_copy_back_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage pp h →
dirty_ppage pp h´.
Proof.
intros.
eapply dirty_ppage_gss_copy´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma 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 →
dirty_ppage pp h →
dirty_ppage pp h´.
Proof.
intros.
eapply dirty_ppage_gss_page_copy_back´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma 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) →
dirty_ppage´ pp h →
flatmem_copy_aux (n + 1) from to h = Some h´ →
dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply 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 dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma 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) →
dirty_ppage´ pp h →
page_copy_back_aux (n + 1) to l h = Some h´ →
dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply 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 dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma dirty_ppage´_gss_copy´:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
dirty_ppage´ pp h →
flatmem_copy_aux n from to h = Some h´ →
dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage´_gss_copy_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage´ pp h →
page_copy_back_aux n to l h = Some h´ →
dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage´_gss_page_copy_back_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage´ pp h →
dirty_ppage´ pp h´.
Proof.
intros.
eapply dirty_ppage´_gss_page_copy_back´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma dirty_ppage´_gso_alloc:
∀ pp h,
dirty_ppage´ pp h →
∀ n,
dirty_ppage´ (ZMap.set n PGAlloc pp) h.
Proof.
intros. apply dirty_ppage´_gso; try assumption.
Qed.
End COPY_INV.
Function flatmem_copy´_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Context `{waittime: WaitTime}.
Function page_copy´´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match Q_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Require Import CalMCSLock.
Function mcs_page_copy´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match QS_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back´_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function flatmem_copy0_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match (ZMap.get (PageI from) (pperm adt), ZMap.get (PageI to) (pperm adt)) with
| (PGAlloc, PGAlloc) ⇒
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Function page_copy0_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back0_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function flatmem_copy_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match (ZMap.get (PageI from) (pperm adt), ZMap.get (PageI to) (pperm adt)) with
| (PGAlloc, PGAlloc) ⇒
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
End OBJ_FLATMEM.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{waittime: WaitTime}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section FSTORE´_SIM.
Context {re2: relate_impl_HP}.
Lemma flatmem_store´_exists:
∀ s hadt ladt hadt´ t addr v v´ f,
flatmem_store´ hadt t addr v = Some hadt´
→ relate_AbData s f hadt ladt
→ val_inject f v v´
→ ∃ ladt´,
flatmem_store´ ladt t addr v´ = Some ladt´
∧ relate_AbData s f hadt´ ladt´.
Proof.
unfold flatmem_store´. intros.
revert H. subrewrite. inv HQ.
refine_split´; eauto.
eapply relate_impl_HP_update; eauto.
eapply (FlatMem.store_mapped_inj f); trivial.
eapply relate_impl_HP_eq; eauto. assumption.
Qed.
Context {re1: relate_impl_iflags}.
Lemma fstore´_exist:
∀ s habd habd´ labd i v f,
fstore´_spec i v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fstore´_spec i v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold fstore´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
subdestruct. eapply flatmem_store´_exists; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma fstore´_match:
∀ s d d´ m i v f,
fstore´_spec i v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fstore´_spec, flatmem_store´; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) fstore´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) fstore´_spec}.
Lemma fstore´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fstore´_spec)
(id ↦ gensem fstore´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fstore´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply fstore´_match; eauto.
Qed.
End FSTORE´_SIM.
Section FSTORE_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Lemma flatmem_store_exists:
∀ s hadt ladt hadt´ t addr v v´ f,
flatmem_store hadt t addr v = Some hadt´
→ relate_AbData s f hadt ladt
→ val_inject f v v´
→ ∃ ladt´,
flatmem_store ladt t addr v´ = Some ladt´
∧ relate_AbData s f hadt´ ladt´.
Proof.
unfold flatmem_store. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite. subdestruct. inv HQ.
refine_split´; eauto.
eapply relate_impl_HP_update; eauto.
eapply (FlatMem.store_mapped_inj f); trivial.
eapply relate_impl_HP_eq; eauto. assumption.
Qed.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_ipt}.
Lemma fstore_exist:
∀ s habd habd´ labd i v f,
fstore_spec i v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fstore_spec i v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold fstore_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. eapply flatmem_store_exists; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_store_match:
∀ s d d´ m i v t f,
flatmem_store d t i v = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_store; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Lemma fstore_match:
∀ s d d´ m i v f,
fstore_spec i v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fstore_spec, flatmem_store; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) fstore_spec}.
Context {inv0: PreservesInvariants (HD:= data0) fstore_spec}.
Lemma fstore_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fstore_spec)
(id ↦ gensem fstore_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fstore_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply fstore_match; eauto.
Qed.
End FSTORE_SIM.
Section FLOAD´_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_HP}.
Lemma fload´_exist:
∀ s habd labd i z f,
fload´_spec i habd = Some z
→ relate_AbData s f habd labd
→ fload´_spec i labd = Some z.
Proof.
unfold fload´_spec; intros.
exploit relate_impl_iflags_eq; eauto.
inversion 1.
pose proof (relate_impl_HP_eq _ _ _ _ H0) as Hre.
specialize (FlatMem.load_inj _ _ Mint32 (i × 4) _ f Hre refl_equal).
revert H. subrewrite.
subdestruct. intros (v2 & HLD & HVAL).
rewrite HLD. inv HVAL. assumption.
Qed.
Lemma fload´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fload´_spec) (id ↦ gensem fload´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite fload´_exist; eauto.
reflexivity.
Qed.
End FLOAD´_SIM.
Section FLOAD_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_HP}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_pperm}.
Lemma fload_exist:
∀ s habd labd i z f,
fload_spec i habd = Some z
→ relate_AbData s f habd labd
→ fload_spec i labd = Some z.
Proof.
unfold fload_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_pperm_eq; eauto. intros.
pose proof (relate_impl_HP_eq _ _ _ _ H0) as Hre.
specialize (FlatMem.load_inj _ _ Mint32 (i × 4) _ f Hre refl_equal).
revert H. subrewrite.
subdestruct. intros (v2 & HLD & HVAL).
rewrite HLD. inv HVAL. assumption.
Qed.
Lemma fload_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fload_spec) (id ↦ gensem fload_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite fload_exist; eauto.
reflexivity.
Qed.
End FLOAD_SIM.
Section MEM_COPY_AUX_SIM.
Context {re1: relate_impl_HP}.
Lemma flatmem_copy_aux_exists:
∀ n hh hh´ lh from to (f: meminj),
flatmem_copy_aux n from to hh = Some hh´ →
FlatMem.flatmem_inj hh lh →
∃ lh´,
flatmem_copy_aux n from to lh = Some lh´
∧ FlatMem.flatmem_inj hh´ lh´.
Proof.
induction n.
- simpl. intros. inv H.
refine_split´; trivial.
- intros. simpl in ×.
subdestruct.
specialize (FlatMem.load_inj _ _ Mint32 from _ f H0 Hdestruct).
intros (v´ & HLD & HVA).
rewrite HLD. inv HVA.
set (hh0:= FlatMem.store Mint32 hh to (Vint i)) in ×.
set (lh0:=FlatMem.store Mint32 lh to (Vint i)).
assert (HF_INJ: FlatMem.flatmem_inj hh0 lh0).
{
subst hh0 lh0.
eapply (FlatMem.store_mapped_inj f); eauto.
}
exploit IHn; eauto.
Qed.
End MEM_COPY_AUX_SIM.
Section PAGE_COPY_AUX_SIM.
Lemma page_copy_aux_exists:
∀ n hh l lh from (f: meminj),
page_copy_aux n from hh = Some l →
FlatMem.flatmem_inj hh lh →
page_copy_aux n from lh = Some l.
Proof.
induction n.
- simpl. intros. inv H. trivial.
- intros. simpl in ×.
subdestruct.
specialize (FlatMem.load_inj _ _ Mint32 from _ f H0 Hdestruct).
intros (v´ & HLD & HVA).
rewrite HLD. inv HVA.
exploit IHn; eauto.
intro Hcopy. rewrite Hcopy.
trivial.
Qed.
End PAGE_COPY_AUX_SIM.
Section PAGE_COPY_BACK_AUX_SIM.
Lemma page_copy_back_aux_exists:
∀ n hh hh´ lh to l (f: meminj),
page_copy_back_aux n to l hh = Some hh´ →
FlatMem.flatmem_inj hh lh →
∃ lh´,
page_copy_back_aux n to l lh = Some lh´
∧ FlatMem.flatmem_inj hh´ lh´.
Proof.
induction n.
- simpl. intros. inv H.
refine_split´; trivial.
- intros. simpl in ×.
subdestruct.
set (hh0:= FlatMem.store Mint32 hh to (Vint i)) in ×.
set (lh0:=FlatMem.store Mint32 lh to (Vint i)).
assert (HF_INJ: FlatMem.flatmem_inj hh0 lh0).
{
subst hh0 lh0.
eapply (FlatMem.store_mapped_inj f); eauto.
}
exploit IHn; eauto.
Qed.
End PAGE_COPY_BACK_AUX_SIM.
Section MEM_COPY´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Lemma flatmem_copy´_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy´_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy´_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy´_match:
∀ s d d´ m i from to f,
flatmem_copy´_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy´_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy´_spec}.
Lemma flatmem_copy´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy´_spec)
(id ↦ gensem flatmem_copy´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy´_match; eauto.
Qed.
End MEM_COPY´_SIM.
Section PAGE_COPY_BACK´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy_back´_exist:
∀ s habd habd´ labd i to index 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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
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. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back´_match; eauto.
Qed.
End PAGE_COPY_BACK´_SIM.
Section PAGE_COPY´´´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy´´´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy´´´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY´´´_SIM.
Section PAGE_COPY´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct9. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy´_match; eauto.
Qed.
End PAGE_COPY´_SIM.
Section MEM_COPY0_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Context {re3: relate_impl_iflags}.
Lemma flatmem_copy0_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy0_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy0_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy0 & Hinj).
rewrite HCopy0. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy0_match:
∀ s d d´ m i from to f,
flatmem_copy0_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy0_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy0_spec}.
Lemma flatmem_copy0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy0_spec)
(id ↦ gensem flatmem_copy0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy0_match; eauto.
Qed.
End MEM_COPY0_SIM.
Section PAGE_COPY_BACK0_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy_back0_exist:
∀ s habd habd´ labd index i to f,
page_copy_back0_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back0_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma page_copy_back0_match:
∀ s d d´ m index i to f,
page_copy_back0_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back0_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back0_spec}.
Lemma page_copy_back0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back0_spec)
(id ↦ gensem page_copy_back0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back0_match; eauto.
Qed.
End PAGE_COPY_BACK0_SIM.
Section PAGE_COPY0_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy0_exist:
∀ s habd habd´ labd index i from f,
page_copy0_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy0_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct10. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
Lemma page_copy0_match:
∀ s d d´ m index i from f,
page_copy0_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy0_spec; intros. subdestruct.
inv H. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy0_spec}.
Lemma page_copy0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy0_spec)
(id ↦ gensem page_copy0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy0_match; eauto.
Qed.
End PAGE_COPY0_SIM.
Section MEM_COPY_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_ipt}.
Lemma flatmem_copy_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy & Hinj).
rewrite HCopy. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy_match:
∀ s d d´ m i from to f,
flatmem_copy_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy_spec}.
Lemma flatmem_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy_spec)
(id ↦ gensem flatmem_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy_match; eauto.
Qed.
End MEM_COPY_SIM.
Section PAGE_COPY_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct11. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_match; eauto.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_lock}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
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. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back_match; eauto.
Qed.
End PAGE_COPY_BACK_SIM.
End OBJ_SIM.
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store´ adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fstore0_spec (addr v: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fstore_spec (addr v: Z) (adt: RData): option RData :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 addr adr_low then
flatmem_store adt Mint32 (addr × 4) (Vint (Int.repr v))
else None
| _ ⇒ None
end.
Function fload´_spec (addr: Z) (adt: RData): option Z :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 addr adr_low then
match FlatMem.load Mint32 (HP adt) (addr × 4) with
| Vint n ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function fload_spec (addr: Z) (adt: RData): option Z :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 addr adr_low then
match (ZMap.get (PageI (addr × 4)) (pperm adt),
FlatMem.load Mint32 (HP adt) (addr × 4)) with
| (PGAlloc, Vint n) ⇒ Some (Int.unsigned n)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Fixpoint flatmem_copy_aux (n: nat) (from to: Z) (h: flatmem) :=
match n with
| O ⇒ Some h
| S n´ ⇒
match FlatMem.load Mint32 h from with
| Vint v ⇒
flatmem_copy_aux n´ (from + 4) (to + 4) (FlatMem.store Mint32 h to (Vint v))
| _ ⇒ None
end
end.
Fixpoint page_copy_aux (n: nat) (from: Z) (h: flatmem) :=
match n with
| O ⇒ Some nil
| S n´ ⇒
match FlatMem.load Mint32 h from with
| Vint v ⇒
match page_copy_aux n´ (from + 4) h with
| Some l ⇒ Some (v :: l)
| _ ⇒ None
end
| _ ⇒ None
end
end.
Fixpoint page_copy_back_aux (n: nat) (to: Z) (l: PageBuffer) (h: flatmem) :=
match n with
| O ⇒ Some h
| S n´ ⇒
match l with
| v :: l´ ⇒
page_copy_back_aux n´ (to + 4) l´ (FlatMem.store Mint32 h to (Vint v))
| _ ⇒ None
end
end.
Section COPY_INV.
Lemma PageI_monotonic:
∀ a b,
a ≤ b →
PageI a ≤ PageI b.
Proof.
unfold PageI.
intros. eapply Z_div_le; eauto.
omega.
Qed.
Lemma PageI_range:
∀ a b c,
a ≤ b ≤ c→
PageI a = PageI c →
PageI b = PageI a.
Proof.
intros.
assert (HR1: PageI a ≤ PageI b) by (eapply PageI_monotonic; try omega).
assert (HR2: PageI b ≤ PageI c) by (eapply PageI_monotonic; try omega).
omega.
Qed.
Lemma to_range:
∀ to n,
to ≤ to + 4 ≤ to + Z.of_nat (S (n + 1)) × 4 - 4.
Proof.
intros.
erewrite Nat2Z.inj_succ.
replace ((n + 1)%nat) with (S n) by omega.
erewrite Nat2Z.inj_succ.
pose proof (Nat2Z.is_nonneg n).
omega.
Qed.
Lemma to_mod_le:
∀ to,
(4 | to) →
to mod 4096 ≤ 4092.
Proof.
intros.
destruct H as (i & He).
subst.
change 4096 with (4 × 1024) in ×.
replace (i × 4) with (4 × i) by omega.
rewrite Zmult_mod_distr_l in ×.
assert (i mod 1024 < 1024).
{
eapply Z_mod_lt. omega.
}
omega.
Qed.
Lemma to_add_divide:
∀ to,
(4 | to) →
(4 | to + 4).
Proof.
intros.
destruct H as (i & He).
subst.
∃ (i + 1). omega.
Qed.
Lemma PageI_eq:
∀ to n,
PageI to = PageI (to + Z.of_nat (S (n + 1)) × 4 - 4) →
PageI (to + 4) = PageI (to + 4 + Z.of_nat (n + 1) × 4 - 4).
Proof.
intros.
rewrite Nat2Z.inj_succ in H.
replace ((n + 1)%nat) with (S n) in × by omega.
rewrite Nat2Z.inj_succ in ×.
pose proof (Nat2Z.is_nonneg n).
erewrite (PageI_range to (to + 4 + Z.succ (Z.of_nat n) × 4 - 4)); eauto.
erewrite (PageI_range to (to + 4)); eauto.
omega.
omega.
Qed.
Lemma 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) →
dirty_ppage pp h →
flatmem_copy_aux (n + 1) from to h = Some h´ →
dirty_ppage pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply dirty_ppage_store_unmaped´; 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 dirty_ppage_store_unmaped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma 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) →
dirty_ppage pp h →
page_copy_back_aux (n + 1) to l h = Some h´ →
dirty_ppage pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply dirty_ppage_store_unmaped´; 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 dirty_ppage_store_unmaped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma PageI_divide´:
∀ to n,
(4096 | to) →
1 ≤ n ≤ 1024 →
PageI to = PageI (to + n × 4 - 4).
Proof.
intros. destruct H as (i & He). subst.
unfold PageI.
assert (4096 > 0) by omega.
replace (i × 4096 + n × 4 - 4)
with (n × 4 - 4 + i × 4096) by omega.
rewrite Z_div_plus; trivial.
rewrite Z_div_mult; trivial.
rewrite Zdiv_small; trivial.
omega.
Qed.
Lemma PageI_divide:
∀ to n,
(4096 | to) →
Z.of_nat (n + 1) ≤ 1024 →
PageI to = PageI (to + Z.of_nat (n + 1) × 4 - 4).
Proof.
intros. eapply PageI_divide´; eauto.
replace ((n + 1)%nat) with (S n) in × by omega.
rewrite Nat2Z.inj_succ in ×.
pose proof (Nat2Z.is_nonneg n).
omega.
Qed.
Lemma dirty_ppage_gss_copy´:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
dirty_ppage pp h →
flatmem_copy_aux n from to h = Some h´ →
dirty_ppage pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage_gss_copy_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage pp h →
page_copy_back_aux n to l h = Some h´ →
dirty_ppage pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage_gss_page_copy_back_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage pp h →
dirty_ppage pp h´.
Proof.
intros.
eapply dirty_ppage_gss_copy´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma 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 →
dirty_ppage pp h →
dirty_ppage pp h´.
Proof.
intros.
eapply dirty_ppage_gss_page_copy_back´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma 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) →
dirty_ppage´ pp h →
flatmem_copy_aux (n + 1) from to h = Some h´ →
dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply 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 dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma 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) →
dirty_ppage´ pp h →
page_copy_back_aux (n + 1) to l h = Some h´ →
dirty_ppage´ pp h´.
Proof.
intros until n.
induction n.
- simpl; intros.
subdestruct. inv H3.
eapply 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 dirty_ppage´_store_unmapped´; eauto.
eapply to_mod_le; eauto.
Qed.
Lemma dirty_ppage´_gss_copy´:
∀ n h h´ pp from to,
ZMap.get (PageI to) pp = PGAlloc →
(PgSize | to) →
Z.of_nat n ≤ one_k →
dirty_ppage´ pp h →
flatmem_copy_aux n from to h = Some h´ →
dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage´_gss_copy_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage´ pp h →
page_copy_back_aux n to l h = Some h´ →
dirty_ppage´ pp h´.
Proof.
destruct n; intros.
- simpl in ×. inv H3. assumption.
- replace (S n) with ((n + 1)%nat) in × by omega.
eapply dirty_ppage´_gss_page_copy_back_plus; eauto.
destruct H0 as (i & He).
∃ (i × 1024).
subst. omega.
eapply PageI_divide; eauto.
Qed.
Lemma 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 →
dirty_ppage´ pp h →
dirty_ppage´ pp h´.
Proof.
intros.
eapply dirty_ppage´_gss_page_copy_back´; eauto.
rewrite Z2Nat.id; try omega.
Qed.
Lemma dirty_ppage´_gso_alloc:
∀ pp h,
dirty_ppage´ pp h →
∀ n,
dirty_ppage´ (ZMap.set n PGAlloc pp) h.
Proof.
intros. apply dirty_ppage´_gso; try assumption.
Qed.
End COPY_INV.
Function flatmem_copy´_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Context `{waittime: WaitTime}.
Function page_copy´´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match Q_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Require Import CalMCSLock.
Function mcs_page_copy´´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match QS_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy´_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back´_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function flatmem_copy0_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt) with
| (true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match (ZMap.get (PageI from) (pperm adt), ZMap.get (PageI to) (pperm adt)) with
| (PGAlloc, PGAlloc) ⇒
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Function page_copy0_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back0_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, index2Z ID_SC index) with
| (true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt) with
| MultiDef l ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function flatmem_copy_spec (count: Z) (from to: Z) (adt: RData) :=
match (ikern adt, ihost adt, ipt adt) with
| (true, true, true) ⇒
if zle_lt 0 to adr_low then
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
if Zdivide_dec PgSize from HPS then
match (ZMap.get (PageI from) (pperm adt), ZMap.get (PageI to) (pperm adt)) with
| (PGAlloc, PGAlloc) ⇒
match flatmem_copy_aux (Z.to_nat count) from to (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_spec (cv: Z) (count: Z) (from: Z) (adt: RData) :=
let cpu := CPU_ID adt in
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match page_copy_aux (Z.to_nat count) from (HP adt) with
| Some b ⇒
let l´ := TEVENT cpu (TSHARED (OBUFFERE b)) :: l in
match H_CalLock l´ with
| Some _ ⇒ Some adt {multi_log: ZMap.set abid (MultiDef l´) (multi_log adt)}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function page_copy_back_spec (cv: Z) (count: Z) (to: Z) (adt: RData) :=
let index := slp_q_id cv 0 in
match (ikern adt, ihost adt, ipt adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm adt) with
| PGAlloc ⇒
match ZMap.get abid (multi_log adt), ZMap.get abid (lock adt) with
| MultiDef l, LockOwn true ⇒
match GetSharedBuffer l with
| Some b ⇒
match page_copy_back_aux (Z.to_nat count) to b (HP adt) with
| Some h ⇒ Some adt {HP: h}
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
End OBJ_FLATMEM.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{waittime: WaitTime}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Section FSTORE´_SIM.
Context {re2: relate_impl_HP}.
Lemma flatmem_store´_exists:
∀ s hadt ladt hadt´ t addr v v´ f,
flatmem_store´ hadt t addr v = Some hadt´
→ relate_AbData s f hadt ladt
→ val_inject f v v´
→ ∃ ladt´,
flatmem_store´ ladt t addr v´ = Some ladt´
∧ relate_AbData s f hadt´ ladt´.
Proof.
unfold flatmem_store´. intros.
revert H. subrewrite. inv HQ.
refine_split´; eauto.
eapply relate_impl_HP_update; eauto.
eapply (FlatMem.store_mapped_inj f); trivial.
eapply relate_impl_HP_eq; eauto. assumption.
Qed.
Context {re1: relate_impl_iflags}.
Lemma fstore´_exist:
∀ s habd habd´ labd i v f,
fstore´_spec i v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fstore´_spec i v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold fstore´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
subdestruct. eapply flatmem_store´_exists; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma fstore´_match:
∀ s d d´ m i v f,
fstore´_spec i v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fstore´_spec, flatmem_store´; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) fstore´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) fstore´_spec}.
Lemma fstore´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fstore´_spec)
(id ↦ gensem fstore´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fstore´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply fstore´_match; eauto.
Qed.
End FSTORE´_SIM.
Section FSTORE_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Lemma flatmem_store_exists:
∀ s hadt ladt hadt´ t addr v v´ f,
flatmem_store hadt t addr v = Some hadt´
→ relate_AbData s f hadt ladt
→ val_inject f v v´
→ ∃ ladt´,
flatmem_store ladt t addr v´ = Some ladt´
∧ relate_AbData s f hadt´ ladt´.
Proof.
unfold flatmem_store. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite. subdestruct. inv HQ.
refine_split´; eauto.
eapply relate_impl_HP_update; eauto.
eapply (FlatMem.store_mapped_inj f); trivial.
eapply relate_impl_HP_eq; eauto. assumption.
Qed.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_ipt}.
Lemma fstore_exist:
∀ s habd habd´ labd i v f,
fstore_spec i v habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, fstore_spec i v labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold fstore_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. eapply flatmem_store_exists; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_store_match:
∀ s d d´ m i v t f,
flatmem_store d t i v = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_store; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Lemma fstore_match:
∀ s d d´ m i v f,
fstore_spec i v d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold fstore_spec, flatmem_store; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) fstore_spec}.
Context {inv0: PreservesInvariants (HD:= data0) fstore_spec}.
Lemma fstore_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fstore_spec)
(id ↦ gensem fstore_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit fstore_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply fstore_match; eauto.
Qed.
End FSTORE_SIM.
Section FLOAD´_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_HP}.
Lemma fload´_exist:
∀ s habd labd i z f,
fload´_spec i habd = Some z
→ relate_AbData s f habd labd
→ fload´_spec i labd = Some z.
Proof.
unfold fload´_spec; intros.
exploit relate_impl_iflags_eq; eauto.
inversion 1.
pose proof (relate_impl_HP_eq _ _ _ _ H0) as Hre.
specialize (FlatMem.load_inj _ _ Mint32 (i × 4) _ f Hre refl_equal).
revert H. subrewrite.
subdestruct. intros (v2 & HLD & HVAL).
rewrite HLD. inv HVAL. assumption.
Qed.
Lemma fload´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fload´_spec) (id ↦ gensem fload´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite fload´_exist; eauto.
reflexivity.
Qed.
End FLOAD´_SIM.
Section FLOAD_SIM.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_HP}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_pperm}.
Lemma fload_exist:
∀ s habd labd i z f,
fload_spec i habd = Some z
→ relate_AbData s f habd labd
→ fload_spec i labd = Some z.
Proof.
unfold fload_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_pperm_eq; eauto. intros.
pose proof (relate_impl_HP_eq _ _ _ _ H0) as Hre.
specialize (FlatMem.load_inj _ _ Mint32 (i × 4) _ f Hre refl_equal).
revert H. subrewrite.
subdestruct. intros (v2 & HLD & HVAL).
rewrite HLD. inv HVAL. assumption.
Qed.
Lemma fload_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem fload_spec) (id ↦ gensem fload_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
match_external_states_simpl.
erewrite fload_exist; eauto.
reflexivity.
Qed.
End FLOAD_SIM.
Section MEM_COPY_AUX_SIM.
Context {re1: relate_impl_HP}.
Lemma flatmem_copy_aux_exists:
∀ n hh hh´ lh from to (f: meminj),
flatmem_copy_aux n from to hh = Some hh´ →
FlatMem.flatmem_inj hh lh →
∃ lh´,
flatmem_copy_aux n from to lh = Some lh´
∧ FlatMem.flatmem_inj hh´ lh´.
Proof.
induction n.
- simpl. intros. inv H.
refine_split´; trivial.
- intros. simpl in ×.
subdestruct.
specialize (FlatMem.load_inj _ _ Mint32 from _ f H0 Hdestruct).
intros (v´ & HLD & HVA).
rewrite HLD. inv HVA.
set (hh0:= FlatMem.store Mint32 hh to (Vint i)) in ×.
set (lh0:=FlatMem.store Mint32 lh to (Vint i)).
assert (HF_INJ: FlatMem.flatmem_inj hh0 lh0).
{
subst hh0 lh0.
eapply (FlatMem.store_mapped_inj f); eauto.
}
exploit IHn; eauto.
Qed.
End MEM_COPY_AUX_SIM.
Section PAGE_COPY_AUX_SIM.
Lemma page_copy_aux_exists:
∀ n hh l lh from (f: meminj),
page_copy_aux n from hh = Some l →
FlatMem.flatmem_inj hh lh →
page_copy_aux n from lh = Some l.
Proof.
induction n.
- simpl. intros. inv H. trivial.
- intros. simpl in ×.
subdestruct.
specialize (FlatMem.load_inj _ _ Mint32 from _ f H0 Hdestruct).
intros (v´ & HLD & HVA).
rewrite HLD. inv HVA.
exploit IHn; eauto.
intro Hcopy. rewrite Hcopy.
trivial.
Qed.
End PAGE_COPY_AUX_SIM.
Section PAGE_COPY_BACK_AUX_SIM.
Lemma page_copy_back_aux_exists:
∀ n hh hh´ lh to l (f: meminj),
page_copy_back_aux n to l hh = Some hh´ →
FlatMem.flatmem_inj hh lh →
∃ lh´,
page_copy_back_aux n to l lh = Some lh´
∧ FlatMem.flatmem_inj hh´ lh´.
Proof.
induction n.
- simpl. intros. inv H.
refine_split´; trivial.
- intros. simpl in ×.
subdestruct.
set (hh0:= FlatMem.store Mint32 hh to (Vint i)) in ×.
set (lh0:=FlatMem.store Mint32 lh to (Vint i)).
assert (HF_INJ: FlatMem.flatmem_inj hh0 lh0).
{
subst hh0 lh0.
eapply (FlatMem.store_mapped_inj f); eauto.
}
exploit IHn; eauto.
Qed.
End PAGE_COPY_BACK_AUX_SIM.
Section MEM_COPY´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Lemma flatmem_copy´_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy´_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy´_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy´_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy´_match:
∀ s d d´ m i from to f,
flatmem_copy´_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy´_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy´_spec}.
Lemma flatmem_copy´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy´_spec)
(id ↦ gensem flatmem_copy´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy´_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy´_match; eauto.
Qed.
End MEM_COPY´_SIM.
Section PAGE_COPY_BACK´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy_back´_exist:
∀ s habd habd´ labd i to index 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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
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. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back´_match; eauto.
Qed.
End PAGE_COPY_BACK´_SIM.
Section PAGE_COPY´´´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy´´´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy´´´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY´´´_SIM.
Section PAGE_COPY´_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct9. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy´_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy´_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy´_match; eauto.
Qed.
End PAGE_COPY´_SIM.
Section MEM_COPY0_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Context {re3: relate_impl_iflags}.
Lemma flatmem_copy0_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy0_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy0_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy0 & Hinj).
rewrite HCopy0. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy0_match:
∀ s d d´ m i from to f,
flatmem_copy0_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy0_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy0_spec}.
Lemma flatmem_copy0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy0_spec)
(id ↦ gensem flatmem_copy0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy0_match; eauto.
Qed.
End MEM_COPY0_SIM.
Section PAGE_COPY_BACK0_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy_back0_exist:
∀ s habd habd´ labd index i to f,
page_copy_back0_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back0_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma page_copy_back0_match:
∀ s d d´ m index i to f,
page_copy_back0_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back0_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back0_spec}.
Lemma page_copy_back0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back0_spec)
(id ↦ gensem page_copy_back0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back0_match; eauto.
Qed.
End PAGE_COPY_BACK0_SIM.
Section PAGE_COPY0_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
Lemma page_copy0_exist:
∀ s habd habd´ labd index i from f,
page_copy0_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy0_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct10. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
Lemma page_copy0_match:
∀ s d d´ m index i from f,
page_copy0_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy0_spec; intros. subdestruct.
inv H. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy0_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy0_spec}.
Lemma page_copy0_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy0_spec)
(id ↦ gensem page_copy0_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy0_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy0_match; eauto.
Qed.
End PAGE_COPY0_SIM.
Section MEM_COPY_SIM.
Context {re1: relate_impl_HP}.
Context {re2: relate_impl_pperm}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_ipt}.
Lemma flatmem_copy_exist:
∀ s habd habd´ labd i from to f,
flatmem_copy_spec i from to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, flatmem_copy_spec i from to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold flatmem_copy_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit flatmem_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy & Hinj).
rewrite HCopy. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
Lemma flatmem_copy_match:
∀ s d d´ m i from to f,
flatmem_copy_spec i from to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold flatmem_copy_spec; intros. subdestruct.
inv H. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) flatmem_copy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) flatmem_copy_spec}.
Lemma flatmem_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem flatmem_copy_spec)
(id ↦ gensem flatmem_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit flatmem_copy_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply flatmem_copy_match; eauto.
Qed.
End MEM_COPY_SIM.
Section PAGE_COPY_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_lock}.
Context {re400: relate_impl_CPU_ID}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros HCopy´.
rewrite HCopy´. rewrite Hdestruct11. refine_split´; trivial.
eapply relate_impl_multi_log_update; eauto.
Qed.
Context {mt1: match_impl_multi_log}.
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. eapply match_impl_multi_log_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_match; eauto.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Context {re1: relate_impl_HP}.
Context {re3: relate_impl_iflags}.
Context {re4: relate_impl_pperm}.
Context {re5: relate_impl_ipt}.
Context {re6: relate_impl_lock}.
Context {re30: relate_impl_multi_log}.
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.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_multi_log_eq; eauto. intros.
exploit relate_impl_lock_eq; eauto. intros.
revert H. subrewrite.
subdestruct. inv HQ.
exploit page_copy_back_aux_exists; eauto.
eapply relate_impl_HP_eq; eauto.
intros (lh´ & HCopy´ & Hinj).
rewrite HCopy´. refine_split´; trivial.
eapply relate_impl_HP_update; eauto.
Qed.
Context {mt1: match_impl_HP}.
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. eapply match_impl_HP_update. assumption.
Qed.
Context {inv: PreservesInvariants (HD:= data) page_copy_back_spec}.
Context {inv0: PreservesInvariants (HD:= data0) page_copy_back_spec}.
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; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply page_copy_back_match; eauto.
Qed.
End PAGE_COPY_BACK_SIM.
End OBJ_SIM.