Library mcertikos.invariants.INVLemmaQLock
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 Values.
Require Import AsmX.
Require Import Integers.
Require Import liblayers.compat.CompatLayers.
Require Import GlobalOracle.
Require Import GlobalOracleProp.
Require Import CalTicketLock.
Section ORACLE.
Context `{waittime: WaitTime}.
Local Transparent Q_CalLock H_CalLock.
Lemma valid_hlock_pool_init:
valid_hlock_pool (ZMap.init MultiUndef).
Proof.
unfold valid_hlock_pool; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma valid_qlock_pool_init:
valid_qlock_pool (ZMap.init MultiUndef).
Proof.
unfold valid_qlock_pool; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma valid_qlock_pool_gss:
∀ t l p
(Hvalid: valid_qlock_pool t)
(Hlock: valid_qlock l),
valid_qlock_pool (ZMap.set p (MultiDef l) t).
Proof.
unfold valid_qlock_pool; intros.
destruct (zeq p r); subst.
- rewrite ZMap.gss in Hdef. inv Hdef. trivial.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_qlock_pool_gss´:
∀ t l p x
(Hvalid: valid_qlock_pool t)
(Hlock: Q_CalLock l = Some x),
valid_qlock_pool (ZMap.set p (MultiDef l) t).
Proof.
intros. eapply valid_qlock_pool_gss; eauto.
unfold valid_qlock.
destruct x. repeat destruct p0. eauto 20.
Qed.
Lemma real_valid_qlock_pool_pb:
∀ n l
(Hvalid: valid_qlock_pool l),
valid_qlock_pool (real_multi_log_pb n l).
Proof.
induction n.
- simpl; intros. trivial.
- simpl; intros. eapply IHn in Hvalid.
eapply valid_qlock_pool_gss; trivial.
unfold valid_qlock. simpl. eauto 10.
Qed.
Lemma real_valid_qlock_pool:
∀ l
(Hvalid: valid_qlock_pool l),
valid_qlock_pool (real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_qlock_pool_pb.
Qed.
Lemma valid_hlock_pool_gss:
∀ t l p
(Hvalid: valid_hlock_pool t)
(Hlock: valid_hlock l),
valid_hlock_pool (ZMap.set p (MultiDef l) t).
Proof.
unfold valid_hlock_pool; intros.
destruct (zeq p r); subst.
- rewrite ZMap.gss in Hdef. inv Hdef. trivial.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_hlock_pool_gss´:
∀ t l p x
(Hvalid: valid_hlock_pool t)
(Hlock: H_CalLock l = Some x),
valid_hlock_pool (ZMap.set p (MultiDef l) t).
Proof.
intros. eapply valid_hlock_pool_gss; eauto.
unfold valid_hlock. destruct x. destruct p0.
eauto.
Qed.
Lemma real_valid_hlock_pool_pb:
∀ n l
(Hvalid: valid_hlock_pool l),
valid_hlock_pool (real_multi_log_pb n l).
Proof.
induction n.
- simpl; intros. trivial.
- simpl; intros. eapply IHn in Hvalid.
eapply valid_hlock_pool_gss; trivial.
unfold valid_hlock. simpl. eauto 10.
Qed.
Lemma real_valid_hlock_pool:
∀ l
(Hvalid: valid_hlock_pool l),
valid_hlock_pool (real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_hlock_pool_pb.
Qed.
Lemma Shared2ID1_neq:
∀ i p ofs z,
Shared2ID1 i = Some p →
index2Z i ofs = Some z →
z ≠ lock_AT_start.
Proof.
unfold lock_AT_start.
intros. functional inversion H; subst.
- functional inversion H0.
functional inversion H3; subst.
functional inversion H2; subst.
unfold ID_AT_range in ×. omega.
- functional inversion H0.
functional inversion H3; subst.
functional inversion H2; subst.
unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma Shared2ID2_neq:
∀ i p ofs z,
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
z ≠ lock_AT_start.
Proof.
unfold lock_AT_start.
intros. functional inversion H; subst.
functional inversion H0.
functional inversion H3; subst.
functional inversion H2; subst.
unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma TCB_neq:
∀ i,
(Int.unsigned i + ID_AT_range ≠ lock_AT_start) % Z.
Proof.
unfold ID_AT_range, lock_AT_start. intros.
specialize (Int.unsigned_range i).
rewrite_omega.
Qed.
Lemma TCB_neq´:
∀ i
(Hi: (0 ≤ i)%Z),
(i + ID_AT_range ≠ lock_AT_start) % Z.
Proof.
unfold ID_AT_range, lock_AT_start. intros.
rewrite_omega.
Qed.
Lemma SC_neq´:
∀ i
(Hi: (0 ≤ i)%Z),
(i + lock_TCB_range ≠ lock_AT_start) % Z.
Proof.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range, lock_AT_start. intros.
rewrite_omega.
Qed.
Lemma valid_AT_log_TICKET:
∀ l n c l´ e
(Hvalid: valid_AT_log l n)
(Hwait: l´ = TEVENT c (TTICKET e) :: l),
valid_AT_log l´ n.
Proof.
unfold valid_AT_log. intros; subst.
simpl in H. eauto.
Qed.
Lemma valid_AT_log_pull:
∀ l n c l´
(Hvalid: valid_AT_log l n)
(Hwait: l´ = TEVENT c (TSHARED OPULL) :: l),
valid_AT_log l´ n.
Proof.
unfold valid_AT_log. intros; subst.
simpl in H. eauto.
Qed.
Lemma valid_AT_log_imply:
∀ l to n ml c
(Hget: ZMap.get lock_AT_start ml = MultiDef l)
(Hvalid: valid_AT_log_pool ml n)
(Hvalid_oracle: valid_AT_oracle to)
,
valid_AT_log (to c l ++ l) n.
Proof.
unfold valid_AT_log. intros; subst.
unfold valid_AT_log_pool in ×.
rewrite Hget in Hvalid.
destruct Hvalid as (q & ? & Hv). subst.
inv H0.
unfold valid_AT_oracle in ×.
eapply (Hvalid_oracle q c n) in Hv.
eapply Hv. trivial.
Qed.
Lemma valid_AT_log_TICKET_imply:
∀ l to n ml c l´ e
(Hget: ZMap.get lock_AT_start ml = MultiDef l)
(Hvalid: valid_AT_log_pool ml n)
(Hvalid_oracle: valid_AT_oracle to)
(Hwait: l´ = TEVENT c (TTICKET e) :: to c l ++ l),
valid_AT_log l´ n.
Proof.
intros. subst.
eapply valid_AT_log_TICKET; eauto.
eapply valid_AT_log_imply; eauto.
Qed.
Lemma valid_AT_log_pool_gss´:
∀ t l p n
(Hvalid: valid_AT_log_pool t n)
(Hlock: valid_AT_log l n),
valid_AT_log_pool (ZMap.set p (MultiDef l) t) n.
Proof.
unfold valid_AT_log_pool; intros.
destruct (zeq p lock_AT_start); subst.
- rewrite ZMap.gss. refine_split´; trivial.
- rewrite ZMap.gso; eauto.
Qed.
Lemma valid_AT_log_pool_TICKET:
∀ t l l0 n curid e a
(Hl0: l0 = TEVENT curid (TTICKET e) :: TEVENT curid (TSHARED (OATE a)) :: l)
(Hkern: AT_kern a n)
(Husr: AT_usr a n),
valid_AT_log_pool (ZMap.set lock_AT_start (MultiDef l0) t) n.
Proof.
intros. subst. unfold valid_AT_log_pool. rewrite ZMap.gss.
refine_split´; eauto.
unfold valid_AT_log. simpl. intros. inv H. eauto.
Qed.
Lemma real_valid_AT_log_pool_pb:
∀ n0 l n
(Hneq: n0 ≠ O),
valid_AT_log_pool (real_multi_log_pb n0 l) n.
Proof.
induction n0.
- intros. congruence.
- simpl; intros.
unfold valid_AT_log_pool.
unfold lock_AT_start.
destruct (zeq (Z.of_nat n0) 0).
+ rewrite e.
rewrite ZMap.gss. refine_split´; eauto.
unfold valid_AT_log.
intros. inv H.
+ rewrite ZMap.gso; eauto.
eapply IHn0; eauto. omega.
Qed.
Lemma real_valid_AT_log_pool:
∀ l n,
valid_AT_log_pool (CalTicketLock.real_multi_log l) n.
Proof.
unfold real_multi_log. intros.
eapply real_valid_AT_log_pool_pb.
unfold lock_range, ID_AT_range, ID_TCB_range, ID_SC_range.
simpl. xomega.
Qed.
Lemma real_lock_pb_exists:
∀ n loc,
∃ loc´, real_lock_pb n loc = loc´.
Proof.
induction n; intros; [∃ loc; simpl | ]; auto.
destruct (IHn loc).
∃ (ZMap.set (Z.of_nat n) LockFalse x).
simpl; subst; auto.
Qed.
Lemma real_lock_pb_imples_lock_false´:
∀ n loc loc´ id
(Hrel: real_lock_pb n loc = loc´)
(Hid: (0 ≤ id < Z.of_nat n)%Z),
ZMap.get id loc´ = LockFalse.
Proof.
induction n; intros.
- simpl in Hid. omega.
- Local Opaque Z.of_nat.
simpl in ×. rewrite <- Hrel.
destruct (zeq id (Z.of_nat n)); subst.
+ rewrite ZMap.gss; trivial.
+ rewrite ZMap.gso; auto.
eapply IHn; eauto.
Local Transparent Z.of_nat.
rewrite Nat2Z.inj_succ in Hid.
omega.
Qed.
Lemma real_lock_implies_lock_false:
∀ loc loc´ id,
real_lock loc = loc´ →
(0 ≤ id < lock_range)%Z →
ZMap.get id loc´ = LockFalse.
Proof.
intros.
unfold real_lock in H.
eapply real_lock_pb_imples_lock_false´. eapply H.
rewrite Z2Nat.id; trivial.
unfold lock_range, ID_AT_range, ID_TCB_range, ID_SC_range. omega.
Qed.
Require Import RealParams.
Context `{real_params: RealParams}.
Lemma valid_AT_log_pool_H_init:
valid_AT_log_pool_H (ZMap.init MultiUndef).
Proof.
unfold valid_AT_log_pool_H; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma valid_AT_log_pool_H_gso:
∀ l e q,
valid_AT_log_pool_H l →
e ≠ lock_AT_start →
valid_AT_log_pool_H (ZMap.set e q l).
Proof.
unfold valid_AT_log_pool_H.
intros.
rewrite ZMap.gso in Hdef; auto.
Qed.
Lemma valid_AT_log_pool_H_gss:
∀ l o q i,
valid_AT_log_pool_H l →
valid_AT_oracle_pool_H o →
ZMap.get lock_AT_start l = MultiDef q →
let o´ := ZMap.get lock_AT_start o in
valid_AT_log_pool_H (ZMap.set lock_AT_start (MultiDef ((o´ i q) ++ q)) l).
Proof.
unfold valid_AT_log_pool_H.
unfold valid_AT_oracle_pool_H.
intros. rewrite ZMap.gss in Hdef. inv Hdef.
specialize (H _ H1).
eapply H0. trivial.
Qed.
Lemma valid_AT_log_pool_H_gss´:
∀ l q i
(Hvalid´: valid_AT_log_H q)
(Hvalid: valid_AT_log_pool_H l),
valid_AT_log_pool_H (ZMap.set i (MultiDef q) l).
Proof.
unfold valid_AT_log_pool_H; intros.
destruct (zeq i lock_AT_start); subst.
- rewrite ZMap.gss in Hdef. inv Hdef.
trivial.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_hlock_pool_init1:
valid_hlock_pool1 (ZMap.init MultiUndef).
Proof.
unfold valid_hlock_pool1; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma valid_hlock_pool1_gss:
∀ t l p
(Hvalid: valid_hlock_pool1 t)
(Hlock: valid_hlock l),
valid_hlock_pool1 (ZMap.set p (MultiDef l) t).
Proof.
unfold valid_hlock_pool1; intros.
destruct (zeq p r); subst.
- rewrite ZMap.gss in Hdef. inv Hdef. trivial.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_hlock_pool1_gss´:
∀ t l p x
(Hvalid: valid_hlock_pool1 t)
(Hlock: H_CalLock l = Some x),
valid_hlock_pool1 (ZMap.set p (MultiDef l) t).
Proof.
intros. eapply valid_hlock_pool1_gss; eauto.
unfold valid_hlock. destruct x. destruct p0.
eauto.
Qed.
Lemma real_valid_AT_log_pool_H_pb:
∀ n0 l
(Hvalid: valid_AT_log_pool_H l),
valid_AT_log_pool_H (real_multi_log_pb n0 l).
Proof.
induction n0.
- simpl; intros. trivial.
- simpl; intros. eapply IHn0 in Hvalid.
eapply valid_AT_log_pool_H_gss´; trivial.
econstructor.
unfold CalAT_log_real. simpl. trivial.
Qed.
Lemma real_valid_AT_log_pool_H:
∀ l
(Hvalid: valid_AT_log_pool_H l),
valid_AT_log_pool_H (CalTicketLock.real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_AT_log_pool_H_pb.
Qed.
Lemma real_valid_hlock_pool1_pb:
∀ n l
(Hvalid: valid_hlock_pool1 l),
valid_hlock_pool1 (real_multi_log_pb n l).
Proof.
induction n.
- simpl; intros. trivial.
- simpl; intros. eapply IHn in Hvalid.
eapply valid_hlock_pool1_gss; trivial.
unfold valid_hlock. simpl. eauto 10.
Qed.
Lemma real_valid_hlock_pool1:
∀ l
(Hvalid: valid_hlock_pool1 l),
valid_hlock_pool1 (real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_hlock_pool1_pb.
Qed.
Lemma valid_AT_log_pool_H_gss´´:
∀ l q,
valid_AT_log_H q →
valid_AT_log_pool_H (ZMap.set lock_AT_start (MultiDef q) l).
Proof.
unfold valid_AT_log_pool_H.
intros. rewrite ZMap.gss in Hdef. inv Hdef.
trivial.
Qed.
Lemma valid_AT_log_pool_H_0´:
∀ l d c
(Hcal: valid_AT_log_H l),
valid_AT_log_pool_H (ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE 0)) :: l)) d).
Proof.
unfold valid_AT_log_pool_H.
unfold valid_AT_log_H.
intros. rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
destruct Hcal as (a & Hcal).
simpl. rewrite Hcal. eauto.
Qed.
Lemma valid_AT_log_pool_H_0:
∀ l a d c
(Hcal: CalAT_log_real l = Some a),
valid_AT_log_pool_H (ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE 0)) :: l)) d).
Proof.
intros. eapply valid_AT_log_pool_H_0´; eauto.
unfold valid_AT_log_H.
rewrite Hcal. eauto.
Qed.
Lemma valid_AT_log_pool_H_n:
∀ l a d c n
(Hcal: CalAT_log_real l = Some a)
(Hv: ZMap.get n a = ATValid false ATNorm),
valid_AT_log_pool_H (ZMap.set lock_AT_start (MultiDef (TEVENT c (TSHARED (OPALLOCE n)) :: l)) d).
Proof.
unfold valid_AT_log_pool_H.
unfold valid_AT_log_H.
intros. rewrite ZMap.gss in Hdef. inv Hdef.
unfold CalAT_log_real in ×.
simpl. rewrite Hcal.
destruct (zeq n 0); eauto. rewrite Hv. eauto.
Qed.
Lemma index2Z1_false:
∀ i ofs,
¬ (index2Z1 i ofs = Some lock_AT_start).
Proof.
intros ? ? HF. functional inversion HF.
functional inversion H0; subst; simpl in ×.
- inv H1. unfold ID_AT_range, lock_AT_start in ×. omega.
- inv H1. unfold lock_TCB_range, lock_AT_start in ×.
unfold ID_TCB_range, ID_AT_range in ×.
omega.
Qed.
Lemma valid_hlock_pool1_gso:
∀ d l
(Hv: valid_hlock_pool1 d),
valid_hlock_pool1 (ZMap.set lock_AT_start l d).
Proof.
unfold valid_hlock_pool1; intros.
destruct (zeq r lock_AT_start); subst.
- eapply index2Z1_false in Hrange. inv Hrange.
- rewrite ZMap.gso in Hdef; eauto.
Qed.
Section TCB_INV.
Local Open Scope Z_scope.
Lemma SC_neq0:
∀ i,
0 ≤ i < num_chan →
(∀ i0, 0 ≤ i0 < num_chan →
i0 + ID_AT_range ≠ i + lock_TCB_range).
Proof.
unfold lock_TCB_range, ID_AT_range, ID_TCB_range.
intros. omega.
Qed.
Lemma Shared2ID2_neq´:
∀ i p ofs z,
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
(∀ i0, 0 ≤ i0 < num_chan → i0 + ID_AT_range ≠ z).
Proof.
intros. functional inversion H; subst.
functional inversion H0.
functional inversion H3; subst.
functional inversion H4; subst.
unfold ID_SC_range, lock_TCB_range, ID_TCB_range, ID_AT_range in ×. omega.
Qed.
Lemma neq_add:
∀ a b c,
a ≠ b →
a + c ≠ b + c.
Proof.
intros. omega.
Qed.
Lemma valid_TCB_log_pool_init:
valid_TCB_log_pool (ZMap.init MultiUndef).
Proof.
unfold valid_TCB_log_pool; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma real_valid_TCB_log_pool_pb:
∀ n0 l
(Hvalid: valid_TCB_log_pool l),
valid_TCB_log_pool (real_multi_log_pb n0 l).
Proof.
induction n0.
- simpl; intros. trivial.
- simpl; intros. eapply IHn0 in Hvalid. clear IHn0.
unfold valid_TCB_log_pool in ×.
intros.
destruct (zeq (i + ID_AT_range) (Z.of_nat n0)).
+ rewrite e in Hdef. rewrite ZMap.gss in Hdef.
inv Hdef. unfold valid_TCB_log. intros.
inv Hshared.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma real_valid_TCB_log_pool:
∀ l
(Hvalid: valid_TCB_log_pool l),
valid_TCB_log_pool (CalTicketLock.real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_TCB_log_pool_pb.
Qed.
Lemma valid_TCB_log_pool_gso:
∀ l e q,
valid_TCB_log_pool l →
(∀ i, 0 ≤ i < num_chan → i + ID_AT_range ≠ e) →
valid_TCB_log_pool (ZMap.set e q l).
Proof.
unfold valid_TCB_log_pool.
intros.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_TCB_log_pool_gso´:
∀ l z i p q ofs,
valid_TCB_log_pool l →
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
valid_TCB_log_pool (ZMap.set z q l).
Proof.
intros.
eapply valid_TCB_log_pool_gso; eauto.
eapply Shared2ID2_neq´; eauto.
Qed.
Lemma valid_TCB_log_pool_gso_AT:
∀ l q,
valid_TCB_log_pool l →
valid_TCB_log_pool (ZMap.set lock_AT_start q l).
Proof.
intros.
eapply valid_TCB_log_pool_gso; eauto.
intros. eapply TCB_neq´; eauto. omega.
Qed.
Lemma valid_TCB_log_pool_gss:
∀ l q i
(Hvalid: valid_TCB_log q)
(Hvalid´: valid_TCB_log_pool l),
valid_TCB_log_pool (ZMap.set (i + ID_AT_range) (MultiDef q) l).
Proof.
unfold valid_TCB_log_pool. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in Hdef. inv Hdef; trivial.
- rewrite ZMap.gso in Hdef; eauto.
eapply neq_add. auto.
Qed.
Lemma valid_TCB_log_wait:
∀ l c b
(Hvalid: valid_TCB_log l),
valid_TCB_log (TEVENT c (TTICKET (WAIT_LOCK b)) :: l).
Proof.
unfold valid_TCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_TCB_log_rel:
∀ l c
(Hvalid: valid_TCB_log l),
valid_TCB_log (TEVENT c (TTICKET REL_LOCK) :: l).
Proof.
unfold valid_TCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_TCB_log_pull:
∀ l c
(Hvalid: valid_TCB_log l),
valid_TCB_log (TEVENT c (TSHARED OPULL) :: l).
Proof.
unfold valid_TCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_TCB_log_shared:
∀ l c t tq
(Hvalid: valid_TCB_log l)
(Htcb: TCBCorrect_range t)
(Htdq: TDQCorrect_range tq),
valid_TCB_log (TEVENT c (TSHARED (OTCBE t tq)) :: l).
Proof.
unfold valid_TCB_log; intros.
simpl in Hshared. inv Hshared. eauto.
Qed.
Lemma AbTCBStrong_range_impl:
∀ t,
AbTCBStrong_range t →
AbTCBCorrect_range t.
Proof.
unfold AbTCBStrong_range, AbTCBCorrect_range, AbTCBStrong, AbTCBCorrect. intros.
exploit H; eauto. intros (? & ? & ? & Hr1 & Hr2 & Hr3 & Hr4).
rewrite Hr1. esplit; esplit; esplit. split; trivial.
destruct x.
- exploit Hr4; trivial. omega.
- exploit Hr2; auto. omega.
- exploit Hr3; trivial. left; trivial. omega.
- exploit Hr2; auto. omega.
- exploit Hr3; trivial. right; trivial. omega.
Qed.
Lemma valid_SABTCB_log_imply:
∀ l,
valid_SABTCB_log l →
valid_ABTCB_log l.
Proof.
unfold valid_SABTCB_log, valid_ABTCB_log.
intros. exploit H; eauto.
intros (? & ? & ? & ?).
refine_split´; eauto.
eapply AbTCBStrong_range_impl; eauto.
Qed.
Lemma valid_ABTCB_log_pool_init:
valid_ABTCB_log_pool (ZMap.init MultiUndef).
Proof.
unfold valid_ABTCB_log_pool; intros.
rewrite ZMap.gi in Hdef. inv Hdef.
Qed.
Lemma real_valid_ABTCB_log_pool_pb:
∀ n0 l
(Hvalid: valid_ABTCB_log_pool l),
valid_ABTCB_log_pool (real_multi_log_pb n0 l).
Proof.
induction n0.
- simpl; intros. trivial.
- simpl; intros. eapply IHn0 in Hvalid. clear IHn0.
unfold valid_ABTCB_log_pool in ×.
intros.
destruct (zeq (i + ID_AT_range) (Z.of_nat n0)).
+ rewrite e in Hdef. rewrite ZMap.gss in Hdef.
inv Hdef. unfold valid_ABTCB_log. intros.
inv Hshared.
+ rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma real_valid_ABTCB_log_pool:
∀ l
(Hvalid: valid_ABTCB_log_pool l),
valid_ABTCB_log_pool (CalTicketLock.real_multi_log l).
Proof.
unfold real_multi_log.
eapply real_valid_ABTCB_log_pool_pb.
Qed.
Lemma valid_ABTCB_log_pool_gso:
∀ l e q,
valid_ABTCB_log_pool l →
(∀ i, 0 ≤ i < num_chan → i + ID_AT_range ≠ e) →
valid_ABTCB_log_pool (ZMap.set e q l).
Proof.
unfold valid_ABTCB_log_pool.
intros.
rewrite ZMap.gso in Hdef; eauto.
Qed.
Lemma valid_ABTCB_log_pool_gso´:
∀ l z i p q ofs,
valid_ABTCB_log_pool l →
Shared2ID2 i = Some p →
index2Z i ofs = Some z →
valid_ABTCB_log_pool (ZMap.set z q l).
Proof.
intros.
eapply valid_ABTCB_log_pool_gso; eauto.
eapply Shared2ID2_neq´; eauto.
Qed.
Lemma valid_ABTCB_log_pool_gso_AT:
∀ l q,
valid_ABTCB_log_pool l →
valid_ABTCB_log_pool (ZMap.set lock_AT_start q l).
Proof.
intros.
eapply valid_ABTCB_log_pool_gso; eauto.
intros. eapply TCB_neq´; eauto. omega.
Qed.
Lemma valid_ABTCB_log_pool_gss:
∀ l q i
(Hvalid: valid_ABTCB_log q)
(Hvalid´: valid_ABTCB_log_pool l),
valid_ABTCB_log_pool (ZMap.set (i + ID_AT_range) (MultiDef q) l).
Proof.
unfold valid_ABTCB_log_pool. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss in Hdef. inv Hdef; trivial.
- rewrite ZMap.gso in Hdef; eauto.
eapply neq_add. auto.
Qed.
Lemma valid_ABTCB_log_wait:
∀ l c b
(Hvalid: valid_ABTCB_log l),
valid_ABTCB_log (TEVENT c (TTICKET (WAIT_LOCK b)) :: l).
Proof.
unfold valid_ABTCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_ABTCB_log_pull:
∀ l c
(Hvalid: valid_ABTCB_log l),
valid_ABTCB_log (TEVENT c (TSHARED OPULL) :: l).
Proof.
unfold valid_ABTCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_ABTCB_log_rel:
∀ l c
(Hvalid: valid_ABTCB_log l),
valid_ABTCB_log (TEVENT c (TTICKET REL_LOCK) :: l).
Proof.
unfold valid_ABTCB_log; intros.
simpl in Hshared. eauto.
Qed.
Lemma valid_ABTCB_log_shared:
∀ l c t tq
(Hvalid: valid_ABTCB_log l)
(Htcb: AbTCBCorrect_range t)
(Htdq: AbQCorrect_range tq)
(Hcount: QCount t tq)
(HinQ: InQ t tq),
valid_ABTCB_log (TEVENT c (TSHARED (OABTCBE t tq)) :: l).
Proof.
unfold valid_ABTCB_log; intros.
simpl in Hshared. inv Hshared. eauto.
Qed.
End TCB_INV.
End ORACLE.