Library mcertikos.invariants.INVLemmaMemory
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import FlatMemory.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import CalTicketLock.
Require Import GlobalOracle.
Require Import GlobalOracleProp.
Require Import LogReplay.
Require Import RealParams.
Section ATABLE.
Lemma AT_kern_norm:
∀ a np,
AT_kern a np →
∀ n b,
ZMap.get n a = ATValid b ATNorm →
∀ b´,
AT_kern (ZMap.set n (ATValid b´ ATNorm) a) np.
Proof.
unfold AT_kern; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss.
exploit H; eauto.
subrewrite´. intros. congruence.
- rewrite ZMap.gso; auto.
Qed.
Lemma AT_kern_norm´:
∀ a np,
AT_kern a np →
∀ n b P1 P2,
(P1 ∧ (ZMap.get n a = ATValid b ATNorm) ∧ P2)->
∀ b´,
AT_kern (ZMap.set n (ATValid b´ ATNorm) a) np.
Proof.
intros. destruct H0 as (_ & Hr & _).
eapply AT_kern_norm; eauto.
Qed.
Lemma AT_usr_norm:
∀ a np,
AT_usr a np →
∀ n b,
AT_usr (ZMap.set n (ATValid b ATNorm) a) np.
Proof.
unfold AT_usr; intros.
destruct (zeq i n); subst.
- rewrite ZMap.gss. eauto.
- rewrite ZMap.gso; auto.
Qed.
End ATABLE.
Section DIRTY_PPAGE.
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.
red; intros; congruence.
Qed.
Lemma dirty_ppage_gso_undef:
∀ pp h,
dirty_ppage pp h →
∀ n,
dirty_ppage (ZMap.set n PGUndef pp) h.
Proof.
intros. apply dirty_ppage_gso; try assumption.
red; intros; congruence.
Qed.
End DIRTY_PPAGE.
Section PPAGE_INV.
Context `{real_params: RealParams}.
Lemma consistent_ppage_defined:
∀ a p n,
consistent_ppage a p n →
∀ i,
ZMap.get i p ≠ PGUndef →
∀ o,
o ≠ PGUndef →
consistent_ppage a (ZMap.set i o p) n.
Proof.
unfold consistent_ppage. intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss; split; intros; trivial.
exploit H; eauto.
+ intros [HG _]. eapply HG. assumption.
- rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_ppage_alloc_hide:
∀ a p n,
consistent_ppage a p n →
∀ i,
ZMap.get i p = PGAlloc →
∀ o,
consistent_ppage a (ZMap.set i (PGHide o) p) n.
Proof.
intros. apply consistent_ppage_defined; auto; congruence.
Qed.
Lemma consistent_ppage_hide_alloc:
∀ a p n,
consistent_ppage a p n →
∀ i o,
ZMap.get i p = PGHide o →
consistent_ppage a (ZMap.set i PGAlloc p) n.
Proof.
intros. apply consistent_ppage_defined; auto; congruence.
Qed.
Lemma consistent_ppage_norm_alloc:
∀ a p np,
consistent_ppage a p np →
∀ n,
consistent_ppage (ZMap.set n (ATValid true ATNorm) a)
(ZMap.set n PGAlloc p) np.
Proof.
unfold consistent_ppage; intros.
destruct (zeq i n); subst.
+ repeat rewrite ZMap.gss.
split; intros; eauto.
red; intros HM´; inv HM´.
+ repeat rewrite ZMap.gso; auto.
Qed.
Lemma consistent_ppage_norm_hide:
∀ a p np,
consistent_ppage a p np →
∀ n o,
consistent_ppage (ZMap.set n (ATValid true ATNorm) a)
(ZMap.set n (PGHide o) p) np.
Proof.
unfold consistent_ppage; intros.
destruct (zeq i n); subst.
+ repeat rewrite ZMap.gss.
split; intros; eauto.
red; intros HM´; inv HM´.
+ repeat rewrite ZMap.gso; auto.
Qed.
Lemma consistent_ppage_norm_undef:
∀ a p np,
consistent_ppage a p np →
∀ n,
consistent_ppage (ZMap.set n (ATValid false ATNorm) a)
(ZMap.set n PGUndef p) np.
Proof.
unfold consistent_ppage; intros.
destruct (zeq i n); subst.
+ repeat rewrite ZMap.gss.
split; intros HM.
elim HM. trivial. inv HM.
+ repeat rewrite ZMap.gso; auto.
Qed.
Lemma consistent_ppage_norm:
∀ a p np,
consistent_ppage a p np →
∀ n,
ZMap.get n a = ATValid true ATNorm →
consistent_ppage (ZMap.set n (ATValid true ATNorm) a) p np.
Proof.
unfold consistent_ppage; intros.
destruct (zeq i n); subst.
+ repeat rewrite ZMap.gss.
split; intros; eauto.
exploit H; eauto.
intros [_ HP]. eapply HP; eauto.
+ repeat rewrite ZMap.gso; auto.
Qed.
Definition weak_consistent_ppage (att: ATable) (ppt: PPermT) (nps: Z): Prop :=
∀ i,
0≤ i < nps →
(¬ (ZMap.get i ppt = PGUndef)
→
ZMap.get i att = ATValid true ATNorm).
Definition consistent_ppage_log l (p: PPermT) (nps: Z) :=
∀ q a
(Hdef: ZMap.get lock_AT_start l = MultiDef q)
(Hcal: CalAT_log_real q = Some a),
weak_consistent_ppage a p nps.
Lemma consistent_ppage_log_gso:
∀ l p nps e q
(Hv: consistent_ppage_log l p nps)
(Hneq: e ≠ lock_AT_start),
consistent_ppage_log (ZMap.set e q l) p nps.
Proof.
unfold consistent_ppage_log; intros.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma weak_consistent_ppage_set_true:
∀ a p nps b
(Hweak: weak_consistent_ppage a p nps),
weak_consistent_ppage (ZMap.set b (ATValid true ATNorm) a) p nps.
Proof.
unfold weak_consistent_ppage; intros.
destruct (zeq i b); subst.
- rewrite ZMap.gss; eauto.
- rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_ppage_log_gss:
∀ q q´ l p nps
(Hv: consistent_ppage_log l p nps)
(Hget: ZMap.get lock_AT_start l = MultiDef q´),
consistent_ppage_log (ZMap.set lock_AT_start (MultiDef (q ++q´)) l) p nps.
Proof.
induction q; simpl; unfold consistent_ppage_log in *; intros.
- rewrite ZMap.gss in Hdef. inv Hdef. eauto.
- rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
simpl in Hcal.
subdestruct; inv Hcal.
+ eapply IHq; eauto.
rewrite ZMap.gss; eauto.
+ eapply weak_consistent_ppage_set_true; eauto.
eapply IHq; eauto.
rewrite ZMap.gss; eauto.
Qed.
Lemma consistent_ppage_log_norm_alloc´´:
∀ p np q l n c
(Hcon: consistent_ppage_log l p np)
(Hget: ZMap.get lock_AT_start l = MultiDef q)
(Hpos: 0 ≠ n),
consistent_ppage_log
(ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: q)) l)
(ZMap.set n PGAlloc p) np.
Proof.
unfold consistent_ppage_log, weak_consistent_ppage; intros.
rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
simpl in Hcal.
subdestruct; inv Hcal.
- eapply Hcon; eauto.
- destruct (zeq i n); subst.
+ rewrite ZMap.gss; trivial.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma consistent_ppage_log_norm_alloc´:
∀ p np q q´ l n c
(Hcon: consistent_ppage_log l p np)
(Hget: ZMap.get lock_AT_start l = MultiDef q´)
(Hpos: 0 ≠ n),
consistent_ppage_log
(ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: q ++ q´))
(ZMap.set lock_AT_start (MultiDef (q ++ q´)) l))
(ZMap.set n PGAlloc p) np.
Proof.
intros. specialize (consistent_ppage_log_gss q _ _ _ _ Hcon Hget); eauto.
intros Hcon´.
eapply consistent_ppage_log_norm_alloc´´; eauto.
rewrite ZMap.gss. trivial.
Qed.
Lemma consistent_ppage_log_norm_alloc:
∀ p np q q´ l n c
(Hcon: consistent_ppage_log l p np)
(Hget: ZMap.get lock_AT_start l = MultiDef q´)
(Hpos: 0 ≠ n),
consistent_ppage_log
(ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: q ++ q´)) l)
(ZMap.set n PGAlloc p) np.
Proof.
intros.
specialize (consistent_ppage_log_norm_alloc´ p np q q´ l n c Hcon Hget Hpos); eauto.
rewrite ZMap.set2. trivial.
Qed.
Lemma real_pperm_log_valid:
∀ d,
consistent_ppage_log (real_multi_log d)
(ZMap.init PGUndef) real_nps.
Proof.
unfold consistent_ppage_log, CalAT_log_real, weak_consistent_ppage; intros.
rewrite ZMap.gi in H0. congruence.
Qed.
Lemma consistent_ppage_log_defined:
∀ a p n,
consistent_ppage_log a p n →
∀ i,
ZMap.get i p ≠ PGUndef →
∀ o,
o ≠ PGUndef →
consistent_ppage_log a (ZMap.set i o p) n.
Proof.
unfold consistent_ppage_log, weak_consistent_ppage. intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in *; eauto.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma consistent_ppage_log_hide_alloc:
∀ a p n,
consistent_ppage_log a p n →
∀ i o,
ZMap.get i p = PGHide o →
consistent_ppage_log a (ZMap.set i PGAlloc p) n.
Proof.
intros.
apply consistent_ppage_log_defined; auto; congruence.
Qed.
Lemma consistent_ppage_log_alloc_hide:
∀ a p n,
consistent_ppage_log a p n →
∀ i,
ZMap.get i p = PGAlloc →
∀ o,
consistent_ppage_log a (ZMap.set i (PGHide o) p) n.
Proof.
intros. apply consistent_ppage_log_defined; auto; congruence.
Qed.
Lemma consistent_ppage_log_init:
∀ p nps,
consistent_ppage_log (ZMap.init MultiUndef) p nps.
Proof.
unfold consistent_ppage_log; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
End PPAGE_INV.
Section LATABLE.
Lemma LAT_kern_consistent_pmap:
∀ a np,
AT_kern a np →
∀ ptp p la,
consistent_pmap ptp p a la np →
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ n x,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid n x →
∀ b,
AT_kern (ZMap.set n (ATValid b ATNorm) a) np.
Proof.
intros. exploit H0; eauto.
intros (_ & _ & He & _).
eapply AT_kern_norm; eauto.
Qed.
Context `{real_params: RealParams}.
Definition LATCTable_log l lat :=
∀ q a
(Hdef: ZMap.get lock_AT_start l = MultiDef q)
(Hcal: CalAT_log_real q = Some a),
LATCTable_nil lat a.
Lemma LATCTable_log_init:
∀ a,
LATCTable_log (ZMap.init MultiUndef) a.
Proof.
unfold LATCTable_log; intros.
rewrite ZMap.gi in Hdef.
inv Hdef.
Qed.
Lemma LATCTable_log_gso:
∀ l lat e q
(Hv: LATCTable_log l lat)
(Hneq: e ≠ lock_AT_start),
LATCTable_log (ZMap.set e q l) lat.
Proof.
unfold LATCTable_log; intros.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma LATCTable_nil_set_true:
∀ a la b
(Hweak: LATCTable_nil la a),
LATCTable_nil la (ZMap.set b (ATValid true ATNorm) a).
Proof.
unfold LATCTable_nil; intros.
destruct (zeq i b); subst.
- rewrite ZMap.gss in H; eauto. inv H.
- rewrite ZMap.gso in H; eauto.
Qed.
Lemma LATCTable_log_gss:
∀ q q´ l lat
(Hv: LATCTable_log l lat)
(Hget: ZMap.get lock_AT_start l = MultiDef q´),
LATCTable_log (ZMap.set lock_AT_start (MultiDef (q ++q´)) l) lat.
Proof.
induction q; simpl; unfold LATCTable_log in *; intros.
- rewrite ZMap.gss in Hdef. inv Hdef. eauto.
- rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
simpl in Hcal.
subdestruct; inv Hcal.
+ eapply IHq; eauto.
rewrite ZMap.gss; eauto.
+ eapply LATCTable_nil_set_true; eauto.
eapply IHq; eauto.
rewrite ZMap.gss; eauto.
Qed.
Lemma LATCTable_log_alloc:
∀ lat n c q q´ l
(Hcon: LATCTable_log l lat)
(Hget: ZMap.get lock_AT_start l = MultiDef q´),
LATCTable_log
(ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: q ++ q´)) l) lat.
Proof.
intros.
eapply (LATCTable_log_gss q) in Hcon; eauto.
unfold LATCTable_log in ×.
intros. rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
simpl in Hcal.
subdestruct; inv Hcal.
+ eapply Hcon; eauto.
rewrite ZMap.gss; eauto.
+ eapply LATCTable_nil_set_true; eauto.
eapply Hcon; eauto.
rewrite ZMap.gss; eauto.
Qed.
Lemma LATCTable_log_alloc´:
∀ lat q q´ l n c
(Hcon: LATCTable_log l lat)
(Hget: ZMap.get lock_AT_start l = MultiDef q´),
LATCTable_log
(ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: q ++ q´)) l)
(ZMap.set n (LATCValid nil) lat).
Proof.
intros.
eapply (LATCTable_log_alloc lat n c q) in Hcon; eauto.
unfold LATCTable_log in ×.
intros. eapply LATCTable_nil_gss_nil; eauto.
Qed.
Lemma real_multi_log_pb_get:
∀ n d q,
n ≠ O →
ZMap.get lock_AT_start (real_multi_log_pb n d) = MultiDef q →
q = nil.
Proof.
induction n; simpl; intros; try omega.
destruct (zeq lock_AT_start (Z.of_nat n)); subst.
- rewrite e in H0. rewrite ZMap.gss in H0. inv H0; trivial.
- rewrite ZMap.gso in H0; eauto. eapply IHn; eauto.
red; intros. elim n0. subst. trivial.
Qed.
Lemma Calculate_AT_LAT_nil:
∀ n i nps mm size a l
(HAT: ZMap.get i (Calculate_AT n nps mm size
(ZMap.init ATUndef)) = ATValid false ATNorm)
(HLAT: ZMap.get i (Calculate_LAT n nps a) = LATCValid l),
l = nil.
Proof.
induction n; simpl; intros.
- destruct (zeq i 0); subst.
+ rewrite ZMap.gss in ×. inv HAT.
+ rewrite ZMap.gso in HAT; auto.
rewrite ZMap.gi in HAT. inv HAT.
- destruct (zeq i (Z.pos (Pos.of_succ_nat n))); subst.
+ rewrite ZMap.gss in ×. inv HLAT. trivial.
+ rewrite ZMap.gso in HLAT; auto.
subdestruct.
× rewrite ZMap.gso in HAT; eauto.
× rewrite ZMap.gso in HAT; eauto.
× rewrite ZMap.gso in HAT; eauto.
× rewrite ZMap.gso in HAT; eauto.
Qed.
Lemma LATCTable_log_real:
∀ d a
,
LATCTable_log (real_multi_log d)
(real_LAT a).
Proof.
unfold LATCTable_log, real_multi_log, real_LAT. intros.
exploit real_multi_log_pb_get; try eapply Hdef.
{
unfold lock_range, ID_AT_range, ID_TCB_range, ID_SC_range.
simpl. xomega.
}
intros; subst. inv Hcal.
unfold LATCTable_nil. intros.
eapply Calculate_AT_LAT_nil; eauto.
Qed.
Lemma LATCTable_log_nil_gso:
∀ l lat e q a
(Hv: LATCTable_log l lat)
(Hget: ZMap.get e lat = LATCValid q)
(Hneq: q ≠ nil),
LATCTable_log l (ZMap.set e a lat).
Proof.
unfold LATCTable_log; intros.
unfold LATCTable_nil in ×. intros.
destruct (zeq i e); subst.
- rewrite ZMap.gss in H0. subst.
exploit Hv; eauto. congruence.
- rewrite ZMap.gso in H0; eauto.
Qed.
Lemma LATCTable_log_not_nil_gso_true:
∀ l lat e q p n
(Hv: LATCTable_log l lat)
(Hcon: consistent_ppage_log l p n)
(Hget: ZMap.get e p = PGAlloc)
(Hrange: 0 ≤ e < n),
LATCTable_log l (ZMap.set e (LATCValid q) lat).
Proof.
unfold LATCTable_log; intros.
unfold LATCTable_nil in ×. intros.
unfold consistent_ppage_log in ×.
specialize (Hcon _ _ Hdef Hcal).
destruct (zeq i e); subst.
- rewrite ZMap.gss in H0. inv H0.
unfold weak_consistent_ppage in Hcon.
specialize (Hcon _ Hrange).
rewrite Hcon in H. congruence.
rewrite Hget. congruence.
- rewrite ZMap.gso in H0; eauto.
Qed.
End LATABLE.
Section PMAP_INV.
Lemma consistent_pmap_gso_at:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
(ZMap.get i a ≠ ATValid true ATNorm
∨ ZMap.get i la ≠ LATCValid nil) →
∀ pp aa laa,
consistent_pmap ptp (ZMap.set i pp p) (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
unfold consistent_pmap; intros.
destruct (zeq pi i); subst.
- exploit H; eauto.
intros (_ & _ & HP1 & HP2).
destruct H0; congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_gso_at_false:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i an,
ZMap.get i a = ATValid false an →
∀ pp aa laa,
consistent_pmap ptp (ZMap.set i pp p) (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
intros. eapply consistent_pmap_gso_at; eauto.
left.
congruence.
Qed.
Lemma consistent_pmap_gso_pperm:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
(∀ o, ZMap.get i p ≠ PGHide o) →
∀ pp aa laa,
consistent_pmap ptp (ZMap.set i pp p) (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
unfold consistent_pmap; intros.
destruct (zeq pi i); subst.
- exploit H; eauto.
intros (_ & HP & _).
congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_gso_pperm_alloc:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
ZMap.get i p = PGAlloc →
∀ pp aa laa,
consistent_pmap ptp (ZMap.set i pp p) (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
intros. eapply consistent_pmap_gso_pperm; eauto.
congruence.
Qed.
Lemma consistent_pmap_gso_pperm´:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
(∀ o, ZMap.get i p ≠ PGHide o) →
∀ aa laa,
consistent_pmap ptp p (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
unfold consistent_pmap; intros.
destruct (zeq pi i); subst.
- exploit H; eauto.
intros (_ & HP & _).
congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_gso_pperm_alloc´:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
ZMap.get i p = PGAlloc →
∀ aa laa,
consistent_pmap ptp p (ZMap.set i aa a) (ZMap.set i laa la) n.
Proof.
intros. eapply consistent_pmap_gso_pperm´; eauto.
congruence.
Qed.
Lemma consistent_pmap_ptp_same:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i pdi pi pdt,
ZMap.get pdi (ZMap.get i ptp) = PDEValid pi pdt →
∀ pdt´,
consistent_pmap (ZMap.set i (ZMap.set pdi (PDEValid pi pdt´) (ZMap.get i ptp)) ptp)
p a la n.
Proof.
unfold consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H3.
exploit H; eauto.
+ rewrite ZMap.gso in *; eauto.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma consistent_pmap_at_same:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
consistent_pmap_domain ptp p la n →
∀ i,
0≤ i < num_proc →
∀ vadr,
0≤ vadr < adr_max →
∀ pi pdt,
ZMap.get (PDX vadr) (ZMap.get i ptp) = PDEValid pi pdt →
∀ z x,
ZMap.get (PTX vadr) pdt = PTEValid z x →
∀ aa laa,
consistent_pmap ptp p (ZMap.set z aa a) (ZMap.set z laa la) n.
Proof.
unfold consistent_pmap, consistent_pmap_domain. intros.
exploit (H0 _ H1 vadr); try eassumption.
intros (_ & Hp & _).
destruct (zeq pi0 z); subst.
- exploit H; eauto. rewrite Hp.
intros (_ & HF & _). inv HF.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_at_ptp_same:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
consistent_pmap_domain ptp p la n →
∀ i,
0≤ i < num_proc →
∀ vadr,
0≤ vadr < adr_max →
∀ pi pdt,
ZMap.get (PDX vadr) (ZMap.get i ptp) = PDEValid pi pdt →
∀ z x,
ZMap.get (PTX vadr) pdt = PTEValid z x →
∀ pdt´ aa laa,
consistent_pmap (ZMap.set i (ZMap.set (PDX vadr) (PDEValid pi pdt´) (ZMap.get i ptp)) ptp)
p (ZMap.set z aa a) (ZMap.set z laa la) n.
Proof.
intros. eapply consistent_pmap_ptp_same; eauto.
eapply consistent_pmap_at_same; eauto.
Qed.
Lemma consistent_pmap_ptp_gss:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i pdi v pte,
0 < v < n →
ZMap.get v a = ATValid false ATNorm →
ZMap.get v la = LATCValid nil →
consistent_pmap (ZMap.set i (ZMap.set pdi (PDEValid v pte) (ZMap.get i ptp)) ptp)
(ZMap.set v (PGHide (PGPMap i pdi)) p)
(ZMap.set v (ATValid true ATNorm) a)
(ZMap.set v (LATCValid nil) la) n.
Proof.
unfold consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H5.
repeat rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & _ & He1 & He2). congruence.
× repeat rewrite ZMap.gso; eauto.
- rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & _ & He1 & He2). congruence.
× repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_ptp_gss0:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i pdi v pte,
0 < v < n →
ZMap.get v a = ATValid true ATNorm →
ZMap.get v la = LATCValid nil →
ZMap.get v p = PGAlloc →
consistent_pmap (ZMap.set i (ZMap.set pdi (PDEValid v pte) (ZMap.get i ptp)) ptp)
(ZMap.set v (PGHide (PGPMap i pdi)) p) a la n.
Proof.
unfold consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H6.
repeat rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso in H6; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & He & _). congruence.
× repeat rewrite ZMap.gso; eauto.
- rewrite ZMap.gso in H6; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & He & _). congruence.
× repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_ptp_gss´:
∀ ptp p a la n,
consistent_pmap ptp p a la n →
∀ i,
0 ≤ i < num_proc →
∀ vadr,
0 ≤ vadr < adr_max →
∀ v x,
ZMap.get (PDX vadr) (ZMap.get i ptp) = PDEValid v x →
consistent_pmap (ZMap.set i (ZMap.set (PDX vadr) PDEUnPresent (ZMap.get i ptp)) ptp)
(ZMap.set v PGUndef p)
(ZMap.set v (ATValid false ATNorm) a)
(ZMap.set v (LATCValid nil) la) n.
Proof.
unfold consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq (PDX vadr) (PDX j)).
+ rewrite e in ×. rewrite ZMap.gss in ×. congruence.
+ rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto. intros (_ & He & _). clear H4.
exploit H; eauto. intros (_ & He´ & _). congruence.
× repeat rewrite ZMap.gso; eauto.
- rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto. intros (_ & He & _). clear H3 H4.
exploit H; eauto. intros (_ & He´ & _). congruence.
× repeat rewrite ZMap.gso; eauto.
Qed.
Definition weak_consistent_pmap (ptp: PMapPool) (ppt: PPermT)
(lat: LATCTable) (nps: Z): Prop :=
∀ i,
0 ≤ i < num_proc →
∀ j,
0≤ j < adr_max →
∀ pte pi,
ZMap.get (PDX j) (ZMap.get i ptp) = PDEValid pi pte →
0 < pi < nps
∧ ZMap.get pi ppt = PGHide (PGPMap i (PDX j))
∧ ZMap.get pi lat = LATCValid nil.
Lemma weak_consistent_pmap_init:
∀ pg la nps,
weak_consistent_pmap (ZMap.init (ZMap.init PDEUndef)) pg la nps.
Proof.
unfold weak_consistent_pmap.
intros. repeat rewrite ZMap.gi in H1. inv H1.
Qed.
Lemma weak_consistent_pmap_gso_pperm:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
∀ i,
(∀ o, ZMap.get i p ≠ PGHide o) →
∀ pp laa,
weak_consistent_pmap ptp (ZMap.set i pp p) (ZMap.set i laa la) n.
Proof.
unfold weak_consistent_pmap; intros.
destruct (zeq pi i); subst.
- exploit H; eauto.
intros (_ & HP & _).
congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Context `{real_params: RealParams}.
Lemma weak_consistent_pmap_gso_at_palloc:
∀ j ptp p la n AT q q´ l
(Hweak: weak_consistent_pmap ptp p la n)
(Hcal: CalAT_log_real (q´ ++ q) = Some AT)
(Hcon: consistent_ppage_log l p n)
(Hrange: 0 < j < n)
(Hfalse: ZMap.get j AT = ATValid false ATNorm)
(Hdef: ZMap.get lock_AT_start l = MultiDef q),
∀ pp laa,
weak_consistent_pmap ptp (ZMap.set j pp p) (ZMap.set j laa la) n.
Proof.
intros.
assert (Hcon´: consistent_ppage_log
(ZMap.set lock_AT_start (MultiDef (q´ ++ q)) l) p n).
{
eapply consistent_ppage_log_gss; eauto.
}
eapply weak_consistent_pmap_gso_pperm; eauto.
red; intros. exploit Hcon´; eauto.
- rewrite ZMap.gss; eauto.
- instantiate (1:= j). omega.
- congruence.
- congruence.
Qed.
Require Import CalRealPT.
Require Import CalRealPTPool.
Require Import XOmega.
Lemma real_pt_weak_consistent_pmap:
∀ ptp p la n,
weak_consistent_pmap (real_pt ptp) p la n.
Proof.
intros.
unfold weak_consistent_pmap.
intros.
destruct (Z.eq_dec i 0).
{
rewrite e in ×.
destruct (zle_lt (kern_low/one_k) (PDX j) (kern_high/one_k)).
rewrite real_pt_0_PDEID in H1.
discriminate H1.
assumption.
assert (tmp : ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEUnPresent ∨
ZMap.get (PDX j) (ZMap.get 0 (real_ptp ptp)) = PDEID).
apply real_ptp_usr.
unfold PDX in ×.
xomega.
xomega.
rewrite real_pt_0_local in H1.
destruct tmp; rewrite H2 in H1; discriminate H1.
unfold PDX in ×.
destruct o.
left.
xomega.
right.
assumption.
}
{
assert (ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEUnPresent ∨
ZMap.get (PDX j) (ZMap.get i (real_pt ptp)) = PDEID).
rewrite real_pt_nonkern_local.
apply real_ptp_usr.
unfold PDX.
xomega.
assumption.
assumption.
destruct H2; rewrite H2 in H1; discriminate H1.
}
Qed.
Lemma weak_consistent_pmap_ptp_same:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
∀ i pdi pi pdt,
ZMap.get pdi (ZMap.get i ptp) = PDEValid pi pdt →
∀ pdt´,
weak_consistent_pmap (ZMap.set i (ZMap.set pdi (PDEValid pi pdt´) (ZMap.get i ptp)) ptp)
p la n.
Proof.
unfold weak_consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H3.
exploit H; eauto.
+ rewrite ZMap.gso in *; eauto.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma weak_consistent_pmap_at_same:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
consistent_pmap_domain ptp p la n →
∀ i,
0≤ i < num_proc →
∀ vadr,
0≤ vadr < adr_max →
∀ pi pdt,
ZMap.get (PDX vadr) (ZMap.get i ptp) = PDEValid pi pdt →
∀ z x,
ZMap.get (PTX vadr) pdt = PTEValid z x →
∀ laa,
weak_consistent_pmap ptp p (ZMap.set z laa la) n.
Proof.
unfold weak_consistent_pmap, consistent_pmap_domain. intros.
exploit (H0 _ H1 vadr); try eassumption.
intros (_ & Hp & _).
destruct (zeq pi0 z); subst.
- exploit H; eauto. rewrite Hp.
intros (_ & HF & _). inv HF.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma weak_consistent_pmap_at_ptp_same:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
consistent_pmap_domain ptp p la n →
∀ i,
0≤ i < num_proc →
∀ vadr,
0≤ vadr < adr_max →
∀ pi pdt,
ZMap.get (PDX vadr) (ZMap.get i ptp) = PDEValid pi pdt →
∀ z x,
ZMap.get (PTX vadr) pdt = PTEValid z x →
∀ pdt´ laa,
weak_consistent_pmap (ZMap.set i (ZMap.set (PDX vadr) (PDEValid pi pdt´) (ZMap.get i ptp)) ptp)
p (ZMap.set z laa la) n.
Proof.
intros. eapply weak_consistent_pmap_ptp_same; eauto.
eapply weak_consistent_pmap_at_same; eauto.
Qed.
Lemma weak_consistent_pmap_gso_pperm´:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
∀ i,
(∀ o, ZMap.get i p ≠ PGHide o) →
∀ laa,
weak_consistent_pmap ptp p (ZMap.set i laa la) n.
Proof.
unfold weak_consistent_pmap; intros.
destruct (zeq pi i); subst.
- exploit H; eauto.
intros (_ & HP & _).
congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma weak_consistent_pmap_gso_pperm_alloc´:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
∀ i,
ZMap.get i p = PGAlloc →
∀ laa,
weak_consistent_pmap ptp p (ZMap.set i laa la) n.
Proof.
intros. eapply weak_consistent_pmap_gso_pperm´; eauto.
congruence.
Qed.
Lemma weak_consistent_pmap_ptp_gss0:
∀ ptp p la n,
weak_consistent_pmap ptp p la n →
∀ i pdi v pte,
0 < v < n →
ZMap.get v la = LATCValid nil →
ZMap.get v p = PGAlloc →
weak_consistent_pmap (ZMap.set i (ZMap.set pdi (PDEValid v pte) (ZMap.get i ptp)) ptp)
(ZMap.set v (PGHide (PGPMap i pdi)) p) la n.
Proof.
unfold weak_consistent_pmap. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H5.
repeat rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & He & _). congruence.
× repeat rewrite ZMap.gso; eauto.
- rewrite ZMap.gso in H5; eauto.
destruct (zeq pi v); subst.
× exploit H; eauto.
intros (_ & He & _). congruence.
× repeat rewrite ZMap.gso; eauto.
Qed.
End PMAP_INV.
Section PMAP_DOMAIN_INV.
Lemma consistent_pmap_domain_gso_at:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i,
(∀ c,
c ≠ nil →
ZMap.get i a ≠ LATCValid c) →
∀ pp aa,
consistent_pmap_domain ptp (ZMap.set i pp p) (ZMap.set i aa a) n.
Proof.
unfold consistent_pmap_domain; intros.
destruct (zeq v i); subst.
- exploit H; eauto.
intros (_ & _ & n0 & HP & Hgt).
assert (Hgt´: n0 ≠ nil).
{
red; intros; subst. inv Hgt.
}
specialize (H0 _ Hgt´).
congruence.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_domain_gso_at_false:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i,
ZMap.get i a = LATCValid nil →
∀ pp aa,
consistent_pmap_domain ptp (ZMap.set i pp p) (ZMap.set i aa a) n.
Proof.
intros. eapply consistent_pmap_domain_gso_at; eauto.
congruence.
Qed.
Lemma consistent_pmap_domain_gso_at_0:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i,
ZMap.get i a = LATCValid nil →
∀ pp aa,
consistent_pmap_domain ptp (ZMap.set i pp p) (ZMap.set i aa a) n.
Proof.
intros. eapply consistent_pmap_domain_gso_at; eauto.
subrewrite´. red; intros. congruence.
Qed.
Lemma consistent_pmap_domain_gso_at_00:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i,
ZMap.get i a = LATCValid nil →
∀ pp,
consistent_pmap_domain ptp (ZMap.set i pp p) a n.
Proof.
unfold consistent_pmap_domain; intros.
destruct (zeq v i); subst.
- exploit H; eauto.
intros (_ & _ & n0 & HP & Hgt).
rewrite H0 in HP. inv HP.
inv Hgt.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_pmap_domain_ptp_unp:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i pdi pte v,
(∀ j,
0 ≤ j < one_k →
ZMap.get j pte = PTEUnPresent) →
consistent_pmap_domain (ZMap.set i (ZMap.set pdi (PDEValid v pte) (ZMap.get i ptp)) ptp) p a n.
Proof.
unfold consistent_pmap_domain. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H3.
rewrite H0 in H4. congruence.
apply Z_mod_lt. omega.
+ rewrite ZMap.gso in H3; eauto.
- rewrite ZMap.gso in H3; eauto.
Qed.
Lemma consistent_pmap_domain_ptp_pde_unp:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i pdi,
consistent_pmap_domain (ZMap.set i (ZMap.set pdi PDEUnPresent (ZMap.get i ptp)) ptp) p a n.
Proof.
unfold consistent_pmap_domain. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. congruence.
+ rewrite ZMap.gso in H2; eauto.
- rewrite ZMap.gso in H2; eauto.
Qed.
Lemma Lremove_count_outside:
∀ l x y, y ≠ x → count_occ LATOwner_dec (Lremove x l) y = count_occ LATOwner_dec l y.
Proof.
induction l; intros.
- trivial.
- simpl.
destruct (LATOwner_dec x a).
+ destruct (LATOwner_dec a y).
× congruence.
× eauto.
+ destruct (LATOwner_dec a y); subst.
× rewrite count_occ_cons_eq; trivial.
rewrite IHl; trivial.
× rewrite count_occ_cons_neq; auto.
Qed.
Lemma consistent_pmap_domain_remove:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ i pdi pi pdt,
ZMap.get pdi (ZMap.get i ptp) = PDEValid pi pdt →
∀ pti z x,
ZMap.get pti pdt = PTEValid z x →
∀ l,
ZMap.get z a = LATCValid l →
consistent_pmap_domain (ZMap.set i (ZMap.set pdi (PDEValid pi (ZMap.set pti PTEUnPresent pdt))
(ZMap.get i ptp)) ptp) p
(ZMap.set z (LATCValid (Lremove (LATO i pdi pti) l)) a) n.
Proof.
unfold consistent_pmap_domain. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H5.
destruct (zeq pti (PTX j)); subst.
× rewrite ZMap.gss in ×. congruence.
× rewrite ZMap.gso in H6; auto.
exploit H; eauto.
intros (Hr & He & Hex).
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
split; auto.
refine_split´; trivial.
rewrite Lremove_count_outside; eauto.
congruence.
}
{
rewrite ZMap.gso; eauto.
}
+ rewrite ZMap.gso in H5; eauto.
exploit H; eauto.
intros (Hr & He & Hex).
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
split; auto.
refine_split´; trivial.
rewrite Lremove_count_outside; eauto.
congruence.
}
{
rewrite ZMap.gso; eauto.
}
- rewrite ZMap.gso in H5; eauto.
exploit H; eauto.
intros (Hr & He & Hex).
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
split; auto.
refine_split´; trivial.
rewrite Lremove_count_outside; eauto.
congruence.
}
{
rewrite ZMap.gso; eauto.
}
Qed.
Lemma consistent_pmap_domain_append:
∀ ptp p a n,
consistent_pmap_domain ptp p a n →
∀ HConsist: (consistent_lat_domain ptp a n),
∀ i pdi pi pdt,
ZMap.get pdi (ZMap.get i ptp) = PDEValid pi pdt →
∀ pti z l,
0 < z < n →
ZMap.get z a = LATCValid l →
ZMap.get z p = PGAlloc →
∀ x,
∀ Hnot: (¬ (∃ v0 p0, ZMap.get pti pdt = PTEValid v0 p0)),
consistent_pmap_domain (ZMap.set i (ZMap.set pdi (PDEValid pi (ZMap.set pti (PTEValid z x) pdt))
(ZMap.get i ptp)) ptp) p
(ZMap.set z (LATCValid ((LATO i pdi pti) :: l)) a) n.
Proof.
unfold consistent_pmap_domain. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in ×.
destruct (zeq pdi (PDX j)); subst.
+ rewrite ZMap.gss in ×. inv H6.
destruct (zeq pti (PTX j)); subst.
× rewrite ZMap.gss in ×. inv H7.
rewrite ZMap.gss. split; trivial.
refine_split´; trivial.
simpl.
destruct (LATOwner_dec (LATO i0 (PDX j) (PTX j)) (LATO i0 (PDX j) (PTX j))); try congruence.
assert (HnotInQ: ¬ In (LATO i0 (PDX j) (PTX j)) l).
{
red; intros.
exploit HConsist; eauto. intros.
elim Hnot. destruct H7 as (_ & pi & pte & HR1 & p1 & HR2).
rewrite H0 in HR1. inv HR1.
rewrite HR2. eauto.
}
assert (Heq: count_occ LATOwner_dec l (LATO i0 (PDX j) (PTX j)) = O).
{
destruct (count_occ LATOwner_dec l (LATO i0 (PDX j) (PTX j))) eqn: Heq; trivial.
elim HnotInQ.
apply <- (count_occ_In LATOwner_dec). rewrite Heq. omega.
}
rewrite Heq. trivial.
× rewrite ZMap.gso in H7; auto.
exploit H; eauto.
intros (Hr & He & Hex).
split; trivial. split; trivial.
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
refine_split´; trivial.
simpl.
destruct (LATOwner_dec (LATO i0 (PDX j) pti) (LATO i0 (PDX j) (PTX j))); try congruence.
}
{
rewrite ZMap.gso; eauto.
}
+ rewrite ZMap.gso in H6; eauto.
exploit H; eauto.
intros (Hr & He & Hex).
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
split; auto.
refine_split´; trivial.
simpl.
destruct (LATOwner_dec (LATO i0 pdi pti) (LATO i0 (PDX j) (PTX j))); try congruence.
}
{
rewrite ZMap.gso; eauto.
}
- rewrite ZMap.gso in H6; eauto.
exploit H; eauto.
intros (Hr & He & Hex).
destruct (zeq v z); subst.
{
rewrite ZMap.gss.
destruct Hex as (l´ & He´ & Hin).
rewrite H2 in He´. inv He´.
split; auto.
refine_split´; trivial.
simpl.
destruct (LATOwner_dec (LATO i pdi pti) (LATO i0 (PDX j) (PTX j))); try congruence.
}
{
rewrite ZMap.gso; eauto.
}
Qed.
End PMAP_DOMAIN_INV.
Section LAT_DOMAIN_INV.
Lemma consistent_lat_domain_gss_nil:
∀ p a n,
consistent_lat_domain p a n →
∀ i,
consistent_lat_domain p (ZMap.set i (LATCValid nil) a) n.
Proof.
unfold consistent_lat_domain; intros.
destruct (zeq v i); subst.
- rewrite ZMap.gss in H1. inv H1. inv H2.
- rewrite ZMap.gso in H1; eauto.
Qed.
Lemma consistent_lat_domain_gss_remove:
∀ a z l p n ppt,
ZMap.get z a = LATCValid l →
consistent_lat_domain p a n →
consistent_pmap_domain p ppt a n →
∀ i j pi pdt p´,
0 ≤ i < num_proc →
0 ≤ j < 4294967296 →
ZMap.get (PDX j) (ZMap.get i p) = PDEValid pi pdt →
ZMap.get (PTX j) pdt = PTEValid z p´ →
consistent_lat_domain
(ZMap.set i (ZMap.set (PDX j) (PDEValid pi (ZMap.set (PTX j) PTEUnPresent pdt))
(ZMap.get i p)) p)
(ZMap.set z (LATCValid (Lremove (LATO i (PDX j) (PTX j)) l)) a) n.
Proof.
unfold consistent_lat_domain; intros.
destruct (zeq v z); subst.
- rewrite ZMap.gss in ×. inv H7.
destruct (zeq n0 i); subst.
+ rewrite ZMap.gss.
destruct (zeq pdi (PDX j)); subst.
× rewrite ZMap.gss.
destruct (zeq pti (PTX j)); subst.
{
contradict H8.
eapply remove_In; eauto.
}
{
assert (In (LATO i (PDX j) pti) l).
{
eapply Lremove_incl in H8. trivial.
}
exploit H0; eauto.
rewrite H4. intros (Hrange & pi0 & pte & HR1 & p0 & HR2).
inv HR1.
refine_split´; trivial.
rewrite ZMap.gso; eauto.
}
× rewrite ZMap.gso; eauto.
eapply H0; eauto.
eapply Lremove_incl; eauto.
+ rewrite ZMap.gso; eauto.
eapply H0; eauto.
eapply Lremove_incl; eauto.
- rewrite ZMap.gso in H7; eauto.
exploit H1; eauto.
rewrite H. intros (_ & _ & HP).
destruct HP as (l1 & He & Hc). inv He.
assert (HIn: In (LATO i (PDX j) (PTX j)) l1).
{
eapply (count_occ_In LATOwner_dec). omega.
}
destruct (zeq i n0); subst.
exploit H0; eauto.
+ rewrite ZMap.gss.
destruct (zeq pdi (PDX j)); subst.
× rewrite ZMap.gss.
destruct (zeq pti (PTX j)); subst.
{
rewrite H4. intros (Hrange & pi0 & pte & HR1 & HR2).
inv HR1. rewrite H5 in HR2.
destruct HR2 as (p0 & He). inv He.
congruence.
}
{
rewrite H4. intros (Hrange & pi0 & pte & HR1 & HR2).
inv HR1. destruct HR2 as(p0 & He).
refine_split´; trivial.
rewrite ZMap.gso; eauto.
}
× rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma Lremove_outside:
∀ (l: list LATOwner) x y, y ≠ x → In y l → In y (Lremove x l).
Proof.
induction l; intros.
- inv H0.
- simpl. destruct (LATOwner_dec x a); subst.
+ inv H0. congruence. auto.
+ inv H0. left; trivial.
right; auto.
Qed.
Require Import Integers.
Lemma PTX_range:
∀ i,
0 ≤ PTX i ≤ PTX Int.max_unsigned.
Proof.
rewrite_omega.
unfold PTX.
intros.
exploit (Z_mod_lt (i / 4096) 1024);
intros; omega.
Qed.
Lemma consistent_lat_domain_gss_append:
∀ a p n,
consistent_lat_domain p a n →
∀ i pdi j pi pdt z pp l,
ZMap.get pdi (ZMap.get i p) = PDEValid pi pdt →
ZMap.get z a = LATCValid l →
¬ (∃ v´ p´, ZMap.get (PTX j) pdt = PTEValid v´ p´) →
consistent_lat_domain
(ZMap.set i (ZMap.set pdi (PDEValid pi (ZMap.set (PTX j) (PTEValid z pp) pdt))
(ZMap.get i p)) p)
(ZMap.set z (LATCValid ((LATO i pdi (PTX j)) :: l)) a) n.
Proof.
unfold consistent_lat_domain; intros.
destruct (zeq v z); subst.
- rewrite ZMap.gss in ×. inv H4.
destruct (zeq n0 i); subst.
+ rewrite ZMap.gss.
destruct (zeq pdi pdi0); subst.
× rewrite ZMap.gss.
destruct (zeq pti (PTX j)); subst.
{
refine_split´; trivial.
eapply PTX_range.
rewrite ZMap.gss; trivial.
}
{
inv H5; try congruence.
exploit H; eauto.
rewrite H0.
intros (Hrange & pi0 & pte & HR1 & p0 & HR2).
inv HR1.
refine_split´; trivial.
rewrite ZMap.gso; eauto.
}
× rewrite ZMap.gso; eauto.
eapply H; eauto.
inv H5; try congruence.
+ rewrite ZMap.gso; eauto.
eapply H; eauto.
inv H5; try congruence.
- rewrite ZMap.gso in H4; eauto.
destruct (zeq i n0); subst.
+ rewrite ZMap.gss.
destruct (zeq pdi pdi0); subst.
× rewrite ZMap.gss.
exploit H; eauto.
rewrite H0.
intros (Hrange & pi0 & pte & HR1 & HR2).
inv HR1.
destruct (zeq pti (PTX j)); subst.
{
elim H2; eauto.
}
{
destruct HR2 as (p0 & HR2).
refine_split´; trivial.
rewrite ZMap.gso; eauto.
}
× rewrite ZMap.gso; eauto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_lat_domain_gso_p:
∀ p a np pdi,
consistent_lat_domain p a np →
∀ pd n,
ZMap.get pdi (ZMap.get n p) = PDEUnPresent →
consistent_lat_domain
(ZMap.set n (ZMap.set pdi pd (ZMap.get n p)) p) a np.
Proof.
unfold consistent_lat_domain; intros.
destruct (zeq n0 n); subst.
- rewrite ZMap.gss.
destruct (zeq pdi pdi0); subst.
+ rewrite ZMap.gss.
exploit H; eauto.
rewrite H0.
intros (Hrange & pi0 & pte & HR1 & _).
inv HR1.
+ rewrite ZMap.gso; eauto.
- rewrite ZMap.gso; eauto.
Qed.
Lemma consistent_lat_domain_gso_free:
∀ p a np pdi,
consistent_lat_domain p a np →
∀ pd n pte pi,
ZMap.get pdi (ZMap.get n p) = PDEValid pi pte →
(∀ i, 0 ≤ i ≤ PTX Int.max_unsigned
→ ZMap.get i pte = PTEUnPresent) →
consistent_lat_domain
(ZMap.set n (ZMap.set pdi pd (ZMap.get n p)) p) a np.
Proof.
unfold consistent_lat_domain; intros.
destruct (zeq n0 n); subst.
- rewrite ZMap.gss.
destruct (zeq pdi pdi0); subst.
+ rewrite ZMap.gss.
exploit H; eauto.
rewrite H0.
intros (Hrange & pi0 & pte´ & HR1 & HE2).
inv HR1.
specialize(H1 _ Hrange).
rewrite H1 in HE2.
destruct HE2 as (? & He). inv He.
+ rewrite ZMap.gso; eauto.
- rewrite ZMap.gso; eauto.
Qed.
End LAT_DOMAIN_INV.
Section PMAP_VALID_KERN_INV.
Lemma PMap_valid_gso:
∀ ptp i,
PMap_valid (ZMap.get i ptp) →
∀ i´ pdi pi pdt,
ZMap.get pdi (ZMap.get i´ ptp) = PDEValid pi pdt →
∀ pti p,
p ≠ PTEUndef →
PMap_valid
(ZMap.get i (ZMap.set i´ (ZMap.set pdi (PDEValid pi (ZMap.set pti p pdt))
(ZMap.get i´ ptp)) ptp)).
Proof.
unfold PMap_valid; intros.
destruct (zeq i i´); subst.
- rewrite ZMap.gss.
destruct H as (HP1 & HP2). split.
+ unfold PMap_common, PDE_kern in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× erewrite HP1 in H0; eauto. congruence.
× rewrite ZMap.gso; auto.
+ unfold PMap_usr, PDE_usr in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× rewrite ZMap.gss. right. right.
exploit HP2; eauto.
intros HP. destruct HP as [HP | [HP| HP]]; try congruence.
destruct HP as (pte & pi´ & HE & HN).
rewrite H0 in HE. inv HE.
refine_split´. reflexivity.
destruct (zeq pti (PTX (i × PgSize))); subst.
{
rewrite ZMap.gss. congruence.
}
{
rewrite ZMap.gso; auto.
}
× rewrite ZMap.gso; auto.
- rewrite ZMap.gso; auto.
Qed.
Lemma PMap_valid_gso_unp:
∀ ptp i,
PMap_valid (ZMap.get i ptp) →
∀ i´ pdi pi pdt,
ZMap.get pdi (ZMap.get i´ ptp) = PDEValid pi pdt →
∀ pti,
PMap_valid
(ZMap.get i (ZMap.set i´ (ZMap.set pdi (PDEValid pi (ZMap.set pti PTEUnPresent pdt))
(ZMap.get i´ ptp)) ptp)).
Proof.
intros. eapply PMap_valid_gso; eauto. congruence.
Qed.
Lemma PMap_valid_gso_valid:
∀ ptp i,
PMap_valid (ZMap.get i ptp) →
∀ i´ pdi pi pdt,
ZMap.get pdi (ZMap.get i´ ptp) = PDEValid pi pdt →
∀ pti v p,
PMap_valid
(ZMap.get i (ZMap.set i´ (ZMap.set pdi (PDEValid pi (ZMap.set pti (PTEValid v p) pdt))
(ZMap.get i´ ptp)) ptp)).
Proof.
intros. eapply PMap_valid_gso; eauto. congruence.
Qed.
Lemma PMap_kern_gso:
∀ ptp,
PMap_kern (ZMap.get 0 ptp) →
∀ i,
0 < i < num_proc →
∀ pt,
PMap_kern (ZMap.get 0 (ZMap.set i pt ptp)).
Proof.
intros. rewrite ZMap.gso; auto.
red; intros; subst. omega.
Qed.
Lemma PMap_valid_gso_pde_unp:
∀ ptp i,
PMap_valid (ZMap.get i ptp) →
∀ i´ pdi,
ZMap.get pdi (ZMap.get i´ ptp) = PDEUnPresent →
∀ v pt,
(∀ i,
0 ≤ i < one_k →
ZMap.get i pt ≠ PTEUndef) →
PMap_valid
(ZMap.get i (ZMap.set i´ (ZMap.set pdi (PDEValid v pt)
(ZMap.get i´ ptp)) ptp)).
Proof.
unfold PMap_valid; intros.
destruct (zeq i i´); subst.
- rewrite ZMap.gss.
destruct H as (HP1 & HP2). split.
+ unfold PMap_common, PDE_kern in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× erewrite HP1 in H0; eauto. congruence.
× rewrite ZMap.gso; auto.
+ unfold PMap_usr, PDE_usr in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× rewrite ZMap.gss. right. right.
refine_split´; trivial.
apply H1. apply Z_mod_lt. omega.
× rewrite ZMap.gso; auto.
- rewrite ZMap.gso; auto.
Qed.
Lemma PMap_valid_gss_pde_unp:
∀ ptp i,
PMap_valid (ZMap.get i ptp) →
∀ i´ pdi v pt,
ZMap.get pdi (ZMap.get i´ ptp) = PDEValid v pt →
PMap_valid
(ZMap.get i (ZMap.set i´ (ZMap.set pdi PDEUnPresent
(ZMap.get i´ ptp)) ptp)).
Proof.
unfold PMap_valid; intros.
destruct (zeq i i´); subst.
- rewrite ZMap.gss.
destruct H as (HP1 & HP2). split.
+ unfold PMap_common, PDE_kern in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× erewrite HP1 in H0; eauto. congruence.
× rewrite ZMap.gso; auto.
+ unfold PMap_usr, PDE_usr in ×. intros.
destruct (zeq pdi (PDX (i × PgSize))); subst.
× rewrite ZMap.gss. left. trivial.
× rewrite ZMap.gso; auto.
- rewrite ZMap.gso; auto.
Qed.
End PMAP_VALID_KERN_INV.