Library sempost_pure
Require Export sem_common.
Require Export OSQPostPure.
Open Scope code_scope.
Lemma sempost_ltu_trans:
forall n,
Int.ltu n ($ 65535) = true ->
Int.ltu (n+ᵢ$ 1) ($ 65536) = true.
Lemma sempost_inc_cnt_prop:
forall s P a msgq mq a´ msgq´ mq´ n i x2 x3 x4 qid b tcbls,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
R_ECB_ETbl_P qid (a,b) tcbls ->
a = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 n :: x2 :: x3 :: x4 :: nil) ->
msgq = DSem n ->
mq = (abssem n, nil) ->
a´ = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 (n+ᵢ$ 1) :: x2 :: x3 :: x4 :: nil) ->
msgq´ = DSem (n+ᵢ$ 1) ->
mq´ = (abssem (n+ᵢ$ 1), nil) ->
Int.ltu n ($ 65535) = true ->
s |= AEventData a´ msgq´ **
[| RLH_ECBData_P msgq´ mq´ |] **
[| R_ECB_ETbl_P qid (a´,b) tcbls |] ** 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 sempost_grp_wls_nil:
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),
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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem x , x1) v´6 v´10 ->
x1 = nil.
Lemma post_exwt_succ_pre_sem
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´24 : block)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
x (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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem 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 sem_post_get_tcb_stat
: 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_SEM :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_SEM).
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 TCBList_P_post_sem:
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 msg1: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_SEM
:: 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
:: msg1
:: 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, msg1)).
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 ECBList_P_Set_Rdy_hold_sem
: 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_sem 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_sem
: 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 : val) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map)
(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 msg1: msg) (y : int32) (vhold : addrval),
Int.unsigned v´15 <= 65535 ->
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_SEM
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DSem v´15) (abssem v´15, 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) (abssem v´15, 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_SEM
:: 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 ++
(DSem v´15 ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(abssem v´15, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, msg1))
.
Lemma rh_tcblist_ecblist_p_post_exwt_aux_sem
: forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) x
(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 (abssem x, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_sem eid) xl
.
Lemma rh_tcblist_ecblist_p_post_exwt_sem
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) x
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 msg1: 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 (abssem x , x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_sem eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (abssem x, remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, msg1)) v´8
.
Lemma sempost_grp_wls_nil´:
forall v´36 v´6 vhold v´7 v´13 v´12 v´32 x v´24 v´35 v´0 v´11 v´8 v´9 v´10 x1,
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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem x , x1) v´6 v´10 ->
x1 = nil.
Lemma sempost_inc_RH_TCBList_ECBList_P_hold:
forall mqls tcbls ct a n wl,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a = Some (abssem n, wl) ->
Int.ltu n ($ 65535) = true ->
RH_TCBList_ECBList_P
(EcbMod.set mqls a (abssem (Int.add n Int.one), wl)) tcbls ct.
Lemma node_fold´:
forall s P vl t b,
s |= Astruct (b, Int.zero) t vl ** P ->
struct_type_vallist_match t vl ->
s |= node (Vptr (b, Int.zero)) vl t ** P.
Lemma sempost_vallist_match_assert1:
forall x,
Int.ltu x ($ 65535) = true ->
Int.unsigned (Int.add x Int.one) <= 65535.
Lemma sempost_struct_type_vallist_match_sem:
forall i1 x2 x3 v´44,
isptr v´44 ->
isptr x2 ->
Int.ltu i1 ($ 65535) = true ->
struct_type_vallist_match OS_EVENT
(V$OS_EVENT_TYPE_SEM
:: V$0 :: Vint32 (i1+ᵢ$ 1) :: x2 :: x3 :: v´44 :: nil).
Require Export OSQPostPure.
Open Scope code_scope.
Lemma sempost_ltu_trans:
forall n,
Int.ltu n ($ 65535) = true ->
Int.ltu (n+ᵢ$ 1) ($ 65536) = true.
Lemma sempost_inc_cnt_prop:
forall s P a msgq mq a´ msgq´ mq´ n i x2 x3 x4 qid b tcbls,
s |= AEventData a msgq ** P ->
RLH_ECBData_P msgq mq ->
R_ECB_ETbl_P qid (a,b) tcbls ->
a = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 n :: x2 :: x3 :: x4 :: nil) ->
msgq = DSem n ->
mq = (abssem n, nil) ->
a´ = (V$OS_EVENT_TYPE_SEM :: Vint32 i :: Vint32 (n+ᵢ$ 1) :: x2 :: x3 :: x4 :: nil) ->
msgq´ = DSem (n+ᵢ$ 1) ->
mq´ = (abssem (n+ᵢ$ 1), nil) ->
Int.ltu n ($ 65535) = true ->
s |= AEventData a´ msgq´ **
[| RLH_ECBData_P msgq´ mq´ |] **
[| R_ECB_ETbl_P qid (a´,b) tcbls |] ** 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 sempost_grp_wls_nil:
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),
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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem x , x1) v´6 v´10 ->
x1 = nil.
Lemma post_exwt_succ_pre_sem
: forall (v´36 v´13 : vallist) (v´12 : int32)
(v´32 : block) (v´24 : block)
(v´35 v´0 : val) (v´8 : tid) (v´9 v´11 : EcbMod.map)
x (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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem 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 sem_post_get_tcb_stat
: 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_SEM :: vle, etbl) tcbls ->
V_OSTCBStat vl = Some (V$OS_STAT_SEM).
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 TCBList_P_post_sem:
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 msg1: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_SEM
:: 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
:: msg1
:: 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, msg1)).
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 ECBList_P_Set_Rdy_hold_sem
: 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_sem 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_sem
: 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 : val) (x1 : waitset)
(v´0 : val) (v´1 : list EventCtr) (v´5 : list EventData)
(v´6 : EcbMod.map) (v´7 : TcbMod.map)
(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 msg1: msg) (y : int32) (vhold : addrval),
Int.unsigned v´15 <= 65535 ->
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_SEM
:: Vint32 v´12
:: Vint32 v´15 :: v´24 :: v´35 :: v´0 :: nil,
v´13) v´7 ->
RLH_ECBData_P
(DSem v´15) (abssem v´15, 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) (abssem v´15, 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_SEM
:: 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 ++
(DSem v´15 ::nil)
++ v´5)
(EcbMod.set v´11 (v´32, Int.zero)
(abssem v´15, remove_tid (v´58, Int.zero) x1))
(TcbMod.set v´7 (v´58, Int.zero) (prio, rdy, msg1))
.
Lemma rh_tcblist_ecblist_p_post_exwt_aux_sem
: forall (v´8 tid0 : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) x
(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 (abssem x, x1) v´6 v´10 ->
In tid0 x1 ->
TcbMod.get v´7 tid0 = Some (prio, st, msg0) ->
exists xl, st = wait (os_stat_sem eid) xl
.
Lemma rh_tcblist_ecblist_p_post_exwt_sem
: forall (v´8 tid : tid) (v´11 : EcbMod.map)
(v´7 : TcbMod.map) (v´9 v´10 : EcbMod.map)
(eid : tidspec.A) x
(x0 : maxlen) (x1 : waitset) (v´6 : EcbMod.map)
(prio : priority) (msg0 msg1: 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 (abssem x , x1) v´6 v´10 ->
In tid x1 ->
TcbMod.get v´7 tid = Some (prio, wait (os_stat_sem eid) xl, msg0) ->
RH_TCBList_ECBList_P
(EcbMod.set v´11 eid (abssem x, remove_tid tid x1))
(TcbMod.set v´7 tid (prio, rdy, msg1)) v´8
.
Lemma sempost_grp_wls_nil´:
forall v´36 v´6 vhold v´7 v´13 v´12 v´32 x v´24 v´35 v´0 v´11 v´8 v´9 v´10 x1,
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_SEM
:: Vint32 v´12
:: Vint32 x :: 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) (abssem x , x1) v´6 v´10 ->
x1 = nil.
Lemma sempost_inc_RH_TCBList_ECBList_P_hold:
forall mqls tcbls ct a n wl,
RH_TCBList_ECBList_P mqls tcbls ct ->
EcbMod.get mqls a = Some (abssem n, wl) ->
Int.ltu n ($ 65535) = true ->
RH_TCBList_ECBList_P
(EcbMod.set mqls a (abssem (Int.add n Int.one), wl)) tcbls ct.
Lemma node_fold´:
forall s P vl t b,
s |= Astruct (b, Int.zero) t vl ** P ->
struct_type_vallist_match t vl ->
s |= node (Vptr (b, Int.zero)) vl t ** P.
Lemma sempost_vallist_match_assert1:
forall x,
Int.ltu x ($ 65535) = true ->
Int.unsigned (Int.add x Int.one) <= 65535.
Lemma sempost_struct_type_vallist_match_sem:
forall i1 x2 x3 v´44,
isptr v´44 ->
isptr x2 ->
Int.ltu i1 ($ 65535) = true ->
struct_type_vallist_match OS_EVENT
(V$OS_EVENT_TYPE_SEM
:: V$0 :: Vint32 (i1+ᵢ$ 1) :: x2 :: x3 :: v´44 :: nil).