Library mcertikos.clib.CalRealProcModule
Require Export AuxStateDataType.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CLemmas.
Section INITZMAP.
Fixpoint init_zmap_nat {A} (n: nat) (x: A) (f: ZMap.t A): ZMap.t A :=
match n with
| O ⇒ f
| S i ⇒ ZMap.set (Z.of_nat i) x (init_zmap_nat i x f)
end.
Lemma init_zmap_nat_inside {A} (n: nat) (x: A) (f: ZMap.t A) (i: Z):
0 ≤ i < (Z.of_nat n) →
ZMap.get i (init_zmap_nat n x f) = x.
Proof.
induction n; intros.
× rewrite Nat2Z.inj_0 in H.
omega.
× simpl.
destruct (Z.eq_dec i (Z.of_nat n)) as [Hi | Hi].
+ rewrite <- Hi.
rewrite ZMap.gss.
reflexivity.
+ rewrite ZMap.gso.
- apply IHn.
rewrite Nat2Z.inj_succ in H.
omega.
- assumption.
Qed.
Definition init_zmap {A} (n: Z): A → ZMap.t A → ZMap.t A :=
init_zmap_nat (Z.to_nat n).
Lemma init_zmap_inside {A} (n: Z) (x: A) (f: ZMap.t A) (i: Z):
0 ≤ i < n →
ZMap.get i (init_zmap n x f) = x.
Proof.
intros H.
unfold init_zmap.
apply init_zmap_nat_inside.
rewrite Z2Nat.id; omega.
Qed.
Lemma init_zmap_eq {A} (i: Z) (x: A) (f: ZMap.t A):
0 ≤ i →
init_zmap (i+1) x f = ZMap.set i x (init_zmap i x f).
Proof.
intro Hi.
unfold init_zmap.
change (i + 1) with (Z.succ i).
rewrite Z2Nat.inj_succ by assumption.
simpl.
rewrite Z2Nat.id by assumption.
reflexivity.
Qed.
End INITZMAP.
Section CInitSpecsPThreadIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_tcb: TCBPool → TCBPool :=
init_zmap num_proc (TCBValid DEAD 0 num_proc num_proc).
Lemma real_TCB_valid: ∀ tcb, TCBCorrect_range (real_tcb tcb).
Proof.
unfold TCBCorrect_range.
unfold TCBCorrect.
intros.
unfold real_tcb.
rewrite init_zmap_inside by assumption.
∃ DEAD.
∃ 0.
∃ num_proc.
∃ num_proc.
split.
tauto.
omega.
Qed.
Lemma real_TCB_init: ∀ tcb, TCBInit (real_tcb tcb).
Proof.
unfold TCBInit.
intros.
unfold real_tcb.
rewrite init_zmap_inside by assumption.
reflexivity.
Qed.
End CInitSpecsPThreadIntro.
Section CInitSpecsPQueueIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_tdq: TDQueuePool → TDQueuePool :=
init_zmap num_chan (TDQValid num_proc num_proc).
Lemma real_tdq_valid: ∀ tdq, TDQInit (real_tdq tdq).
Proof.
unfold TDQInit.
intros.
unfold real_tdq.
rewrite init_zmap_inside by omega.
reflexivity.
Qed.
Lemma real_TDQ_correct:
∀ t,
TDQCorrect_range (real_tdq t).
Proof.
intros. specialize (real_tdq_valid t).
unfold TDQInit, TDQCorrect_range, TDQCorrect.
intros. specialize (H _ H0).
esplit; esplit. split; eauto.
split; omega.
Qed.
End CInitSpecsPQueueIntro.
Section CInitSpecsAbPThreadIntro.
Definition real_abtcb :=
init_zmap num_proc (AbTCBValid DEAD 0 (-1)).
Lemma real_abtcb_init abtcb:
AbTCBInit (real_abtcb abtcb).
Proof.
intros i.
apply init_zmap_inside.
Qed.
Lemma real_abtcb_valid:
∀ tcbp i,
0 ≤ i < num_proc →
AbTCBCorrect (ZMap.get i (real_abtcb tcbp)).
Proof.
intros; eapply AbTCBInit_valid; eauto.
apply real_abtcb_init.
Qed.
Lemma real_abtcb_range:
∀ tcbp,
AbTCBCorrect_range (real_abtcb tcbp).
Proof.
unfold AbTCBCorrect_range; intros.
eapply real_abtcb_valid; eauto.
Qed.
Lemma real_abtcb_notInQ:
∀ tcbp i s c b,
0 ≤ i < num_proc →
ZMap.get i (real_abtcb tcbp) = AbTCBValid s c b →
b = -1.
Proof.
intros; eapply AbTCBInit_notInQ; eauto.
apply real_abtcb_init.
Qed.
Lemma real_abtcb_pb_notInQ:
∀ tcbp pb,
NotInQ pb (real_abtcb tcbp).
Proof.
unfold NotInQ; intros.
eapply real_abtcb_notInQ; eauto.
Qed.
Lemma real_abtcb_valid´:
∀ tcbp i c,
0 ≤ i < num_proc →
AbTCBCorrect (ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp))).
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss. unfold AbTCBCorrect.
esplit. esplit. esplit. split; eauto.
+
rewrite ZMap.gso; auto.
eapply real_abtcb_valid; eauto.
Qed.
Lemma real_abtcb_range´:
∀ tcbp c,
AbTCBCorrect_range (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold AbTCBCorrect_range; intros.
eapply real_abtcb_valid´; eauto.
Qed.
Lemma real_abtcb_notInQ´:
∀ tcbp i s c c´ b,
0 ≤ i < num_proc →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ b →
b = -1.
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss in ×. inv H0. trivial.
+
rewrite ZMap.gso in *; auto.
eapply real_abtcb_notInQ; eauto.
Qed.
Lemma real_abtcb_pb_notInQ´:
∀ tcbp pb c,
NotInQ pb (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold NotInQ; intros.
eapply real_abtcb_notInQ´; eauto.
Qed.
Lemma real_abtcb_notRun:
∀ tcbp i s c c´ b,
0 ≤ i < num_proc →
i ≠ 0 →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ b →
s ≠ RUN.
Proof.
intros. rewrite ZMap.gso in *; auto.
specialize (real_abtcb_init tcbp).
unfold AbTCBInit. intros. specialize (H2 _ H).
rewrite H1 in H2. inv H2. red; intros; inv H2.
Qed.
Lemma real_abtcb_strong:
∀ tcbp i,
0 ≤ i < num_proc →
AbTCBStrong (ZMap.get i (real_abtcb tcbp)).
Proof.
intros. specialize(real_abtcb_init tcbp).
unfold AbTCBInit, AbTCBStrong; intros.
specialize (H0 _ H). rewrite H0.
esplit. esplit. esplit. split; eauto.
split; trivial.
split; intros HF; inv HF; discriminate.
Qed.
Lemma real_abtcb_strong_range:
∀ tcbp,
AbTCBStrong_range (real_abtcb tcbp).
Proof.
unfold AbTCBStrong_range. intros.
eapply real_abtcb_strong; eauto.
Qed.
Lemma real_abtcb_strong´:
∀ tcbp i c,
0 ≤ i < num_proc →
AbTCBStrong (ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp))).
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss. unfold AbTCBStrong.
esplit. esplit. esplit. split; eauto.
split; trivial.
split; intros HF; inv HF; discriminate.
+
rewrite ZMap.gso; auto.
eapply real_abtcb_strong; eauto.
Qed.
Lemma real_abtcb_strong_range´:
∀ tcbp c,
AbTCBStrong_range (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold AbTCBStrong_range. intros.
eapply real_abtcb_strong´; eauto.
Qed.
End CInitSpecsAbPThreadIntro.
Section CInitSpecsAbPQueueIntro.
Definition real_abq :=
init_zmap (num_chan + 1) (AbQValid nil).
Lemma real_abq_init abq:
AbQInit (real_abq abq).
Proof.
intros i Hi.
apply init_zmap_inside.
omega.
Qed.
Lemma real_abq_valid:
∀ tdqp i,
0 ≤ i < num_chan →
AbQCorrect (ZMap.get i (real_abq tdqp)).
Proof.
intros; eapply AbTDQInit_valid; eauto.
apply real_abq_init; eauto.
Qed.
Lemma real_abq_range:
∀ tdqp,
AbQCorrect_range (real_abq tdqp).
Proof.
unfold AbQCorrect_range; intros.
eapply real_abq_valid; eauto.
Qed.
Lemma real_abq_contra:
∀ tdqp l i j,
0 ≤ j < num_chan →
ZMap.get j (real_abq tdqp) = AbQValid l →
In i l →
False.
Proof.
intros. specialize (real_abq_init tdqp).
unfold AbQInit. intros HTDQ. specialize (HTDQ _ H).
rewrite H0 in HTDQ; inv HTDQ. inv H1.
Qed.
Lemma real_abtcb_abq_valid:
∀ i j tcbp tdqp s c,
0 ≤ i < num_proc →
0 ≤ j < num_chan →
ZMap.get i (real_abtcb tcbp) = AbTCBValid s c j →
∃ l, ZMap.get j (real_abq tdqp) = AbQValid l
∧ count_occ zeq l i = 1%nat.
Proof.
intros. specialize (real_abtcb_init tcbp).
unfold AbTCBInit. intros HTCB.
specialize (HTCB _ H).
rewrite H1 in HTCB. inv HTCB. omega.
Qed.
Lemma real_abtcb_abq_QCount:
∀ tcbp tdqp,
QCount (real_abtcb tcbp) (real_abq tdqp).
Proof.
unfold QCount; intros.
eapply real_abtcb_abq_valid; eauto.
Qed.
Lemma real_abtcb_abq_valid´:
∀ i j tcbp tdqp s c c´,
0 ≤ i < num_proc →
0 ≤ j < num_chan →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ j →
∃ l, ZMap.get j (real_abq tdqp) = AbQValid l
∧ count_occ zeq l i = 1%nat.
Proof.
intros. destruct (zeq i 0); subst.
+ rewrite ZMap.gss in ×. inv H1. omega.
+ rewrite ZMap.gso in *; auto.
eapply real_abtcb_abq_valid; eauto.
Qed.
Lemma real_abtcb_abq_QCount´:
∀ tcbp tdqp c,
QCount (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) (real_abq tdqp).
Proof.
unfold QCount; intros.
eapply real_abtcb_abq_valid´; eauto.
Qed.
Lemma real_abq_inQ:
∀ tdqp l i j tcbp,
0 ≤ j < num_chan →
ZMap.get j (real_abq tdqp) = AbQValid l →
In i l →
∃ s c, ZMap.get i tcbp = AbTCBValid s c j.
Proof.
intros. exploit real_abq_contra; eauto.
intros HF; inv HF.
Qed.
Lemma real_abq_tcb_inQ:
∀ tcbp tdqp,
InQ tcbp (real_abq tdqp).
Proof.
unfold InQ; intros.
exploit real_abq_contra; eauto.
intros HF; inv HF.
Qed.
End CInitSpecsAbPQueueIntro.
Section CInitSpecsThreadSched.
Context `{real_params_ops : RealParamsOps}.
Fixpoint Calculate_cidpool (i: nat) (cidpool: ZMap.t Z) : ZMap.t Z :=
match i with
| O ⇒ ZMap.set 0 1 cidpool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Z.of_nat (S k) + 1) (Calculate_cidpool k cidpool)
end.
Definition real_cidpool (cidpool: ZMap.t Z) : ZMap.t Z :=
Calculate_cidpool (Z.to_nat (TOTAL_CPU - 1)) cidpool.
Lemma real_cidpool_valid:
∀ cidpool i n,
0 ≤ i ≤ Z.of_nat n →
ZMap.get i (Calculate_cidpool n cidpool) = i + 1.
Proof.
induction n; intros irange; simpl.
- rewrite Nat2Z.inj_0 in irange.
replace i with 0 by omega.
rewrite ZMap.gss.
omega.
- simpl in irange.
rewrite Pos2Z.inj_add.
rewrite Zpos_P_of_succ_nat in ×.
unfold Z.succ in ×.
case_eq (zeq i (Z.of_nat n + 1)); intros; subst.
+ rewrite ZMap.gss.
reflexivity.
+ rewrite ZMap.gso; try auto.
apply IHn; omega.
Qed.
Lemma real_valid_cidpool:
∀ i cidpool,
0 ≤ i < TOTAL_CPU →
ZMap.get i (real_cidpool cidpool) = i + 1.
Proof.
unfold real_cidpool; intros i cidpool irange.
assert (range´: 8 ≥ 0) by omega.
rewrite <- (nat_of_Z_eq _ range´).
rewrite Z2Nat.id by omega.
eapply real_cidpool_valid.
rewrite Z2Nat.id; omega.
Qed.
End CInitSpecsThreadSched.
Section CInitSpecsPIPCIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_syncchpool: SyncChanPool → SyncChanPool :=
init_zmap num_chan (SyncChanValid (Int.repr num_chan) Int.zero Int.zero Int.zero).
Lemma real_syncchpool_valid:
∀ syncchpool, SyncChanPool_Init (real_syncchpool syncchpool).
Proof.
generalize max_unsigned_val; intros muval.
unfold SyncChanPool_Init.
unfold SyncChannel_Init.
intros.
unfold real_syncchpool.
rewrite init_zmap_inside by omega.
reflexivity.
Qed.
Lemma real_syncchpool_valid´:
∀ syncchpool, SyncChanPool_Valid (real_syncchpool syncchpool).
Proof.
intros. apply SyncChannel_Init_Correct.
apply real_syncchpool_valid.
Qed.
End CInitSpecsPIPCIntro.
Require Import Constant.
Require Import Coqlib.
Require Import Maps.
Require Import Integers.
Require Import XOmega.
Require Import CLemmas.
Section INITZMAP.
Fixpoint init_zmap_nat {A} (n: nat) (x: A) (f: ZMap.t A): ZMap.t A :=
match n with
| O ⇒ f
| S i ⇒ ZMap.set (Z.of_nat i) x (init_zmap_nat i x f)
end.
Lemma init_zmap_nat_inside {A} (n: nat) (x: A) (f: ZMap.t A) (i: Z):
0 ≤ i < (Z.of_nat n) →
ZMap.get i (init_zmap_nat n x f) = x.
Proof.
induction n; intros.
× rewrite Nat2Z.inj_0 in H.
omega.
× simpl.
destruct (Z.eq_dec i (Z.of_nat n)) as [Hi | Hi].
+ rewrite <- Hi.
rewrite ZMap.gss.
reflexivity.
+ rewrite ZMap.gso.
- apply IHn.
rewrite Nat2Z.inj_succ in H.
omega.
- assumption.
Qed.
Definition init_zmap {A} (n: Z): A → ZMap.t A → ZMap.t A :=
init_zmap_nat (Z.to_nat n).
Lemma init_zmap_inside {A} (n: Z) (x: A) (f: ZMap.t A) (i: Z):
0 ≤ i < n →
ZMap.get i (init_zmap n x f) = x.
Proof.
intros H.
unfold init_zmap.
apply init_zmap_nat_inside.
rewrite Z2Nat.id; omega.
Qed.
Lemma init_zmap_eq {A} (i: Z) (x: A) (f: ZMap.t A):
0 ≤ i →
init_zmap (i+1) x f = ZMap.set i x (init_zmap i x f).
Proof.
intro Hi.
unfold init_zmap.
change (i + 1) with (Z.succ i).
rewrite Z2Nat.inj_succ by assumption.
simpl.
rewrite Z2Nat.id by assumption.
reflexivity.
Qed.
End INITZMAP.
Section CInitSpecsPThreadIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_tcb: TCBPool → TCBPool :=
init_zmap num_proc (TCBValid DEAD 0 num_proc num_proc).
Lemma real_TCB_valid: ∀ tcb, TCBCorrect_range (real_tcb tcb).
Proof.
unfold TCBCorrect_range.
unfold TCBCorrect.
intros.
unfold real_tcb.
rewrite init_zmap_inside by assumption.
∃ DEAD.
∃ 0.
∃ num_proc.
∃ num_proc.
split.
tauto.
omega.
Qed.
Lemma real_TCB_init: ∀ tcb, TCBInit (real_tcb tcb).
Proof.
unfold TCBInit.
intros.
unfold real_tcb.
rewrite init_zmap_inside by assumption.
reflexivity.
Qed.
End CInitSpecsPThreadIntro.
Section CInitSpecsPQueueIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_tdq: TDQueuePool → TDQueuePool :=
init_zmap num_chan (TDQValid num_proc num_proc).
Lemma real_tdq_valid: ∀ tdq, TDQInit (real_tdq tdq).
Proof.
unfold TDQInit.
intros.
unfold real_tdq.
rewrite init_zmap_inside by omega.
reflexivity.
Qed.
Lemma real_TDQ_correct:
∀ t,
TDQCorrect_range (real_tdq t).
Proof.
intros. specialize (real_tdq_valid t).
unfold TDQInit, TDQCorrect_range, TDQCorrect.
intros. specialize (H _ H0).
esplit; esplit. split; eauto.
split; omega.
Qed.
End CInitSpecsPQueueIntro.
Section CInitSpecsAbPThreadIntro.
Definition real_abtcb :=
init_zmap num_proc (AbTCBValid DEAD 0 (-1)).
Lemma real_abtcb_init abtcb:
AbTCBInit (real_abtcb abtcb).
Proof.
intros i.
apply init_zmap_inside.
Qed.
Lemma real_abtcb_valid:
∀ tcbp i,
0 ≤ i < num_proc →
AbTCBCorrect (ZMap.get i (real_abtcb tcbp)).
Proof.
intros; eapply AbTCBInit_valid; eauto.
apply real_abtcb_init.
Qed.
Lemma real_abtcb_range:
∀ tcbp,
AbTCBCorrect_range (real_abtcb tcbp).
Proof.
unfold AbTCBCorrect_range; intros.
eapply real_abtcb_valid; eauto.
Qed.
Lemma real_abtcb_notInQ:
∀ tcbp i s c b,
0 ≤ i < num_proc →
ZMap.get i (real_abtcb tcbp) = AbTCBValid s c b →
b = -1.
Proof.
intros; eapply AbTCBInit_notInQ; eauto.
apply real_abtcb_init.
Qed.
Lemma real_abtcb_pb_notInQ:
∀ tcbp pb,
NotInQ pb (real_abtcb tcbp).
Proof.
unfold NotInQ; intros.
eapply real_abtcb_notInQ; eauto.
Qed.
Lemma real_abtcb_valid´:
∀ tcbp i c,
0 ≤ i < num_proc →
AbTCBCorrect (ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp))).
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss. unfold AbTCBCorrect.
esplit. esplit. esplit. split; eauto.
+
rewrite ZMap.gso; auto.
eapply real_abtcb_valid; eauto.
Qed.
Lemma real_abtcb_range´:
∀ tcbp c,
AbTCBCorrect_range (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold AbTCBCorrect_range; intros.
eapply real_abtcb_valid´; eauto.
Qed.
Lemma real_abtcb_notInQ´:
∀ tcbp i s c c´ b,
0 ≤ i < num_proc →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ b →
b = -1.
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss in ×. inv H0. trivial.
+
rewrite ZMap.gso in *; auto.
eapply real_abtcb_notInQ; eauto.
Qed.
Lemma real_abtcb_pb_notInQ´:
∀ tcbp pb c,
NotInQ pb (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold NotInQ; intros.
eapply real_abtcb_notInQ´; eauto.
Qed.
Lemma real_abtcb_notRun:
∀ tcbp i s c c´ b,
0 ≤ i < num_proc →
i ≠ 0 →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ b →
s ≠ RUN.
Proof.
intros. rewrite ZMap.gso in *; auto.
specialize (real_abtcb_init tcbp).
unfold AbTCBInit. intros. specialize (H2 _ H).
rewrite H1 in H2. inv H2. red; intros; inv H2.
Qed.
Lemma real_abtcb_strong:
∀ tcbp i,
0 ≤ i < num_proc →
AbTCBStrong (ZMap.get i (real_abtcb tcbp)).
Proof.
intros. specialize(real_abtcb_init tcbp).
unfold AbTCBInit, AbTCBStrong; intros.
specialize (H0 _ H). rewrite H0.
esplit. esplit. esplit. split; eauto.
split; trivial.
split; intros HF; inv HF; discriminate.
Qed.
Lemma real_abtcb_strong_range:
∀ tcbp,
AbTCBStrong_range (real_abtcb tcbp).
Proof.
unfold AbTCBStrong_range. intros.
eapply real_abtcb_strong; eauto.
Qed.
Lemma real_abtcb_strong´:
∀ tcbp i c,
0 ≤ i < num_proc →
AbTCBStrong (ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp))).
Proof.
intros. destruct (zeq i 0); subst.
+
rewrite ZMap.gss. unfold AbTCBStrong.
esplit. esplit. esplit. split; eauto.
split; trivial.
split; intros HF; inv HF; discriminate.
+
rewrite ZMap.gso; auto.
eapply real_abtcb_strong; eauto.
Qed.
Lemma real_abtcb_strong_range´:
∀ tcbp c,
AbTCBStrong_range (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)).
Proof.
unfold AbTCBStrong_range. intros.
eapply real_abtcb_strong´; eauto.
Qed.
End CInitSpecsAbPThreadIntro.
Section CInitSpecsAbPQueueIntro.
Definition real_abq :=
init_zmap (num_chan + 1) (AbQValid nil).
Lemma real_abq_init abq:
AbQInit (real_abq abq).
Proof.
intros i Hi.
apply init_zmap_inside.
omega.
Qed.
Lemma real_abq_valid:
∀ tdqp i,
0 ≤ i < num_chan →
AbQCorrect (ZMap.get i (real_abq tdqp)).
Proof.
intros; eapply AbTDQInit_valid; eauto.
apply real_abq_init; eauto.
Qed.
Lemma real_abq_range:
∀ tdqp,
AbQCorrect_range (real_abq tdqp).
Proof.
unfold AbQCorrect_range; intros.
eapply real_abq_valid; eauto.
Qed.
Lemma real_abq_contra:
∀ tdqp l i j,
0 ≤ j < num_chan →
ZMap.get j (real_abq tdqp) = AbQValid l →
In i l →
False.
Proof.
intros. specialize (real_abq_init tdqp).
unfold AbQInit. intros HTDQ. specialize (HTDQ _ H).
rewrite H0 in HTDQ; inv HTDQ. inv H1.
Qed.
Lemma real_abtcb_abq_valid:
∀ i j tcbp tdqp s c,
0 ≤ i < num_proc →
0 ≤ j < num_chan →
ZMap.get i (real_abtcb tcbp) = AbTCBValid s c j →
∃ l, ZMap.get j (real_abq tdqp) = AbQValid l
∧ count_occ zeq l i = 1%nat.
Proof.
intros. specialize (real_abtcb_init tcbp).
unfold AbTCBInit. intros HTCB.
specialize (HTCB _ H).
rewrite H1 in HTCB. inv HTCB. omega.
Qed.
Lemma real_abtcb_abq_QCount:
∀ tcbp tdqp,
QCount (real_abtcb tcbp) (real_abq tdqp).
Proof.
unfold QCount; intros.
eapply real_abtcb_abq_valid; eauto.
Qed.
Lemma real_abtcb_abq_valid´:
∀ i j tcbp tdqp s c c´,
0 ≤ i < num_proc →
0 ≤ j < num_chan →
ZMap.get i (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) = AbTCBValid s c´ j →
∃ l, ZMap.get j (real_abq tdqp) = AbQValid l
∧ count_occ zeq l i = 1%nat.
Proof.
intros. destruct (zeq i 0); subst.
+ rewrite ZMap.gss in ×. inv H1. omega.
+ rewrite ZMap.gso in *; auto.
eapply real_abtcb_abq_valid; eauto.
Qed.
Lemma real_abtcb_abq_QCount´:
∀ tcbp tdqp c,
QCount (ZMap.set 0 (AbTCBValid RUN c (-1)) (real_abtcb tcbp)) (real_abq tdqp).
Proof.
unfold QCount; intros.
eapply real_abtcb_abq_valid´; eauto.
Qed.
Lemma real_abq_inQ:
∀ tdqp l i j tcbp,
0 ≤ j < num_chan →
ZMap.get j (real_abq tdqp) = AbQValid l →
In i l →
∃ s c, ZMap.get i tcbp = AbTCBValid s c j.
Proof.
intros. exploit real_abq_contra; eauto.
intros HF; inv HF.
Qed.
Lemma real_abq_tcb_inQ:
∀ tcbp tdqp,
InQ tcbp (real_abq tdqp).
Proof.
unfold InQ; intros.
exploit real_abq_contra; eauto.
intros HF; inv HF.
Qed.
End CInitSpecsAbPQueueIntro.
Section CInitSpecsThreadSched.
Context `{real_params_ops : RealParamsOps}.
Fixpoint Calculate_cidpool (i: nat) (cidpool: ZMap.t Z) : ZMap.t Z :=
match i with
| O ⇒ ZMap.set 0 1 cidpool
| S k ⇒ ZMap.set (Z.of_nat (S k)) (Z.of_nat (S k) + 1) (Calculate_cidpool k cidpool)
end.
Definition real_cidpool (cidpool: ZMap.t Z) : ZMap.t Z :=
Calculate_cidpool (Z.to_nat (TOTAL_CPU - 1)) cidpool.
Lemma real_cidpool_valid:
∀ cidpool i n,
0 ≤ i ≤ Z.of_nat n →
ZMap.get i (Calculate_cidpool n cidpool) = i + 1.
Proof.
induction n; intros irange; simpl.
- rewrite Nat2Z.inj_0 in irange.
replace i with 0 by omega.
rewrite ZMap.gss.
omega.
- simpl in irange.
rewrite Pos2Z.inj_add.
rewrite Zpos_P_of_succ_nat in ×.
unfold Z.succ in ×.
case_eq (zeq i (Z.of_nat n + 1)); intros; subst.
+ rewrite ZMap.gss.
reflexivity.
+ rewrite ZMap.gso; try auto.
apply IHn; omega.
Qed.
Lemma real_valid_cidpool:
∀ i cidpool,
0 ≤ i < TOTAL_CPU →
ZMap.get i (real_cidpool cidpool) = i + 1.
Proof.
unfold real_cidpool; intros i cidpool irange.
assert (range´: 8 ≥ 0) by omega.
rewrite <- (nat_of_Z_eq _ range´).
rewrite Z2Nat.id by omega.
eapply real_cidpool_valid.
rewrite Z2Nat.id; omega.
Qed.
End CInitSpecsThreadSched.
Section CInitSpecsPIPCIntro.
Context `{real_params_ops : RealParamsOps}.
Definition real_syncchpool: SyncChanPool → SyncChanPool :=
init_zmap num_chan (SyncChanValid (Int.repr num_chan) Int.zero Int.zero Int.zero).
Lemma real_syncchpool_valid:
∀ syncchpool, SyncChanPool_Init (real_syncchpool syncchpool).
Proof.
generalize max_unsigned_val; intros muval.
unfold SyncChanPool_Init.
unfold SyncChannel_Init.
intros.
unfold real_syncchpool.
rewrite init_zmap_inside by omega.
reflexivity.
Qed.
Lemma real_syncchpool_valid´:
∀ syncchpool, SyncChanPool_Valid (real_syncchpool syncchpool).
Proof.
intros. apply SyncChannel_Init_Correct.
apply real_syncchpool_valid.
Qed.
End CInitSpecsPIPCIntro.