Library OSMutexPostPure
Require Import ucert.
Require Import ucert.
Require Import os_code_defs.
Require Import mathlib.
Require Import lab.
Open Scope code_scope.
Lemma post_exwt_succ_pre_mutex´´
: 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) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval) pr o a,
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_MUTEX
:: 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) (absmutexsem pr o , 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 ->
a = (v´38<<$ 3)+ᵢv´39/\ b<> rdy /\x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma post_exwt_succ_pre_mutex
: 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) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval) pr o a,
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_MUTEX
:: 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) (absmutexsem pr o , 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 ->
a = (v´38<<$ 3)+ᵢv´39/\ x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma rl_tbl_grp_p_set_hold:
forall v´12 v´38 v´13 v´69 v´39 v´36 v´58 v´40 v´41,
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 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = true ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 (v´12&Int.not v´41)).
Lemma rl_tbl_grp_p_set_hold´:
forall v´12 v´38 v´37 v´57 v´69 v´39 v´36 v´13 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_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 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
RL_Tbl_Grp_P (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))))
(Vint32 (Int.or v´57 v´41)).
Lemma prio_in_rtbl_hold:
forall rtbl x y prio,
Int.unsigned prio < 64 ->
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl prio rtbl ->
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma idle_in_rtbl_hold´:
forall rtbl x y,
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
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 msglist_p_compose_mutex
: 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_MUTEX
:: 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_MUTEX
:: Vint32 i :: Vint32 i1 :: a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) mqls
tcbls.
Lemma ECBList_P_Set_Rdy_hold_mutex
: 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_mutexsem 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_mutex
: 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´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)
(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) tag (a_very_long_name : Int.ltu (tag>>ᵢ$ 8) prio = true ) optr,
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_MUTEX
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (optr, $ 0) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMutex (Vint32 tag) (Vptr (optr, $0))) (absmutexsem (tag>>ᵢ$ 8) (Some (optr, $ 0, tag&$ OS_MUTEX_KEEP_LOWER_8)) , 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) (absmutexsem (tag>>ᵢ$ 8) (Some (optr,$ 0, tag&$ OS_MUTEX_KEEP_LOWER_8)), 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_MUTEX
:: Vint32 y
:: Vint32 v´15 ::Vptr( v´58, $0) :: 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 ++
(DMutex (Vint32 (Int.or (tag&$ OS_MUTEX_KEEP_UPPER_8) prio)) (Vptr (v´58, $0)) ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmutexsem (tag>>ᵢ$ 8) (Some (v´58, $ 0, prio )), remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, Vptr x00))
.
Require Import OSQPostPure.
Require Import OSMutex_common.
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)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(st : taskstatus) x y,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmutexsem x y, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_mutexsem eid) xl
.
Lemma rh_tcblist_ecblist_p_post_exwt_mutex
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(x00 : addrval) (xl : int32) x y ,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmutexsem x y, x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_mutexsem eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (absmutexsem x (Some (tid, prio)), remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, Vptr x00)) v´8
.
Lemma TCBList_P_post_msg_gen
: 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) x,
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
:: Vint32 x
:: 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_RDY)
:: 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 mutex_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m y, EcbMod.get v´34 v = Some (absmutexsem m y, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmutexsem m None, w)) v´35 v´37.
Lemma return_rh_ctcb :forall v´52 v´39 a b c, RH_CurTCB (v´52, Int.zero) (TcbMod.set v´39 (v´52, Int.zero) (a, b, c)).
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 something_in_not_nil : forall (T:Type) (y: @list T), y<>nil -> exists x, In x y.
Lemma post_exwt_succ_pre_mutex´
: 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 (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) y,
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_MUTEX
:: 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) (absmutexsem x y , x1) v´6 v´10 ->
x1 = nil
.
Lemma get_tcb_stat_mutex
: 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_MUTEX :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_MUTEX).
Lemma mutexandnotmutex : Int.eq ($ OS_STAT_MUTEX&Int.not ($ OS_STAT_MUTEX)) ($ OS_STAT_RDY) = true.
Require Import ucert.
Require Import os_code_defs.
Require Import mathlib.
Require Import lab.
Open Scope code_scope.
Lemma post_exwt_succ_pre_mutex´´
: 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) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval) pr o a,
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_MUTEX
:: 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) (absmutexsem pr o , 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 ->
a = (v´38<<$ 3)+ᵢv´39/\ b<> rdy /\x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma post_exwt_succ_pre_mutex
: 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) (b : taskstatus)
(c :msg) (v´62 v´7 : TcbMod.map)
(vhold : addrval) pr o a,
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_MUTEX
:: 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) (absmutexsem pr o , 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 ->
a = (v´38<<$ 3)+ᵢv´39/\ x1 <> nil /\
GetHWait v´7 x1 (v´58, Int.zero) /\
TcbMod.get v´7 (v´58, Int.zero) = Some (a, b, c)
.
Lemma rl_tbl_grp_p_set_hold:
forall v´12 v´38 v´13 v´69 v´39 v´36 v´58 v´40 v´41,
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 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
Int.eq (v´69&Int.not v´40) Int.zero = true ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P
(update_nth_val (Z.to_nat (Int.unsigned v´38)) v´13
(Vint32 (v´69&Int.not v´40))) (Vint32 (v´12&Int.not v´41)).
Lemma rl_tbl_grp_p_set_hold´:
forall v´12 v´38 v´37 v´57 v´69 v´39 v´36 v´13 v´58 v´40 v´41,
v´12 <> Int.zero ->
Int.unsigned v´12 <= 255 ->
array_type_vallist_match Int8u v´13 ->
length v´13 = ∘OS_EVENT_TBL_SIZE ->
array_type_vallist_match Int8u v´37 ->
length v´37 = ∘OS_RDY_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 ->
nth_val´ (Z.to_nat (Int.unsigned v´38)) OSMapVallist = Vint32 v´41 ->
Int.unsigned v´41 <= 128 ->
RL_Tbl_Grp_P v´13 (Vint32 v´12) ->
RL_Tbl_Grp_P v´37 (Vint32 v´57) ->
RL_Tbl_Grp_P (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))))
(Vint32 (Int.or v´57 v´41)).
Lemma prio_in_rtbl_hold:
forall rtbl x y prio,
Int.unsigned prio < 64 ->
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl prio rtbl ->
prio_in_tbl prio
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
Lemma idle_in_rtbl_hold´:
forall rtbl x y,
Int.unsigned x <= 7 ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO) rtbl ->
prio_in_tbl ($ OS_IDLE_PRIO)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 y)))).
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 msglist_p_compose_mutex
: 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_MUTEX
:: 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_MUTEX
:: Vint32 i :: Vint32 i1 :: a :: x3 :: p´ :: nil, v´41)
:: nil) ++ qptrl2) (msgqls1 ++ (msgq :: nil) ++ msgqls2) mqls
tcbls.
Lemma ECBList_P_Set_Rdy_hold_mutex
: 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_mutexsem 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_mutex
: 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´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)
(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) tag (a_very_long_name : Int.ltu (tag>>ᵢ$ 8) prio = true ) optr,
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_MUTEX
:: Vint32 v´12
:: Vint32 v´15 :: Vptr (optr, $ 0) :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DMutex (Vint32 tag) (Vptr (optr, $0))) (absmutexsem (tag>>ᵢ$ 8) (Some (optr, $ 0, tag&$ OS_MUTEX_KEEP_LOWER_8)) , 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) (absmutexsem (tag>>ᵢ$ 8) (Some (optr,$ 0, tag&$ OS_MUTEX_KEEP_LOWER_8)), 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_MUTEX
:: Vint32 y
:: Vint32 v´15 ::Vptr( v´58, $0) :: 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 ++
(DMutex (Vint32 (Int.or (tag&$ OS_MUTEX_KEEP_UPPER_8) prio)) (Vptr (v´58, $0)) ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(absmutexsem (tag>>ᵢ$ 8) (Some (v´58, $ 0, prio )), remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, Vptr x00))
.
Require Import OSQPostPure.
Require Import OSMutex_common.
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)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(st : taskstatus) x y,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmutexsem x y, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_mutexsem eid) xl
.
Lemma rh_tcblist_ecblist_p_post_exwt_mutex
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A)
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 : msg)
(x00 : addrval) (xl : int32) x y ,
RH_TCBList_ECBList_P v´11 v´7 v´8 ->
EcbMod.join v´9 v´10 v´11 ->
EcbMod.joinsig eid (absmutexsem x y, x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_mutexsem eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (absmutexsem x (Some (tid, prio)), remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, Vptr x00)) v´8
.
Lemma TCBList_P_post_msg_gen
: 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) x,
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
:: Vint32 x
:: 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_RDY)
:: 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 mutex_rh_tcblist_ecblist_p_hold: forall v´34 v´35 v´37 v w m y, EcbMod.get v´34 v = Some (absmutexsem m y, w) ->RH_TCBList_ECBList_P v´34 v´35 v´37 ->
RH_TCBList_ECBList_P
(EcbMod.set v´34 v (absmutexsem m None, w)) v´35 v´37.
Lemma return_rh_ctcb :forall v´52 v´39 a b c, RH_CurTCB (v´52, Int.zero) (TcbMod.set v´39 (v´52, Int.zero) (a, b, c)).
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 something_in_not_nil : forall (T:Type) (y: @list T), y<>nil -> exists x, In x y.
Lemma post_exwt_succ_pre_mutex´
: 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 (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) y,
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_MUTEX
:: 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) (absmutexsem x y , x1) v´6 v´10 ->
x1 = nil
.
Lemma get_tcb_stat_mutex
: 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_MUTEX :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_MUTEX).
Lemma mutexandnotmutex : Int.eq ($ OS_STAT_MUTEX&Int.not ($ OS_STAT_MUTEX)) ($ OS_STAT_RDY) = true.