Library OSTimeTickPure
Require Import ucert.
Require Import mathlib.
Require Import OSQPostPure.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.ProofIrrelevanceFacts.
Import TcbMod.
Ltac hoare_ex_intro´ :=
repeat
match goal with
| |- {|_ , _, _, _ , _|}|- {{EX _, _}}_ {{_}} => apply ex_intro_rule; intros
end.
Ltac hoare_split_pure_all´´ :=
hoare normal pre; hoare_ex_intro´; hoare_split_pure_all´.
Ltac pure_intro´ :=
hoare_split_pure_all´´; isptr_intro; array_leneq_intro; hoare_split_pure_all;
mytac; struct_type_vallist_match_elim; simpl_field_eq.
Ltac xunfold´ H:=
let M:= fresh in
match type of H with
| match ?X with
| _ => _
end = Some _ => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xunfold´´ H:=
let M:= fresh in
match type of H with
| Some _ = match ?X with
| _ => _
end => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xunfold´´´´ H:=
match type of H with
| (Some ?p) = _
=> destruct p as [[[]]]
| _ => idtac
end.
Ltac xunfold´´´ H:=
let M:= fresh in
match type of H with
| match ?X with
| _ => _
end = Some _ => remember X as M eqn:Htick;destruct M;tryfalse;auto;xunfold´´´´ Htick;inverts H
| _ => idtac
end.
Ltac xunfold H :=
repeat (xunfold´ H);
subst;
simpl in *;unfold add_option_first in H;(xunfold´´´ H).
Ltac xxunfold´:=
match goal with
| |- match ?X with
| _ => _
end = Some _ => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xxunfold´´ :=
match goal with
| |- Some _ = match ?X with
| _ => _
end => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xxunfold´´´ :=
match goal with
| |- match ?X with
| _ => _
end = Some _ => remember X as M eqn:Htick;destruct M;tryfalse;auto;xunfold´´´´ Htick
| _ => idtac
end.
Ltac xxunfold :=
repeat (xxunfold´);
subst;
simpl in *;unfold add_option_first;(xxunfold´´´).
Ltac inverts_all´ :=
match goal with
| H: Some _ = Some _ |- _ => inverts H
end.
Ltac inverts_all:= repeat inverts_all´.
Ltac mytac_1´ :=
match goal with
| H:exists _, _ |- _ => destruct H; mytac_1´
| H:_ /\ _ |- _ => destruct H; mytac_1´
| _ => try (progress subst; mytac_1´)
end.
Ltac mytac´ := repeat progress mytac_1´.
Fixpoint get_ectr (eid:val) (head:val) (ectrl:list EventCtr) :=
match eid,head,ectrl with
| (Vptr e),(Vptr e´),(osevent, etbl)::vll =>
match beq_addrval e e´ with
| true => Some (osevent,etbl)
| false => match V_OSEventListPtr osevent with
| Some vn => get_ectr eid vn vll
| _ => None
end
end
| _,_,_ => None
end.
Lemma tcbdllseg_compose´
: forall (s : RstateOP) (P : asrt) (h hp t1 tn1 t2 tn2 : val)
(l1 l2 : list vallist),
s |= tcbdllseg h hp t1 tn1 l1 ** tcbdllseg tn1 t1 t2 tn2 l2 ** P ->
s |= tcbdllseg h hp t2 tn2 (l1 ++ l2) ** [| (l1=nil/\tn1=h)\/( exists vl,l1<>nil /\ List.last l1 nil = vl /\ nth_val 0 vl = Some tn1)|] ** P.
Lemma list_split_last: forall l v, exists (x:vallist) (l´:list vallist), (v::l) = (l´++(x::nil)).
Lemma last_get: forall (l´:list vallist) (x:vallist), last (l´++(x::nil)) nil = x.
Qed.
Lemma neq_null_false_elim:forall x v s P, s |= LV x @ OS_TCB ∗ |-> v ** P -> s |= Aisfalse (x ′ !=ₑ NULL) -> v = Vnull.
Lemma neq_null_true_elim:forall x v s P, s |= LV x @ OS_TCB ∗ |-> v ** P -> s |= Aistrue (x ′ !=ₑ NULL) -> v <> Vnull.
Lemma ne_0_minus_1_in_range:
forall i2 : int32,
Int.unsigned i2 <= 65535 ->
Int.eq i2 ($ 0) = false ->
Int.unsigned (i2-ᵢ$ 1) <= Int16.max_unsigned.
Lemma z_to_nat_shr3:
forall x,0 <= Int.unsigned x -> Int.unsigned x < 64 -> (0 <= Z.to_nat (Int.unsigned (Int.shru x ($ 3))) < 8)%nat.
Lemma TCBList_P_RL_TCBblk_P :
forall l l´ a x x1 x2,
TCBList_P x (l++a::l´) x1 x2 -> RL_TCBblk_P a.
Import TcbMod.
Lemma join_join_minus : forall m1 m2 m3 ma mb,
join m1 m2 m3 -> join ma mb m1 -> join mb m2 (minus m3 ma).
Lemma tcbnode_rl_prop´:
forall v´13 v´14 v´12 v v´4 v´7 v´3 v´5 v´6 v´15 v´16 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
TcbMod.join v´13 v´14 v´12 ->
TCBList_P v v´4 v´7 v´13 ->
TCBList_P v´3 (v´5 :: v´6) v´7 v´14 ->
v´4 ++ v´5 :: v´6 =
v´15 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´16 ->
RL_TCBblk_P (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil).
Lemma join_join_disj :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m2 -> disj m1 m4.
Lemma tcbnode_rl_prop:
forall v´13 v´14 v´12 v´2 v´4 v´7 v´3 v´5 v´6 v´15 v´16 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
TcbMod.join v´13 v´14 v´12 ->
TCBList_P (Vptr v´2) v´4 v´7 v´13 ->
TCBList_P v´3 (v´5 :: v´6) v´7 v´14 ->
v´4 ++ v´5 :: v´6 =
v´15 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´16 ->
RL_TCBblk_P (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil).
Lemma TCBList_P_split :
forall {l1 l2 rtbl tcbls v},
TCBList_P v (l1++l2) rtbl tcbls ->
exists tcbls´ tcbls´´,
(TCBList_P v l1 rtbl tcbls´ /\ TcbMod.join tcbls´ tcbls´´ tcbls).
Lemma TCBList_P_combine :
forall {l1 l2 v1 v2 rtbl tcbls1 tcbls2 tcbls},
TcbMod.join tcbls1 tcbls2 tcbls ->
TCBList_P v1 l1 rtbl tcbls1 ->
TCBList_P v2 l2 rtbl tcbls2 ->
l1 <> nil ->
V_OSTCBNext (last l1 nil) = Some v2 ->
TCBList_P v1 (l1++l2) rtbl tcbls.
Lemma tcblist_p_recombine:
forall v´14 v´12 v´2 v´7 v´13 l1 l2 v´3 l1´ l2´,
l1 = nil /\ v´3 = Vptr v´2 \/
(exists vl, l1 <> nil /\ last l1 nil = vl /\ nth_val 0 vl = Some v´3) ->
TcbMod.join v´13 v´14 v´12 ->
TCBList_P (Vptr v´2) l1 v´7 v´13 ->
TCBList_P v´3 l2 v´7 v´14 ->
l1 ++ l2 =
l1´ ++ l2´ ->
exists rtbl´ tcbls´, TCBList_P (Vptr v´2) l1´ rtbl´ tcbls´.
Lemma rl_tcbblk_tcby_range:
forall v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
RL_TCBblk_P
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
Int.unsigned i2 < 8.
Lemma tcbdllseg_compose_tail:
forall s v´22 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0 v´2 v´18,
struct_type_vallist_match OS_TCB (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
s|=
Astruct (v´22, Int.zero) OS_TCB
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) **
tcbdllseg (Vptr v´2) Vnull v´8 (Vptr (v´22, Int.zero)) v´18 ->
s |= tcbdllseg (Vptr v´2) Vnull (Vptr (v´22, Int.zero)) v´21
(v´18 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil).
Lemma nth_val_length : forall l i v, nth_val i l = Some v -> (i < length l)%nat.
Lemma array_type_vallist_match_rule_type_val_match :
forall l n t x,
array_type_vallist_match t l -> nth_val n l = Some x ->
rule_type_val_match t x = true.
Lemma set_rdy_tbl_grp_hold:
forall v´7 i x1 m i0 i2 p l i3 i4 i5 v0 v4 x,
RL_Tbl_Grp_P v´7 (Vint32 i) ->
array_type_vallist_match Int8u v´7 ->
length v´7 = Pos.to_nat 8 ->
(Int.unsigned i <= 255)%Z ->
RL_TCBblk_P
(x1
:: v0
:: x
:: m
:: Vint32 i0
:: v4
:: Vint32 p
:: Vint32 i2
:: Vint32 i3 :: Vint32 i4 :: Vint32 i5 :: nil) ->
set_rdy_tbl (Vint32 i4) (Vint32 i3) v´7 = Some l ->
array_type_vallist_match Int8u l /\
length l = Pos.to_nat 8 /\
(Int.unsigned (Int.or i i5) <= 255)%Z /\
RL_Tbl_Grp_P l (Vint32 (Int.or i i5)).
Lemma timetick_update_prop:
forall v´12 v´7 i v´15 v´16 v´17 x y y´ head rtbl tcbls,
TCBList_P head v´12 rtbl tcbls ->
array_type_vallist_match Int8u v´7 ->
length v´7 = ∘OS_RDY_TBL_SIZE ->
(Int.unsigned i <= 255)%Z ->
RL_Tbl_Grp_P v´7 (Vint32 i) ->
tcbls_rtbl_timetci_update v´12 v´7 (Vint32 i) x y =
Some (v´15, v´16, Vint32 v´17, y´) ->
array_type_vallist_match Int8u v´16 /\
length v´16 = ∘OS_RDY_TBL_SIZE /\
(Int.unsigned v´17 <= 255)%Z /\
RL_Tbl_Grp_P v´16 (Vint32 v´17).
Lemma tick_rdy_ectr_get_ectr_eq:
forall els vl head l eid, tick_rdy_ectr vl head els = Some l -> (exists et etbl,get_ectr (Vptr eid) head els = Some (et, etbl)) -> (exists et etbl,get_ectr (Vptr eid) head l = Some (et, etbl)).
Lemma tcbls_rtbl_timetci_update_get_ectr_eq:
forall tls els els´ tls´ rtbl rtbl´ rgrp rgrp´ head eid,
tcbls_rtbl_timetci_update tls rtbl (Vint32 rgrp) head els =
Some (tls´, rtbl´, Vint32 rgrp´, els´) ->
(exists et etbl,get_ectr (Vptr eid) head els = Some (et,etbl)) ->
exists et etbl,get_ectr (Vptr eid) head els´ = Some (et,etbl).
Lemma TCBList_P_in_list_get_some_q :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_Q::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_q a) n, m).
Lemma TCBList_P_in_list_get_some_mbox :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_MBOX::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_mbox a) n, m).
Lemma TCBList_P_in_list_get_some_sem :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_SEM::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_sem a) n, m).
Lemma TCBList_P_in_list_get_some_mutex :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_MUTEX::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_mutexsem a) n, m).
Lemma list_app_in :
forall (A:Type) (l1:list A) l2 l3 l4 x,
l1 ++ l2 = l3 ++ x :: l4 -> In x l1 \/ In x l2.
Import EcbMod.
Lemma joinsig_beq_addrval_false_get : forall a a1 x x1 m1 m2,
joinsig a x m1 m2 -> get m2 a1 = Some x1 -> a <> a1 -> get m1 a1 = Some x1.
Lemma beq_pos_true : forall p, beq_pos p p = true.
Lemma beq_addrval_false_neq : forall a1 a2, beq_addrval a1 a2 = false -> a1 <> a2.
Lemma ECBList_P_get_ectr_some : forall (l:list EventCtr) tl ecbls mqls tcbls a x v,
EcbMod.get mqls a = Some x -> ECBList_P v tl l ecbls mqls tcbls ->
exists et etbl, get_ectr (Vptr a) v l = Some (et, etbl).
Lemma in_TCBList_P_TCBNode_P :
forall l a h r m, In a l -> TCBList_P h l r m-> exists rtbl abstcb, TCBNode_P a rtbl abstcb.
Lemma tcb_eptr_get_ectr´:
forall v´14 v´15 v´3 v´4 v´5 v´6 v´7 v´21 v´28 v´9
b i7 x6 i6 i5 i4 i3 i2 i1 i0 v´17 v´18 v´13 v´8 v´20 v´16 v´22 v´19,
TcbMod.join v´14 v´15 v´13 ->
TCBList_P (Vptr v´3) v´5 v´8 v´14 ->
TCBList_P v´4 (v´6 :: v´7) v´8 v´15 ->
v´5 ++ v´6 :: v´7 =
v´21 ++
(v´28
:: v´9
:: Vptr (b, i7)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´22 ->
ECBList_P v´20 Vnull v´16 v´17 v´18 v´13 ->
RH_TCBList_ECBList_P v´18 v´13 v´19 ->
0 <= Int.unsigned i4 < 64 -> array_type_vallist_match Int8u v´8 -> length v´8 = ∘OS_RDY_TBL_SIZE ->
exists et etbl, get_ectr (Vptr (b, i7)) v´20 v´16 = Some (et,etbl) .
Lemma tcb_eptr_get_ectr:
forall v´14 v´15 v´3 v´4 v´5 v´6 v´7 v´21 v´28 v´9
b i7 x6 i6 i5 i4 i3 i2 i1 i0 v´17 v´18 v´13 v´8 i v´20 v´16 v´24 v´25 v´26 v´27 v´22 v´19,
TcbMod.join v´14 v´15 v´13 ->
TCBList_P (Vptr v´3) v´5 v´8 v´14 ->
TCBList_P v´4 (v´6 :: v´7) v´8 v´15 ->
v´5 ++ v´6 :: v´7 =
v´21 ++
(v´28
:: v´9
:: Vptr (b, i7)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´22 ->
ECBList_P v´20 Vnull v´16 v´17 v´18 v´13 ->
RH_TCBList_ECBList_P v´18 v´13 v´19 ->
tcbls_rtbl_timetci_update v´21 v´8 (Vint32 i) v´20 v´16 =
Some (v´24, v´25, Vint32 v´26, v´27) ->
0 <= Int.unsigned i4 < 64 -> array_type_vallist_match Int8u v´8 -> length v´8 = ∘OS_RDY_TBL_SIZE ->
exists et etbl, get_ectr (Vptr (b, i7)) v´20 v´27 = Some (et,etbl) .
Lemma beq_addrval_eq: forall a b, beq_addrval a b = true -> a = b.
Lemma eq_beq_addrval: forall a, beq_addrval a a = true.
Lemma get_ectr_decompose:
forall qptrl s P msgqls l x p eid,
s |= evsllseg p Vnull qptrl msgqls ** P ->
get_ectr (Vptr eid) p qptrl = Some (l,x) ->
s |= EX vn qptrl1 qptrl2 msgqls1 msgqls2 msgq,
[| V_OSEventListPtr l = Some vn /\
qptrl = qptrl1 ++ ((l, x) :: nil) ++ qptrl2 /\
msgqls = msgqls1 ++ (msgq :: nil) ++ msgqls2 /\ get_ectr (Vptr eid) p qptrl1 = None /\
(get_ectr (Vptr eid) p (qptrl1++ ((l, x) :: nil)) = Some (l,x)) /\ p <> Vnull /\ forall l,In l qptrl1 -> exists x,V_OSEventListPtr (fst l) = Some (Vptr x)|] **
AEventNode (Vptr eid) l x msgq **
evsllseg p (Vptr eid) qptrl1 msgqls1 ** evsllseg vn Vnull qptrl2 msgqls2 ** P.
Lemma vl_elem_neq_dec: forall l x,vl_elem_neq (x::l) -> vl_elem_neq l.
Lemma val_elem_neq_one:
forall x,vl_elem_neq (x::nil).
Lemma beq_tid_true :
forall tid, beq_tid tid tid = true.
Lemma in_remove_tid_false :
forall l tid, In tid (remove_tid tid l) -> False.
Lemma in_remove_in: forall tid t wl, In tid (remove_tid t wl) -> In tid wl.
Lemma beq_tid_true_eq :
forall t1 t2, beq_tid t1 t2 = true -> t1 = t2.
Lemma in_neq_remove_in: forall tid wl t, t <> tid -> In tid wl -> In tid (remove_tid t wl).
Lemma tick_rdy_ectr_imp_x:
forall (v´33 : list (vallist * vallist)) (v´31 v´10 : val)
(v´37 : block) (x6 : val) (i6 i5 i4 i3 i2 i1 i0 i8 i10 : int32)
(v x5 v´24 : val) (x0 : vallist) (v´34 : list (list val * vallist))
(x1 : int32) x xx,
(forall l : vallist * vallist,
In l v´33 -> exists x2, V_OSEventListPtr (fst l) = Some (Vptr x2)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x1&Int.not i1) ($ 0) = true ->
Int.unsigned x1 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x1 ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: nil) =
Some
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
(Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 (i8&Int.not i0) :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x1&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp_x´:
forall (v´33 : list (vallist * vallist)) (v´31 v´10 : val)
(v´37 : block) (x6 : val) (i6 i5 i4 i3 i2 i1 i0 i8 i10 : int32)
(v x5 v´24 : val) (x0 : vallist) (v´34 : list (list val * vallist))
(x1 : int32) x xx,
(forall l : vallist * vallist,
In l v´33 -> exists x2, V_OSEventListPtr (fst l) = Some (Vptr x2)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x1&Int.not i1) ($ 0) = false ->
Int.unsigned x1 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x1 ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) (v´33 ++ (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
(Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x1&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp:
forall v´21,
isptr v´21 ->
v´21 <> Vnull ->
forall v´33 v´31 v´10 v´37 x6 i6 i5 i4 i3 i2 i1 i0 i8 i10 v x5 v´24 x0 v´34 x xx,
(forall l,In l v´33 -> exists x, V_OSEventListPtr (fst l) = Some (Vptr x)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x&Int.not i1) ($ 0) = true ->
(Int.unsigned x <= 255)%Z ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x ->
get_ectr (Vptr (v´37, Int.zero)) v´21 v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) v´21 (v´33 ++ (xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0)->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 (i8&Int.not i0) :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp´:
forall v´21,
isptr v´21 ->
v´21 <> Vnull ->
forall v´33 v´31 v´10 v´37 x6 i6 i5 i4 i3 i2 i1 i0 i8 i10 v x5 v´24 x0 v´34 x xx,
(forall l,In l v´33 -> exists x, V_OSEventListPtr (fst l) = Some (Vptr x)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x&Int.not i1) ($ 0) = false ->
Int.unsigned x <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x ->
get_ectr (Vptr (v´37, Int.zero)) v´21 v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) v´21 (v´33 ++ (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21
(v´33 ++
(xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x&Int.not i1)))
:: v´34).
Lemma tcbls_rtbl_timetci_update_compose:
forall tls1 rtbl rgrp head els tls1´ rtbl´ rgrp´ els´ tls2 tls2´ rtbl´´ rgrp´´ els´´,
tcbls_rtbl_timetci_update tls1 rtbl (Vint32 rgrp) head els =
Some (tls1´,rtbl´, Vint32 rgrp´, els´) ->
tcbls_rtbl_timetci_update tls2 rtbl´ (Vint32 rgrp´) head els´ = Some (tls2´,rtbl´´,Vint32 rgrp´´,els´´) ->
tcbls_rtbl_timetci_update (tls1++tls2) rtbl (Vint32 rgrp) head els = Some (tls1´++tls2´,rtbl´´,Vint32 rgrp´´,els´´).
Lemma tcbls_rtbl_timetci_update_decompose:
forall v´25 v´26 v´27 v´28 v´29 v´33 v´34 v´35 head els els´´,
tcbls_rtbl_timetci_update (v´25 ++ v´26 :: v´27) v´28 v´29 head els =
Some (v´35, v´33, v´34, els´´) ->
exists vl1 v vl2 rtbl´ rgrp´ els´,
v´35 = vl1 ++ v::vl2 /\
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els =
Some (vl1, rtbl´, rgrp´,els´) /\
tcbls_rtbl_timetci_update (v´26 :: v´27) rtbl´ rgrp´ head els´ =
Some ((v::vl2), v´33, v´34, els´´).
Lemma tick_rdy_ectr_ignore:
forall v´28 next pre msg tm stat next´ pre´ msg´ tm´ stat´ x1 x y z w v v´21,
(tick_rdy_ectr
(next
:: pre
:: Vptr x1
:: msg
:: tm
:: stat
:: Vint32 x
:: Vint32 y
:: Vint32 z
:: Vint32 w
:: Vint32 v :: nil) v´21
v´28) =
(tick_rdy_ectr
(next´
:: pre´
:: Vptr x1
:: msg´
:: tm´
:: stat´
:: Vint32 x
:: Vint32 y
:: Vint32 z
:: Vint32 w
:: Vint32 v :: nil) v´21
v´28).
Lemma tcbls_rtbl_timetci_update_hold:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´24 v´25 x7 i5 head rtbl tcbls,
isptr x7 ->
TCBList_P head v´22 rtbl tcbls ->
array_type_vallist_match Int8u v´9 ->
length v´9 = ∘OS_RDY_TBL_SIZE ->
Int.unsigned i <= 255 ->
Int.eq i6 ($ 0) = false ->
Int.eq (i6-ᵢ$ 1) ($ 0) = true ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vnull
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P v´9 (Vint32 i) ->
tick_rdy_ectr
(v´31
:: v´10
:: x7
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21 v´28 = Some v´24 ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: Vnull
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) v´26
(val_inj (or (nth_val´ (Z.to_nat (Int.unsigned i2)) v´26) (Vint32 i1))),
Vint32 (Int.or v´27 i0), v´24).
Lemma tcbls_rtbl_timetci_update_hold´:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´25 x7 i5,
Int.eq i6 ($ 0) = false ->
Int.eq (i6-ᵢ$ 1) ($ 0) = false ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
v´26,
Vint32 v´27, v´28).
Lemma tcbls_rtbl_timetci_update_hold´´:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´25 x7 i5,
Int.eq i6 ($ 0) = true ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
v´26,
Vint32 v´27, v´28).
Definition rel_st_els (st : taskstatus) (els : EcbMod.map) :=
match st with
| (wait (os_stat_sem eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_q eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_mbox eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_mutexsem eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| _ => true
end.
Definition R_Prio_No_Dup_L´ (ll:list vallist):=
forall n l ,
nth_vallist n ll = Some l ->
(
exists prio, V_OSTCBPrio l = Some (Vint32 prio) /\
forall n´ l´, n <> n´ ->
nth_vallist n´ ll = Some l´ ->
exists prio´,V_OSTCBPrio l´ = Some (Vint32 prio´) /\
prio <> prio´
).
Fixpoint Prio_Not_In (prio : int32) (ll : list vallist) {struct ll} :=
match ll with
| nil => True
| l :: ll´ => exists prio´, V_OSTCBPrio l = Some (Vint32 prio´)
/\ prio <> prio´ /\ Prio_Not_In prio ll´
end.
Fixpoint R_Prio_No_Dup_L (ll : list vallist) {struct ll} :=
match ll with
| nil => True
| l :: ll´ => exists prio,
V_OSTCBPrio l = Some (Vint32 prio) /\
Prio_Not_In prio ll´/\ R_Prio_No_Dup_L ll´
end.
Fixpoint not_in {A B:Type} (e:B) (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e´, f h = Some e´ -> e´ <> e) /\ not_in e t f
end.
Fixpoint set_nth {A:Type} (n:nat) (v:A) (vl: list A) : option (list A) :=
match vl with
| nil => None
| h::t => match n with
| O => Some (v::t)
| S x => match set_nth x v t with
| Some r => Some (h::r)
| None => None
end
end
end.
Definition set_tcb_next (tcb:vallist) next := set_nth 0%nat next tcb.
Definition get_last_ecb_ptr :=
fun (l : list (vallist * vallist)) (x : val) =>
match l with
| nil => Some x
| _ :: _ => V_OSEventListPtr (fst (last l (nil,nil)))
end.
Fixpoint eq_next l1 l2:=
match l1,l2 with
| v1::l1´,v2::l2´ => nth_val 0%nat v1 = nth_val 0%nat v2 /\ eq_next l1´ l2´
| nil,nil => True
| _ ,_ => False
end.
Import TcbMod.
Lemma join_fst:
forall a b lstx (l:TcbMod.lb a lstx) (i:TcbMod.is_orderset lstx) (j:TcbMod.is_orderset ((a,b)::lstx)),
TcbMod.join (TcbMod.listset_con (lst:=lstx) i) (TcbMod.sig a b) (TcbMod.listset_con (lst:=(a, b) :: lstx)j).
Lemma disj_eqdom :
forall m1 m1´ m2,
disj m1 m2 -> eqdom m1 m1´ -> disj m1´ m2.
Lemma tcb_domeq_joinsig_ex:
forall x1 a b b´ x x1´,
TcbMod.join x1 (TcbMod.sig a b) x -> (forall t,TcbMod.indom x1 t <-> TcbMod.indom x1´ t) ->exists x´, TcbMod.join x1´ (TcbMod.sig a b´) x´.
Lemma int_dec_zero_one : forall n:int32,
n = Int.zero \/ n = Int.one \/ (Int.eq Int.one n = false /\ Int.eq Int.zero n = false).
Lemma tid_beq_true :
forall tid, tidspec.beq tid tid = true.
Lemma in_remove_tid : forall {l t1 t2}, In t1 (remove_tid t2 l) -> In t1 l.
Lemma in_remove_tid´ : forall l t1 t2, In t1 l -> t1 <> t2 -> In t1 (remove_tid t2 l).
Lemma joinsig_listset_con :
forall l a x i (j:lb a l),
joinsig a x (listset_con (lst:=l) i) (listset_con (lst:=(a, x):: l) (conj j i)).
Lemma tid_blt_false : forall tid, tidspec.blt tid tid = false.
Lemma lb_get_false :
forall (l:rlist) a b i, lb a l -> get (listset_con (lst:=l) i) a = Some b -> False.
Lemma isrupd_empisr:(isrupd (isrupd empisr 0%nat true) 0%nat false) = empisr.
Lemma ih_no_lvar
: forall (aop : absop) (isrreg : isr) (si : is) (cs : cs) (ie : ie),
<|| aop ||> ** Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** isr_inv ** OSInv ** A_dom_lenv nil ==>
<|| aop ||> **
Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** [|exists k,gettopis si = k /\ forall j, (0 <= j < k)%nat -> isrreg j = false|] ** OSInv ** A_dom_lenv nil.
Lemma isrupd_true_false:
forall ir i,
isrupd (isrupd ir i true) i false = isrupd ir i false.
Lemma a_isr_is_prop_split:
forall s P isr is, s |= Aisr isr ** Ais is ** A_isr_is_prop ** P -> s |= Aisr isr ** Ais is ** P ** [| isr_is_prop isr is |].
Lemma tcbjoinsig_set_sub_sub:
forall t x tcbls tcbls´ tls y tls´,
TcbMod.joinsig t x tcbls tcbls´ ->
TcbMod.set tls t y = tls´ ->
TcbMod.sub tcbls´ tls ->
TcbMod.sub tcbls tls´.
Lemma sub_joinsig_set_sud:
forall tls_used tls t x x´ tls_used´ tls´,
TcbMod.sub tls_used tls ->
TcbMod.joinsig t x tls_used´ tls_used ->
TcbMod.set tls t x´ = tls´ ->TcbMod.sub tls_used´ tls´.
Lemma sub_joinsig_get:
forall tls_used tls t x tls_used´,
TcbMod.sub tls_used tls -> TcbMod.joinsig t x tls_used´ tls_used -> TcbMod.get tls t = Some x.
Lemma ecbmod_set_neq_change:
forall eid eid´ x a b,
eid <> eid´ ->
EcbMod.set (EcbMod.set x eid a) eid´ b =
EcbMod.set (EcbMod.set x eid´ b) eid a.
Lemma tcbmod_set_neq_change:
forall eid eid´ x a b,
eid <> eid´ ->
TcbMod.set (TcbMod.set x eid a) eid´ b =
TcbMod.set (TcbMod.set x eid´ b) eid a.
Lemma sub_emp:
forall x,
TcbMod.sub x emp -> x = emp.
Lemma joinsig_false:
forall t x y,
~ joinsig t x y emp.
Lemma tcb_joinsig_get_sub_ex:
forall t t´ st0 st1 tl1´ tl1 a tl2 tl2´,
t <> t´ ->
TcbMod.joinsig t st0 tl1´ tl1 ->
TcbMod.get tl1 t´ = Some a ->
TcbMod.sub tl1 tl2 ->
TcbMod.set tl2 t st1 = tl2´ ->
TcbMod.get tl1´ t´ = Some a /\
TcbMod.sub tl1´ tl2´ /\ exists x,
TcbMod.joinsig t´ a x tl1.
Lemma remove_tid_eq:
forall wl t t´ ,
remove_tid t´ (remove_tid t wl) = remove_tid t (remove_tid t´ wl).
Lemma ecbmod_set_eq:
forall x a b b´ c,
EcbMod.set (EcbMod.set x a b) a c =
EcbMod.set (EcbMod.set x a b´) a c.
Lemma joinsig3_neqtid_joinsig:
forall t0 t a x3 b x1 c y,
joinsig t a x3 b ->
joinsig t a x1 c ->
joinsig t0 y c b ->
joinsig t0 y x1 x3.
Lemma tcbjoin_joinsig_eq:
forall x y x1 z x2,
TcbJoin x y x1 z ->
TcbMod.joinsig x y x2 z -> x1 = x2.
Lemma tcbmod_sub_joinsig_sub:
forall a b x y z y´,
TcbMod.sub a b ->
TcbMod.joinsig x y z a ->
TcbMod.sub z (TcbMod.set b x y´).
Lemma tcb_minus_self_emp: forall x, TcbMod.minus x x = TcbMod.emp.
Lemma Prio_Not_In_ex :
forall ll a x,
Prio_Not_In x (a::ll) ->
Prio_Not_In x ll.
Lemma nth_vallist_inc_eq:
forall n´ a ll a0 l´,
0%nat <> n´ ->
(nth_vallist n´ (a :: ll) = Some l´ <->
nth_vallist (S n´) (a :: a0 :: ll) = Some l´).
Lemma tcbjoin_join_ex_join:
forall x x2 x1 tcbls´´ tcbx tcbls,
TcbJoin x x2 x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
exists y, TcbMod.join x1 tcbx y /\ TcbJoin x x2 y tcbls.
Lemma TCBList_P_nth_prio:
forall l n l´ (prio:priority) x0 x1 rtbl,
nth_vallist n l = Some l´ ->
V_OSTCBPrio l´ = Some (Vint32 prio) ->
TCBList_P x0 l rtbl x1 ->
exists tid st msg, TcbMod.get x1 tid = Some (prio,st,msg) .
Lemma tcbjoin_get_none:
forall x2 a x4 x1 x,
TcbJoin x2 a x4 x1 ->
TcbMod.get x1 x = None ->
TcbMod.get x4 x = None.
Lemma TCBList_P_imp_Prio_Not_In:
forall l tcbls x p t m x1 x0 rtbl,
TcbMod.get tcbls x = Some (p,t,m) ->
TcbMod.get x1 x = None ->
sub x1 tcbls ->
R_Prio_No_Dup tcbls ->
TCBList_P x0 l rtbl x1 ->
Prio_Not_In p l.
Lemma tcbjoin_get_n:
forall x y x1 tcbls,
TcbJoin x y x1 tcbls ->
TcbMod.get x1 x =None.
Lemma int_eq_false_false:
forall n,
Int.eq Int.one n = false ->
Int.eq n Int.zero = false ->
Int.eq (n-ᵢInt.one) Int.zero = false.
Lemma R_Prio_No_Dup_Convert :
forall ll, R_Prio_No_Dup_L´ ll -> R_Prio_No_Dup_L ll.
Lemma R_Prio_No_Dup_Convert_rev :
forall ll, R_Prio_No_Dup_L ll -> R_Prio_No_Dup_L´ ll.
Lemma R_Prio_No_Dup_Eq :
forall ll, R_Prio_No_Dup_L ll <-> R_Prio_No_Dup_L´ ll.
Lemma R_Prio_No_Dup_Sub_hold:
forall x3 tcbls,
sub x3 tcbls ->
R_Prio_No_Dup tcbls ->
R_Prio_No_Dup x3.
Lemma r_prio_no_dup_join_imp:
forall l tcbls´´ tcbx tcbls v rtbl,
join tcbls´´ tcbx tcbls ->
R_Prio_No_Dup tcbls ->
TCBList_P v l rtbl tcbls´´ ->
R_Prio_No_Dup_L l.
Ltac solve_tblk :=
unfolds; splits;
try solve [unfolds; simpl; auto];
try solve [do 6 eexists;splits; try unfolds; simpl; eauto; splits; eauto;
eexists;split; [unfolds; simpl;eauto | auto]].
Lemma tickchange_eq_ostcbnext:
forall l x0 rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´,
V_OSTCBNext l = Some x0 ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
V_OSTCBNext l´ = Some x0.
Lemma joinsig_joinsig_neq :
forall {a1 a2 x1 x2 m2 m2´ m3},
joinsig a1 x1 m2 m3 -> joinsig a2 x2 m2´ m2 -> a1 <> a2.
Lemma joinsig_joinsig_neq_ecb :
forall {a1 a2 x1 x2 m2 m2´ m3},
EcbMod.joinsig a1 x1 m2 m3 -> EcbMod.joinsig a2 x2 m2´ m2 -> a1 <> a2.
Lemma neq_set_comm :
forall a1 a2 x1 x2 m,
a1 <> a2 -> set (set m a1 x1) a2 x2 = set (set m a2 x2) a1 x1.
Lemma tickstep´_other_get_eq:
forall x y tcbls´´ y´ x3 tcbls´ els´ x1 tcbls,
TcbJoin x y x1 tcbls´´ ->
tickstep´ (set tcbls x y´) x3 tcbls´ els´ x1 ->
TcbMod.get tcbls´ x = Some y´.
Lemma tcb_joinsig_join_get_minus_eq:
forall x y x1 tcbls´´ tcbx tcbls y´ tcbls´,
TcbJoin x y x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
TcbMod.get tcbls´ x = Some y´ ->
TcbJoin x y´ (minus (minus tcbls´ tcbx) (sig x y´))
(minus tcbls´ tcbx).
Lemma tcb_minus_mergesig_minus_minus_eq:
forall tcbls´ x y tcbx,
TcbMod.minus tcbls´ (TcbMod.merge (TcbMod.sig x y) tcbx) =
TcbMod.minus (TcbMod.minus tcbls´ tcbx) (TcbMod.sig x y).
Lemma r_prio_no_dup_setst_hold:
forall x p t m x1 tcbls´´ tcbx tcbls x2,
TcbJoin x (p, t, m) x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
R_Prio_No_Dup tcbls ->
R_Prio_No_Dup (TcbMod.set tcbls x (p, x2, m)).
Lemma joinsig_join_joinmergesig_eq_set:
forall x y x1 tcbls´´ tcbx tcbls y´,
TcbMod.joinsig x y x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
TcbMod.join x1 (TcbMod.merge (TcbMod.sig x y´) tcbx) (TcbMod.set tcbls x y´).
Lemma tcb_minus_emp_eq: forall x, TcbMod.minus x TcbMod.emp = x.
Lemma tickstep_l_get_last_tcb_ptr_eq´:
forall v´25 v´26 v´27 v´28 v´33 (v´39:int32) head els x1 x2 x3 (x6:int32) xx els´ i1 i2,
tickstep_l (v´25 ++ v´26 :: v´27) v´28 i1 head els
(x1 ++ x2 :: x3) v´33 i2 els´ ->
length v´25 = length x1 ->
get_last_tcb_ptr x1 xx = get_last_tcb_ptr v´25 xx.
Lemma tickstep_l_get_last_tcb_ptr_eq:
forall v´25 v´26 v´27 v´28 v´33 v´39 head els x1 x2 x3 x6 xx els´,
tickstep_l (v´25 ++ v´26 :: v´27) v´28 (Vint32 v´39) head els
(x1 ++ x2 :: x3) v´33 (Vint32 x6) els´ ->
length v´25 = length x1 ->
get_last_tcb_ptr x1 xx = get_last_tcb_ptr v´25 xx.
Lemma tcbls_rtbl_timetci_update_tls_eq_next:
forall v´25 v´28 v´29 x1 x4 x5 head els els´,
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
eq_next v´25 x1.
Lemma tcbls_rtbl_timetci_update_tls_link:
forall v´25 v´15 v´23 v´28 v´29 x1 x4 x5 head els els´,
v´25 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
v´25 <> nil /\ last v´25 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)) ->
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
x1 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
x1 <> nil /\ last x1 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)).
Lemma tcbls_rtbl_timetci_update_tls_split:
forall v´25 v´15 v´23 v´28 v´29 x1 x4 x5 v´32 x2 x3 s P head els els´,
v´25 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
v´25 <> nil /\ last v´25 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)) ->
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
s |= tcbdllseg (Vptr v´23) Vnull v´32 Vnull (x1 ++ x2 :: x3) ** P ->
s |= EX x, tcbdllseg (Vptr v´23) Vnull x (Vptr v´15) x1 **
tcbdllseg (Vptr v´15) x v´32 Vnull (x2::x3) ** P.
Lemma tcbls_rtbl_timetci_update_rgrp_vint:
forall a b c a´ b´ c´ d e e´,
tcbls_rtbl_timetci_update a b (Vint32 c) d e= Some (a´,b´,c´,e´) ->
exists x, c´ = Vint32 x.
Lemma tick_fixpoint_convert:
forall vl x y head els vl´ x´ y´ els´,
tcbls_rtbl_timetci_update vl x y head els = Some (vl´, x´, y´, els´) ->
tickstep_l vl x y head els vl´ x´ y´ els´.
Lemma tick_fixpoint_convert_rev:
forall vl x y head els vl´ x´ y´ els´,
tickstep_l vl x y head els vl´ x´ y´ els´ ->
tcbls_rtbl_timetci_update vl x y head els = Some (vl´, x´, y´, els´).
Lemma tcbls_rtbl_timetci_update_len_eq´:
forall v´24 v´27 v´39 v´40 x1 x4 x5 x6 i,
tcbls_rtbl_timetci_update v´24 v´27 i v´39 v´40 =
Some (x1, x4, x5, x6) ->
length v´24 = length x1.
Lemma tcbls_rtbl_timetci_update_len_eq:
forall v´24 v´27 v´38 v´39 v´40 x1 x4 x5 x6,
tcbls_rtbl_timetci_update v´24 v´27 (Vint32 v´38) v´39 v´40 =
Some (x1, x4, x5, x6) ->
length v´24 = length x1.
Lemma tickchange_shift :
forall t t´ a els b els´ c d els´´,
t <> t´ ->
tickchange t a els b els´ ->
tickchange t´ c els´ d els´´ ->
exists x, tickchange t´ c els d x /\ tickchange t a x b els´´.
Lemma join_join_merge :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m1 -> join m4 (merge m5 m2) m3.
Lemma join_join_merge´ :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m1 -> join m4 (merge m2 m5) m3.
Lemma join_join_merge_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m1 -> EcbMod.join m4 (EcbMod.merge m5 m2) m3.
Lemma join_join_merge´_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m1 -> EcbMod.join m4 (EcbMod.merge m2 m5) m3.
Lemma tcb_join_joinsig_ex_joinsig:
forall htls´´ tcbx htls x y x1,
join htls´´ tcbx htls ->
joinsig x y x1 htls´´ ->
exists z, joinsig x y z htls.
Lemma nth_vallist_append : forall l1 l2 n x, nth_vallist n l1 = Some x -> nth_vallist n (l1++l2) = Some x.
Lemma Prio_Not_In_app :
forall l2 l3 x,
Prio_Not_In x (l2 ++ l3) -> Prio_Not_In x l2.
Lemma R_Prio_No_Dup_L_proc : forall a l, R_Prio_No_Dup_L (a::l) -> R_Prio_No_Dup_L (l).
Lemma r_prio_no_dup_l_mid:
forall l1 l2 l3,
R_Prio_No_Dup_L (l1++l2++l3) ->
R_Prio_No_Dup_L l2.
Lemma tcbjoin_set:
forall (x:addrval) y y´ htls1 htls,
TcbJoin x y htls1 htls ->
TcbJoin x y´ htls1 (set htls x y´).
Lemma joinsig_eq : forall x y1 y2 m1 m2 m3, joinsig x y1 m1 m3 -> joinsig x y2 m2 m3 -> y1 = y2.
Lemma join_tcbjoin_joinsig_eq´
: forall (x : tidspec.A) (y1 y2 : abstcb.B) (x1 z x2 : map),
TcbJoin x y1 x1 z -> joinsig x y2 x2 z-> y1 = y2.
Lemma V_OSTCBNext_set_tcb_next :
forall v x1 x2, V_OSTCBNext v = Some x1 -> exists x´, set_tcb_next v x2 = Some x´.
Lemma set_nth_nth_val :
forall n l x l´, set_nth n x l = Some l´ -> nth_val n l´ = Some x.
Lemma set_nth_nth_val´ :
forall l l´ n1 n2 x, n1 <> n2 -> set_nth n1 x l = Some l´ -> nth_val n2 l´ = nth_val n2 l.
Lemma TCBNode_P_change_next_ptr :
forall vl vl´ rtbl abstcb x,
TCBNode_P vl rtbl abstcb -> set_tcb_next vl x = Some vl´ ->
TCBNode_P vl´ rtbl abstcb.
Lemma V_OSTCBMsg_change_next_ptr :
forall vl vl´ a x,
V_OSTCBMsg vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBMsg vl´ = Some a.
Lemma V_OSTCBPrio_change_next_ptr :
forall vl vl´ a x,
V_OSTCBPrio vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBPrio vl´ = Some a.
Lemma V_OSTCBX_change_next_ptr :
forall vl vl´ a x,
V_OSTCBX vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBX vl´ = Some a.
Lemma V_OSTCBY_change_next_ptr :
forall vl vl´ a x,
V_OSTCBY vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBY vl´ = Some a.
Lemma V_OSTCBBitX_change_next_ptr :
forall vl vl´ a x,
V_OSTCBBitX vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBBitX vl´ = Some a.
Lemma V_OSTCBBitY_change_next_ptr :
forall vl vl´ a x,
V_OSTCBBitY vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBBitY vl´ = Some a.
Lemma V_OSTCBStat_change_next_ptr :
forall vl vl´ a x,
V_OSTCBStat vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBStat vl´ = Some a.
Lemma V_OSTCBEventPtr_change_next_ptr :
forall vl vl´ a x,
V_OSTCBEventPtr vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBEventPtr vl´ = Some a.
Lemma V_OSTCBDly_change_next_ptr :
forall vl vl´ a x,
V_OSTCBDly vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBDly vl´ = Some a.
Lemma V_OSTCBPrio_change_next_ptr´ :
forall vl vl´ prio x,
V_OSTCBPrio vl´ = Some prio -> set_tcb_next vl x = Some vl´ ->
V_OSTCBPrio vl = Some prio.
Lemma V_OSTCBDly_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBDly vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBDly vl = Some a.
Lemma V_OSTCBStat_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBStat vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBStat vl = Some a.
Lemma V_OSTCBEventPtr_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBEventPtr vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBEventPtr vl = Some a.
Lemma RdyTCBblk_change_next_ptr :
forall vl x vl´ rtbl prio,
RdyTCBblk vl rtbl prio -> set_tcb_next vl x = Some vl´ -> RdyTCBblk vl´ rtbl prio.
Lemma RdyTCBblk_change_next_ptr´ :
forall vl x vl´ rtbl prio,
RdyTCBblk vl´ rtbl prio -> set_tcb_next vl x = Some vl´ -> RdyTCBblk vl rtbl prio.
Qed.
Lemma TCBList_P_not_in_remove_last :
forall l head rtbl htls,
TCBList_P head l rtbl htls -> not_in head (removelast l) V_OSTCBNext.
Lemma get_last_tcb_ptr_in :
forall l a head x,
get_last_tcb_ptr (a::l) head = Some x -> ~ (not_in x (a::l) V_OSTCBNext).
Lemma not_in_remove_last :
forall {A B:Type} l1 l2 (a:A) (x:B) f,
not_in x (removelast (l1 ++ a :: l2)) f -> not_in x l1 f.
Lemma tcblist_p_tid_neq´:
forall ltlsy´´ a a1 h x l rtbl htls,
get_last_tcb_ptr (a :: ltlsy´´) h = Some (Vptr x) -> TCBList_P h ((a :: ltlsy´´) ++ (a1::l)) rtbl htls ->
h <> Vptr x.
Lemma joinsig_emp : forall m a x, joinsig a x emp m -> m = sig a x.
Lemma join_sig_false : forall a x1 x2 m, join (sig a x1) (sig a x2) m -> False.
Lemma join_sig_neq_set : forall a x m1 m2 a1 x1, a <> a1 -> joinsig a x m1 m2 -> joinsig a x (set m1 a1 x1) (set m2 a1 x1).
Lemma tcbjoin_neq:
forall x x0 x6 x5 htls y,
Vptr x <> Vptr x0 ->
TcbJoin x0 x6 x5 htls ->
TcbJoin x0 x6 (set x5 x y) (set htls x y).
Lemma r_prio_no_dup_two_neq:
forall a l l1 l2 ll,
R_Prio_No_Dup_L ((a :: l1) ++ (l :: ll) ++ l2) ->
V_OSTCBPrio a <> V_OSTCBPrio l.
Lemma joinsig_in_other :
forall m1 m2 m3 a1 x1 a2 x2, a1 <> a2 -> joinsig a1 x1 m1 m3 -> joinsig a2 x2 m2 m3 -> get m2 a1 = Some x1.
Lemma joinsig_get_minus : forall a x m, get m a = Some x -> joinsig a x (minus m (sig a x)) m.
Lemma tcb_neq_joinsig_tcbjoin_joinsig_minus:
forall x0 x y htls´´ htls x5 x4,
Vptr x0 <> Vptr x ->
joinsig x y htls´´ htls ->
TcbJoin x0 x5 x4 htls ->
joinsig x y (minus x4 (sig x y)) x4.
Lemma get_last_ecb_ptr_eq:
forall head x9 x0 x6 x2 htls eid,
ECBList_P head (Vptr x9) x0 x6 x2 htls ->
get_last_ecb_ptr x0 head = Some (Vptr eid) ->
x9 = eid.
Lemma ECBList_P_get_last_ecb_ptr:
forall {l1 l2 m1 m2 head x},
ECBList_P head (Vptr x) l1 l2 m1 m2 ->
get_last_ecb_ptr l1 head = Some (Vptr x).
Lemma ECBList_P_get_last_ecb_ptr_split_joinsig:
forall l1 l2 l3 m1 m2 e a head tail,
ECBList_P head tail (l1 ++ e :: l2) l3 m1 m2 ->
get_last_ecb_ptr l1 head = Some (Vptr a) ->
exists m11 m12 mx x, EcbMod.join m11 m12 m1 /\ EcbMod.joinsig a x mx m12.
Lemma join_join_merge_1_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m2 ->
EcbMod.join m1 m4 (EcbMod.merge m1 m4).
Lemma ECBList_P_els_get_split :
forall {els edata head tail tcbls hels m wl eptr},
ECBList_P head tail els edata hels tcbls ->
EcbMod.get hels eptr = Some (m, wl) ->
exists els1 els2 edata1 edata2 hels1 hels2,
ECBList_P head (Vptr eptr) els1 edata1 hels1 tcbls /\
ECBList_P (Vptr eptr) tail els2 edata2 hels2 tcbls /\
els = els1 ++ els2 /\ edata = edata1 ++ edata2 /\
EcbMod.join hels1 hels2 hels.
Lemma ECBList_P_vptr :
forall l1 l2 m1 m2 head tail a,
ECBList_P head tail (a::l1) l2 m1 m2 ->
(exists x, head = Vptr x).
Lemma ECBList_P_get_eidls_not_in :
forall {l1 l2 l3 m1 m2 e x h head tail},
ECBList_P head tail (((h::l1)++e::nil)++l2) l3 m1 m2 ->
get_last_ecb_ptr (h::l1) head = Some x ->
~In x (get_eidls head (h::l1)).
Lemma ecblist_p_compose´:
forall p qid mqls qptrl1 qptrl2 i i1 a x3 p´ v´41
msgqls1 msgqls2 msgq mqls1 mqls2 mq mqls´ tcbls x,
R_ECB_ETbl_P qid
(x
:: Vint32 i :: i1 :: a :: x3 :: p´ :: nil, v´41) tcbls ->
ECBList_P p (Vptr qid) qptrl1 msgqls1 mqls1 tcbls->
ECBList_P p´ Vnull qptrl2 msgqls2 mqls2 tcbls->
RLH_ECBData_P msgq mq ->
EcbMod.joinsig qid mq mqls2 mqls´->
EcbMod.join mqls1 mqls´ mqls ->
ECBList_P p Vnull (qptrl1 ++ ((x
:: Vint32 i :: i1 :: a :: x3 :: p´ :: nil, v´41)::nil) ++ qptrl2) (msgqls1 ++ (msgq::nil) ++msgqls2) mqls tcbls.
Lemma ecbmod_get_joinsig_join_eq:
forall eid x1´ x1 x2 x3 x4 hels,
EcbMod.get hels eid = Some x1´ ->
EcbMod.joinsig eid x1 x2 x4 ->
EcbMod.join x3 x4 hels ->
x1 = x1´.
Lemma ECBList_P_Set_Rdy_SEM_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_sem eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ECBList_P_Set_Rdy_MBOX_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ECBList_P_Set_Rdy_MUTEX_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mutexsem eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma tcblist_p_imp_tcbnode_p:
forall htls x y l1 h l ll l2 rtbl,
TcbMod.get htls x = Some y ->
get_last_tcb_ptr l1 h = Some (Vptr x) ->
TCBList_P h (l1++(l::ll)++l2) rtbl htls ->
TCBNode_P l rtbl y.
Lemma ecblist_p_wait_set_rdy:
forall ectr´ htls x p t m head Vnull edata x3,
get htls x = Some (p, wait os_stat_time t, m) ->
ECBList_P head Vnull ectr´ edata x3 htls ->
ECBList_P head Vnull ectr´ edata x3 (set htls x (p, rdy, m)).
Lemma r_ecb_etbl_p_wait_rdy_hold:
forall x x0 a htls n m m´ p,
TcbMod.get htls x = Some (p, wait os_stat_time n, m) ->
R_ECB_ETbl_P x0 a htls ->
R_ECB_ETbl_P x0 a (set htls x (p, rdy, m´)).
Qed.
Lemma ecblist_p_stat_time_minus1_eq:
forall ectr htls x p n m head edata x3 st,
get htls x = Some (p, wait st n, m) ->
ECBList_P head Vnull ectr edata x3 htls ->
ECBList_P head Vnull ectr edata x3
(set htls x (p, wait st (n-ᵢInt.one), m)).
Lemma r_ecb_etbl_p_tcbstats_eq_hold:
forall x x0 a htls (st:tcbstats) n m n´ m´ p,
TcbMod.get htls x = Some (p, wait st n, m) ->
R_ECB_ETbl_P x0 a htls ->
R_ECB_ETbl_P x0 a (set htls x (p, wait st n´, m´)).
Qed.
Import TcbMod.
Lemma tickchange_exists: forall t st els,
rel_st_els st els = true ->
exists st´ els´, tickchange t st els st´ els´.
Lemma RH_TCBList_ECBList_P_rel_st_els :
forall els tls ct t p st msg,
TcbMod.get tls t = Some (p, st, msg) ->
RH_TCBList_ECBList_P els tls ct -> rel_st_els st els = true.
Lemma RH_TCBList_ECBList_SEM_P_tickchange : forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_SEM_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_SEM_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_MBOX_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_MBOX_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_MBOX_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma rh_tcblist_ecblist_mutex_owner_set:
forall els´ tls t x y,
RH_TCBList_ECBList_MUTEX_OWNER els´ tls ->
get tls t = Some x ->
RH_TCBList_ECBList_MUTEX_OWNER els´
(set tls t y) .
Lemma rh_tcblist_ecblist_mutex_owner_set´:
forall els tls t m wl eid,
RH_TCBList_ECBList_MUTEX_OWNER els tls ->
EcbMod.get els eid = Some (m, wl) ->
RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set els eid (m, remove_tid t wl))
tls .
Lemma RH_TCBList_ECBList_MUTEX_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_MUTEX_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_MUTEX_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_Q_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_Q_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_Q_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_P_tickchange : forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma tickstep_exists´´:
forall tls_used tls els ct,
RH_TCBList_ECBList_P els tls ct ->
TcbMod.sub tls_used tls ->
exists tls´ els´, tickstep´ tls els tls´ els´ tls_used.
Lemma tickstep_exists´:
forall tls els ct,
RH_TCBList_ECBList_P els tls ct ->
exists tls´ els´, tickstep tls els tls´ els´.
Lemma tickstep_exists:
forall tls els ct,
exists tls´ els´, RH_TCBList_ECBList_P els tls ct ->
tickstep tls els tls´ els´.
Lemma tickstep_rh_curtcb´:
forall tls els tls´ els´ tls´´ ct,
tickstep´ tls els tls´ els´ tls´´ ->
sub tls´´ tls ->
RH_CurTCB ct tls -> RH_CurTCB ct tls´.
Lemma tickstep_rh_curtcb:
forall ct tls els tls´ els´,
tickstep tls els tls´ els´ ->
RH_CurTCB ct tls -> RH_CurTCB ct tls´.
Lemma tickstep_rh_tcblist_ecblist_p´:
forall ct tls els tls´ els´ tls´´,
TcbMod.sub tls´´ tls ->
tickstep´ tls els tls´ els´ tls´´-> RH_TCBList_ECBList_P els tls ct -> RH_TCBList_ECBList_P els´ tls´ ct.
Lemma tickstep_rh_tcblist_ecblist_p: forall ct tls els tls´ els´, tickstep tls els tls´ els´-> RH_TCBList_ECBList_P els tls ct -> RH_TCBList_ECBList_P els´ tls´ ct.
Lemma tickstep_r_priotbl_p´:
forall v´36 v´12 x x0 v´4 tls vhold,
TcbMod.sub tls v´36 ->
tickstep´ v´36 v´12 x x0 tls-> R_PrioTbl_P v´4 v´36 vhold-> R_PrioTbl_P v´4 x vhold.
Lemma tickstep_r_priotbl_p:
forall v´36 v´12 x x0 v´4 vhold,
tickstep v´36 v´12 x x0 -> R_PrioTbl_P v´4 v´36 vhold-> R_PrioTbl_P v´4 x vhold.
Lemma rl_rtbl_priotbl_p_set_hold:
forall next pre eptr msg stat dly i1 i2 i3 i4 i5 v1 v3 ptbl x rtbl vhold,
x <> vhold ->
RL_TCBblk_P
(next
:: pre
:: eptr
:: msg
:: stat
:: dly
:: Vint32 i1
:: Vint32 i2
:: Vint32 i3 :: Vint32 i4 :: Vint32 i5 :: nil) ->
nth_val (Z.to_nat (Int.unsigned i3)) rtbl = Some v1 ->
or v1 (Vint32 i4) = Some v3 ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold ->
nth_val (nat_of_Z (Int.unsigned i1)) ptbl = Some (Vptr x) ->
RL_RTbl_PrioTbl_P (update_nth_val (Z.to_nat (Int.unsigned i3)) rtbl v3) ptbl vhold.
Lemma tcbls_rtbl_timetci_update_rl_rtbl_priotbl_p´:
forall a b c a´ b´ c´ v´4 head els els´ vhold,
RL_TCBListblk_P a ->
RL_PrioTbl_P v´4 a vhold ->
tcbls_rtbl_timetci_update a b (Vint32 c) head els=
Some (a´, b´, Vint32 c´,els´) ->
RL_RTbl_PrioTbl_P b v´4 vhold ->
RL_RTbl_PrioTbl_P b´ v´4 vhold.
Lemma tcbls_rtbl_timetci_update_rl_rtbl_priotbl_p:
forall a b c a´ b´ c´ v´4 head els els´ tls x vhold,
TCBList_P x a b tls ->
RL_PrioTbl_P v´4 a vhold ->
tcbls_rtbl_timetci_update a b (Vint32 c) head els=
Some (a´, b´, Vint32 c´,els´) ->
RL_RTbl_PrioTbl_P b v´4 vhold ->
RL_RTbl_PrioTbl_P b´ v´4 vhold.
Lemma tickstep_decompose :
forall t p st msg tcbls tcbls´´ els els´ tcbls´,
TcbMod.get tcbls´´ t = Some (p, st, msg) ->
TcbMod.sub tcbls´´ tcbls ->
tickstep´ tcbls els tcbls´ els´ tcbls´´ ->
exists st´ els´´ ts tc,
joinsig t (p, st, msg) ts tcbls´´ /\
tickchange t st els st´ els´´ /\
TcbMod.set tcbls t (p,st´,msg) = tc /\
tickstep´ tc els´´ tcbls´ els´ ts /\
TcbMod.sub ts tc.
Lemma tickchange_nodup:
forall l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ll,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
R_Prio_No_Dup_L (l :: ll) ->
R_Prio_No_Dup_L (l´ :: ll).
Lemma set_rdy_grp_simpl:
forall x0 rgrp rgrp´ rtbl rtbl´,
Int.unsigned x0 < 64 ->
set_rdy_grp (Vint32 ($ 1<<(Int.shru x0 ($ 3)))) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 ($ 1<<(x0&$ 7))) (Vint32 (Int.shru x0 ($ 3))) rtbl = Some rtbl´ ->
exists i g,
nth_val (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))) rtbl = Some (Vint32 i) /\
rgrp = Vint32 g /\ rgrp´ = Vint32 (Int.or g ($ 1<<(Int.shru x0 ($ 3)))) /\
rtbl´ = update_nth_val (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))) rtbl
(Vint32 (Int.or i ($ 1<<(x0&$ 7)))) /\ Int.unsigned (Int.shru x0 ($ 3)) <8 /\ Int.unsigned (x0&$ 7) < 8.
Lemma tickchange_tcbnode_p_hold:
forall l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x t els t´ els´ p m,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
tickchange x t els t´ els´ ->
TCBNode_P l rtbl (p, t, m) ->
TCBNode_P l´ rtbl´ (p, t´, m).
Lemma tickchange_other_tcbnode_p_hold´:
forall a l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x6,
V_OSTCBPrio a <> V_OSTCBPrio l ->
RL_TCBblk_P l ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
TCBNode_P a rtbl x6 -> TCBNode_P a rtbl´ x6.
Fixpoint RL_TCBblk_P_List (ll : list vallist):=
match ll with
| nil => True
| l :: ll´ => RL_TCBblk_P l /\ RL_TCBblk_P_List ll´
end.
Lemma tickchange_other_tcbnode_p_hold:
forall l´ ll rtbl´ x rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´,
tickstep_l ll rtbl´ rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´ ->
R_Prio_No_Dup_L (l´ :: ll) ->
RL_TCBblk_P_List ll ->
TCBNode_P l´ rtbl´ x ->
TCBNode_P l´ rtbl´´ x.
Lemma timetick_idle_in_rtbl:
forall rtbl tls rgrp head els els´ rgrp´ rtbl´ tls´ ,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
RL_TCBblk_P_List tls->
tcbls_rtbl_timetci_update tls rtbl
(Vint32 rgrp) head els = Some (tls´, rtbl´, Vint32 rgrp´, els´) ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl´.
Lemma tickchange_other_tcblist_p_hold:
forall ll l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x0 x1,
R_Prio_No_Dup_L (l :: ll) ->
RL_TCBblk_P l ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
TCBList_P x0 ll rtbl x1 ->
TCBList_P x0 ll rtbl´ x1 .
Lemma TCBList_P_imp_RL:
forall ll x0 rtbl x1,
TCBList_P x0 ll rtbl x1 ->
RL_TCBblk_P_List ll.
Lemma timetick_tcblist_prop_hold:
forall vl x y v head ls vl´ x´ y´ els els´ ls´ tcbls tcbls´ tcbls´´ tcbx,
tickstep_l vl x y head ls vl´ x´ y´ ls´ ->
R_Prio_No_Dup tcbls ->
TCBList_P v vl x tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
tickstep´ tcbls els tcbls´ els´ tcbls´´ ->
TCBList_P v vl´ x´ (TcbMod.minus tcbls´ tcbx).
Lemma timetick_tcblist_p:
forall v´25 v´26 v´27 v´28 v´39 x1 x2 x3 v´33 x6 v´37 v´15 v´38 v´23 v´36 x0 v´12 x head els els´,
length v´25 = length x1 ->
tcbls_rtbl_timetci_update (v´25 ++ v´26 :: v´27) v´28 (Vint32 v´39) head els=
Some (x1 ++ x2 :: x3, v´33, Vint32 x6, els´) ->
get_last_tcb_ptr v´25 (Vptr v´23) = Some (Vptr v´15) ->
TCBList_P (Vptr v´23) v´25 v´28 v´37 ->
TCBList_P (Vptr v´15) (v´26 :: v´27) v´28 v´38 ->
tickstep v´36 v´12 x x0 ->
TcbMod.join v´37 v´38 v´36 ->
R_Prio_No_Dup v´36 ->
exists tl1 tl2, TcbMod.join tl2 tl1 x /\ TCBList_P (Vptr v´15) (x2 :: x3) v´33 tl1 /\ TCBList_P (Vptr v´23) x1 v´33 tl2.
Lemma tick_rdy_ectr´_decompose :
forall el1 el2 x eptr e vl ectr´ edl hels htls,
get_last_ecb_ptr el1 (Vptr x) = Some (Vptr eptr) ->
~ In (Vptr eptr) (get_eidls (Vptr x) el1) ->
tick_rdy_ectr´ eptr vl (Vptr x) (el1 ++ e :: el2) = Some ectr´->
ECBList_P (Vptr x) Vnull (el1 ++ e :: el2) edl hels htls ->
exists x, rdy_ectr vl e = Some x /\ ectr´ = (el1 ++ x :: el2).
Lemma tick_rdy_ectr_split:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ m wl hels htls edata,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´ ->
EcbMod.get hels eptr = Some (m, wl) ->
ECBList_P head Vnull ectr edata hels htls ->
exists l1 l2 a b a´ b´ c d e,
rdy_ectr (vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil) (a,b) = Some (a´,b´) /\
ectr = l1 ++ ((a,b)::nil) ++ l2 /\
edata = c ++ (e::nil) ++ d /\
length c = length l1 /\
ectr´ = l1 ++ ((a´,b´)::nil) ++ l2 /\
get_last_ecb_ptr l1 head = Some (Vptr eptr).
Lemma ecblist_p_tick_rdy_ectr_q:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_q eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_sem:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_sem eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_mbox:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_mbox eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_mutexsem:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_mutexsem eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma tickchange_ecblist_p:
forall h p l rtbl rgrp htls l1 l2 ll hels cur x t x2 x3 head ectr ectr´ edata l´ rgrp´ rtbl´ (m:msg),
TcbMod.get htls x = Some (p, t, m) ->
get_last_tcb_ptr l1 h = Some (Vptr x) ->
TCBList_P h (l1++(l::ll)++l2) rtbl htls ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
R_Prio_No_Dup_L (l1++(l::ll)++l2) ->
RH_TCBList_ECBList_P hels htls cur ->
tickchange x t hels x2 x3 ->
ECBList_P head Vnull ectr edata hels htls ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata x3 (TcbMod.set htls x (p, x2, m)).
Lemma tickchange_tcblist_p_hold_mid:
forall ltlsy´´ x p t m htls´´ htls rtbl hels x2 x3
l rgrp head ectr l´ rtbl´ rgrp´ ectr´ h ll ltlsx´´ ,
joinsig x (p, t, m) htls´´ htls ->
tickchange x t hels x2 x3 ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
get_last_tcb_ptr ltlsy´´ h = Some (Vptr x) ->
TCBList_P h (ltlsy´´ ++ (l :: ll) ++ ltlsx´´) rtbl htls ->
R_Prio_No_Dup_L (ltlsy´´ ++ (l :: ll) ++ ltlsx´´) ->
TCBList_P h ((ltlsy´´ ++ l´ :: nil) ++ ll ++ ltlsx´´) rtbl´
(set htls x (p, x2, m)).
Lemma tickstep_ecblist_p´:
forall ltls´´ rtbl rgrp head lels ltls´ rtbl´ rgrp´ lels´,
tickstep_l ltls´´ rtbl rgrp head lels ltls´ rtbl´ rgrp´ lels´ ->
forall htls edata cur hels hels´ htls´ h ltlsx´´ ltls tcbx ltlsy´´ htls´´ h´,
R_Prio_No_Dup htls ->
tickstep´ htls hels htls´ hels´ htls´´->
ltls = ltlsy´´++ ltls´´ ++ ltlsx´´ ->
get_last_tcb_ptr ltlsy´´ h = Some h´ ->
TCBList_P h´ ltls´´ rtbl htls´´ ->
TCBList_P h ltls rtbl htls ->
TcbMod.join htls´´ tcbx htls ->
RH_TCBList_ECBList_P hels htls cur ->
ECBList_P head Vnull lels edata hels htls ->
ECBList_P head Vnull lels´ edata hels´ htls´.
Lemma tickstep_ecblist_p:
forall h h´ ltls1 ltls2 htls lels hels cur rgrp rtbl head edata rtbl´ rgrp´ hels´ htls´ lels´ ltls´ htls1 htls2,
TcbMod.join htls1 htls2 htls ->
TCBList_P h ltls1 rtbl htls1 ->
TCBList_P h´ ltls2 rtbl htls2 ->
RH_TCBList_ECBList_P hels htls cur ->
tcbls_rtbl_timetci_update (ltls1++ltls2) rtbl
rgrp head lels =
Some (ltls´, rtbl´, rgrp´, lels´) ->
ECBList_P head Vnull lels edata hels htls ->
tickstep htls hels htls´ hels´ ->
R_Prio_No_Dup htls ->
get_last_tcb_ptr ltls1 h = Some h´ ->
ECBList_P head Vnull lels´ edata hels´ htls´.
Require Import mathlib.
Require Import OSQPostPure.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Logic.ProofIrrelevanceFacts.
Import TcbMod.
Ltac hoare_ex_intro´ :=
repeat
match goal with
| |- {|_ , _, _, _ , _|}|- {{EX _, _}}_ {{_}} => apply ex_intro_rule; intros
end.
Ltac hoare_split_pure_all´´ :=
hoare normal pre; hoare_ex_intro´; hoare_split_pure_all´.
Ltac pure_intro´ :=
hoare_split_pure_all´´; isptr_intro; array_leneq_intro; hoare_split_pure_all;
mytac; struct_type_vallist_match_elim; simpl_field_eq.
Ltac xunfold´ H:=
let M:= fresh in
match type of H with
| match ?X with
| _ => _
end = Some _ => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xunfold´´ H:=
let M:= fresh in
match type of H with
| Some _ = match ?X with
| _ => _
end => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xunfold´´´´ H:=
match type of H with
| (Some ?p) = _
=> destruct p as [[[]]]
| _ => idtac
end.
Ltac xunfold´´´ H:=
let M:= fresh in
match type of H with
| match ?X with
| _ => _
end = Some _ => remember X as M eqn:Htick;destruct M;tryfalse;auto;xunfold´´´´ Htick;inverts H
| _ => idtac
end.
Ltac xunfold H :=
repeat (xunfold´ H);
subst;
simpl in *;unfold add_option_first in H;(xunfold´´´ H).
Ltac xxunfold´:=
match goal with
| |- match ?X with
| _ => _
end = Some _ => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xxunfold´´ :=
match goal with
| |- Some _ = match ?X with
| _ => _
end => remember X as M;destruct M;tryfalse;auto
| _ => idtac
end.
Ltac xxunfold´´´ :=
match goal with
| |- match ?X with
| _ => _
end = Some _ => remember X as M eqn:Htick;destruct M;tryfalse;auto;xunfold´´´´ Htick
| _ => idtac
end.
Ltac xxunfold :=
repeat (xxunfold´);
subst;
simpl in *;unfold add_option_first;(xxunfold´´´).
Ltac inverts_all´ :=
match goal with
| H: Some _ = Some _ |- _ => inverts H
end.
Ltac inverts_all:= repeat inverts_all´.
Ltac mytac_1´ :=
match goal with
| H:exists _, _ |- _ => destruct H; mytac_1´
| H:_ /\ _ |- _ => destruct H; mytac_1´
| _ => try (progress subst; mytac_1´)
end.
Ltac mytac´ := repeat progress mytac_1´.
Fixpoint get_ectr (eid:val) (head:val) (ectrl:list EventCtr) :=
match eid,head,ectrl with
| (Vptr e),(Vptr e´),(osevent, etbl)::vll =>
match beq_addrval e e´ with
| true => Some (osevent,etbl)
| false => match V_OSEventListPtr osevent with
| Some vn => get_ectr eid vn vll
| _ => None
end
end
| _,_,_ => None
end.
Lemma tcbdllseg_compose´
: forall (s : RstateOP) (P : asrt) (h hp t1 tn1 t2 tn2 : val)
(l1 l2 : list vallist),
s |= tcbdllseg h hp t1 tn1 l1 ** tcbdllseg tn1 t1 t2 tn2 l2 ** P ->
s |= tcbdllseg h hp t2 tn2 (l1 ++ l2) ** [| (l1=nil/\tn1=h)\/( exists vl,l1<>nil /\ List.last l1 nil = vl /\ nth_val 0 vl = Some tn1)|] ** P.
Lemma list_split_last: forall l v, exists (x:vallist) (l´:list vallist), (v::l) = (l´++(x::nil)).
Lemma last_get: forall (l´:list vallist) (x:vallist), last (l´++(x::nil)) nil = x.
Qed.
Lemma neq_null_false_elim:forall x v s P, s |= LV x @ OS_TCB ∗ |-> v ** P -> s |= Aisfalse (x ′ !=ₑ NULL) -> v = Vnull.
Lemma neq_null_true_elim:forall x v s P, s |= LV x @ OS_TCB ∗ |-> v ** P -> s |= Aistrue (x ′ !=ₑ NULL) -> v <> Vnull.
Lemma ne_0_minus_1_in_range:
forall i2 : int32,
Int.unsigned i2 <= 65535 ->
Int.eq i2 ($ 0) = false ->
Int.unsigned (i2-ᵢ$ 1) <= Int16.max_unsigned.
Lemma z_to_nat_shr3:
forall x,0 <= Int.unsigned x -> Int.unsigned x < 64 -> (0 <= Z.to_nat (Int.unsigned (Int.shru x ($ 3))) < 8)%nat.
Lemma TCBList_P_RL_TCBblk_P :
forall l l´ a x x1 x2,
TCBList_P x (l++a::l´) x1 x2 -> RL_TCBblk_P a.
Import TcbMod.
Lemma join_join_minus : forall m1 m2 m3 ma mb,
join m1 m2 m3 -> join ma mb m1 -> join mb m2 (minus m3 ma).
Lemma tcbnode_rl_prop´:
forall v´13 v´14 v´12 v v´4 v´7 v´3 v´5 v´6 v´15 v´16 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
TcbMod.join v´13 v´14 v´12 ->
TCBList_P v v´4 v´7 v´13 ->
TCBList_P v´3 (v´5 :: v´6) v´7 v´14 ->
v´4 ++ v´5 :: v´6 =
v´15 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´16 ->
RL_TCBblk_P (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil).
Lemma join_join_disj :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m2 -> disj m1 m4.
Lemma tcbnode_rl_prop:
forall v´13 v´14 v´12 v´2 v´4 v´7 v´3 v´5 v´6 v´15 v´16 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
TcbMod.join v´13 v´14 v´12 ->
TCBList_P (Vptr v´2) v´4 v´7 v´13 ->
TCBList_P v´3 (v´5 :: v´6) v´7 v´14 ->
v´4 ++ v´5 :: v´6 =
v´15 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´16 ->
RL_TCBblk_P (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil).
Lemma TCBList_P_split :
forall {l1 l2 rtbl tcbls v},
TCBList_P v (l1++l2) rtbl tcbls ->
exists tcbls´ tcbls´´,
(TCBList_P v l1 rtbl tcbls´ /\ TcbMod.join tcbls´ tcbls´´ tcbls).
Lemma TCBList_P_combine :
forall {l1 l2 v1 v2 rtbl tcbls1 tcbls2 tcbls},
TcbMod.join tcbls1 tcbls2 tcbls ->
TCBList_P v1 l1 rtbl tcbls1 ->
TCBList_P v2 l2 rtbl tcbls2 ->
l1 <> nil ->
V_OSTCBNext (last l1 nil) = Some v2 ->
TCBList_P v1 (l1++l2) rtbl tcbls.
Lemma tcblist_p_recombine:
forall v´14 v´12 v´2 v´7 v´13 l1 l2 v´3 l1´ l2´,
l1 = nil /\ v´3 = Vptr v´2 \/
(exists vl, l1 <> nil /\ last l1 nil = vl /\ nth_val 0 vl = Some v´3) ->
TcbMod.join v´13 v´14 v´12 ->
TCBList_P (Vptr v´2) l1 v´7 v´13 ->
TCBList_P v´3 l2 v´7 v´14 ->
l1 ++ l2 =
l1´ ++ l2´ ->
exists rtbl´ tcbls´, TCBList_P (Vptr v´2) l1´ rtbl´ tcbls´.
Lemma rl_tcbblk_tcby_range:
forall v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0,
RL_TCBblk_P
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
Int.unsigned i2 < 8.
Lemma tcbdllseg_compose_tail:
forall s v´22 v´21 v´8 x7 x6 i6 i5 i4 i3 i2 i1 i0 v´2 v´18,
struct_type_vallist_match OS_TCB (v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
s|=
Astruct (v´22, Int.zero) OS_TCB
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) **
tcbdllseg (Vptr v´2) Vnull v´8 (Vptr (v´22, Int.zero)) v´18 ->
s |= tcbdllseg (Vptr v´2) Vnull (Vptr (v´22, Int.zero)) v´21
(v´18 ++
(v´21
:: v´8
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil).
Lemma nth_val_length : forall l i v, nth_val i l = Some v -> (i < length l)%nat.
Lemma array_type_vallist_match_rule_type_val_match :
forall l n t x,
array_type_vallist_match t l -> nth_val n l = Some x ->
rule_type_val_match t x = true.
Lemma set_rdy_tbl_grp_hold:
forall v´7 i x1 m i0 i2 p l i3 i4 i5 v0 v4 x,
RL_Tbl_Grp_P v´7 (Vint32 i) ->
array_type_vallist_match Int8u v´7 ->
length v´7 = Pos.to_nat 8 ->
(Int.unsigned i <= 255)%Z ->
RL_TCBblk_P
(x1
:: v0
:: x
:: m
:: Vint32 i0
:: v4
:: Vint32 p
:: Vint32 i2
:: Vint32 i3 :: Vint32 i4 :: Vint32 i5 :: nil) ->
set_rdy_tbl (Vint32 i4) (Vint32 i3) v´7 = Some l ->
array_type_vallist_match Int8u l /\
length l = Pos.to_nat 8 /\
(Int.unsigned (Int.or i i5) <= 255)%Z /\
RL_Tbl_Grp_P l (Vint32 (Int.or i i5)).
Lemma timetick_update_prop:
forall v´12 v´7 i v´15 v´16 v´17 x y y´ head rtbl tcbls,
TCBList_P head v´12 rtbl tcbls ->
array_type_vallist_match Int8u v´7 ->
length v´7 = ∘OS_RDY_TBL_SIZE ->
(Int.unsigned i <= 255)%Z ->
RL_Tbl_Grp_P v´7 (Vint32 i) ->
tcbls_rtbl_timetci_update v´12 v´7 (Vint32 i) x y =
Some (v´15, v´16, Vint32 v´17, y´) ->
array_type_vallist_match Int8u v´16 /\
length v´16 = ∘OS_RDY_TBL_SIZE /\
(Int.unsigned v´17 <= 255)%Z /\
RL_Tbl_Grp_P v´16 (Vint32 v´17).
Lemma tick_rdy_ectr_get_ectr_eq:
forall els vl head l eid, tick_rdy_ectr vl head els = Some l -> (exists et etbl,get_ectr (Vptr eid) head els = Some (et, etbl)) -> (exists et etbl,get_ectr (Vptr eid) head l = Some (et, etbl)).
Lemma tcbls_rtbl_timetci_update_get_ectr_eq:
forall tls els els´ tls´ rtbl rtbl´ rgrp rgrp´ head eid,
tcbls_rtbl_timetci_update tls rtbl (Vint32 rgrp) head els =
Some (tls´, rtbl´, Vint32 rgrp´, els´) ->
(exists et etbl,get_ectr (Vptr eid) head els = Some (et,etbl)) ->
exists et etbl,get_ectr (Vptr eid) head els´ = Some (et,etbl).
Lemma TCBList_P_in_list_get_some_q :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_Q::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_q a) n, m).
Lemma TCBList_P_in_list_get_some_mbox :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_MBOX::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_mbox a) n, m).
Lemma TCBList_P_in_list_get_some_sem :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_SEM::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_sem a) n, m).
Lemma TCBList_P_in_list_get_some_mutex :
forall l v rtbl tcbls i0 i1 i3 i4 i6 i7 i8 i9 i10 a,
TCBList_P v l rtbl tcbls ->
In (i0::i1::Vptr a::i3::Vint32 i4::V$OS_STAT_MUTEX::Vint32 i6::i7::i8::i9::i10::nil) l ->
0 <= Int.unsigned i6 < 64 ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
exists tid p n m, TcbMod.get tcbls tid = Some(p, wait(os_stat_mutexsem a) n, m).
Lemma list_app_in :
forall (A:Type) (l1:list A) l2 l3 l4 x,
l1 ++ l2 = l3 ++ x :: l4 -> In x l1 \/ In x l2.
Import EcbMod.
Lemma joinsig_beq_addrval_false_get : forall a a1 x x1 m1 m2,
joinsig a x m1 m2 -> get m2 a1 = Some x1 -> a <> a1 -> get m1 a1 = Some x1.
Lemma beq_pos_true : forall p, beq_pos p p = true.
Lemma beq_addrval_false_neq : forall a1 a2, beq_addrval a1 a2 = false -> a1 <> a2.
Lemma ECBList_P_get_ectr_some : forall (l:list EventCtr) tl ecbls mqls tcbls a x v,
EcbMod.get mqls a = Some x -> ECBList_P v tl l ecbls mqls tcbls ->
exists et etbl, get_ectr (Vptr a) v l = Some (et, etbl).
Lemma in_TCBList_P_TCBNode_P :
forall l a h r m, In a l -> TCBList_P h l r m-> exists rtbl abstcb, TCBNode_P a rtbl abstcb.
Lemma tcb_eptr_get_ectr´:
forall v´14 v´15 v´3 v´4 v´5 v´6 v´7 v´21 v´28 v´9
b i7 x6 i6 i5 i4 i3 i2 i1 i0 v´17 v´18 v´13 v´8 v´20 v´16 v´22 v´19,
TcbMod.join v´14 v´15 v´13 ->
TCBList_P (Vptr v´3) v´5 v´8 v´14 ->
TCBList_P v´4 (v´6 :: v´7) v´8 v´15 ->
v´5 ++ v´6 :: v´7 =
v´21 ++
(v´28
:: v´9
:: Vptr (b, i7)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´22 ->
ECBList_P v´20 Vnull v´16 v´17 v´18 v´13 ->
RH_TCBList_ECBList_P v´18 v´13 v´19 ->
0 <= Int.unsigned i4 < 64 -> array_type_vallist_match Int8u v´8 -> length v´8 = ∘OS_RDY_TBL_SIZE ->
exists et etbl, get_ectr (Vptr (b, i7)) v´20 v´16 = Some (et,etbl) .
Lemma tcb_eptr_get_ectr:
forall v´14 v´15 v´3 v´4 v´5 v´6 v´7 v´21 v´28 v´9
b i7 x6 i6 i5 i4 i3 i2 i1 i0 v´17 v´18 v´13 v´8 i v´20 v´16 v´24 v´25 v´26 v´27 v´22 v´19,
TcbMod.join v´14 v´15 v´13 ->
TCBList_P (Vptr v´3) v´5 v´8 v´14 ->
TCBList_P v´4 (v´6 :: v´7) v´8 v´15 ->
v´5 ++ v´6 :: v´7 =
v´21 ++
(v´28
:: v´9
:: Vptr (b, i7)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: v´22 ->
ECBList_P v´20 Vnull v´16 v´17 v´18 v´13 ->
RH_TCBList_ECBList_P v´18 v´13 v´19 ->
tcbls_rtbl_timetci_update v´21 v´8 (Vint32 i) v´20 v´16 =
Some (v´24, v´25, Vint32 v´26, v´27) ->
0 <= Int.unsigned i4 < 64 -> array_type_vallist_match Int8u v´8 -> length v´8 = ∘OS_RDY_TBL_SIZE ->
exists et etbl, get_ectr (Vptr (b, i7)) v´20 v´27 = Some (et,etbl) .
Lemma beq_addrval_eq: forall a b, beq_addrval a b = true -> a = b.
Lemma eq_beq_addrval: forall a, beq_addrval a a = true.
Lemma get_ectr_decompose:
forall qptrl s P msgqls l x p eid,
s |= evsllseg p Vnull qptrl msgqls ** P ->
get_ectr (Vptr eid) p qptrl = Some (l,x) ->
s |= EX vn qptrl1 qptrl2 msgqls1 msgqls2 msgq,
[| V_OSEventListPtr l = Some vn /\
qptrl = qptrl1 ++ ((l, x) :: nil) ++ qptrl2 /\
msgqls = msgqls1 ++ (msgq :: nil) ++ msgqls2 /\ get_ectr (Vptr eid) p qptrl1 = None /\
(get_ectr (Vptr eid) p (qptrl1++ ((l, x) :: nil)) = Some (l,x)) /\ p <> Vnull /\ forall l,In l qptrl1 -> exists x,V_OSEventListPtr (fst l) = Some (Vptr x)|] **
AEventNode (Vptr eid) l x msgq **
evsllseg p (Vptr eid) qptrl1 msgqls1 ** evsllseg vn Vnull qptrl2 msgqls2 ** P.
Lemma vl_elem_neq_dec: forall l x,vl_elem_neq (x::l) -> vl_elem_neq l.
Lemma val_elem_neq_one:
forall x,vl_elem_neq (x::nil).
Lemma beq_tid_true :
forall tid, beq_tid tid tid = true.
Lemma in_remove_tid_false :
forall l tid, In tid (remove_tid tid l) -> False.
Lemma in_remove_in: forall tid t wl, In tid (remove_tid t wl) -> In tid wl.
Lemma beq_tid_true_eq :
forall t1 t2, beq_tid t1 t2 = true -> t1 = t2.
Lemma in_neq_remove_in: forall tid wl t, t <> tid -> In tid wl -> In tid (remove_tid t wl).
Lemma tick_rdy_ectr_imp_x:
forall (v´33 : list (vallist * vallist)) (v´31 v´10 : val)
(v´37 : block) (x6 : val) (i6 i5 i4 i3 i2 i1 i0 i8 i10 : int32)
(v x5 v´24 : val) (x0 : vallist) (v´34 : list (list val * vallist))
(x1 : int32) x xx,
(forall l : vallist * vallist,
In l v´33 -> exists x2, V_OSEventListPtr (fst l) = Some (Vptr x2)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x1&Int.not i1) ($ 0) = true ->
Int.unsigned x1 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x1 ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: nil) =
Some
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
(Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 (i8&Int.not i0) :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x1&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp_x´:
forall (v´33 : list (vallist * vallist)) (v´31 v´10 : val)
(v´37 : block) (x6 : val) (i6 i5 i4 i3 i2 i1 i0 i8 i10 : int32)
(v x5 v´24 : val) (x0 : vallist) (v´34 : list (list val * vallist))
(x1 : int32) x xx,
(forall l : vallist * vallist,
In l v´33 -> exists x2, V_OSEventListPtr (fst l) = Some (Vptr x2)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x1&Int.not i1) ($ 0) = false ->
Int.unsigned x1 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x1 ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) (Vptr x) (v´33 ++ (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
(Vptr x)
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x1&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp:
forall v´21,
isptr v´21 ->
v´21 <> Vnull ->
forall v´33 v´31 v´10 v´37 x6 i6 i5 i4 i3 i2 i1 i0 i8 i10 v x5 v´24 x0 v´34 x xx,
(forall l,In l v´33 -> exists x, V_OSEventListPtr (fst l) = Some (Vptr x)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x&Int.not i1) ($ 0) = true ->
(Int.unsigned x <= 255)%Z ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x ->
get_ectr (Vptr (v´37, Int.zero)) v´21 v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) v´21 (v´33 ++ (xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0)->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21
(v´33 ++
(xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 (i8&Int.not i0) :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x&Int.not i1)))
:: v´34).
Lemma tick_rdy_ectr_imp´:
forall v´21,
isptr v´21 ->
v´21 <> Vnull ->
forall v´33 v´31 v´10 v´37 x6 i6 i5 i4 i3 i2 i1 i0 i8 i10 v x5 v´24 x0 v´34 x xx,
(forall l,In l v´33 -> exists x, V_OSEventListPtr (fst l) = Some (Vptr x)) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2
:: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P x0 (Vint32 i8) ->
Int.eq (x&Int.not i1) ($ 0) = false ->
Int.unsigned x <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned i2)) x0 = Vint32 x ->
get_ectr (Vptr (v´37, Int.zero)) v´21 v´33 = None ->
get_ectr (Vptr (v´37, Int.zero)) v´21 (v´33 ++ (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ::nil) = Some (xx :: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil, x0) ->
tick_rdy_ectr
(v´31
:: v´10
:: Vptr (v´37, Int.zero)
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21
(v´33 ++
(xx:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
x0) :: v´34) =
Some
(v´33 ++
(xx
:: Vint32 i8 :: Vint32 i10 :: v :: x5 :: v´24 :: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) x0 (Vint32 (x&Int.not i1)))
:: v´34).
Lemma tcbls_rtbl_timetci_update_compose:
forall tls1 rtbl rgrp head els tls1´ rtbl´ rgrp´ els´ tls2 tls2´ rtbl´´ rgrp´´ els´´,
tcbls_rtbl_timetci_update tls1 rtbl (Vint32 rgrp) head els =
Some (tls1´,rtbl´, Vint32 rgrp´, els´) ->
tcbls_rtbl_timetci_update tls2 rtbl´ (Vint32 rgrp´) head els´ = Some (tls2´,rtbl´´,Vint32 rgrp´´,els´´) ->
tcbls_rtbl_timetci_update (tls1++tls2) rtbl (Vint32 rgrp) head els = Some (tls1´++tls2´,rtbl´´,Vint32 rgrp´´,els´´).
Lemma tcbls_rtbl_timetci_update_decompose:
forall v´25 v´26 v´27 v´28 v´29 v´33 v´34 v´35 head els els´´,
tcbls_rtbl_timetci_update (v´25 ++ v´26 :: v´27) v´28 v´29 head els =
Some (v´35, v´33, v´34, els´´) ->
exists vl1 v vl2 rtbl´ rgrp´ els´,
v´35 = vl1 ++ v::vl2 /\
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els =
Some (vl1, rtbl´, rgrp´,els´) /\
tcbls_rtbl_timetci_update (v´26 :: v´27) rtbl´ rgrp´ head els´ =
Some ((v::vl2), v´33, v´34, els´´).
Lemma tick_rdy_ectr_ignore:
forall v´28 next pre msg tm stat next´ pre´ msg´ tm´ stat´ x1 x y z w v v´21,
(tick_rdy_ectr
(next
:: pre
:: Vptr x1
:: msg
:: tm
:: stat
:: Vint32 x
:: Vint32 y
:: Vint32 z
:: Vint32 w
:: Vint32 v :: nil) v´21
v´28) =
(tick_rdy_ectr
(next´
:: pre´
:: Vptr x1
:: msg´
:: tm´
:: stat´
:: Vint32 x
:: Vint32 y
:: Vint32 z
:: Vint32 w
:: Vint32 v :: nil) v´21
v´28).
Lemma tcbls_rtbl_timetci_update_hold:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´24 v´25 x7 i5 head rtbl tcbls,
isptr x7 ->
TCBList_P head v´22 rtbl tcbls ->
array_type_vallist_match Int8u v´9 ->
length v´9 = ∘OS_RDY_TBL_SIZE ->
Int.unsigned i <= 255 ->
Int.eq i6 ($ 0) = false ->
Int.eq (i6-ᵢ$ 1) ($ 0) = true ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
RL_TCBblk_P
(v´31
:: v´10
:: Vnull
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil) ->
RL_Tbl_Grp_P v´9 (Vint32 i) ->
tick_rdy_ectr
(v´31
:: v´10
:: x7
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
v´21 v´28 = Some v´24 ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: Vnull
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: V$OS_STAT_RDY
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
update_nth_val (Z.to_nat (Int.unsigned i2)) v´26
(val_inj (or (nth_val´ (Z.to_nat (Int.unsigned i2)) v´26) (Vint32 i1))),
Vint32 (Int.or v´27 i0), v´24).
Lemma tcbls_rtbl_timetci_update_hold´:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´25 x7 i5,
Int.eq i6 ($ 0) = false ->
Int.eq (i6-ᵢ$ 1) ($ 0) = false ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 (i6-ᵢ$ 1)
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
v´26,
Vint32 v´27, v´28).
Lemma tcbls_rtbl_timetci_update_hold´´:
forall v´22 v´9 i v´17 v´26 v´27 v´31 v´10 x6 i6 i4 i3 i2 i1 i0 v´21 v´28 v´25 x7 i5,
Int.eq i6 ($ 0) = true ->
tcbls_rtbl_timetci_update v´22 v´9 (Vint32 i) v´21 v´17 = Some (v´25, v´26, Vint32 v´27, v´28) ->
tcbls_rtbl_timetci_update
(v´22 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil) v´9 (Vint32 i) v´21 v´17 =
Some
(v´25 ++
(v´31
:: v´10
:: x7
:: x6
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3
:: Vint32 i2 :: Vint32 i1 :: Vint32 i0 :: nil)
:: nil,
v´26,
Vint32 v´27, v´28).
Definition rel_st_els (st : taskstatus) (els : EcbMod.map) :=
match st with
| (wait (os_stat_sem eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_q eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_mbox eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| (wait (os_stat_mutexsem eid) one) =>
match EcbMod.get els eid with
| Some (m, wl) => true
| None => false
end
| _ => true
end.
Definition R_Prio_No_Dup_L´ (ll:list vallist):=
forall n l ,
nth_vallist n ll = Some l ->
(
exists prio, V_OSTCBPrio l = Some (Vint32 prio) /\
forall n´ l´, n <> n´ ->
nth_vallist n´ ll = Some l´ ->
exists prio´,V_OSTCBPrio l´ = Some (Vint32 prio´) /\
prio <> prio´
).
Fixpoint Prio_Not_In (prio : int32) (ll : list vallist) {struct ll} :=
match ll with
| nil => True
| l :: ll´ => exists prio´, V_OSTCBPrio l = Some (Vint32 prio´)
/\ prio <> prio´ /\ Prio_Not_In prio ll´
end.
Fixpoint R_Prio_No_Dup_L (ll : list vallist) {struct ll} :=
match ll with
| nil => True
| l :: ll´ => exists prio,
V_OSTCBPrio l = Some (Vint32 prio) /\
Prio_Not_In prio ll´/\ R_Prio_No_Dup_L ll´
end.
Fixpoint not_in {A B:Type} (e:B) (l:list A) (f:A -> option B) :=
match l with
| nil => True
| h :: t => (forall e´, f h = Some e´ -> e´ <> e) /\ not_in e t f
end.
Fixpoint set_nth {A:Type} (n:nat) (v:A) (vl: list A) : option (list A) :=
match vl with
| nil => None
| h::t => match n with
| O => Some (v::t)
| S x => match set_nth x v t with
| Some r => Some (h::r)
| None => None
end
end
end.
Definition set_tcb_next (tcb:vallist) next := set_nth 0%nat next tcb.
Definition get_last_ecb_ptr :=
fun (l : list (vallist * vallist)) (x : val) =>
match l with
| nil => Some x
| _ :: _ => V_OSEventListPtr (fst (last l (nil,nil)))
end.
Fixpoint eq_next l1 l2:=
match l1,l2 with
| v1::l1´,v2::l2´ => nth_val 0%nat v1 = nth_val 0%nat v2 /\ eq_next l1´ l2´
| nil,nil => True
| _ ,_ => False
end.
Import TcbMod.
Lemma join_fst:
forall a b lstx (l:TcbMod.lb a lstx) (i:TcbMod.is_orderset lstx) (j:TcbMod.is_orderset ((a,b)::lstx)),
TcbMod.join (TcbMod.listset_con (lst:=lstx) i) (TcbMod.sig a b) (TcbMod.listset_con (lst:=(a, b) :: lstx)j).
Lemma disj_eqdom :
forall m1 m1´ m2,
disj m1 m2 -> eqdom m1 m1´ -> disj m1´ m2.
Lemma tcb_domeq_joinsig_ex:
forall x1 a b b´ x x1´,
TcbMod.join x1 (TcbMod.sig a b) x -> (forall t,TcbMod.indom x1 t <-> TcbMod.indom x1´ t) ->exists x´, TcbMod.join x1´ (TcbMod.sig a b´) x´.
Lemma int_dec_zero_one : forall n:int32,
n = Int.zero \/ n = Int.one \/ (Int.eq Int.one n = false /\ Int.eq Int.zero n = false).
Lemma tid_beq_true :
forall tid, tidspec.beq tid tid = true.
Lemma in_remove_tid : forall {l t1 t2}, In t1 (remove_tid t2 l) -> In t1 l.
Lemma in_remove_tid´ : forall l t1 t2, In t1 l -> t1 <> t2 -> In t1 (remove_tid t2 l).
Lemma joinsig_listset_con :
forall l a x i (j:lb a l),
joinsig a x (listset_con (lst:=l) i) (listset_con (lst:=(a, x):: l) (conj j i)).
Lemma tid_blt_false : forall tid, tidspec.blt tid tid = false.
Lemma lb_get_false :
forall (l:rlist) a b i, lb a l -> get (listset_con (lst:=l) i) a = Some b -> False.
Lemma isrupd_empisr:(isrupd (isrupd empisr 0%nat true) 0%nat false) = empisr.
Lemma ih_no_lvar
: forall (aop : absop) (isrreg : isr) (si : is) (cs : cs) (ie : ie),
<|| aop ||> ** Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** isr_inv ** OSInv ** A_dom_lenv nil ==>
<|| aop ||> **
Aisr isrreg ** Ais si ** Acs cs ** Aie ie ** [|exists k,gettopis si = k /\ forall j, (0 <= j < k)%nat -> isrreg j = false|] ** OSInv ** A_dom_lenv nil.
Lemma isrupd_true_false:
forall ir i,
isrupd (isrupd ir i true) i false = isrupd ir i false.
Lemma a_isr_is_prop_split:
forall s P isr is, s |= Aisr isr ** Ais is ** A_isr_is_prop ** P -> s |= Aisr isr ** Ais is ** P ** [| isr_is_prop isr is |].
Lemma tcbjoinsig_set_sub_sub:
forall t x tcbls tcbls´ tls y tls´,
TcbMod.joinsig t x tcbls tcbls´ ->
TcbMod.set tls t y = tls´ ->
TcbMod.sub tcbls´ tls ->
TcbMod.sub tcbls tls´.
Lemma sub_joinsig_set_sud:
forall tls_used tls t x x´ tls_used´ tls´,
TcbMod.sub tls_used tls ->
TcbMod.joinsig t x tls_used´ tls_used ->
TcbMod.set tls t x´ = tls´ ->TcbMod.sub tls_used´ tls´.
Lemma sub_joinsig_get:
forall tls_used tls t x tls_used´,
TcbMod.sub tls_used tls -> TcbMod.joinsig t x tls_used´ tls_used -> TcbMod.get tls t = Some x.
Lemma ecbmod_set_neq_change:
forall eid eid´ x a b,
eid <> eid´ ->
EcbMod.set (EcbMod.set x eid a) eid´ b =
EcbMod.set (EcbMod.set x eid´ b) eid a.
Lemma tcbmod_set_neq_change:
forall eid eid´ x a b,
eid <> eid´ ->
TcbMod.set (TcbMod.set x eid a) eid´ b =
TcbMod.set (TcbMod.set x eid´ b) eid a.
Lemma sub_emp:
forall x,
TcbMod.sub x emp -> x = emp.
Lemma joinsig_false:
forall t x y,
~ joinsig t x y emp.
Lemma tcb_joinsig_get_sub_ex:
forall t t´ st0 st1 tl1´ tl1 a tl2 tl2´,
t <> t´ ->
TcbMod.joinsig t st0 tl1´ tl1 ->
TcbMod.get tl1 t´ = Some a ->
TcbMod.sub tl1 tl2 ->
TcbMod.set tl2 t st1 = tl2´ ->
TcbMod.get tl1´ t´ = Some a /\
TcbMod.sub tl1´ tl2´ /\ exists x,
TcbMod.joinsig t´ a x tl1.
Lemma remove_tid_eq:
forall wl t t´ ,
remove_tid t´ (remove_tid t wl) = remove_tid t (remove_tid t´ wl).
Lemma ecbmod_set_eq:
forall x a b b´ c,
EcbMod.set (EcbMod.set x a b) a c =
EcbMod.set (EcbMod.set x a b´) a c.
Lemma joinsig3_neqtid_joinsig:
forall t0 t a x3 b x1 c y,
joinsig t a x3 b ->
joinsig t a x1 c ->
joinsig t0 y c b ->
joinsig t0 y x1 x3.
Lemma tcbjoin_joinsig_eq:
forall x y x1 z x2,
TcbJoin x y x1 z ->
TcbMod.joinsig x y x2 z -> x1 = x2.
Lemma tcbmod_sub_joinsig_sub:
forall a b x y z y´,
TcbMod.sub a b ->
TcbMod.joinsig x y z a ->
TcbMod.sub z (TcbMod.set b x y´).
Lemma tcb_minus_self_emp: forall x, TcbMod.minus x x = TcbMod.emp.
Lemma Prio_Not_In_ex :
forall ll a x,
Prio_Not_In x (a::ll) ->
Prio_Not_In x ll.
Lemma nth_vallist_inc_eq:
forall n´ a ll a0 l´,
0%nat <> n´ ->
(nth_vallist n´ (a :: ll) = Some l´ <->
nth_vallist (S n´) (a :: a0 :: ll) = Some l´).
Lemma tcbjoin_join_ex_join:
forall x x2 x1 tcbls´´ tcbx tcbls,
TcbJoin x x2 x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
exists y, TcbMod.join x1 tcbx y /\ TcbJoin x x2 y tcbls.
Lemma TCBList_P_nth_prio:
forall l n l´ (prio:priority) x0 x1 rtbl,
nth_vallist n l = Some l´ ->
V_OSTCBPrio l´ = Some (Vint32 prio) ->
TCBList_P x0 l rtbl x1 ->
exists tid st msg, TcbMod.get x1 tid = Some (prio,st,msg) .
Lemma tcbjoin_get_none:
forall x2 a x4 x1 x,
TcbJoin x2 a x4 x1 ->
TcbMod.get x1 x = None ->
TcbMod.get x4 x = None.
Lemma TCBList_P_imp_Prio_Not_In:
forall l tcbls x p t m x1 x0 rtbl,
TcbMod.get tcbls x = Some (p,t,m) ->
TcbMod.get x1 x = None ->
sub x1 tcbls ->
R_Prio_No_Dup tcbls ->
TCBList_P x0 l rtbl x1 ->
Prio_Not_In p l.
Lemma tcbjoin_get_n:
forall x y x1 tcbls,
TcbJoin x y x1 tcbls ->
TcbMod.get x1 x =None.
Lemma int_eq_false_false:
forall n,
Int.eq Int.one n = false ->
Int.eq n Int.zero = false ->
Int.eq (n-ᵢInt.one) Int.zero = false.
Lemma R_Prio_No_Dup_Convert :
forall ll, R_Prio_No_Dup_L´ ll -> R_Prio_No_Dup_L ll.
Lemma R_Prio_No_Dup_Convert_rev :
forall ll, R_Prio_No_Dup_L ll -> R_Prio_No_Dup_L´ ll.
Lemma R_Prio_No_Dup_Eq :
forall ll, R_Prio_No_Dup_L ll <-> R_Prio_No_Dup_L´ ll.
Lemma R_Prio_No_Dup_Sub_hold:
forall x3 tcbls,
sub x3 tcbls ->
R_Prio_No_Dup tcbls ->
R_Prio_No_Dup x3.
Lemma r_prio_no_dup_join_imp:
forall l tcbls´´ tcbx tcbls v rtbl,
join tcbls´´ tcbx tcbls ->
R_Prio_No_Dup tcbls ->
TCBList_P v l rtbl tcbls´´ ->
R_Prio_No_Dup_L l.
Ltac solve_tblk :=
unfolds; splits;
try solve [unfolds; simpl; auto];
try solve [do 6 eexists;splits; try unfolds; simpl; eauto; splits; eauto;
eexists;split; [unfolds; simpl;eauto | auto]].
Lemma tickchange_eq_ostcbnext:
forall l x0 rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´,
V_OSTCBNext l = Some x0 ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
V_OSTCBNext l´ = Some x0.
Lemma joinsig_joinsig_neq :
forall {a1 a2 x1 x2 m2 m2´ m3},
joinsig a1 x1 m2 m3 -> joinsig a2 x2 m2´ m2 -> a1 <> a2.
Lemma joinsig_joinsig_neq_ecb :
forall {a1 a2 x1 x2 m2 m2´ m3},
EcbMod.joinsig a1 x1 m2 m3 -> EcbMod.joinsig a2 x2 m2´ m2 -> a1 <> a2.
Lemma neq_set_comm :
forall a1 a2 x1 x2 m,
a1 <> a2 -> set (set m a1 x1) a2 x2 = set (set m a2 x2) a1 x1.
Lemma tickstep´_other_get_eq:
forall x y tcbls´´ y´ x3 tcbls´ els´ x1 tcbls,
TcbJoin x y x1 tcbls´´ ->
tickstep´ (set tcbls x y´) x3 tcbls´ els´ x1 ->
TcbMod.get tcbls´ x = Some y´.
Lemma tcb_joinsig_join_get_minus_eq:
forall x y x1 tcbls´´ tcbx tcbls y´ tcbls´,
TcbJoin x y x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
TcbMod.get tcbls´ x = Some y´ ->
TcbJoin x y´ (minus (minus tcbls´ tcbx) (sig x y´))
(minus tcbls´ tcbx).
Lemma tcb_minus_mergesig_minus_minus_eq:
forall tcbls´ x y tcbx,
TcbMod.minus tcbls´ (TcbMod.merge (TcbMod.sig x y) tcbx) =
TcbMod.minus (TcbMod.minus tcbls´ tcbx) (TcbMod.sig x y).
Lemma r_prio_no_dup_setst_hold:
forall x p t m x1 tcbls´´ tcbx tcbls x2,
TcbJoin x (p, t, m) x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
R_Prio_No_Dup tcbls ->
R_Prio_No_Dup (TcbMod.set tcbls x (p, x2, m)).
Lemma joinsig_join_joinmergesig_eq_set:
forall x y x1 tcbls´´ tcbx tcbls y´,
TcbMod.joinsig x y x1 tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
TcbMod.join x1 (TcbMod.merge (TcbMod.sig x y´) tcbx) (TcbMod.set tcbls x y´).
Lemma tcb_minus_emp_eq: forall x, TcbMod.minus x TcbMod.emp = x.
Lemma tickstep_l_get_last_tcb_ptr_eq´:
forall v´25 v´26 v´27 v´28 v´33 (v´39:int32) head els x1 x2 x3 (x6:int32) xx els´ i1 i2,
tickstep_l (v´25 ++ v´26 :: v´27) v´28 i1 head els
(x1 ++ x2 :: x3) v´33 i2 els´ ->
length v´25 = length x1 ->
get_last_tcb_ptr x1 xx = get_last_tcb_ptr v´25 xx.
Lemma tickstep_l_get_last_tcb_ptr_eq:
forall v´25 v´26 v´27 v´28 v´33 v´39 head els x1 x2 x3 x6 xx els´,
tickstep_l (v´25 ++ v´26 :: v´27) v´28 (Vint32 v´39) head els
(x1 ++ x2 :: x3) v´33 (Vint32 x6) els´ ->
length v´25 = length x1 ->
get_last_tcb_ptr x1 xx = get_last_tcb_ptr v´25 xx.
Lemma tcbls_rtbl_timetci_update_tls_eq_next:
forall v´25 v´28 v´29 x1 x4 x5 head els els´,
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
eq_next v´25 x1.
Lemma tcbls_rtbl_timetci_update_tls_link:
forall v´25 v´15 v´23 v´28 v´29 x1 x4 x5 head els els´,
v´25 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
v´25 <> nil /\ last v´25 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)) ->
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
x1 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
x1 <> nil /\ last x1 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)).
Lemma tcbls_rtbl_timetci_update_tls_split:
forall v´25 v´15 v´23 v´28 v´29 x1 x4 x5 v´32 x2 x3 s P head els els´,
v´25 = nil /\ Vptr v´15 = Vptr v´23 \/
(exists vl,
v´25 <> nil /\ last v´25 nil = vl /\ nth_val 0 vl = Some (Vptr v´15)) ->
tcbls_rtbl_timetci_update v´25 v´28 v´29 head els = Some (x1, x4, x5,els´) ->
s |= tcbdllseg (Vptr v´23) Vnull v´32 Vnull (x1 ++ x2 :: x3) ** P ->
s |= EX x, tcbdllseg (Vptr v´23) Vnull x (Vptr v´15) x1 **
tcbdllseg (Vptr v´15) x v´32 Vnull (x2::x3) ** P.
Lemma tcbls_rtbl_timetci_update_rgrp_vint:
forall a b c a´ b´ c´ d e e´,
tcbls_rtbl_timetci_update a b (Vint32 c) d e= Some (a´,b´,c´,e´) ->
exists x, c´ = Vint32 x.
Lemma tick_fixpoint_convert:
forall vl x y head els vl´ x´ y´ els´,
tcbls_rtbl_timetci_update vl x y head els = Some (vl´, x´, y´, els´) ->
tickstep_l vl x y head els vl´ x´ y´ els´.
Lemma tick_fixpoint_convert_rev:
forall vl x y head els vl´ x´ y´ els´,
tickstep_l vl x y head els vl´ x´ y´ els´ ->
tcbls_rtbl_timetci_update vl x y head els = Some (vl´, x´, y´, els´).
Lemma tcbls_rtbl_timetci_update_len_eq´:
forall v´24 v´27 v´39 v´40 x1 x4 x5 x6 i,
tcbls_rtbl_timetci_update v´24 v´27 i v´39 v´40 =
Some (x1, x4, x5, x6) ->
length v´24 = length x1.
Lemma tcbls_rtbl_timetci_update_len_eq:
forall v´24 v´27 v´38 v´39 v´40 x1 x4 x5 x6,
tcbls_rtbl_timetci_update v´24 v´27 (Vint32 v´38) v´39 v´40 =
Some (x1, x4, x5, x6) ->
length v´24 = length x1.
Lemma tickchange_shift :
forall t t´ a els b els´ c d els´´,
t <> t´ ->
tickchange t a els b els´ ->
tickchange t´ c els´ d els´´ ->
exists x, tickchange t´ c els d x /\ tickchange t a x b els´´.
Lemma join_join_merge :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m1 -> join m4 (merge m5 m2) m3.
Lemma join_join_merge´ :
forall m1 m2 m3 m4 m5,
join m1 m2 m3 -> join m4 m5 m1 -> join m4 (merge m2 m5) m3.
Lemma join_join_merge_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m1 -> EcbMod.join m4 (EcbMod.merge m5 m2) m3.
Lemma join_join_merge´_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m1 -> EcbMod.join m4 (EcbMod.merge m2 m5) m3.
Lemma tcb_join_joinsig_ex_joinsig:
forall htls´´ tcbx htls x y x1,
join htls´´ tcbx htls ->
joinsig x y x1 htls´´ ->
exists z, joinsig x y z htls.
Lemma nth_vallist_append : forall l1 l2 n x, nth_vallist n l1 = Some x -> nth_vallist n (l1++l2) = Some x.
Lemma Prio_Not_In_app :
forall l2 l3 x,
Prio_Not_In x (l2 ++ l3) -> Prio_Not_In x l2.
Lemma R_Prio_No_Dup_L_proc : forall a l, R_Prio_No_Dup_L (a::l) -> R_Prio_No_Dup_L (l).
Lemma r_prio_no_dup_l_mid:
forall l1 l2 l3,
R_Prio_No_Dup_L (l1++l2++l3) ->
R_Prio_No_Dup_L l2.
Lemma tcbjoin_set:
forall (x:addrval) y y´ htls1 htls,
TcbJoin x y htls1 htls ->
TcbJoin x y´ htls1 (set htls x y´).
Lemma joinsig_eq : forall x y1 y2 m1 m2 m3, joinsig x y1 m1 m3 -> joinsig x y2 m2 m3 -> y1 = y2.
Lemma join_tcbjoin_joinsig_eq´
: forall (x : tidspec.A) (y1 y2 : abstcb.B) (x1 z x2 : map),
TcbJoin x y1 x1 z -> joinsig x y2 x2 z-> y1 = y2.
Lemma V_OSTCBNext_set_tcb_next :
forall v x1 x2, V_OSTCBNext v = Some x1 -> exists x´, set_tcb_next v x2 = Some x´.
Lemma set_nth_nth_val :
forall n l x l´, set_nth n x l = Some l´ -> nth_val n l´ = Some x.
Lemma set_nth_nth_val´ :
forall l l´ n1 n2 x, n1 <> n2 -> set_nth n1 x l = Some l´ -> nth_val n2 l´ = nth_val n2 l.
Lemma TCBNode_P_change_next_ptr :
forall vl vl´ rtbl abstcb x,
TCBNode_P vl rtbl abstcb -> set_tcb_next vl x = Some vl´ ->
TCBNode_P vl´ rtbl abstcb.
Lemma V_OSTCBMsg_change_next_ptr :
forall vl vl´ a x,
V_OSTCBMsg vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBMsg vl´ = Some a.
Lemma V_OSTCBPrio_change_next_ptr :
forall vl vl´ a x,
V_OSTCBPrio vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBPrio vl´ = Some a.
Lemma V_OSTCBX_change_next_ptr :
forall vl vl´ a x,
V_OSTCBX vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBX vl´ = Some a.
Lemma V_OSTCBY_change_next_ptr :
forall vl vl´ a x,
V_OSTCBY vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBY vl´ = Some a.
Lemma V_OSTCBBitX_change_next_ptr :
forall vl vl´ a x,
V_OSTCBBitX vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBBitX vl´ = Some a.
Lemma V_OSTCBBitY_change_next_ptr :
forall vl vl´ a x,
V_OSTCBBitY vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBBitY vl´ = Some a.
Lemma V_OSTCBStat_change_next_ptr :
forall vl vl´ a x,
V_OSTCBStat vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBStat vl´ = Some a.
Lemma V_OSTCBEventPtr_change_next_ptr :
forall vl vl´ a x,
V_OSTCBEventPtr vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBEventPtr vl´ = Some a.
Lemma V_OSTCBDly_change_next_ptr :
forall vl vl´ a x,
V_OSTCBDly vl = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBDly vl´ = Some a.
Lemma V_OSTCBPrio_change_next_ptr´ :
forall vl vl´ prio x,
V_OSTCBPrio vl´ = Some prio -> set_tcb_next vl x = Some vl´ ->
V_OSTCBPrio vl = Some prio.
Lemma V_OSTCBDly_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBDly vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBDly vl = Some a.
Lemma V_OSTCBStat_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBStat vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBStat vl = Some a.
Lemma V_OSTCBEventPtr_change_next_ptr´ :
forall vl vl´ a x,
V_OSTCBEventPtr vl´ = Some a -> set_tcb_next vl x = Some vl´ ->
V_OSTCBEventPtr vl = Some a.
Lemma RdyTCBblk_change_next_ptr :
forall vl x vl´ rtbl prio,
RdyTCBblk vl rtbl prio -> set_tcb_next vl x = Some vl´ -> RdyTCBblk vl´ rtbl prio.
Lemma RdyTCBblk_change_next_ptr´ :
forall vl x vl´ rtbl prio,
RdyTCBblk vl´ rtbl prio -> set_tcb_next vl x = Some vl´ -> RdyTCBblk vl rtbl prio.
Qed.
Lemma TCBList_P_not_in_remove_last :
forall l head rtbl htls,
TCBList_P head l rtbl htls -> not_in head (removelast l) V_OSTCBNext.
Lemma get_last_tcb_ptr_in :
forall l a head x,
get_last_tcb_ptr (a::l) head = Some x -> ~ (not_in x (a::l) V_OSTCBNext).
Lemma not_in_remove_last :
forall {A B:Type} l1 l2 (a:A) (x:B) f,
not_in x (removelast (l1 ++ a :: l2)) f -> not_in x l1 f.
Lemma tcblist_p_tid_neq´:
forall ltlsy´´ a a1 h x l rtbl htls,
get_last_tcb_ptr (a :: ltlsy´´) h = Some (Vptr x) -> TCBList_P h ((a :: ltlsy´´) ++ (a1::l)) rtbl htls ->
h <> Vptr x.
Lemma joinsig_emp : forall m a x, joinsig a x emp m -> m = sig a x.
Lemma join_sig_false : forall a x1 x2 m, join (sig a x1) (sig a x2) m -> False.
Lemma join_sig_neq_set : forall a x m1 m2 a1 x1, a <> a1 -> joinsig a x m1 m2 -> joinsig a x (set m1 a1 x1) (set m2 a1 x1).
Lemma tcbjoin_neq:
forall x x0 x6 x5 htls y,
Vptr x <> Vptr x0 ->
TcbJoin x0 x6 x5 htls ->
TcbJoin x0 x6 (set x5 x y) (set htls x y).
Lemma r_prio_no_dup_two_neq:
forall a l l1 l2 ll,
R_Prio_No_Dup_L ((a :: l1) ++ (l :: ll) ++ l2) ->
V_OSTCBPrio a <> V_OSTCBPrio l.
Lemma joinsig_in_other :
forall m1 m2 m3 a1 x1 a2 x2, a1 <> a2 -> joinsig a1 x1 m1 m3 -> joinsig a2 x2 m2 m3 -> get m2 a1 = Some x1.
Lemma joinsig_get_minus : forall a x m, get m a = Some x -> joinsig a x (minus m (sig a x)) m.
Lemma tcb_neq_joinsig_tcbjoin_joinsig_minus:
forall x0 x y htls´´ htls x5 x4,
Vptr x0 <> Vptr x ->
joinsig x y htls´´ htls ->
TcbJoin x0 x5 x4 htls ->
joinsig x y (minus x4 (sig x y)) x4.
Lemma get_last_ecb_ptr_eq:
forall head x9 x0 x6 x2 htls eid,
ECBList_P head (Vptr x9) x0 x6 x2 htls ->
get_last_ecb_ptr x0 head = Some (Vptr eid) ->
x9 = eid.
Lemma ECBList_P_get_last_ecb_ptr:
forall {l1 l2 m1 m2 head x},
ECBList_P head (Vptr x) l1 l2 m1 m2 ->
get_last_ecb_ptr l1 head = Some (Vptr x).
Lemma ECBList_P_get_last_ecb_ptr_split_joinsig:
forall l1 l2 l3 m1 m2 e a head tail,
ECBList_P head tail (l1 ++ e :: l2) l3 m1 m2 ->
get_last_ecb_ptr l1 head = Some (Vptr a) ->
exists m11 m12 mx x, EcbMod.join m11 m12 m1 /\ EcbMod.joinsig a x mx m12.
Lemma join_join_merge_1_ecb :
forall m1 m2 m3 m4 m5,
EcbMod.join m1 m2 m3 -> EcbMod.join m4 m5 m2 ->
EcbMod.join m1 m4 (EcbMod.merge m1 m4).
Lemma ECBList_P_els_get_split :
forall {els edata head tail tcbls hels m wl eptr},
ECBList_P head tail els edata hels tcbls ->
EcbMod.get hels eptr = Some (m, wl) ->
exists els1 els2 edata1 edata2 hels1 hels2,
ECBList_P head (Vptr eptr) els1 edata1 hels1 tcbls /\
ECBList_P (Vptr eptr) tail els2 edata2 hels2 tcbls /\
els = els1 ++ els2 /\ edata = edata1 ++ edata2 /\
EcbMod.join hels1 hels2 hels.
Lemma ECBList_P_vptr :
forall l1 l2 m1 m2 head tail a,
ECBList_P head tail (a::l1) l2 m1 m2 ->
(exists x, head = Vptr x).
Lemma ECBList_P_get_eidls_not_in :
forall {l1 l2 l3 m1 m2 e x h head tail},
ECBList_P head tail (((h::l1)++e::nil)++l2) l3 m1 m2 ->
get_last_ecb_ptr (h::l1) head = Some x ->
~In x (get_eidls head (h::l1)).
Lemma ecblist_p_compose´:
forall p qid mqls qptrl1 qptrl2 i i1 a x3 p´ v´41
msgqls1 msgqls2 msgq mqls1 mqls2 mq mqls´ tcbls x,
R_ECB_ETbl_P qid
(x
:: Vint32 i :: i1 :: a :: x3 :: p´ :: nil, v´41) tcbls ->
ECBList_P p (Vptr qid) qptrl1 msgqls1 mqls1 tcbls->
ECBList_P p´ Vnull qptrl2 msgqls2 mqls2 tcbls->
RLH_ECBData_P msgq mq ->
EcbMod.joinsig qid mq mqls2 mqls´->
EcbMod.join mqls1 mqls´ mqls ->
ECBList_P p Vnull (qptrl1 ++ ((x
:: Vint32 i :: i1 :: a :: x3 :: p´ :: nil, v´41)::nil) ++ qptrl2) (msgqls1 ++ (msgq::nil) ++msgqls2) mqls tcbls.
Lemma ecbmod_get_joinsig_join_eq:
forall eid x1´ x1 x2 x3 x4 hels,
EcbMod.get hels eid = Some x1´ ->
EcbMod.joinsig eid x1 x2 x4 ->
EcbMod.join x3 x4 hels ->
x1 = x1´.
Lemma ECBList_P_Set_Rdy_SEM_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_sem eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ECBList_P_Set_Rdy_MBOX_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma ECBList_P_Set_Rdy_MUTEX_hold:
forall a tcbls tid prio msg msg´ x y b c eid nl,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mutexsem eid) nl, msg) ->
EcbMod.get c eid = None ->
ECBList_P x y a b c tcbls ->
ECBList_P x y a b c (TcbMod.set tcbls tid (prio,rdy,msg´)).
Lemma tcblist_p_imp_tcbnode_p:
forall htls x y l1 h l ll l2 rtbl,
TcbMod.get htls x = Some y ->
get_last_tcb_ptr l1 h = Some (Vptr x) ->
TCBList_P h (l1++(l::ll)++l2) rtbl htls ->
TCBNode_P l rtbl y.
Lemma ecblist_p_wait_set_rdy:
forall ectr´ htls x p t m head Vnull edata x3,
get htls x = Some (p, wait os_stat_time t, m) ->
ECBList_P head Vnull ectr´ edata x3 htls ->
ECBList_P head Vnull ectr´ edata x3 (set htls x (p, rdy, m)).
Lemma r_ecb_etbl_p_wait_rdy_hold:
forall x x0 a htls n m m´ p,
TcbMod.get htls x = Some (p, wait os_stat_time n, m) ->
R_ECB_ETbl_P x0 a htls ->
R_ECB_ETbl_P x0 a (set htls x (p, rdy, m´)).
Qed.
Lemma ecblist_p_stat_time_minus1_eq:
forall ectr htls x p n m head edata x3 st,
get htls x = Some (p, wait st n, m) ->
ECBList_P head Vnull ectr edata x3 htls ->
ECBList_P head Vnull ectr edata x3
(set htls x (p, wait st (n-ᵢInt.one), m)).
Lemma r_ecb_etbl_p_tcbstats_eq_hold:
forall x x0 a htls (st:tcbstats) n m n´ m´ p,
TcbMod.get htls x = Some (p, wait st n, m) ->
R_ECB_ETbl_P x0 a htls ->
R_ECB_ETbl_P x0 a (set htls x (p, wait st n´, m´)).
Qed.
Import TcbMod.
Lemma tickchange_exists: forall t st els,
rel_st_els st els = true ->
exists st´ els´, tickchange t st els st´ els´.
Lemma RH_TCBList_ECBList_P_rel_st_els :
forall els tls ct t p st msg,
TcbMod.get tls t = Some (p, st, msg) ->
RH_TCBList_ECBList_P els tls ct -> rel_st_els st els = true.
Lemma RH_TCBList_ECBList_SEM_P_tickchange : forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_SEM_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_SEM_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_MBOX_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_MBOX_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_MBOX_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma rh_tcblist_ecblist_mutex_owner_set:
forall els´ tls t x y,
RH_TCBList_ECBList_MUTEX_OWNER els´ tls ->
get tls t = Some x ->
RH_TCBList_ECBList_MUTEX_OWNER els´
(set tls t y) .
Lemma rh_tcblist_ecblist_mutex_owner_set´:
forall els tls t m wl eid,
RH_TCBList_ECBList_MUTEX_OWNER els tls ->
EcbMod.get els eid = Some (m, wl) ->
RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set els eid (m, remove_tid t wl))
tls .
Lemma RH_TCBList_ECBList_MUTEX_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_MUTEX_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_MUTEX_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_Q_P_tickchange :
forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_Q_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_Q_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma RH_TCBList_ECBList_P_tickchange : forall tls els els´ ct t p st st´ msg,
RH_TCBList_ECBList_P els tls ct ->
TcbMod.get tls t = Some (p, st, msg) ->
tickchange t st els st´ els´ ->
RH_TCBList_ECBList_P els´ (TcbMod.set tls t (p, st´, msg)) ct.
Lemma tickstep_exists´´:
forall tls_used tls els ct,
RH_TCBList_ECBList_P els tls ct ->
TcbMod.sub tls_used tls ->
exists tls´ els´, tickstep´ tls els tls´ els´ tls_used.
Lemma tickstep_exists´:
forall tls els ct,
RH_TCBList_ECBList_P els tls ct ->
exists tls´ els´, tickstep tls els tls´ els´.
Lemma tickstep_exists:
forall tls els ct,
exists tls´ els´, RH_TCBList_ECBList_P els tls ct ->
tickstep tls els tls´ els´.
Lemma tickstep_rh_curtcb´:
forall tls els tls´ els´ tls´´ ct,
tickstep´ tls els tls´ els´ tls´´ ->
sub tls´´ tls ->
RH_CurTCB ct tls -> RH_CurTCB ct tls´.
Lemma tickstep_rh_curtcb:
forall ct tls els tls´ els´,
tickstep tls els tls´ els´ ->
RH_CurTCB ct tls -> RH_CurTCB ct tls´.
Lemma tickstep_rh_tcblist_ecblist_p´:
forall ct tls els tls´ els´ tls´´,
TcbMod.sub tls´´ tls ->
tickstep´ tls els tls´ els´ tls´´-> RH_TCBList_ECBList_P els tls ct -> RH_TCBList_ECBList_P els´ tls´ ct.
Lemma tickstep_rh_tcblist_ecblist_p: forall ct tls els tls´ els´, tickstep tls els tls´ els´-> RH_TCBList_ECBList_P els tls ct -> RH_TCBList_ECBList_P els´ tls´ ct.
Lemma tickstep_r_priotbl_p´:
forall v´36 v´12 x x0 v´4 tls vhold,
TcbMod.sub tls v´36 ->
tickstep´ v´36 v´12 x x0 tls-> R_PrioTbl_P v´4 v´36 vhold-> R_PrioTbl_P v´4 x vhold.
Lemma tickstep_r_priotbl_p:
forall v´36 v´12 x x0 v´4 vhold,
tickstep v´36 v´12 x x0 -> R_PrioTbl_P v´4 v´36 vhold-> R_PrioTbl_P v´4 x vhold.
Lemma rl_rtbl_priotbl_p_set_hold:
forall next pre eptr msg stat dly i1 i2 i3 i4 i5 v1 v3 ptbl x rtbl vhold,
x <> vhold ->
RL_TCBblk_P
(next
:: pre
:: eptr
:: msg
:: stat
:: dly
:: Vint32 i1
:: Vint32 i2
:: Vint32 i3 :: Vint32 i4 :: Vint32 i5 :: nil) ->
nth_val (Z.to_nat (Int.unsigned i3)) rtbl = Some v1 ->
or v1 (Vint32 i4) = Some v3 ->
RL_RTbl_PrioTbl_P rtbl ptbl vhold ->
nth_val (nat_of_Z (Int.unsigned i1)) ptbl = Some (Vptr x) ->
RL_RTbl_PrioTbl_P (update_nth_val (Z.to_nat (Int.unsigned i3)) rtbl v3) ptbl vhold.
Lemma tcbls_rtbl_timetci_update_rl_rtbl_priotbl_p´:
forall a b c a´ b´ c´ v´4 head els els´ vhold,
RL_TCBListblk_P a ->
RL_PrioTbl_P v´4 a vhold ->
tcbls_rtbl_timetci_update a b (Vint32 c) head els=
Some (a´, b´, Vint32 c´,els´) ->
RL_RTbl_PrioTbl_P b v´4 vhold ->
RL_RTbl_PrioTbl_P b´ v´4 vhold.
Lemma tcbls_rtbl_timetci_update_rl_rtbl_priotbl_p:
forall a b c a´ b´ c´ v´4 head els els´ tls x vhold,
TCBList_P x a b tls ->
RL_PrioTbl_P v´4 a vhold ->
tcbls_rtbl_timetci_update a b (Vint32 c) head els=
Some (a´, b´, Vint32 c´,els´) ->
RL_RTbl_PrioTbl_P b v´4 vhold ->
RL_RTbl_PrioTbl_P b´ v´4 vhold.
Lemma tickstep_decompose :
forall t p st msg tcbls tcbls´´ els els´ tcbls´,
TcbMod.get tcbls´´ t = Some (p, st, msg) ->
TcbMod.sub tcbls´´ tcbls ->
tickstep´ tcbls els tcbls´ els´ tcbls´´ ->
exists st´ els´´ ts tc,
joinsig t (p, st, msg) ts tcbls´´ /\
tickchange t st els st´ els´´ /\
TcbMod.set tcbls t (p,st´,msg) = tc /\
tickstep´ tc els´´ tcbls´ els´ ts /\
TcbMod.sub ts tc.
Lemma tickchange_nodup:
forall l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ll,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
R_Prio_No_Dup_L (l :: ll) ->
R_Prio_No_Dup_L (l´ :: ll).
Lemma set_rdy_grp_simpl:
forall x0 rgrp rgrp´ rtbl rtbl´,
Int.unsigned x0 < 64 ->
set_rdy_grp (Vint32 ($ 1<<(Int.shru x0 ($ 3)))) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 ($ 1<<(x0&$ 7))) (Vint32 (Int.shru x0 ($ 3))) rtbl = Some rtbl´ ->
exists i g,
nth_val (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))) rtbl = Some (Vint32 i) /\
rgrp = Vint32 g /\ rgrp´ = Vint32 (Int.or g ($ 1<<(Int.shru x0 ($ 3)))) /\
rtbl´ = update_nth_val (Z.to_nat (Int.unsigned (Int.shru x0 ($ 3)))) rtbl
(Vint32 (Int.or i ($ 1<<(x0&$ 7)))) /\ Int.unsigned (Int.shru x0 ($ 3)) <8 /\ Int.unsigned (x0&$ 7) < 8.
Lemma tickchange_tcbnode_p_hold:
forall l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x t els t´ els´ p m,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
tickchange x t els t´ els´ ->
TCBNode_P l rtbl (p, t, m) ->
TCBNode_P l´ rtbl´ (p, t´, m).
Lemma tickchange_other_tcbnode_p_hold´:
forall a l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x6,
V_OSTCBPrio a <> V_OSTCBPrio l ->
RL_TCBblk_P l ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
TCBNode_P a rtbl x6 -> TCBNode_P a rtbl´ x6.
Fixpoint RL_TCBblk_P_List (ll : list vallist):=
match ll with
| nil => True
| l :: ll´ => RL_TCBblk_P l /\ RL_TCBblk_P_List ll´
end.
Lemma tickchange_other_tcbnode_p_hold:
forall l´ ll rtbl´ x rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´,
tickstep_l ll rtbl´ rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´ ->
R_Prio_No_Dup_L (l´ :: ll) ->
RL_TCBblk_P_List ll ->
TCBNode_P l´ rtbl´ x ->
TCBNode_P l´ rtbl´´ x.
Lemma timetick_idle_in_rtbl:
forall rtbl tls rgrp head els els´ rgrp´ rtbl´ tls´ ,
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
RL_TCBblk_P_List tls->
tcbls_rtbl_timetci_update tls rtbl
(Vint32 rgrp) head els = Some (tls´, rtbl´, Vint32 rgrp´, els´) ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl´.
Lemma tickchange_other_tcblist_p_hold:
forall ll l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ x0 x1,
R_Prio_No_Dup_L (l :: ll) ->
RL_TCBblk_P l ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
TCBList_P x0 ll rtbl x1 ->
TCBList_P x0 ll rtbl´ x1 .
Lemma TCBList_P_imp_RL:
forall ll x0 rtbl x1,
TCBList_P x0 ll rtbl x1 ->
RL_TCBblk_P_List ll.
Lemma timetick_tcblist_prop_hold:
forall vl x y v head ls vl´ x´ y´ els els´ ls´ tcbls tcbls´ tcbls´´ tcbx,
tickstep_l vl x y head ls vl´ x´ y´ ls´ ->
R_Prio_No_Dup tcbls ->
TCBList_P v vl x tcbls´´ ->
TcbMod.join tcbls´´ tcbx tcbls ->
tickstep´ tcbls els tcbls´ els´ tcbls´´ ->
TCBList_P v vl´ x´ (TcbMod.minus tcbls´ tcbx).
Lemma timetick_tcblist_p:
forall v´25 v´26 v´27 v´28 v´39 x1 x2 x3 v´33 x6 v´37 v´15 v´38 v´23 v´36 x0 v´12 x head els els´,
length v´25 = length x1 ->
tcbls_rtbl_timetci_update (v´25 ++ v´26 :: v´27) v´28 (Vint32 v´39) head els=
Some (x1 ++ x2 :: x3, v´33, Vint32 x6, els´) ->
get_last_tcb_ptr v´25 (Vptr v´23) = Some (Vptr v´15) ->
TCBList_P (Vptr v´23) v´25 v´28 v´37 ->
TCBList_P (Vptr v´15) (v´26 :: v´27) v´28 v´38 ->
tickstep v´36 v´12 x x0 ->
TcbMod.join v´37 v´38 v´36 ->
R_Prio_No_Dup v´36 ->
exists tl1 tl2, TcbMod.join tl2 tl1 x /\ TCBList_P (Vptr v´15) (x2 :: x3) v´33 tl1 /\ TCBList_P (Vptr v´23) x1 v´33 tl2.
Lemma tick_rdy_ectr´_decompose :
forall el1 el2 x eptr e vl ectr´ edl hels htls,
get_last_ecb_ptr el1 (Vptr x) = Some (Vptr eptr) ->
~ In (Vptr eptr) (get_eidls (Vptr x) el1) ->
tick_rdy_ectr´ eptr vl (Vptr x) (el1 ++ e :: el2) = Some ectr´->
ECBList_P (Vptr x) Vnull (el1 ++ e :: el2) edl hels htls ->
exists x, rdy_ectr vl e = Some x /\ ectr´ = (el1 ++ x :: el2).
Lemma tick_rdy_ectr_split:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ m wl hels htls edata,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´ ->
EcbMod.get hels eptr = Some (m, wl) ->
ECBList_P head Vnull ectr edata hels htls ->
exists l1 l2 a b a´ b´ c d e,
rdy_ectr (vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil) (a,b) = Some (a´,b´) /\
ectr = l1 ++ ((a,b)::nil) ++ l2 /\
edata = c ++ (e::nil) ++ d /\
length c = length l1 /\
ectr´ = l1 ++ ((a´,b´)::nil) ++ l2 /\
get_last_ecb_ptr l1 head = Some (Vptr eptr).
Lemma ecblist_p_tick_rdy_ectr_q:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_q eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_sem:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_sem eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_mbox:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_mbox eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma ecblist_p_tick_rdy_ectr_mutexsem:
forall ectr head vnext vprev eptr msg vdly stat prio vx vy vbitx vbity ectr´ ,
tick_rdy_ectr´ eptr
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
head ectr = Some ectr´->
forall htls x p m x0 eid edata hels cur m0 wl rtbl,
get htls x = Some (p, wait x0 Int.one, m) ->
x0 = os_stat_mutexsem eid ->
ECBList_P head Vnull ectr edata hels htls ->
RH_TCBList_ECBList_P hels htls cur ->
EcbMod.get hels eid = Some (m0, wl) ->
TCBNode_P
(vnext
:: vprev
:: Vptr eptr
:: msg
:: Vint32 vdly
:: stat
:: Vint32 prio
:: Vint32 vx
:: Vint32 vy
:: Vint32 vbitx :: Vint32 vbity :: nil)
rtbl (p, wait x0 Int.one, m) ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata
(EcbMod.set hels eid (m0, remove_tid x wl)) (set htls x (p, rdy, m)).
Lemma tickchange_ecblist_p:
forall h p l rtbl rgrp htls l1 l2 ll hels cur x t x2 x3 head ectr ectr´ edata l´ rgrp´ rtbl´ (m:msg),
TcbMod.get htls x = Some (p, t, m) ->
get_last_tcb_ptr l1 h = Some (Vptr x) ->
TCBList_P h (l1++(l::ll)++l2) rtbl htls ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
R_Prio_No_Dup_L (l1++(l::ll)++l2) ->
RH_TCBList_ECBList_P hels htls cur ->
tickchange x t hels x2 x3 ->
ECBList_P head Vnull ectr edata hels htls ->
R_Prio_No_Dup htls ->
ECBList_P head Vnull ectr´ edata x3 (TcbMod.set htls x (p, x2, m)).
Lemma tickchange_tcblist_p_hold_mid:
forall ltlsy´´ x p t m htls´´ htls rtbl hels x2 x3
l rgrp head ectr l´ rtbl´ rgrp´ ectr´ h ll ltlsx´´ ,
joinsig x (p, t, m) htls´´ htls ->
tickchange x t hels x2 x3 ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
get_last_tcb_ptr ltlsy´´ h = Some (Vptr x) ->
TCBList_P h (ltlsy´´ ++ (l :: ll) ++ ltlsx´´) rtbl htls ->
R_Prio_No_Dup_L (ltlsy´´ ++ (l :: ll) ++ ltlsx´´) ->
TCBList_P h ((ltlsy´´ ++ l´ :: nil) ++ ll ++ ltlsx´´) rtbl´
(set htls x (p, x2, m)).
Lemma tickstep_ecblist_p´:
forall ltls´´ rtbl rgrp head lels ltls´ rtbl´ rgrp´ lels´,
tickstep_l ltls´´ rtbl rgrp head lels ltls´ rtbl´ rgrp´ lels´ ->
forall htls edata cur hels hels´ htls´ h ltlsx´´ ltls tcbx ltlsy´´ htls´´ h´,
R_Prio_No_Dup htls ->
tickstep´ htls hels htls´ hels´ htls´´->
ltls = ltlsy´´++ ltls´´ ++ ltlsx´´ ->
get_last_tcb_ptr ltlsy´´ h = Some h´ ->
TCBList_P h´ ltls´´ rtbl htls´´ ->
TCBList_P h ltls rtbl htls ->
TcbMod.join htls´´ tcbx htls ->
RH_TCBList_ECBList_P hels htls cur ->
ECBList_P head Vnull lels edata hels htls ->
ECBList_P head Vnull lels´ edata hels´ htls´.
Lemma tickstep_ecblist_p:
forall h h´ ltls1 ltls2 htls lels hels cur rgrp rtbl head edata rtbl´ rgrp´ hels´ htls´ lels´ ltls´ htls1 htls2,
TcbMod.join htls1 htls2 htls ->
TCBList_P h ltls1 rtbl htls1 ->
TCBList_P h´ ltls2 rtbl htls2 ->
RH_TCBList_ECBList_P hels htls cur ->
tcbls_rtbl_timetci_update (ltls1++ltls2) rtbl
rgrp head lels =
Some (ltls´, rtbl´, rgrp´, lels´) ->
ECBList_P head Vnull lels edata hels htls ->
tickstep htls hels htls´ hels´ ->
R_Prio_No_Dup htls ->
get_last_tcb_ptr ltls1 h = Some h´ ->
ECBList_P head Vnull lels´ edata hels´ htls´.