Library mcertikos.invariants.INVLemmaThread
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 AbstractDataType.
Section KCTXT_INJECT_NEUTRAL_INV.
Lemma kctxt_inject_neutral_gss:
∀ kp n (rs: regset),
kctxt_inject_neutral kp n →
(∀ r,
val_inject (Mem.flat_inj n) (rs r) (rs r)) →
wt_regset rs →
∀ i,
kctxt_inject_neutral
(ZMap.set i
(Pregmap.init Vundef) # ESP <- (rs ESP)
# EDI <- (rs EDI) # ESI <- (rs ESI)
# EBX <- (rs EBX) # EBP <- (rs EBP)
# RA <- (rs RA) kp) n.
Proof.
intros. intros until 2.
destruct (zeq ofs i); subst.
- rewrite ZMap.gss.
repeat (rewrite Pregmap_Simpl).
erewrite ZtoPreg_type; eauto.
inv_uctx_primitive H; split; subst; auto.
constructor.
- rewrite ZMap.gso; eauto.
Qed.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Local Open Scope Z_scope.
Lemma kctxt_inject_neutral_gss_flatinj´:
∀ i k kp n,
kctxt_inject_neutral (ZMap.set i k kp) n →
∀ b,
Mem.flat_inj n b = Some (b, 0) →
∀ ofs r,
kctxt_inject_neutral
(ZMap.set i k # r <- (Vptr b ofs) kp) n.
Proof.
intros. intros until 2.
destruct (zeq ofs0 i); subst; simpl.
+ specialize (H _ H1 _ _ H2).
rewrite ZMap.gss in ×.
rewrite Pregmap_Simpl.
destruct (Pregmap.elt_eq r0 r); trivial.
split. constructor.
econstructor; eauto.
rewrite Int.add_zero; trivial.
+ specialize (H _ H1 _ _ H2).
rewrite ZMap.gso in *; eauto.
Qed.
Lemma kctxt_inject_neutral_gss_flatinj:
∀ kp n,
kctxt_inject_neutral kp n →
∀ b,
Mem.flat_inj n b = Some (b, 0) →
∀ i ofs r,
kctxt_inject_neutral
(ZMap.set i (ZMap.get i kp) # r <- (Vptr b ofs) kp) n.
Proof.
intros. intros until 2.
destruct (zeq ofs0 i); subst; simpl.
+ rewrite ZMap.gss.
specialize (H _ H1 _ _ H2).
rewrite Pregmap_Simpl.
destruct (Pregmap.elt_eq r0 r); trivial.
split. constructor.
econstructor; eauto.
rewrite Int.add_zero; trivial.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma kctxt_inject_neutral_gss_ptr:
∀ kp n,
kctxt_inject_neutral kp n →
∀ s b,
(∃ fun_id, find_symbol s fun_id = Some b) →
(genv_next s ≤ n)%positive →
∀ i ofs r,
kctxt_inject_neutral
(ZMap.set i (ZMap.get i kp) # r <- (Vptr b ofs) kp) n.
Proof.
intros.
eapply kctxt_inject_neutral_gss_flatinj; eauto.
destruct H0 as [fun_id HSy].
eapply stencil_find_symbol_inject´; eauto.
eapply flat_inj_inject_incr; assumption.
Qed.
Lemma kctxt_inject_neutral_gss_mem:
∀ s kp m (rs: regset),
kctxt_inject_neutral kp (Mem.nextblock m) →
asm_invariant s rs m →
∀ i,
kctxt_inject_neutral
(ZMap.set i
(Pregmap.init Vundef) # ESP <- (rs ESP)
# EDI <- (rs EDI) # ESI <- (rs ESI)
# EBX <- (rs EBX) # EBP <- (rs EBP)
# RA <- (rs RA) kp) (Mem.nextblock m).
Proof.
intros. inv H0. inv inv_inject_neutral.
eapply kctxt_inject_neutral_gss; eauto.
Qed.
End WITHMEM.
End KCTXT_INJECT_NEUTRAL_INV.
Section TCB_INV.
Local Open Scope Z_scope.
Lemma TCBCorrect_range_gss:
∀ t,
TCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ s´ c´ n´ p´,
0 ≤ n´ ≤ num_proc →
0 ≤ p´ ≤ num_proc →
TCBCorrect_range
(ZMap.set i (TCBValid s´ c´ p´ n´) t).
Proof.
unfold TCBCorrect_range; intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss.
specialize (H _ H0). unfold TCBCorrect in ×.
refine_split´; eauto.
- rewrite ZMap.gso; auto.
Qed.
Lemma TCBCorrect_range_gss_num_proc:
∀ t,
TCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ s´ c,
TCBCorrect_range
(ZMap.set i (TCBValid s´ c num_proc num_proc) t).
Proof.
intros. eapply TCBCorrect_range_gss; eauto; omega.
Qed.
Lemma TCBCorrect_range_valid_prev:
∀ q,
TCBCorrect_range q →
∀ i s c n p,
ZMap.get i q = TCBValid s c n p →
0 ≤ i < num_proc →
0 ≤ n ≤ num_proc.
Proof.
unfold TCBCorrect_range, TCBCorrect. intros.
specialize (H _ H1). rewrite H0 in H.
destruct H as (st & cu & next & prev & He & Hr & Hr´).
inv He. assumption.
Qed.
Lemma TCBCorrect_range_valid_next:
∀ q,
TCBCorrect_range q →
∀ i s c n p,
ZMap.get i q = TCBValid s c n p →
0 ≤ i < num_proc →
0 ≤ p ≤ num_proc.
Proof.
unfold TCBCorrect_range, TCBCorrect. intros.
specialize (H _ H1). rewrite H0 in H.
destruct H as (st & cu & next & prev & He & Hr & Hr´).
inv He. assumption.
Qed.
Lemma TCBCorrect_range_gso:
∀ t,
TCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ p n s c,
ZMap.get i t = TCBValid s c p n →
∀ s´ c´,
TCBCorrect_range
(ZMap.set i (TCBValid s´ c´ p n) t).
Proof.
intros. eapply TCBCorrect_range_gss; eauto.
- eapply TCBCorrect_range_valid_next; eauto.
- eapply TCBCorrect_range_valid_prev; eauto.
Qed.
Lemma TCBCorrect_range_gss_prev:
∀ t,
TCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ p n s c,
ZMap.get i t = TCBValid s c p n →
∀ s´ p´ c´,
0 ≤ p´ ≤ num_proc →
TCBCorrect_range
(ZMap.set i (TCBValid s´ c´ p´ n) t).
Proof.
intros. eapply TCBCorrect_range_gss; eauto.
eapply TCBCorrect_range_valid_next; eauto.
Qed.
Lemma TCBCorrect_range_gss_next:
∀ t,
TCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ p n s c,
ZMap.get i t = TCBValid s c p n →
∀ s´ n´ c´,
0 ≤ n´ ≤ num_proc →
TCBCorrect_range
(ZMap.set i (TCBValid s´ c´ p n´) t).
Proof.
intros. eapply TCBCorrect_range_gss; eauto.
eapply TCBCorrect_range_valid_prev; eauto.
Qed.
End TCB_INV.
Section TDQ_INV.
Local Open Scope Z_scope.
Lemma TDQCorrect_range_gss:
∀ q,
TDQCorrect_range q →
∀ i,
0 ≤ i < num_chan →
∀ h t,
0 ≤ h ≤ num_proc →
0 ≤ t ≤ num_proc →
TDQCorrect_range
(ZMap.set i (TDQValid h t) q).
Proof.
unfold TDQCorrect_range. intros.
destruct (zeq i i0); subst.
- rewrite ZMap.gss. unfold TDQCorrect.
esplit; esplit. split; trivial.
split; assumption.
- rewrite ZMap.gso; auto 2.
Qed.
Lemma TDQCorrect_range_gss_num_proc:
∀ q,
TDQCorrect_range q →
∀ i,
0 ≤ i < num_chan →
TDQCorrect_range
(ZMap.set i (TDQValid num_proc num_proc) q).
Proof.
intros. eapply TDQCorrect_range_gss; eauto; omega.
Qed.
Lemma TDQCorrect_range_valid_head:
∀ q,
TDQCorrect_range q →
∀ i h t,
ZMap.get i q = TDQValid h t →
0 ≤ i < num_chan →
0 ≤ h ≤ num_proc.
Proof.
unfold TDQCorrect_range, TDQCorrect. intros.
specialize (H _ H1). rewrite H0 in H.
destruct H as (head & tail & He & Hr & Hr´).
inv He. assumption.
Qed.
Lemma TDQCorrect_range_valid_tail:
∀ q,
TDQCorrect_range q →
∀ i h t,
ZMap.get i q = TDQValid h t →
0 ≤ i < num_chan →
0 ≤ t ≤ num_proc.
Proof.
unfold TDQCorrect_range, TDQCorrect. intros.
specialize (H _ H1). rewrite H0 in H.
destruct H as (head & tail & He & Hr & Hr´).
inv He. assumption.
Qed.
Lemma TDQCorrect_range_gss_tail:
∀ q,
TDQCorrect_range q →
∀ i h t,
0 ≤ i < num_chan →
ZMap.get i q = TDQValid h t →
∀ t´,
0 ≤ t´ ≤ num_proc →
TDQCorrect_range
(ZMap.set i (TDQValid h t´) q).
Proof.
intros. eapply TDQCorrect_range_gss; eauto.
eapply TDQCorrect_range_valid_head; eauto.
Qed.
End TDQ_INV.
Section AbTCB_INV.
Local Open Scope Z_scope.
Lemma AbTCBCorrect_range_gss:
∀ t,
AbTCBCorrect_range t →
∀ i s c b,
-1 ≤ b < num_chan →
AbTCBCorrect_range (ZMap.set i (AbTCBValid s c b) t).
Proof.
unfold AbTCBCorrect_range; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. unfold AbTCBCorrect.
esplit; esplit; esplit. split; trivial.
- rewrite ZMap.gso; eauto.
Qed.
Lemma AbTCBCorrect_range_valid_b:
∀ t,
AbTCBCorrect_range t →
∀ i,
0 ≤ i < num_proc →
∀ s c b,
ZMap.get i t = AbTCBValid s c b →
-1 ≤ b < num_chan.
Proof.
unfold AbTCBCorrect_range, AbTCBCorrect; intros.
specialize (H _ H0). rewrite H1 in H.
destruct H as (? & ? & ? & He & Hr). inv He. assumption.
Qed.
Lemma AbQCorrect_range_gss_enqueue:
∀ q,
AbQCorrect_range q →
∀ i l,
ZMap.get i q = AbQValid l →
∀ a,
0 ≤ a < num_proc →
AbQCorrect_range
(ZMap.set i (AbQValid (l ++ (a :: nil))) q).
Proof.
unfold AbQCorrect_range, AbQCorrect. intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. exploit H; eauto. rewrite H0.
intros (l0 & He & Hr). inv He.
refine_split´; trivial.
intros. eapply in_app_or in H3.
inv H3; eauto. inv H4. trivial. inv H3.
- rewrite ZMap.gso; eauto.
Qed.
Lemma AbTCBStrong_range_gss_READY:
∀ t,
AbTCBStrong_range t →
∀ i c,
AbTCBStrong_range (ZMap.set i (AbTCBValid READY c num_proc) t).
Proof.
unfold AbTCBStrong_range; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. unfold AbTCBStrong.
refine_split´; eauto; intros.
+ inv H1; congruence.
+ inv H1; congruence.
- rewrite ZMap.gso; eauto.
Qed.
Lemma AbTCBStrong_range_gss_SLEEP:
∀ t,
AbTCBStrong_range t →
∀ i n c,
0 ≤ n < num_proc →
AbTCBStrong_range (ZMap.set i (AbTCBValid SLEEP c n) t).
Proof.
unfold AbTCBStrong_range; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. unfold AbTCBStrong.
refine_split´; eauto; intros; inv H2; congruence.
- rewrite ZMap.gso; eauto.
Qed.
Lemma AbTCBStrong_range_gss_RUN:
∀ t,
AbTCBStrong_range t →
∀ i c,
AbTCBStrong_range (ZMap.set i (AbTCBValid RUN c (-1)) t).
Proof.
unfold AbTCBStrong_range; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. unfold AbTCBStrong.
refine_split´; eauto; intros; inv H1; try congruence.
- rewrite ZMap.gso; eauto.
Qed.
End AbTCB_INV.
Section AbQ_INV.
Local Open Scope Z_scope.
Lemma AbQCorrect_range_gss:
∀ q,
AbQCorrect_range q →
∀ l,
(∀ x, In x l → 0 ≤ x < num_proc) →
∀ i,
AbQCorrect_range
(ZMap.set i (AbQValid l) q).
Proof.
unfold AbQCorrect_range, AbQCorrect. intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss.
refine_split´; trivial.
- rewrite ZMap.gso; eauto.
Qed.
Lemma remove_property:
∀ l P,
(∀ x, In x l → P x) →
∀ a,
(∀ x, In x (remove zeq a l) → P x).
Proof.
intros. eapply X.
specialize (remove_incl l a). intros Hcl.
apply Hcl in H. auto.
Qed.
Lemma AbQCorrect_range_gss_remove´:
∀ q,
AbQCorrect_range q →
∀ l,
(∀ x, In x l → 0 ≤ x < num_proc) →
∀ i a,
AbQCorrect_range
(ZMap.set i (AbQValid (remove zeq a l)) q).
Proof.
intros. eapply AbQCorrect_range_gss; eauto.
eapply remove_property; eauto.
Qed.
Lemma list_range_enqueue:
∀ l,
(∀ x, In x l → 0 ≤ x < num_proc) →
∀ a,
0 ≤ a < num_proc →
(∀ x, In x (l ++ (a::nil)) → 0 ≤ x < num_proc).
Proof.
intros.
eapply in_app_or in H1. inv H1; eauto.
inv H2; trivial. inv H1.
Qed.
Lemma AbQCorrect_range_gss_enqueue´:
∀ q,
AbQCorrect_range q →
∀ l,
(∀ x, In x l → 0 ≤ x < num_proc) →
∀ a,
0 ≤ a < num_proc →
∀ i,
AbQCorrect_range
(ZMap.set i (AbQValid (l ++ (a::nil))) q).
Proof.
intros. eapply AbQCorrect_range_gss; eauto.
eapply list_range_enqueue; eauto.
Qed.
Lemma AbQCorrect_range_impl:
∀ q,
AbQCorrect_range q →
∀ i l,
0 ≤ i < num_chan →
ZMap.get i q = AbQValid l →
(∀ x, In x l → 0 ≤ x < num_proc).
Proof.
unfold AbQCorrect_range, AbQCorrect. intros.
exploit H; eauto. rewrite H1.
intros (? & He & Hr). inv He. eauto.
Qed.
Lemma AbQCorrect_range_gss_remove:
∀ q,
AbQCorrect_range q →
∀ i l r,
ZMap.get i q = AbQValid (r :: l) →
AbQCorrect_range
(ZMap.set i (AbQValid l) q).
Proof.
unfold AbQCorrect_range, AbQCorrect. intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. exploit H; eauto. rewrite H0.
intros (l0 & He & Hr). inv He.
refine_split´; trivial.
intros. eapply Hr. right. trivial.
- rewrite ZMap.gso; eauto.
Qed.
Lemma last_range_AbQ:
∀ q,
AbQCorrect_range q →
∀ i,
0 ≤ i < num_chan →
∀ l,
ZMap.get i q = AbQValid l →
last l num_proc ≠ num_proc →
0 ≤ last l num_proc < num_proc.
Proof.
unfold AbQCorrect_range, AbQCorrect; intros.
exploit H; eauto. rewrite H1.
intros (? & He & Hr). inv He.
eapply Hr. apply last_correct; auto.
Qed.
End AbQ_INV.
Section THREAD_INV.
Local Open Scope Z_scope.
Section NOTINQ_INV.
Lemma NotInQ_gso_state:
∀ p t,
NotInQ p t →
∀ i,
0 ≤ i < num_proc →
∀ s c b,
ZMap.get i t = AbTCBValid s c b →
∀ s´ c´,
NotInQ p (ZMap.set i (AbTCBValid s´ c´ b) t).
Proof.
unfold NotInQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in H4. inv H4. eapply H; eauto.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma NotInQ_gso_cused:
∀ p t,
NotInQ p t →
∀ i,
cused (ZMap.get i p) = true →
∀ s,
NotInQ p (ZMap.set i s t).
Proof.
unfold NotInQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in H3. inv H3. congruence.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma NotInQ_gso_neg:
∀ p t,
NotInQ p t →
∀ i s c,
NotInQ p (ZMap.set i (AbTCBValid s c (-1)) t).
Proof.
unfold NotInQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in H2. inv H2. trivial.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma NotInQ_InQ_gss_wakeup´:
∀ p t q,
NotInQ p t →
InQ t q →
∀ i,
0 ≤ i < num_chan →
∀ l,
ZMap.get i q = AbQValid l →
∀ i´,
0 ≤ i´ < num_proc →
In i´ l →
∀ s c b,
NotInQ p (ZMap.set i´ (AbTCBValid s c b) t).
Proof.
unfold NotInQ, InQ; intros.
destruct (zeq i0 i´); subst.
- rewrite ZMap.gss in H7. inv H7.
exploit H0; eauto.
intros (? & ? & He). exploit H; eauto. omega.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma NotInQ_InQ_gss_wakeup:
∀ p t q,
NotInQ p t →
InQ t q →
AbQCorrect_range q →
∀ i,
0 ≤ i < num_chan →
∀ l,
ZMap.get i q = AbQValid l →
last l num_proc ≠ num_proc →
∀ s c b,
NotInQ p (ZMap.set (last l num_proc) (AbTCBValid s c b) t).
Proof.
intros. eapply NotInQ_InQ_gss_wakeup´; eauto.
- eapply last_range_AbQ; eauto.
- apply last_correct; auto.
Qed.
End NOTINQ_INV.
Section QCOUNT_INV.
Lemma QCount_gso_state:
∀ t q,
QCount t q →
∀ i,
0 ≤ i < num_proc →
∀ s c b,
ZMap.get i t = AbTCBValid s c b →
∀ s´ c´,
QCount (ZMap.set i (AbTCBValid s´ c´ b) t) q.
Proof.
unfold QCount; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in H3. inv H3. eauto.
- rewrite ZMap.gso in *; eauto.
Qed.
Lemma count_occ_append:
∀ l l´ x,
(count_occ zeq (l ++ l´) x = count_occ zeq l x + count_occ zeq l´ x) % nat.
Proof.
induction l; simpl; intros; auto.
destruct (zeq a x); subst.
- erewrite IHl. omega.
- eauto.
Qed.
Lemma QCount_gss_enqueue:
∀ t q,
QCount t q →
InQ t q →
∀ i,
0 ≤ i < num_proc →
∀ s´ c´,
ZMap.get i t = AbTCBValid s´ c´ (-1) →
∀ i´,
0 ≤ i´ < num_chan →
∀ l,
ZMap.get i´ q = AbQValid l →
∀ s c,
QCount (ZMap.set i (AbTCBValid s c i´) t)
(ZMap.set i´ (AbQValid (l ++ (i::nil))) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in ×. inv H6. rewrite ZMap.gss.
refine_split´; eauto.
rewrite count_occ_append. simpl.
assert (HW: count_occ zeq l i = 0%nat).
{
caseEq (count_occ zeq l i); trivial.
intros.
assert (HR: (count_occ zeq l i > 0)%nat) by omega.
eapply count_occ_In in HR.
exploit (H0 i b); eauto.
rewrite H2. intros (? & ? & He). inv He. omega.
}
rewrite HW. rewrite zeq_true; auto.
- rewrite ZMap.gso in H6; auto.
destruct (zeq b i´); subst.
+ rewrite ZMap.gss.
exploit H; eauto. rewrite H4.
intros (? & He & Hr). inv He.
refine_split´; trivial.
rewrite count_occ_append. simpl.
rewrite Hr.
rewrite zeq_false; auto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma QCount_gss_remove:
∀ t q,
QCount t q →
∀ i i´,
0 ≤ i´ < num_chan →
∀ l,
ZMap.get i´ q = AbQValid (i :: l) →
∀ s c,
QCount (ZMap.set i (AbTCBValid s c (-1)) t)
(ZMap.set i´ (AbQValid l) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq b i´); subst.
- rewrite ZMap.gss.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss in ×. inv H3. omega.
+ rewrite ZMap.gso in *; eauto.
refine_split´; eauto.
exploit H; eauto.
rewrite H1. intros (? & He & Hr). inv He.
rewrite count_occ_cons_neq in Hr; auto.
- rewrite ZMap.gso; eauto.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss in ×. inv H3. omega.
+ rewrite ZMap.gso in *; eauto.
Qed.
Lemma QCount_valid:
∀ t q,
QCount t q →
∀ i i´ s´ c´ l,
0 ≤ i < num_proc →
0 ≤ i´ < num_chan →
ZMap.get i t = AbTCBValid s´ c´ i´ →
ZMap.get i´ q = AbQValid l →
In i l.
Proof.
unfold QCount; intros.
exploit H; eauto. rewrite H3.
intros (? & He & Hr). inv He.
assert (Hl: (count_occ zeq x i > 0) % nat) by omega.
eapply count_occ_In in Hl; eauto.
Qed.
Lemma QCount_gss_wakeup´:
∀ t q i i´ l s c s´ c´ b´
(Hcount: QCount t q)
(Hin: InQ t q)
(Hi: 0 ≤ i < num_proc)
(Hi´: 0 ≤ i´ < num_chan)
(Ht: ZMap.get i t = AbTCBValid s´ c´ b´)
(Hb: b´ = -1 )
(Hl: ZMap.get i´ q = AbQValid l),
QCount (ZMap.set i (AbTCBValid s c i´) t)
(ZMap.set i´ (AbQValid (l ++ (i::nil))) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in ×. inv H0. rewrite ZMap.gss.
refine_split´; eauto.
rewrite count_occ_append. simpl.
rewrite zeq_true.
assert (HW: count_occ zeq l i = 0%nat).
{
caseEq (count_occ zeq l i); trivial.
intros.
assert (HR: (count_occ zeq l i > 0)%nat) by omega.
eapply count_occ_In in HR.
exploit (Hin i b); eauto.
rewrite Ht.
intros (s & c & He). inv He. omega.
}
rewrite HW. auto.
- rewrite ZMap.gso in H0; auto.
destruct (zeq b i´); subst.
+ rewrite ZMap.gss.
exploit Hcount; eauto. rewrite Hl.
intros (? & He & Hr). inv He.
refine_split´; trivial.
rewrite count_occ_append. simpl.
rewrite Hr.
rewrite zeq_false; auto.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma rdyq_range:
∀ i
(Hrange: 0≤ i < TOTAL_CPU),
0 ≤ rdy_q_id i < num_chan.
Proof.
unfold rdy_q_id; intros. omega.
Qed.
Lemma QCount_gss_yield´:
∀ t q i i´ l s c s´ c´ s0 c0 cur
(Hcount: QCount t q)
(Hin: InQ t q)
(Hi: 0 ≤ i´ < num_chan)
(Hl: ZMap.get i´ q = AbQValid (i :: l))
(Hcur: 0 ≤ cur < num_proc)
(Ht: ZMap.get cur t = AbTCBValid s´ c´ (-1)),
QCount (ZMap.set i (AbTCBValid s0 c0 (-1))
(ZMap.set cur (AbTCBValid s c i´) t))
(ZMap.set i´ (AbQValid (l ++ (cur::nil))) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss in ×. inv H0. omega.
- rewrite ZMap.gso in H0; auto.
destruct (zeq i0 cur); subst.
+ rewrite ZMap.gss in ×. inv H0.
rewrite ZMap.gss.
refine_split´; eauto.
rewrite count_occ_append. simpl.
rewrite zeq_true.
assert (HW: count_occ zeq l cur = 0%nat).
{
caseEq (count_occ zeq l cur); trivial.
intros.
assert (HR: (count_occ zeq l cur > 0)%nat) by omega.
eapply count_occ_In in HR.
exploit (Hin cur b); eauto.
{ right. trivial. }
rewrite Ht.
intros (s & c & He). inv He. omega.
}
rewrite HW. auto.
+ rewrite ZMap.gso in H0; auto.
destruct (zeq b i´); subst.
× rewrite ZMap.gss.
exploit Hcount; eauto. rewrite Hl.
intros (? & He & Hr). inv He.
refine_split´; trivial.
rewrite count_occ_append. simpl.
rewrite zeq_false; auto.
erewrite count_occ_cons_neq in Hr; auto.
rewrite Hr. omega.
× rewrite ZMap.gso; eauto.
Qed.
End QCOUNT_INV.
Section INQ_INV.
Lemma InQ_gso_state:
∀ t q,
InQ t q →
∀ i,
0 ≤ i < num_proc →
∀ s c b,
ZMap.get i t = AbTCBValid s c b →
∀ s´ c´,
InQ (ZMap.set i (AbTCBValid s´ c´ b) t) q.
Proof.
unfold InQ; intros.
destruct (zeq i0 i); subst.
- rewrite ZMap.gss. exploit H; eauto. rewrite H1.
intros (? & ? & He). inv He. eauto.
- rewrite ZMap.gso; eauto.
Qed.
Lemma InQ_gss_enqueue:
∀ t q,
InQ t q →
∀ i,
0 ≤ i < num_proc →
∀ s´ c´,
ZMap.get i t = AbTCBValid s´ c´ (-1) →
∀ i´,
0 ≤ i´ < num_chan →
∀ l,
ZMap.get i´ q = AbQValid l →
∀ s c,
InQ (ZMap.set i (AbTCBValid s c i´) t)
(ZMap.set i´ (AbQValid (l ++ (i::nil))) q).
Proof.
unfold InQ; intros.
destruct (zeq j i´); subst.
- rewrite ZMap.gss in ×. inv H6.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss.
refine_split´; eauto.
+ rewrite ZMap.gso; auto.
eapply in_app_or in H7.
inv H7.
× eauto.
× inv H6. congruence. inv H7.
- rewrite ZMap.gso in H6; eauto.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss. exploit H; eauto.
rewrite H1. intros (? & ? & He).
inv He. omega.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma InQ_gss_remove:
∀ t q,
InQ t q →
QCount t q →
∀ i i´,
0 ≤ i´ < num_chan →
∀ l,
ZMap.get i´ q = AbQValid (i :: l) →
∀ s c,
InQ (ZMap.set i (AbTCBValid s c (-1)) t)
(ZMap.set i´ (AbQValid l) q).
Proof.
unfold InQ, QCount; intros.
destruct (zeq j i´); subst.
- rewrite ZMap.gss in ×. inv H5.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss.
exploit H; eauto. left; trivial.
intros (s0 & c0 & Heq).
exploit H0; eauto. rewrite H2.
intros (l & Heq´ & Hcount). inv Heq´.
rewrite count_occ_cons_eq in Hcount; trivial.
inv Hcount. eapply (count_occ_In zeq) in H6. omega.
+ rewrite ZMap.gso; auto.
eapply H; eauto. right; trivial.
- rewrite ZMap.gso in H5; eauto.
destruct (zeq i0 i); subst.
+ exploit H; eauto. intros (? & ? & Hr).
exploit (H i i´); eauto. left; trivial. rewrite Hr.
intros (? & He). inv He. congruence.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma InQ_gss_wakeup´:
∀ t q i i´ l s c s´ c´ b´
(Hin: InQ t q)
(Hcount: QCount t q)
(Hi: 0 ≤ i < num_proc)
(Ht: ZMap.get i t = AbTCBValid s´ c´ b´)
(Hb: b´ = -1 )
(Hi´: 0 ≤ i´ < num_chan)
(Hvalid: ZMap.get i´ q = AbQValid l),
InQ (ZMap.set i (AbTCBValid s c i´) t)
(ZMap.set i´ (AbQValid (l ++ i :: nil)) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq j i´); subst.
- rewrite ZMap.gss in ×. inv H1.
destruct (zeq i0 i); subst.
+ rewrite ZMap.gss. eauto.
+ rewrite ZMap.gso; auto.
eapply in_app_or in H2.
destruct H2 as [HP | HP ]; eauto.
inv HP; try congruence. inv H1.
- rewrite ZMap.gso in H1; auto.
destruct (zeq i0 i); subst.
+ exploit Hin; eauto.
rewrite Ht.
intros (s0 & c0 & Heq). inv Heq.
omega.
+ rewrite ZMap.gso; eauto.
Qed.
Lemma InQ_gss_yield´:
∀ t q i i´ l s c s´ c´ s0 c0 cur
(Hcount: QCount t q)
(Hin: InQ t q)
(Hi: 0 ≤ i´ < num_chan)
(Hl: ZMap.get i´ q = AbQValid (i :: l))
(Hcur: 0 ≤ cur < num_proc)
(Ht: ZMap.get cur t = AbTCBValid s´ c´ (-1)),
InQ (ZMap.set i (AbTCBValid s0 c0 (-1))
(ZMap.set cur (AbTCBValid s c i´) t))
(ZMap.set i´ (AbQValid (l ++ (cur::nil))) q).
Proof.
unfold QCount, InQ; intros.
destruct (zeq j i´); subst.
- rewrite ZMap.gss in ×. inv H1.
destruct (zeq i0 i); subst.
+ eapply in_app_iff in H2.
exploit Hin; eauto.
{ left; trivial. }
intros (s1 & c1 & Hi´).
destruct H2 as [HP | HP ]; eauto.
× exploit Hcount; eauto.
rewrite Hl.
intros (l0 & He & HF). inv He.
rewrite count_occ_cons_eq in HF; trivial.
eapply (count_occ_In zeq) in HP. omega.
× inv HP.
{
rewrite Hi´ in Ht. inv Ht. omega.
}
{ inv H1. }
+ rewrite ZMap.gso; auto.
destruct (zeq i0 cur); subst.
× rewrite ZMap.gss; eauto.
× eapply in_app_or in H2.
destruct H2 as [HP | HP ]; eauto.
{
exploit Hin; eauto.
{ right; trivial. }
intros (s1 & c1 & Hi0).
rewrite ZMap.gso; eauto.
}
{
inv HP; try congruence. inv H1.
}
- rewrite ZMap.gso in H1; auto.
destruct (zeq i0 i); subst.
+ exploit Hin; eauto.
intros (s1 & c1 & Ht´).
exploit (Hin i); try eapply Hl; eauto.
{ left; trivial. }
rewrite Ht´. intros (s2 & c2 & Heq). inv Heq. congruence.
+ rewrite ZMap.gso; eauto.
destruct (zeq i0 cur); subst.
× exploit Hin; eauto.
rewrite Ht. intros (s1 & c1 & Heq).
inv Heq. omega.
× rewrite ZMap.gso; eauto.
Qed.
End INQ_INV.
End THREAD_INV.
Section CID_INV.
Local Open Scope Z_scope.
End CID_INV.