Library Mbox_common
Require Import include.
Require Import memory.
Require Import memdata.
Require Import NPeano.
Require Import os_code_defs.
Require Import os_code_notations.
Require Import os_ucos_h.
Require Import ucert.
Open Scope code_scope.
Require Import os_code_notations.
Require Import List.
Require Export lab.
Require Import common.
Require Import mathlib.
Lemma val_inj_eq
: forall i0 a: int32,
val_inj
(notint
(val_inj
(if Int.eq i0 a
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i0 a
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
i0 = a.
Lemma ecbjoin_sig_join´
: forall (x x1 v´35 x0 : EcbMod.map) (v´61 : block)
v3,
EcbMod.join x x1 v´35 ->
EcbMod.join x0 (EcbMod.sig (v´61, Int.zero) (v3, nil)) x1 ->
exists y,
EcbMod.join x0 x y /\
EcbMod.join y (EcbMod.sig (v´61, Int.zero) (v3, nil)) v´35.
Lemma joinsig_join_ex_my:
forall x1 v1 ma mb mab m,
EcbMod.joinsig x1 v1 mab m ->
EcbMod.join ma mb mab ->
exists mm, EcbMod.joinsig x1 v1 ma mm /\ EcbMod.join mm mb m.
Lemma joinsig_join_ex:
forall x0 x x1 t x4 x5,
EcbMod.joinsig x0 x x1 t ->
EcbMod.join x4 x5 x1 ->
exists y, EcbMod.joinsig x0 x x4 y /\ EcbMod.join y x5 t.
Lemma get_last_prop:
forall (l : list EventCtr) x v y,
l <> nil ->
(get_last_ptr ((x, v) :: l) = y <->
get_last_ptr l = y).
Lemma ecblist_p_decompose :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecb_joinsig_ex_split:
forall x x0 x1 ecbls x3 x4,
EcbMod.joinsig x x0 x1 ecbls ->
EcbMod.join x3 x4 x1 ->
exists y, EcbMod.joinsig x x0 x3 y /\ EcbMod.join y x4 ecbls.
Lemma ecblist_p_decompose´:
forall l1 ll1 l2 ll2 head ecbls tcbls,
length l1 = length ll1 ->
ECBList_P head Vnull
(l1++
l2) (ll1 ++ ll2) ecbls tcbls ->
exists ecbls1 ecbls2 x,
ECBList_P head x l1 ll1 ecbls1 tcbls /\
ECBList_P x Vnull l2 ll2 ecbls2 tcbls /\
EcbMod.join ecbls1 ecbls2 ecbls.
Lemma eventtype_neq_mbox:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
false = Int.eq i1 ($ OS_EVENT_TYPE_MBOX) ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[|~ exists x z, EcbMod.get v´34 (v´49,Int.zero) = Some (absmbox x, z) |] ** P.
Lemma eventtype_neq_mbox´:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
false = Int.eq i1 ($ OS_EVENT_TYPE_MBOX) ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[| exists d, EcbMod.get v´34 (v´49,Int.zero) = Some d /\ (~exists x z, d= (absmbox x, z)) |] ** P.
Lemma length8_ex:
forall v´40 :vallist,
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4 v5 v6 v7 v8,
v´40 = v1::v2::v3::v4::v5::v6::v7::v8::nil.
Lemma ecblist_ecbmod_get_aux_mbox :
forall v´61 i6 x4 x8 v´58 v´42
v´63 x20 v´37 v´35 v´36 v´38,
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(
((V$OS_EVENT_TYPE_MBOX
:: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
((DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls , nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_ecbmod_get_mbox :
forall v´61 i6 x4 x8 v´58 v´42 v´21 v´63 x20 v´37 v´35 v´36 v´38,
length v´21 = O ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_MBOX
:: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls , nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_p_decompose´´ :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecblist_ecbmod_get_mbox´ :
forall v´40 v´52 v´61 i6 x4 x8 v´58 v´42 v´21 xx
v´63 x20 i5 v´37 v´35 v´36 v´38,
Some (Vptr (v´61, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´21 ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P v´52 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_MBOX
:: xx :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls , nil)
/\ exists vg vv vx,
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 vg v´36 /\
EcbMod.join vg vx v´35/\
EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls, nil)) vx/\
ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecb_wt_ex_prop_mbox :
forall
v´43 v´34 v´38 x v´21 tid
v´23 v´35 i i3 x2 x3 v´42 v´40,
Int.eq i ($ 0) = false ->
Int.unsigned i <= 255 ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P v´40 (Vint32 i) ->
ECBList_P v´38 (Vptr x) v´21 v´23 v´43 v´35->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i
:: Vint32 i3 :: x2 :: x3 :: v´42 :: nil,
v´40) v´35 ->
RH_TCBList_ECBList_P v´34 v´35 tid ->
exists z t´ tl,
EcbMod.get v´34 x = Some (absmbox z, t´ :: tl).
Lemma Mutex_owner_set: forall x y z t, (~exists aa bb cc, t = (absmutexsem aa bb, cc))-> RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set x z t) y.
Lemma upd_last_prop:
forall v g x vl z ,
V_OSEventListPtr v = Some x ->
vl = upd_last_ectrls ((v, g) :: nil) z ->
exists v´, vl = ((v´, g) ::nil) /\ V_OSEventListPtr v´ = Some z.
Lemma nth_val_upd_prop:
forall vl n m v x,
(n<>m)%nat ->
(nth_val n (update_nth val m vl v) = Some x <->
nth_val n vl = Some x).
Lemma R_ECB_upd_hold :
forall x1 v v0 v´36 x8,
R_ECB_ETbl_P x1 (v, v0) v´36 ->
R_ECB_ETbl_P x1 (update_nth val 5 v x8, v0) v´36.
Lemma ecb_list_join_join :
forall v´40 v´52 v´61 v´21 x x2 v´36 x8 v´42 v´37 x0 v´51,
v´40 <> nil ->
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 x v´36 ->
ECBList_P x8 Vnull v´42 v´37 x0 v´36 ->
v´51 = upd_last_ectrls v´40 x8 ->
EcbMod.join x0 x x2 ->
ECBList_P v´52 Vnull (v´51 ++ v´42) (v´21 ++ v´37) x2 v´36.
Lemma RH_TCBList_ECBList_MUTEX_OWNER_subset_hold : forall x y z t, RH_TCBList_ECBList_MUTEX_OWNER z t -> EcbMod.join x y z -> RH_TCBList_ECBList_MUTEX_OWNER x t.
Lemma ecb_del_prop_RHhold:
forall v´35 v´36 v´38 x y absmg,
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
EcbMod.join x (EcbMod.sig y (absmg, nil))
v´35 -> RH_TCBList_ECBList_P x v´36 v´38 .
Lemma Mutex_owner_hold_for_set_tcb: forall x y pcur a b c, RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER x (TcbMod.set y pcur (a, b, c)).
Lemma absinfer_mbox_acc_err_return : forall P x ,
can_change_aop P ->
isptr x ->
absinfer (<|| mbox_acc (x :: nil) ||> ** P) ( <|| END (Some Vnull) ||> ** P).
Lemma absinfer_mbox_acc_succ_return:
forall P mqls x wl v v1 v3 v4 a,
can_change_aop P ->
v = Vptr a ->
EcbMod.get mqls x = Some (absmbox v, wl) ->
absinfer
( <|| mbox_acc (Vptr x :: nil) ||> **
HECBList mqls ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P)
(<|| END (Some v) ||> ** HECBList (EcbMod.set mqls x (absmbox Vnull, nil)) ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P).
Lemma absmbox_ptr_wt_nil: forall a w, RH_ECB_P (absmbox (Vptr a), w) -> w = nil.
Lemma ecb_sig_join_sig´_set : forall a b c d b´, EcbMod.joinsig a b c d -> EcbMod.joinsig a b´ c (EcbMod.set d a b´).
Lemma R_ECB_ETbl_P_high_ecb_mbox_acpt_hold :
forall x2 i i1 a x3 v´42 v´40 v´35,
R_ECB_ETbl_P x2
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: v´42 :: nil, v´40) v´35
->
R_ECB_ETbl_P x2
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: Vnull :: x3 :: v´42 :: nil, v´40) v´35
.
Lemma mbox_acpt_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m, EcbMod.get v´34 v = Some (absmbox m, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmbox Vnull, w)) v´35 v´37.
Lemma RLH_ECBData_p_high_mbox_acpt_hold:
forall a e w,
RLH_ECBData_P (DMbox (Vptr a)) (e, w) -> RLH_ECBData_P (DMbox Vnull) (absmbox Vnull, w).
Lemma absinfer_mbox_del_null_return : forall P ,
can_change_aop P ->
absinfer (<|| mbox_del (Vnull :: nil) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_DEL_NULL_ERR))) ||> ** P).
Lemma absinfer_mbox_del_p_not_legal_return : forall x a P tcbls tm curtid,
can_change_aop P ->
~ (exists x0 wls, EcbMod.get x a = Some (absmbox x0, wls)) ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid **
P) ( <|| END (Some (V$ MBOX_DEL_P_NOT_LEGAL_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_wrong_type_return : forall x a P tcbls tm curtid ,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<||mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P) ( <|| END (Some (V$ OS_ERR_EVENT_TYPE)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_task_wt_return : forall x a P tcbls tm curtid,
can_change_aop P ->
(exists y t tl,
EcbMod.get x a = Some (absmbox y, t::tl)) ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P) ( <|| END (Some (V$ MBOX_DEL_TASK_WAITING_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_succ_return :
forall ecbls ecbls´ x a P tid tcbls t,
can_change_aop P ->
EcbMod.get ecbls a = Some (absmbox x, nil) ->
EcbMod.join ecbls´ (EcbMod.sig a (absmbox x, nil)) ecbls ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList ecbls **
HTCBList tcbls ** HTime t ** HCurTCB tid ** P) ( <|| END (Some (V$NO_ERR)) ||> **
HECBList ecbls´ ** HTCBList tcbls ** HTime t ** HCurTCB tid ** P).
Lemma RH_TCBList_ECBList_P_high_get_msg_hold_mbox :
forall ecbls tcbls pcur qid m wl prio m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmbox (Vptr m), wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m´) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmbox Vnull, wl)) (TcbMod.set tcbls pcur (prio, rdy, (Vptr m))) pcur.
Lemma TCBListP_head_in_tcb: forall v´51 v´52 v´22 x9 x8 i9 i8 i6 i5 i4 i3 v´33 v´34 v´50 xx, TCBList_P (Vptr v´52)
((v´51
:: v´22
:: x9
:: x8
:: Vint32 i9
:: Vint32 i8
:: Vint32 xx
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´33)
v´34 v´50 ->
exists st, TcbMod.get v´50 v´52 = Some ( xx, st, x8).
Lemma tcblist_p_node_rl_mbox:
forall v´47 v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1 v´31 v´32 v´36 i,
TCBList_P (Vptr (v´47, Int.zero))
((v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i1 :: nil) :: v´31)
v´32 v´36 ->
RL_TCBblk_P
(v´39
:: v´19
:: x15
:: Vnull
:: Vint32 i
:: V$OS_STAT_MBOX
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil).
Lemma absinfer_mbox_pend_null_return : forall P x,
can_change_aop P ->
tl_vl_match (Tint16 :: nil) x = true ->
absinfer (<|| mbox_pend (Vnull :: x) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_PEND_NULL_ERR))) ||> ** P).
Open Scope code_scope.
Lemma absinfer_mbox_pend_p_not_legal_return : forall x a P b v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b<=65535 ->
EcbMod.get x a = None ->
absinfer (<|| mbox_pend (Vptr a ::Vint32 b:: nil) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 **
P) ( <|| END (Some (V$ MBOX_PEND_P_NOT_LEGAL_ERR)) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_mbox_pend_wrong_type_return : forall x a b P v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<|| mbox_pend (Vptr a :: Vint32 b :: nil) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 **
P) ( <|| END (Some (V$MBOX_PEND_WRONG_TYPE_ERR)) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_mbox_pend_from_idle_return : forall x a b P y t ct,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists st msg, TcbMod.get y ct = Some (Int.repr OS_IDLE_PRIO, st, msg)) ->
absinfer (<|| mbox_pend (Vptr a :: Vint32 b :: nil) ||> ** HECBList x ** HTCBList y ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$MBOX_PEND_FROM_IDLE_ERR)) ||> ** HECBList x ** HTCBList y ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_pend_not_ready_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ st = rdy ->
can_change_aop P ->
absinfer (<|| mbox_pend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_NOT_READY_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_pend_inst_get_return:
forall P mqls x wl v v1 v3 v4 a v00 msg p,
can_change_aop P ->
v = Vptr a ->
Int.unsigned v00 <= 65535 ->
EcbMod.get mqls x = Some (absmbox v, wl) ->
TcbMod.get v1 v4 = Some (p, rdy, msg) ->
absinfer
( <|| mbox_pend (Vptr x ::Vint32 v00 :: nil) ||> **
HECBList mqls ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_SUCC))) ||> ** HECBList (EcbMod.set mqls x (absmbox Vnull, nil)) ** HTCBList (TcbMod.set v1 v4 (p, rdy, v)) **
HTime v3 **
HCurTCB v4 **
P).
Lemma absinfer_mbox_pend_block:
forall P mqls qid v wl p m t ct tls,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmbox Vnull, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| mbox_pend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched;; (mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|) ?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|))||> ** HECBList (EcbMod.set mqls qid (absmbox Vnull,ct::wl)) ** HTCBList (TcbMod.set tls ct (p,wait (os_stat_mbox qid) v, Vnull) ) ** HTime t ** HCurTCB ct ** P).
Lemma low_stat_q_impl_high_stat_q
: forall (tcur : addrval) (tcurl : vallist) (tcblist : list vallist)
(rtbl : vallist) (tcbls : TcbMod.map) (msg : val),
TCBList_P (Vptr tcur) (tcurl :: tcblist) rtbl tcbls ->
V_OSTCBMsg tcurl = Some msg ->
exists prio st,
TcbMod.get tcbls tcur = Some (prio, st, msg).
Lemma low_stat_nordy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> (Int.eq st ($ OS_STAT_RDY) = false \/ Int.eq e ($ 0) = false) ->
~(t = rdy ).
Lemma r_tcb_status_p_nrdy:
forall v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1 p t m v´32,
R_TCB_Status_P
(v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil)
v´32 (p, t, m) ->
Int.eq i9 ($ OS_STAT_RDY) = false \/ Int.eq i10 ($ 0) = false ->
~ t =rdy.
Lemma TCBList_P_impl_high_tcbcur_Some :
forall tcbls tcur tcurl tcblist rtbl,
TCBList_P (Vptr tcur) (tcurl::tcblist) rtbl tcbls ->
exists prio st m, TcbMod.get tcbls tcur = Some (prio, st, m).
Lemma TCBList_P_impl_high_tcbcur_rdy:
forall (tcbls : TcbMod.map) (tcur : addrval)
(tcurl : vallist) (tcblist : list vallist)
(rtbl : vallist) v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1,
Int.eq i9 ($ OS_STAT_RDY) = true ->
Int.eq i10 ($ 0) = true ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
TCBList_P (Vptr tcur) ((v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i1 :: nil) :: tcblist) rtbl tcbls ->
exists prio m, TcbMod.get tcbls tcur = Some (prio, rdy, m).
Require Import OSTimeDlyPure.
Lemma ecb_etbl_set_hold:
forall x y tcbls prio st m ptcb m´,
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
R_ECB_ETbl_P x y tcbls ->
R_ECB_ETbl_P x y (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma ECBList_P_high_tcb_get_msg_hold:
forall ectrl head tail msgql ecbls tcbls ptcb prio st m m´,
ECBList_P head tail ectrl msgql ecbls tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
ECBList_P head tail ectrl msgql ecbls
(TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma TCBList_P_tcb_get_msg_hold :
forall ptcb v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 rtbl vl
tcbls prio st m m´,
TCBList_P (Vptr ptcb) ((v1::v2::v3::v4::v5::v6::v7::v8::v9::v10::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m´::v5::v6::v7::v8::v9::v10::v11::nil)::vl) rtbl (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma RH_CurTCB_high_get_msg_hold :
forall ptcb tcbls prio st m m´,
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma absinfer_mbox_pend_block_get_return
: forall (P : asrt) (mqls : EcbMod.map) (qid : addrval)
(v : int32) (p : priority) (t : ostime) (ct : tidspec.A)
(tls : TcbMod.map) (m : msg) (st : taskstatus),
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p, st, m) ->
m <> Vnull ->
⊢ <|| mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)
||>
**
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P
⇒ <|| END (Some (V$ MBOX_PEND_SUCC)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P
.
Lemma absinfer_mbox_pend_to_return :
forall P mqls qid v t ct tls st prio,
Int.unsigned v <= 65535 ->
TcbMod.get tls ct = Some (prio, st, Vnull) ->
can_change_aop P ->
absinfer
( <||
mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)
||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_TIMEOUT_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma ECBList_P_high_tcb_block_hold_mbox:
forall ectrl head tail msgql ecbls tcbls ptcb prio m qid time m´ ,
ECBList_P head tail ectrl msgql ecbls tcbls ->
TcbMod.get tcbls ptcb = Some (prio, rdy, m) ->
EcbMod.get ecbls qid = None ->
ECBList_P head tail ectrl msgql ecbls
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mbox qid) time, m´)).
Lemma ejoin_get_none_r : forall ma mb mc x a, EcbMod.get ma x = Some a -> EcbMod.join ma mb mc -> EcbMod.get mb x = None.
Lemma ejoin_get_none_l : forall ma mb mc x a, EcbMod.get mb x = Some a -> EcbMod.join ma mb mc -> EcbMod.get ma x = None.
Lemma R_ECB_ETbl_P_high_tcb_block_hold:
forall (l : addrval) (vl : vallist) (egrp : int32)
(v2 v3 v4 v5 : val) (etbl : vallist) (tcbls : TcbMod.map)
(ptcb : tidspec.A) (prio : int32) (st : taskstatus)
(m m´ : msg) (y bity bitx ey time : int32) (av : addrval),
Int.unsigned prio < 64 ->
R_PrioTbl_P vl tcbls av ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MBOX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil, etbl)
tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = Int.shru prio ($ 3) ->
bity = Int.shl ($ 1) y ->
bitx = Int.shl ($ 1) (prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MBOX
:: Vint32 (Int.or egrp bity) :: v2 :: v3 :: v4 :: v5 :: nil,
update_nth_val ∘(Int.unsigned y) etbl (Vint32 (Int.or ey bitx)))
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mbox l) time, m´))
.
Lemma TCBList_P_tcb_block_hold :
forall ptcb v1 v2 v3 v4 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m qid time ry,
TCBList_P (Vptr ptcb) ((v1::v2::v3::v4::v5::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
prio_neq_cur tcbls ptcb ( prio) ->
st = rdy \/ (exists n, st = wait os_stat_time n) ->
nth_val (nat_of_Z (Int.unsigned v9)) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb) ((v1::v2::(Vptr qid)::Vnull::(Vint32 time)::(Vint32 ($ OS_STAT_MBOX))::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (Int.and ry (Int.not v10))))
(TcbMod.set tcbls ptcb ( prio, wait (os_stat_mbox qid) ( time), Vnull)).
Require Import OSTimeDlyPure.
Lemma RH_CurTCB_high_block_hold_mbox :
forall ptcb tcbls prio st m qid time m´,
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb (TcbMod.set tcbls ptcb
(prio, wait (os_stat_mbox qid) time, m´)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mbox :
forall ecbls tcbls pcur qid m ml wl prio time m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmbox ml, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmbox ml, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_mbox qid) time, m´)) pcur.
Lemma TcbMod_set_R_PrioTbl_P_hold :
forall ptbl tcbls ptcb pr st m st´ m´ av,
R_PrioTbl_P ptbl tcbls av ->
TcbMod.get tcbls ptcb = Some (pr, st, m) ->
R_PrioTbl_P ptbl (TcbMod.set tcbls ptcb (pr,st´,m´)) av.
Lemma TCBList_P_tcb_block_hold´´ :
forall v ptcb rtbl vl y bitx
tcbls prio ry x1 tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.join (TcbMod.sig ptcb (prio, t, m)) x1 tcs ->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma TCBList_P_tcb_block_hold´:
forall v ptcb rtbl vl y bitx
tcbls prio ry tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.get tcs ptcb = Some (prio, t, m)->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma absinfer_mbox_post_exwt_succ:
forall P mqls x v wl tls t ct p st m m´ t´ ,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox m ,wl) ->
~ wl=nil ->
GetHWait tls wl t´ ->
TcbMod.get tls t´ = Some (p,st, m´) ->
absinfer
( <|| mbox_post (Vptr x :: Vptr v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched;;END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmbox m, (remove_tid t´ wl))) ** HTCBList (TcbMod.set tls t´ (p,rdy , (Vptr v)) ) ** HTime t ** HCurTCB ct ** P).
Lemma mbox_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m m2, EcbMod.get v´34 v = Some (absmbox m, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmbox m2, w)) v´35 v´37.
Lemma post_exwt_succ_pre_mbox
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´15 : int32) (v´24 : block)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
(x : val) (x0 : maxlen) (x1 : waitset)
(v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
(v´58 : block) (a : priority) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval),
v´12 <> Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox x , x1) v´6 v´10 ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
TcbJoin (v´58, Int.zero) (a, b, c) v´62 v´7 ->
x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma get_tcb_stat_mbox
: forall (p : int32) (etbl : vallist) (ptbl : list val)
(tid : addrval) (tcbls : TcbMod.map) (abstcb : abstcb.B)
(tcbls´ : TcbMod.map) (vl rtbl : vallist)
(qid : addrval) (vle : list val) (vhold : addrval),
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
prio_in_tbl p etbl ->
nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr tid ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbJoin tid abstcb tcbls´ tcbls ->
TCBNode_P vl rtbl abstcb ->
R_ECB_ETbl_P qid (V$OS_EVENT_TYPE_MBOX :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_MBOX).
Lemma msglist_p_compose_mbox
: forall (p : val) (qid : addrval) (mqls : EcbMod.map)
(qptrl1 qptrl2 : list EventCtr) (i i1 : int32)
(a : val) (x3 p´ : val) (v´41 : vallist)
(msgqls1 msgqls2 : list EventData) (msgq : EventData)
(mqls1 mqls2 : EcbMod.map) (mq : absecb.B)
(mqls´ : EcbMod.map) (tcbls : TcbMod.map),
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 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 ++
((V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) mqls
tcbls.
Require Import OSQPostPure.
Lemma TCBList_P_post_mbox
: forall (v´42 : val) (v´48 : list vallist) (v´47 : TcbMod.map)
(v´60 : val) (v´50 : list vallist) (v´37 : vallist)
(v´59 v´49 v´44 : TcbMod.map) (v´63 v´64 v´65 : val)
(v´51 v´52 v´53 v´54 v´55 v´56 : int32) (x00 : addrval)
(v´58 : block) (v´40 v´38 : int32) (prio : priority)
(st : taskstatus) (msg0 :msg)
(v´7 v´62 v´43 : TcbMod.map) (v´36 : vallist)
(v´39 : int32) (v´13 : vallist) (vhold : addrval),
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_MBOX
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg0) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: V$0
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil)
:: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37)
(Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero) (prio, rdy, Vptr x00)).
Lemma ECBList_P_Set_Rdy_hold_mbox
: forall (a : list EventCtr) (tcbls : TcbMod.map)
(tid : tidspec.A) (prio : priority) (msg0 msg´ : msg)
(x y : val) (b : list EventData) (c : EcbMod.map)
(eid : ecbid) (nl : int32),
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) nl, msg0) ->
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_post_exwt_hold_mbox
: forall (v´36 : vallist) (v´12 : int32) (v´13 : vallist)
(v´38 v´69 v´39 : int32) (v´58 : block) (v´40 : int32)
(v´32 : block) (v´15 : int32) (v´24 : val)
(v´35 v´16 v´18 v´19 v´20 v´34 : val) (v´21 v´22 : int32)
(v´23 : block) (v´25 v´26 : val) (v´27 : vallist)
(x : list msg) (x0 : maxlen) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map) (x00 : addrval)
(v´11 : EcbMod.map) (v´31 : list EventData)
(v´30 : list EventCtr) (v´29 : val) (v´10 v´9 : EcbMod.map)
(prio : priority) (v´62 : TcbMod.map) (st : taskstatus)
(msg0 : msg) (y : int32) (vhold : addrval),
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMbox v´24) (absmbox v´24, x1) ->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox v´24, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold ->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_MBOX
:: Vint32 y
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMbox v´24 ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmbox v´24, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, Vptr x00))
.
Lemma rh_tcblist_ecblist_p_post_exwt_mbox
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : val)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(x00 : addrval) (xl : int32),
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmbox x , x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_mbox eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (absmbox x, remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, Vptr x00)) v´8
.
Lemma rh_tcblist_ecblist_p_post_exwt_aux_mbox
: forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : val)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(st : taskstatus),
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmbox x, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_mbox eid) xl
.
Lemma TCBList_P_post_msg_mbox
: forall (v´42 : val) (v´48 : list vallist) (v´47 : TcbMod.map)
(v´60 : val) (v´50 : list vallist) (v´37 : vallist)
(v´59 v´49 v´44 : TcbMod.map) (v´63 v´64 v´65 : val)
(v´51 v´52 v´53 v´54 v´55 v´56 : int32) (x00 : addrval)
(v´58 : block) (v´40 v´38 : int32) (prio : priority)
(st : taskstatus) (msg : msg)
(v´7 v´62 v´43 : TcbMod.map) (v´36 : vallist)
(v´39 : int32) (v´13 : vallist) (vhold : addrval),
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_MBOX
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: Vint32 ($ OS_STAT_MBOX&Int.not ($ OS_STAT_MBOX))
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil)
:: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37)
(Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero) (prio, rdy, Vptr x00)).
Lemma statmbox_and_not_statmbox_eq_rdy : Int.eq ($ OS_STAT_MBOX&Int.not ($ OS_STAT_MBOX)) ($ OS_STAT_RDY) = true.
Lemma tcb_inrtbl_not_vhold: forall v´42 v´62 v´93 v´57 v´81, RL_RTbl_PrioTbl_P v´42 v´62 v´93 -> prio_in_tbl ((v´57)) v´42 -> nth_val´ (Z.to_nat (Int.unsigned ((v´57)))) v´62 = Vptr (v´81, Int.zero) -> 0 <= Int.unsigned v´57 < 64 -> (v´81, Int.zero) <> v´93.
Lemma le7_le7_range64: forall v´57 v´59, Int.unsigned v´57 <= 7 -> Int.unsigned v´59 <= 7 -> 0 <= Int.unsigned ((v´57<<$ 3)+ᵢv´59) < 64.
Lemma absinfer_mbox_post_put_mail_return : forall P x m mqls tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox Vnull, nil) ->
absinfer (<|| mbox_post (Vptr x :: Vptr m ::nil) ||> **HECBList mqls** HTCBList tcbls ** HTime t ** HCurTCB ct ** P) (<|| END (Some (Vint32 (Int.repr MBOX_POST_SUCC))) ||> **HECBList (EcbMod.set mqls x (absmbox (Vptr m),nil))** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_null_return : forall P x,
can_change_aop P ->
tl_vl_match ((Void) ∗ :: nil) x = true ->
absinfer (<|| mbox_post (Vnull :: x) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_POST_NULL_ERR))) ||> ** P).
Lemma absinfer_mbox_post_msg_null_return:
forall P v,
can_change_aop P ->
absinfer
( <|| mbox_post (Vptr v :: Vnull ::nil) ||> **
P) (<|| END (Some (Vint32 (Int.repr OS_ERR_POST_NULL_PTR))) ||> **
P).
Lemma absinfer_mbox_post_p_not_legal_return : forall x a P b tcbls t ct,
can_change_aop P ->
EcbMod.get x a = None ->
absinfer (<|| mbox_post (Vptr a ::Vptr b:: nil) ||> ** HECBList x** HTCBList tcbls ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$ MBOX_POST_P_NOT_LEGAL_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_wrong_type_return : forall x a b P tcbls t ct,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<|| mbox_post (Vptr a :: Vptr b :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$MBOX_POST_WRONG_TYPE_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_full_return : forall P mqls x a wl y tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox a,wl) ->
(exists b, a= Vptr b) ->
absinfer
( <|| mbox_post (Vptr x :: Vptr y :: nil) ||> **HECBList mqls **
HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_POST_FULL_ERR))) ||> **HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma something_in_not_nil : forall (T:Type) (y: @list T), y<>nil -> exists x, In x y.
Lemma rg1 : forall x2 x6 , 0 <= Int.unsigned x2 < 64->
x6 = $ Int.unsigned x2&$ 7 ->
0<= Int.unsigned x6 < 8.
Lemma rg2 : forall x2 x7 , 0 <= Int.unsigned x2 < 64->
x7 = Int.shru ($ Int.unsigned x2) ($ 3) ->
0<= Int.unsigned x7 < 8.
Lemma post_exwt_succ_pre_mbox´
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´15 : int32) (v´24 : val)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
(x : val) (x1 : waitset)
(v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
(v´58 : block) (a : priority)
(c : msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval),
v´12 = Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox x , x1) v´6 v´10 ->
x1 = nil
.
Lemma val_inj_lemma: forall m0 a, val_inj (notint (val_inj (val_eq m0 a))) = Vint32 Int.zero \/
val_inj (notint (val_inj (val_eq m0 a))) = Vnull -> m0 = a.
Lemma AOSTCBPrioTbl_high_tcblist_get_msg :
forall tcbls p prio st m vl rtbl m´ s P av,
TcbMod.get tcbls p = Some (prio, st, m) ->
s|= AOSTCBPrioTbl vl rtbl tcbls av ** P ->
s|= AOSTCBPrioTbl vl rtbl (TcbMod.set tcbls p (prio, st, m´)) av ** P.
Require Import memory.
Require Import memdata.
Require Import NPeano.
Require Import os_code_defs.
Require Import os_code_notations.
Require Import os_ucos_h.
Require Import ucert.
Open Scope code_scope.
Require Import os_code_notations.
Require Import List.
Require Export lab.
Require Import common.
Require Import mathlib.
Lemma val_inj_eq
: forall i0 a: int32,
val_inj
(notint
(val_inj
(if Int.eq i0 a
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vint32 Int.zero \/
val_inj
(notint
(val_inj
(if Int.eq i0 a
then Some (Vint32 Int.one)
else Some (Vint32 Int.zero)))) = Vnull ->
i0 = a.
Lemma ecbjoin_sig_join´
: forall (x x1 v´35 x0 : EcbMod.map) (v´61 : block)
v3,
EcbMod.join x x1 v´35 ->
EcbMod.join x0 (EcbMod.sig (v´61, Int.zero) (v3, nil)) x1 ->
exists y,
EcbMod.join x0 x y /\
EcbMod.join y (EcbMod.sig (v´61, Int.zero) (v3, nil)) v´35.
Lemma joinsig_join_ex_my:
forall x1 v1 ma mb mab m,
EcbMod.joinsig x1 v1 mab m ->
EcbMod.join ma mb mab ->
exists mm, EcbMod.joinsig x1 v1 ma mm /\ EcbMod.join mm mb m.
Lemma joinsig_join_ex:
forall x0 x x1 t x4 x5,
EcbMod.joinsig x0 x x1 t ->
EcbMod.join x4 x5 x1 ->
exists y, EcbMod.joinsig x0 x x4 y /\ EcbMod.join y x5 t.
Lemma get_last_prop:
forall (l : list EventCtr) x v y,
l <> nil ->
(get_last_ptr ((x, v) :: l) = y <->
get_last_ptr l = y).
Lemma ecblist_p_decompose :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecb_joinsig_ex_split:
forall x x0 x1 ecbls x3 x4,
EcbMod.joinsig x x0 x1 ecbls ->
EcbMod.join x3 x4 x1 ->
exists y, EcbMod.joinsig x x0 x3 y /\ EcbMod.join y x4 ecbls.
Lemma ecblist_p_decompose´:
forall l1 ll1 l2 ll2 head ecbls tcbls,
length l1 = length ll1 ->
ECBList_P head Vnull
(l1++
l2) (ll1 ++ ll2) ecbls tcbls ->
exists ecbls1 ecbls2 x,
ECBList_P head x l1 ll1 ecbls1 tcbls /\
ECBList_P x Vnull l2 ll2 ecbls2 tcbls /\
EcbMod.join ecbls1 ecbls2 ecbls.
Lemma eventtype_neq_mbox:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
false = Int.eq i1 ($ OS_EVENT_TYPE_MBOX) ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[|~ exists x z, EcbMod.get v´34 (v´49,Int.zero) = Some (absmbox x, z) |] ** P.
Lemma eventtype_neq_mbox´:
forall v´38 v´21 i1 i0 i2 x2 x3 v´42 v´40 v´22 v´23 v´41 v´24 v´34 v´35 v´49 s P v´43 v´45 v´44 v´46,
length v´21 = length v´23->
ECBList_P v´38 Vnull
(v´21 ++
((Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil,
v´40) :: nil) ++ v´22) (v´23 ++ (v´41 :: nil) ++ v´24) v´34 v´35 ->
ECBList_P v´38 (Vptr (v´49, Int.zero)) v´21 v´23 v´43 v´35 ->
EcbMod.join v´43 v´45 v´34 ->
EcbMod.joinsig (v´49, Int.zero) v´46 v´44 v´45 ->
false = Int.eq i1 ($ OS_EVENT_TYPE_MBOX) ->
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 ** P ->
s |= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil) v´41 **
[| exists d, EcbMod.get v´34 (v´49,Int.zero) = Some d /\ (~exists x z, d= (absmbox x, z)) |] ** P.
Lemma length8_ex:
forall v´40 :vallist,
length v´40 = ∘OS_EVENT_TBL_SIZE ->
exists v1 v2 v3 v4 v5 v6 v7 v8,
v´40 = v1::v2::v3::v4::v5::v6::v7::v8::nil.
Lemma ecblist_ecbmod_get_aux_mbox :
forall v´61 i6 x4 x8 v´58 v´42
v´63 x20 v´37 v´35 v´36 v´38,
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(
((V$OS_EVENT_TYPE_MBOX
:: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
((DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls , nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls, nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_ecbmod_get_mbox :
forall v´61 i6 x4 x8 v´58 v´42 v´21 v´63 x20 v´37 v´35 v´36 v´38,
length v´21 = O ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P (Vptr (v´61, Int.zero)) Vnull
(nil ++
((V$OS_EVENT_TYPE_MBOX
:: V$0 :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls, nil)
/\ exists vv, EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls , nil)) v´35 /\ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecblist_p_decompose´´ :
forall y1 z1 x y2 z2 t z ,
length y1 = length y2 ->
ECBList_P x Vnull (y1++z1) (y2++z2) t z ->
exists x1 t1 t2,
ECBList_P x x1 y1 y2 t1 z /\ ECBList_P x1 Vnull z1 z2 t2 z /\
EcbMod.join t1 t2 t /\ (get_last_ptr y1 = None \/ get_last_ptr y1 = Some x1).
Lemma ecblist_ecbmod_get_mbox´ :
forall v´40 v´52 v´61 i6 x4 x8 v´58 v´42 v´21 xx
v´63 x20 i5 v´37 v´35 v´36 v´38,
Some (Vptr (v´61, Int.zero)) = get_last_ptr v´40 ->
length v´40 = length v´21 ->
Int.unsigned i5 <= 65535 ->
array_type_vallist_match Int8u v´58->
RH_CurTCB v´38 v´36 ->
length v´58 = ∘OS_EVENT_TBL_SIZE ->
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
RL_Tbl_Grp_P v´58 (V$0) ->
ECBList_P v´52 Vnull
(v´40 ++
((V$OS_EVENT_TYPE_MBOX
:: xx :: Vint32 i6 :: v´63 :: x4 :: x8 :: nil,
v´58) :: nil) ++ v´42)
(v´21 ++
(DMbox x20 :: nil) ++ v´37) v´35 v´36 ->
exists msgls,
EcbMod.get v´35 (v´61, Int.zero) = Some (absmbox msgls , nil)
/\ exists vg vv vx,
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 vg v´36 /\
EcbMod.join vg vx v´35/\
EcbMod.join vv (EcbMod.sig (v´61, Int.zero) (absmbox msgls, nil)) vx/\
ECBList_P x8 Vnull v´42 v´37 vv v´36.
Lemma ecb_wt_ex_prop_mbox :
forall
v´43 v´34 v´38 x v´21 tid
v´23 v´35 i i3 x2 x3 v´42 v´40,
Int.eq i ($ 0) = false ->
Int.unsigned i <= 255 ->
array_type_vallist_match Int8u v´40 ->
length v´40 = ∘OS_EVENT_TBL_SIZE ->
RL_Tbl_Grp_P v´40 (Vint32 i) ->
ECBList_P v´38 (Vptr x) v´21 v´23 v´43 v´35->
R_ECB_ETbl_P x
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i
:: Vint32 i3 :: x2 :: x3 :: v´42 :: nil,
v´40) v´35 ->
RH_TCBList_ECBList_P v´34 v´35 tid ->
exists z t´ tl,
EcbMod.get v´34 x = Some (absmbox z, t´ :: tl).
Lemma Mutex_owner_set: forall x y z t, (~exists aa bb cc, t = (absmutexsem aa bb, cc))-> RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER (EcbMod.set x z t) y.
Lemma upd_last_prop:
forall v g x vl z ,
V_OSEventListPtr v = Some x ->
vl = upd_last_ectrls ((v, g) :: nil) z ->
exists v´, vl = ((v´, g) ::nil) /\ V_OSEventListPtr v´ = Some z.
Lemma nth_val_upd_prop:
forall vl n m v x,
(n<>m)%nat ->
(nth_val n (update_nth val m vl v) = Some x <->
nth_val n vl = Some x).
Lemma R_ECB_upd_hold :
forall x1 v v0 v´36 x8,
R_ECB_ETbl_P x1 (v, v0) v´36 ->
R_ECB_ETbl_P x1 (update_nth val 5 v x8, v0) v´36.
Lemma ecb_list_join_join :
forall v´40 v´52 v´61 v´21 x x2 v´36 x8 v´42 v´37 x0 v´51,
v´40 <> nil ->
ECBList_P v´52 (Vptr (v´61, Int.zero)) v´40 v´21 x v´36 ->
ECBList_P x8 Vnull v´42 v´37 x0 v´36 ->
v´51 = upd_last_ectrls v´40 x8 ->
EcbMod.join x0 x x2 ->
ECBList_P v´52 Vnull (v´51 ++ v´42) (v´21 ++ v´37) x2 v´36.
Lemma RH_TCBList_ECBList_MUTEX_OWNER_subset_hold : forall x y z t, RH_TCBList_ECBList_MUTEX_OWNER z t -> EcbMod.join x y z -> RH_TCBList_ECBList_MUTEX_OWNER x t.
Lemma ecb_del_prop_RHhold:
forall v´35 v´36 v´38 x y absmg,
RH_TCBList_ECBList_P v´35 v´36 v´38 ->
EcbMod.join x (EcbMod.sig y (absmg, nil))
v´35 -> RH_TCBList_ECBList_P x v´36 v´38 .
Lemma Mutex_owner_hold_for_set_tcb: forall x y pcur a b c, RH_TCBList_ECBList_MUTEX_OWNER x y -> RH_TCBList_ECBList_MUTEX_OWNER x (TcbMod.set y pcur (a, b, c)).
Lemma absinfer_mbox_acc_err_return : forall P x ,
can_change_aop P ->
isptr x ->
absinfer (<|| mbox_acc (x :: nil) ||> ** P) ( <|| END (Some Vnull) ||> ** P).
Lemma absinfer_mbox_acc_succ_return:
forall P mqls x wl v v1 v3 v4 a,
can_change_aop P ->
v = Vptr a ->
EcbMod.get mqls x = Some (absmbox v, wl) ->
absinfer
( <|| mbox_acc (Vptr x :: nil) ||> **
HECBList mqls ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P)
(<|| END (Some v) ||> ** HECBList (EcbMod.set mqls x (absmbox Vnull, nil)) ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P).
Lemma absmbox_ptr_wt_nil: forall a w, RH_ECB_P (absmbox (Vptr a), w) -> w = nil.
Lemma ecb_sig_join_sig´_set : forall a b c d b´, EcbMod.joinsig a b c d -> EcbMod.joinsig a b´ c (EcbMod.set d a b´).
Lemma R_ECB_ETbl_P_high_ecb_mbox_acpt_hold :
forall x2 i i1 a x3 v´42 v´40 v´35,
R_ECB_ETbl_P x2
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: Vptr a :: x3 :: v´42 :: nil, v´40) v´35
->
R_ECB_ETbl_P x2
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: Vnull :: x3 :: v´42 :: nil, v´40) v´35
.
Lemma mbox_acpt_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m, EcbMod.get v´34 v = Some (absmbox m, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmbox Vnull, w)) v´35 v´37.
Lemma RLH_ECBData_p_high_mbox_acpt_hold:
forall a e w,
RLH_ECBData_P (DMbox (Vptr a)) (e, w) -> RLH_ECBData_P (DMbox Vnull) (absmbox Vnull, w).
Lemma absinfer_mbox_del_null_return : forall P ,
can_change_aop P ->
absinfer (<|| mbox_del (Vnull :: nil) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_DEL_NULL_ERR))) ||> ** P).
Lemma absinfer_mbox_del_p_not_legal_return : forall x a P tcbls tm curtid,
can_change_aop P ->
~ (exists x0 wls, EcbMod.get x a = Some (absmbox x0, wls)) ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid **
P) ( <|| END (Some (V$ MBOX_DEL_P_NOT_LEGAL_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_wrong_type_return : forall x a P tcbls tm curtid ,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<||mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P) ( <|| END (Some (V$ OS_ERR_EVENT_TYPE)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_task_wt_return : forall x a P tcbls tm curtid,
can_change_aop P ->
(exists y t tl,
EcbMod.get x a = Some (absmbox y, t::tl)) ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P) ( <|| END (Some (V$ MBOX_DEL_TASK_WAITING_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime tm ** HCurTCB curtid ** P).
Lemma absinfer_mbox_del_succ_return :
forall ecbls ecbls´ x a P tid tcbls t,
can_change_aop P ->
EcbMod.get ecbls a = Some (absmbox x, nil) ->
EcbMod.join ecbls´ (EcbMod.sig a (absmbox x, nil)) ecbls ->
absinfer (<|| mbox_del (Vptr a :: nil) ||> ** HECBList ecbls **
HTCBList tcbls ** HTime t ** HCurTCB tid ** P) ( <|| END (Some (V$NO_ERR)) ||> **
HECBList ecbls´ ** HTCBList tcbls ** HTime t ** HCurTCB tid ** P).
Lemma RH_TCBList_ECBList_P_high_get_msg_hold_mbox :
forall ecbls tcbls pcur qid m wl prio m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmbox (Vptr m), wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m´) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmbox Vnull, wl)) (TcbMod.set tcbls pcur (prio, rdy, (Vptr m))) pcur.
Lemma TCBListP_head_in_tcb: forall v´51 v´52 v´22 x9 x8 i9 i8 i6 i5 i4 i3 v´33 v´34 v´50 xx, TCBList_P (Vptr v´52)
((v´51
:: v´22
:: x9
:: x8
:: Vint32 i9
:: Vint32 i8
:: Vint32 xx
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´33)
v´34 v´50 ->
exists st, TcbMod.get v´50 v´52 = Some ( xx, st, x8).
Lemma tcblist_p_node_rl_mbox:
forall v´47 v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1 v´31 v´32 v´36 i,
TCBList_P (Vptr (v´47, Int.zero))
((v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i1 :: nil) :: v´31)
v´32 v´36 ->
RL_TCBblk_P
(v´39
:: v´19
:: x15
:: Vnull
:: Vint32 i
:: V$OS_STAT_MBOX
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil).
Lemma absinfer_mbox_pend_null_return : forall P x,
can_change_aop P ->
tl_vl_match (Tint16 :: nil) x = true ->
absinfer (<|| mbox_pend (Vnull :: x) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_PEND_NULL_ERR))) ||> ** P).
Open Scope code_scope.
Lemma absinfer_mbox_pend_p_not_legal_return : forall x a P b v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b<=65535 ->
EcbMod.get x a = None ->
absinfer (<|| mbox_pend (Vptr a ::Vint32 b:: nil) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 **
P) ( <|| END (Some (V$ MBOX_PEND_P_NOT_LEGAL_ERR)) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_mbox_pend_wrong_type_return : forall x a b P v´33 v´16 v´35,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<|| mbox_pend (Vptr a :: Vint32 b :: nil) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 **
P) ( <|| END (Some (V$MBOX_PEND_WRONG_TYPE_ERR)) ||> ** HECBList x **
HTCBList v´33 **
HTime v´16 **
HCurTCB v´35 ** P).
Lemma absinfer_mbox_pend_from_idle_return : forall x a b P y t ct,
can_change_aop P ->
Int.unsigned b <= 65535 ->
(exists st msg, TcbMod.get y ct = Some (Int.repr OS_IDLE_PRIO, st, msg)) ->
absinfer (<|| mbox_pend (Vptr a :: Vint32 b :: nil) ||> ** HECBList x ** HTCBList y ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$MBOX_PEND_FROM_IDLE_ERR)) ||> ** HECBList x ** HTCBList y ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_pend_not_ready_return :
forall P ecbls tcbls t ct st msg v x prio,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (prio, st, msg) ->
~ st = rdy ->
can_change_aop P ->
absinfer (<|| mbox_pend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_NOT_READY_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_pend_inst_get_return:
forall P mqls x wl v v1 v3 v4 a v00 msg p,
can_change_aop P ->
v = Vptr a ->
Int.unsigned v00 <= 65535 ->
EcbMod.get mqls x = Some (absmbox v, wl) ->
TcbMod.get v1 v4 = Some (p, rdy, msg) ->
absinfer
( <|| mbox_pend (Vptr x ::Vint32 v00 :: nil) ||> **
HECBList mqls ** HTCBList v1 **
HTime v3 **
HCurTCB v4 **
P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_SUCC))) ||> ** HECBList (EcbMod.set mqls x (absmbox Vnull, nil)) ** HTCBList (TcbMod.set v1 v4 (p, rdy, v)) **
HTime v3 **
HCurTCB v4 **
P).
Lemma absinfer_mbox_pend_block:
forall P mqls qid v wl p m t ct tls,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmbox Vnull, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| mbox_pend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched;; (mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|) ?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|))||> ** HECBList (EcbMod.set mqls qid (absmbox Vnull,ct::wl)) ** HTCBList (TcbMod.set tls ct (p,wait (os_stat_mbox qid) v, Vnull) ) ** HTime t ** HCurTCB ct ** P).
Lemma low_stat_q_impl_high_stat_q
: forall (tcur : addrval) (tcurl : vallist) (tcblist : list vallist)
(rtbl : vallist) (tcbls : TcbMod.map) (msg : val),
TCBList_P (Vptr tcur) (tcurl :: tcblist) rtbl tcbls ->
V_OSTCBMsg tcurl = Some msg ->
exists prio st,
TcbMod.get tcbls tcur = Some (prio, st, msg).
Lemma low_stat_nordy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> (Int.eq st ($ OS_STAT_RDY) = false \/ Int.eq e ($ 0) = false) ->
~(t = rdy ).
Lemma r_tcb_status_p_nrdy:
forall v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1 p t m v´32,
R_TCB_Status_P
(v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil)
v´32 (p, t, m) ->
Int.eq i9 ($ OS_STAT_RDY) = false \/ Int.eq i10 ($ 0) = false ->
~ t =rdy.
Lemma TCBList_P_impl_high_tcbcur_Some :
forall tcbls tcur tcurl tcblist rtbl,
TCBList_P (Vptr tcur) (tcurl::tcblist) rtbl tcbls ->
exists prio st m, TcbMod.get tcbls tcur = Some (prio, st, m).
Lemma TCBList_P_impl_high_tcbcur_rdy:
forall (tcbls : TcbMod.map) (tcur : addrval)
(tcurl : vallist) (tcblist : list vallist)
(rtbl : vallist) v´39 v´19 x15 x10 i10 i9 i8 i7 i6 i5 i1,
Int.eq i9 ($ OS_STAT_RDY) = true ->
Int.eq i10 ($ 0) = true ->
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
TCBList_P (Vptr tcur) ((v´39
:: v´19
:: x15
:: x10
:: Vint32 i10
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i1 :: nil) :: tcblist) rtbl tcbls ->
exists prio m, TcbMod.get tcbls tcur = Some (prio, rdy, m).
Require Import OSTimeDlyPure.
Lemma ecb_etbl_set_hold:
forall x y tcbls prio st m ptcb m´,
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
R_ECB_ETbl_P x y tcbls ->
R_ECB_ETbl_P x y (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma ECBList_P_high_tcb_get_msg_hold:
forall ectrl head tail msgql ecbls tcbls ptcb prio st m m´,
ECBList_P head tail ectrl msgql ecbls tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
ECBList_P head tail ectrl msgql ecbls
(TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma TCBList_P_tcb_get_msg_hold :
forall ptcb v1 v2 v3 v4 v5 v6 v7 v8 v9 v10 v11 rtbl vl
tcbls prio st m m´,
TCBList_P (Vptr ptcb) ((v1::v2::v3::v4::v5::v6::v7::v8::v9::v10::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
TCBList_P (Vptr ptcb) ((v1::v2::v3::m´::v5::v6::v7::v8::v9::v10::v11::nil)::vl) rtbl (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma RH_CurTCB_high_get_msg_hold :
forall ptcb tcbls prio st m m´,
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma absinfer_mbox_pend_block_get_return
: forall (P : asrt) (mqls : EcbMod.map) (qid : addrval)
(v : int32) (p : priority) (t : ostime) (ct : tidspec.A)
(tls : TcbMod.map) (m : msg) (st : taskstatus),
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p, st, m) ->
m <> Vnull ->
⊢ <|| mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)
||>
**
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P
⇒ <|| END (Some (V$ MBOX_PEND_SUCC)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P
.
Lemma absinfer_mbox_pend_to_return :
forall P mqls qid v t ct tls st prio,
Int.unsigned v <= 65535 ->
TcbMod.get tls ct = Some (prio, st, Vnull) ->
can_change_aop P ->
absinfer
( <||
mbox_pend_timeout_err (|Vptr qid :: Vint32 v :: nil|)
?? mbox_pend_block_get_succ (|Vptr qid :: Vint32 v :: nil|)
||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_PEND_TIMEOUT_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma ECBList_P_high_tcb_block_hold_mbox:
forall ectrl head tail msgql ecbls tcbls ptcb prio m qid time m´ ,
ECBList_P head tail ectrl msgql ecbls tcbls ->
TcbMod.get tcbls ptcb = Some (prio, rdy, m) ->
EcbMod.get ecbls qid = None ->
ECBList_P head tail ectrl msgql ecbls
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mbox qid) time, m´)).
Lemma ejoin_get_none_r : forall ma mb mc x a, EcbMod.get ma x = Some a -> EcbMod.join ma mb mc -> EcbMod.get mb x = None.
Lemma ejoin_get_none_l : forall ma mb mc x a, EcbMod.get mb x = Some a -> EcbMod.join ma mb mc -> EcbMod.get ma x = None.
Lemma R_ECB_ETbl_P_high_tcb_block_hold:
forall (l : addrval) (vl : vallist) (egrp : int32)
(v2 v3 v4 v5 : val) (etbl : vallist) (tcbls : TcbMod.map)
(ptcb : tidspec.A) (prio : int32) (st : taskstatus)
(m m´ : msg) (y bity bitx ey time : int32) (av : addrval),
Int.unsigned prio < 64 ->
R_PrioTbl_P vl tcbls av ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MBOX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil, etbl)
tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = Int.shru prio ($ 3) ->
bity = Int.shl ($ 1) y ->
bitx = Int.shl ($ 1) (prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MBOX
:: Vint32 (Int.or egrp bity) :: v2 :: v3 :: v4 :: v5 :: nil,
update_nth_val ∘(Int.unsigned y) etbl (Vint32 (Int.or ey bitx)))
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mbox l) time, m´))
.
Lemma TCBList_P_tcb_block_hold :
forall ptcb v1 v2 v3 v4 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m qid time ry,
TCBList_P (Vptr ptcb) ((v1::v2::v3::v4::v5::(Vint32 v6)::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl) rtbl tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
prio_neq_cur tcbls ptcb ( prio) ->
st = rdy \/ (exists n, st = wait os_stat_time n) ->
nth_val (nat_of_Z (Int.unsigned v9)) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb) ((v1::v2::(Vptr qid)::Vnull::(Vint32 time)::(Vint32 ($ OS_STAT_MBOX))::(Vint32 prio)::v8::(Vint32 v9)::(Vint32 v10)::v11::nil)::vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (Int.and ry (Int.not v10))))
(TcbMod.set tcbls ptcb ( prio, wait (os_stat_mbox qid) ( time), Vnull)).
Require Import OSTimeDlyPure.
Lemma RH_CurTCB_high_block_hold_mbox :
forall ptcb tcbls prio st m qid time m´,
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb (TcbMod.set tcbls ptcb
(prio, wait (os_stat_mbox qid) time, m´)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mbox :
forall ecbls tcbls pcur qid m ml wl prio time m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmbox ml, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmbox ml, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_mbox qid) time, m´)) pcur.
Lemma TcbMod_set_R_PrioTbl_P_hold :
forall ptbl tcbls ptcb pr st m st´ m´ av,
R_PrioTbl_P ptbl tcbls av ->
TcbMod.get tcbls ptcb = Some (pr, st, m) ->
R_PrioTbl_P ptbl (TcbMod.set tcbls ptcb (pr,st´,m´)) av.
Lemma TCBList_P_tcb_block_hold´´ :
forall v ptcb rtbl vl y bitx
tcbls prio ry x1 tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.join (TcbMod.sig ptcb (prio, t, m)) x1 tcs ->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma TCBList_P_tcb_block_hold´:
forall v ptcb rtbl vl y bitx
tcbls prio ry tcs tcs´ t m,
0 <= Int.unsigned prio < 64 ->
TcbMod.get tcs ptcb = Some (prio, t, m)->
TcbMod.join tcbls tcs tcs´ ->
TCBList_P v vl rtbl tcbls ->
y = Int.shru prio ($ 3) ->
bitx = ($ 1) << (Int.and prio ($ 7)) ->
prio_neq_cur tcbls ptcb prio ->
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) ->
TCBList_P v vl (update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (Int.and ry (Int.not bitx)))) tcbls.
Lemma absinfer_mbox_post_exwt_succ:
forall P mqls x v wl tls t ct p st m m´ t´ ,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox m ,wl) ->
~ wl=nil ->
GetHWait tls wl t´ ->
TcbMod.get tls t´ = Some (p,st, m´) ->
absinfer
( <|| mbox_post (Vptr x :: Vptr v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched;;END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmbox m, (remove_tid t´ wl))) ** HTCBList (TcbMod.set tls t´ (p,rdy , (Vptr v)) ) ** HTime t ** HCurTCB ct ** P).
Lemma mbox_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m m2, EcbMod.get v´34 v = Some (absmbox m, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmbox m2, w)) v´35 v´37.
Lemma post_exwt_succ_pre_mbox
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´15 : int32) (v´24 : block)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
(x : val) (x0 : maxlen) (x1 : waitset)
(v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
(v´58 : block) (a : priority) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval),
v´12 <> Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (v´24, Int.zero) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox x , x1) v´6 v´10 ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
TcbJoin (v´58, Int.zero) (a, b, c) v´62 v´7 ->
x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma get_tcb_stat_mbox
: forall (p : int32) (etbl : vallist) (ptbl : list val)
(tid : addrval) (tcbls : TcbMod.map) (abstcb : abstcb.B)
(tcbls´ : TcbMod.map) (vl rtbl : vallist)
(qid : addrval) (vle : list val) (vhold : addrval),
0 <= Int.unsigned p < 64 ->
array_type_vallist_match Int8u etbl ->
length etbl = ∘OS_EVENT_TBL_SIZE ->
prio_in_tbl p etbl ->
nth_val´ (Z.to_nat (Int.unsigned p)) ptbl = Vptr tid ->
R_PrioTbl_P ptbl tcbls vhold ->
TcbJoin tid abstcb tcbls´ tcbls ->
TCBNode_P vl rtbl abstcb ->
R_ECB_ETbl_P qid (V$OS_EVENT_TYPE_MBOX :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_MBOX).
Lemma msglist_p_compose_mbox
: forall (p : val) (qid : addrval) (mqls : EcbMod.map)
(qptrl1 qptrl2 : list EventCtr) (i i1 : int32)
(a : val) (x3 p´ : val) (v´41 : vallist)
(msgqls1 msgqls2 : list EventData) (msgq : EventData)
(mqls1 mqls2 : EcbMod.map) (mq : absecb.B)
(mqls´ : EcbMod.map) (tcbls : TcbMod.map),
R_ECB_ETbl_P qid
(V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 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 ++
((V$OS_EVENT_TYPE_MBOX
:: Vint32 i :: Vint32 i1 :: a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) mqls
tcbls.
Require Import OSQPostPure.
Lemma TCBList_P_post_mbox
: forall (v´42 : val) (v´48 : list vallist) (v´47 : TcbMod.map)
(v´60 : val) (v´50 : list vallist) (v´37 : vallist)
(v´59 v´49 v´44 : TcbMod.map) (v´63 v´64 v´65 : val)
(v´51 v´52 v´53 v´54 v´55 v´56 : int32) (x00 : addrval)
(v´58 : block) (v´40 v´38 : int32) (prio : priority)
(st : taskstatus) (msg0 :msg)
(v´7 v´62 v´43 : TcbMod.map) (v´36 : vallist)
(v´39 : int32) (v´13 : vallist) (vhold : addrval),
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_MBOX
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg0) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: V$0
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil)
:: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37)
(Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero) (prio, rdy, Vptr x00)).
Lemma ECBList_P_Set_Rdy_hold_mbox
: forall (a : list EventCtr) (tcbls : TcbMod.map)
(tid : tidspec.A) (prio : priority) (msg0 msg´ : msg)
(x y : val) (b : list EventData) (c : EcbMod.map)
(eid : ecbid) (nl : int32),
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) nl, msg0) ->
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_post_exwt_hold_mbox
: forall (v´36 : vallist) (v´12 : int32) (v´13 : vallist)
(v´38 v´69 v´39 : int32) (v´58 : block) (v´40 : int32)
(v´32 : block) (v´15 : int32) (v´24 : val)
(v´35 v´16 v´18 v´19 v´20 v´34 : val) (v´21 v´22 : int32)
(v´23 : block) (v´25 v´26 : val) (v´27 : vallist)
(x : list msg) (x0 : maxlen) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map) (x00 : addrval)
(v´11 : EcbMod.map) (v´31 : list EventData)
(v´30 : list EventCtr) (v´29 : val) (v´10 v´9 : EcbMod.map)
(prio : priority) (v´62 : TcbMod.map) (st : taskstatus)
(msg0 : msg) (y : int32) (vhold : addrval),
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
nth_val´ (Z.to_nat (Int.unsigned v´12)) OSUnMapVallist = Vint32 v´38 ->
Int.unsigned v´38 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) v´13 = Vint32 v´69 ->
Int.unsigned v´69 <= 255 ->
nth_val´ (Z.to_nat (Int.unsigned v´69)) OSUnMapVallist = Vint32 v´39 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
Int.unsigned v´40 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMbox v´24) (absmbox v´24, x1) ->
ECBList_P v´0 Vnull v´1 v´5 v´6 v´7 ->
ECBList_P v´29 (Vptr (v´32, Int.zero)) v´30 v´31 v´9 v´7 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox v´24, x1) v´6 v´10 ->
EcbMod.join v´9 v´10 v´11 ->
TcbJoin (v´58, Int.zero) (prio, st, msg0) v´62 v´7 ->
R_PrioTbl_P v´36 v´7 vhold ->
x1 <> nil ->
ECBList_P v´29 Vnull
(v´30 ++
((V$OS_EVENT_TYPE_MBOX
:: Vint32 y
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) :: nil) ++ v´1)
(v´31 ++
(DMbox v´24 ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmbox v´24, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, Vptr x00))
.
Lemma rh_tcblist_ecblist_p_post_exwt_mbox
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : val)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(x00 : addrval) (xl : int32),
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmbox x , x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_mbox eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (absmbox x, remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, Vptr x00)) v´8
.
Lemma rh_tcblist_ecblist_p_post_exwt_aux_mbox
: forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) (x : val)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(st : taskstatus),
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmbox x, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_mbox eid) xl
.
Lemma TCBList_P_post_msg_mbox
: forall (v´42 : val) (v´48 : list vallist) (v´47 : TcbMod.map)
(v´60 : val) (v´50 : list vallist) (v´37 : vallist)
(v´59 v´49 v´44 : TcbMod.map) (v´63 v´64 v´65 : val)
(v´51 v´52 v´53 v´54 v´55 v´56 : int32) (x00 : addrval)
(v´58 : block) (v´40 v´38 : int32) (prio : priority)
(st : taskstatus) (msg : msg)
(v´7 v´62 v´43 : TcbMod.map) (v´36 : vallist)
(v´39 : int32) (v´13 : vallist) (vhold : addrval),
Int.unsigned v´38 <= 7 ->
Int.unsigned v´39 <= 7 ->
nth_val´ (Z.to_nat (Int.unsigned v´39)) OSMapVallist = Vint32 v´40 ->
prio_in_tbl ((v´38<<$ 3)+ᵢv´39) v´13 ->
RL_RTbl_PrioTbl_P v´13 v´36 vhold ->
nth_val´ (Z.to_nat (Int.unsigned ((v´38<<$ 3)+ᵢv´39))) v´36 =
Vptr (v´58, Int.zero) ->
R_PrioTbl_P v´36 v´7 vhold ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_TBL_SIZE ->
TcbMod.join v´44 v´43 v´7 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´62 v´7 ->
get_last_tcb_ptr v´48 v´42 = Some (Vptr (v´58, Int.zero)) ->
TCBList_P v´42 v´48 v´37 v´47 ->
TCBList_P v´60 v´50 v´37 v´59 ->
TcbJoin (v´58, Int.zero) (prio, st, msg) v´59 v´49 ->
TcbMod.join v´47 v´49 v´44 ->
TCBNode_P
(v´60
:: v´63
:: v´64
:: v´65
:: Vint32 v´51
:: V$OS_STAT_MBOX
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil) v´37
(prio, st, msg) ->
TCBList_P v´42
(v´48 ++
(v´60
:: v´63
:: Vnull
:: Vptr x00
:: V$0
:: Vint32 ($ OS_STAT_MBOX&Int.not ($ OS_STAT_MBOX))
:: Vint32 v´52
:: Vint32 v´53
:: Vint32 v´54
:: Vint32 v´55 :: Vint32 v´56 :: nil)
:: v´50)
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´37
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned v´38)) v´37)
(Vint32 v´40))))
(TcbMod.set v´44 (v´58, Int.zero) (prio, rdy, Vptr x00)).
Lemma statmbox_and_not_statmbox_eq_rdy : Int.eq ($ OS_STAT_MBOX&Int.not ($ OS_STAT_MBOX)) ($ OS_STAT_RDY) = true.
Lemma tcb_inrtbl_not_vhold: forall v´42 v´62 v´93 v´57 v´81, RL_RTbl_PrioTbl_P v´42 v´62 v´93 -> prio_in_tbl ((v´57)) v´42 -> nth_val´ (Z.to_nat (Int.unsigned ((v´57)))) v´62 = Vptr (v´81, Int.zero) -> 0 <= Int.unsigned v´57 < 64 -> (v´81, Int.zero) <> v´93.
Lemma le7_le7_range64: forall v´57 v´59, Int.unsigned v´57 <= 7 -> Int.unsigned v´59 <= 7 -> 0 <= Int.unsigned ((v´57<<$ 3)+ᵢv´59) < 64.
Lemma absinfer_mbox_post_put_mail_return : forall P x m mqls tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox Vnull, nil) ->
absinfer (<|| mbox_post (Vptr x :: Vptr m ::nil) ||> **HECBList mqls** HTCBList tcbls ** HTime t ** HCurTCB ct ** P) (<|| END (Some (Vint32 (Int.repr MBOX_POST_SUCC))) ||> **HECBList (EcbMod.set mqls x (absmbox (Vptr m),nil))** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_null_return : forall P x,
can_change_aop P ->
tl_vl_match ((Void) ∗ :: nil) x = true ->
absinfer (<|| mbox_post (Vnull :: x) ||> ** P) ( <|| END (Some (Vint32 (Int.repr MBOX_POST_NULL_ERR))) ||> ** P).
Lemma absinfer_mbox_post_msg_null_return:
forall P v,
can_change_aop P ->
absinfer
( <|| mbox_post (Vptr v :: Vnull ::nil) ||> **
P) (<|| END (Some (Vint32 (Int.repr OS_ERR_POST_NULL_PTR))) ||> **
P).
Lemma absinfer_mbox_post_p_not_legal_return : forall x a P b tcbls t ct,
can_change_aop P ->
EcbMod.get x a = None ->
absinfer (<|| mbox_post (Vptr a ::Vptr b:: nil) ||> ** HECBList x** HTCBList tcbls ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$ MBOX_POST_P_NOT_LEGAL_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_wrong_type_return : forall x a b P tcbls t ct,
can_change_aop P ->
(exists d,
EcbMod.get x a = Some d /\ ~ (exists x wls, d = (absmbox x, wls))) ->
absinfer (<|| mbox_post (Vptr a :: Vptr b :: nil) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct **
P) ( <|| END (Some (V$MBOX_POST_WRONG_TYPE_ERR)) ||> ** HECBList x ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma absinfer_mbox_post_full_return : forall P mqls x a wl y tcbls t ct,
can_change_aop P ->
EcbMod.get mqls x = Some (absmbox a,wl) ->
(exists b, a= Vptr b) ->
absinfer
( <|| mbox_post (Vptr x :: Vptr y :: nil) ||> **HECBList mqls **
HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MBOX_POST_FULL_ERR))) ||> **HECBList mqls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma something_in_not_nil : forall (T:Type) (y: @list T), y<>nil -> exists x, In x y.
Lemma rg1 : forall x2 x6 , 0 <= Int.unsigned x2 < 64->
x6 = $ Int.unsigned x2&$ 7 ->
0<= Int.unsigned x6 < 8.
Lemma rg2 : forall x2 x7 , 0 <= Int.unsigned x2 < 64->
x7 = Int.shru ($ Int.unsigned x2) ($ 3) ->
0<= Int.unsigned x7 < 8.
Lemma post_exwt_succ_pre_mbox´
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´15 : int32) (v´24 : val)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
(x : val) (x1 : waitset)
(v´6 v´10 : EcbMod.map) (v´38 v´69 v´39 : int32)
(v´58 : block) (a : priority)
(c : msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval),
v´12 = Int.zero ->
R_PrioTbl_P v´36 v´7 vhold ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
R_ECB_ETbl_P (v´32, Int.zero)
(V$OS_EVENT_TYPE_MBOX
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig (v´32, Int.zero) (absmbox x , x1) v´6 v´10 ->
x1 = nil
.
Lemma val_inj_lemma: forall m0 a, val_inj (notint (val_inj (val_eq m0 a))) = Vint32 Int.zero \/
val_inj (notint (val_inj (val_eq m0 a))) = Vnull -> m0 = a.
Lemma AOSTCBPrioTbl_high_tcblist_get_msg :
forall tcbls p prio st m vl rtbl m´ s P av,
TcbMod.get tcbls p = Some (prio, st, m) ->
s|= AOSTCBPrioTbl vl rtbl tcbls av ** P ->
s|= AOSTCBPrioTbl vl rtbl (TcbMod.set tcbls p (prio, st, m´)) av ** P.