Library mcertikos.invariants.INVLemmaThreadContainer
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import Constant.
Require Import XOmega.
Require Import AbstractDataType.
Require Import ObjContainer.
Require Import Integers.
Inductive Thread_Container_valid (C : ContainerPool) : Prop :=
mkContainer_valid {
cvalid_id : ∀ i, cused (ZMap.get i C) = true → 0 ≤ i < num_proc;
cvalid_quota : ∀ i,
cquota (ZMap.get i C) ≤ Int.max_unsigned;
cvalid_usage : ∀ i,
0 ≤ cusage (ZMap.get i C) ≤ cquota (ZMap.get i C)
}.
Lemma thread_empty_container_valid : Thread_Container_valid (ZMap.init Container_unused).
Proof.
constructor; simpl; intros; try rewrite ZMap.gi in *; simpl; auto; try discriminate.
omega.
Qed.
Ltac container_destruct_case_eq i :=
case_eq (zeq i 0); intros; subst;
[ | case_eq (zeq i 1); intros; subst;
[ | case_eq (zeq i 2); intros; subst;
[ | case_eq (zeq i 3); intros; subst;
[ | case_eq (zeq i 4); intros; subst;
[ | case_eq (zeq i 5); intros; subst;
[ | case_eq (zeq i 6); intros; subst;
[ | case_eq (zeq i 7); intros; subst;
[ | case_eq (zeq i 8); intros; subst]]]]]]]].
Lemma thread_AC_init_real_container_valid: Thread_Container_valid init_real_container.
Proof.
unfold init_real_container; simpl.
constructor; simpl.
- intros.
container_destruct_case_eq i; try omega.
do 9 (rewrite ZMap.gso in H; try assumption).
rewrite ZMap.gi in H; simpl in H; inv H.
- intros.
assert (720896/8 = 90112) by xomega.
assert (Integers.Int.max_unsigned = 4294967295).
{ unfold Integers.Int.max_unsigned; simpl; reflexivity. }
container_destruct_case_eq i.
+ do 8 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 7 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 6 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 5 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 4 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 3 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 2 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 1 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ rewrite ZMap.gss; simpl in *; omega.
+ do 9 (rewrite ZMap.gso; [ | assumption]).
rewrite ZMap.gi; simpl; omega.
- intros.
assert (720896/8 = 90112) by xomega.
container_destruct_case_eq i.
+ do 8 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 7 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 6 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 5 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 4 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 3 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 2 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ do 1 (rewrite ZMap.gso; [ | intros contra; inv contra]).
rewrite ZMap.gss; simpl in *; omega.
+ rewrite ZMap.gss; simpl in *; omega.
+ do 9 (rewrite ZMap.gso; [ | assumption]).
rewrite ZMap.gi; simpl; omega.
Qed.
Lemma thread_AC_init_container_valid : Thread_Container_valid AC_init.
Proof.
unfold AC_init; simpl.
generalize thread_AC_init_real_container_valid; intros; auto.
Qed.
Lemma alloc_thread_container_valid´:
∀ i (ac: ContainerPool),
let c := ZMap.get i ac in
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
Thread_Container_valid ac →
(cusage c <? cquota c) = true →
Thread_Container_valid (ZMap.set i cur ac).
Proof.
intros. destruct H.
econstructor; eauto 1; simpl; intros.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in H; auto.
rewrite ZMap.gso in H; auto.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in *; simpl.
apply cvalid_quota; auto.
constructor; eauto.
rewrite ZMap.gso; auto.
-
destruct (zeq i0 i); subst.
rewrite ZMap.gss in *; simpl.
rewrite Z.ltb_lt in H0.
specialize (cvalid_usage0 i); subst c; omega.
rewrite ZMap.gso; auto.
Qed.
Lemma alloc_thread_container_valid i adt adt´ z :
Thread_Container_valid (AC adt) →
container_alloc_spec i adt = Some (adt´,z) →
Thread_Container_valid (AC adt´).
Proof.
intros. functional inversion H0.
eapply alloc_thread_container_valid´; eauto.
subst. assumption.
Qed.
Lemma math_false_aux:
∀ id n,
id × max_children + 1 + n = 0 →
0 ≤ id < num_proc →
0 ≤ n →
False.
Proof.
clear.
intros. omega.
Qed.
Lemma split_thread_container_valid:
∀ id q ac
(Hvalid: Thread_Container_valid ac),
let c := ZMap.get id ac in
let i := id × max_children + 1 + Z.of_nat (length (cchildren c)) in
let cur := {|
cquota := cquota c;
cusage := cusage c + q;
cparent := cparent c;
cchildren := i :: cchildren c;
cused := cused c |} in
∀ (Hrangei: 0 ≤ i < num_proc)
(Hrangeq: 0 ≤ q ≤ (cquota c - cusage c)),
Thread_Container_valid (ZMap.set id cur ac).
Proof.
intros. inv Hvalid. subst c.
constructor; simpl; intros;
rename i0 into i´; [rename H into Hused´ | | ].
-
destruct (zeq i´ id); try subst i´.
+ rewrite ZMap.gss in Hused´.
unfold cur in Hused´.
eapply cvalid_id0; eauto.
+ rewrite ZMap.gso in Hused´; auto.
-
destruct (zeq i´ id); try subst i´.
+ rewrite ZMap.gss; simpl; try omega.
apply cvalid_quota0.
+ rewrite ZMap.gso; auto.
-
destruct (zeq i´ id); try subst i´.
× rewrite ZMap.gss; simpl; split; try omega.
apply Z.add_nonneg_nonneg; auto; try omega.
apply cvalid_usage; auto; constructor; eauto.
× rewrite ZMap.gso; auto.
Qed.