Library sempend_pure
Require Export sem_common.
Require Export OSQPendPure.
Require Import lab.
Open Scope code_scope.
Hint Resolve CltEnvMod.beq_refl: brel .
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 low_stat_rdy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_TCBblk_P (a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
->
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> Int.eq st ($ OS_STAT_RDY) = true ->
Int.eq e ($ 0) = true ->
t = rdy .
Lemma sempend_TCBListP_head_in_tcb_rdy:
forall v´51 v´52 v´22 x9 x8 i9 i8 i6 i5 i4 i3 v´33 v´50 xx rtbl,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
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)
rtbl v´50 ->
i9 = $ 0 ->
i8 = $ OS_STAT_RDY ->
TcbMod.get v´50 v´52 = Some ( xx, rdy, x8).
Lemma tcblist_p_node_rl_sem:
forall v´33 v´49 v´42 v´47 v´21 x10 x9 i i8 i7 i6 i5 i4 i3 i1 v´32 ,
TCBList_P (Vptr (v´49, Int.zero))
((v´47
:: v´21
:: x10
:: x9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i1 :: nil) :: v´32)
v´33 v´42 ->
RL_TCBblk_P
(v´47
:: v´21
:: x10
:: x9
:: Vint32 i
:: V$OS_STAT_SEM
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: Vint32 i1 :: nil).
Lemma ECBList_P_high_tcb_block_hold_sem:
forall ectrl head tail msgql ecbls tcbls ptcb prio m qid time,
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_sem 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 : 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_SEM :: 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_SEM
:: 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_sem l) time, m))
.
Lemma TCBList_P_tcb_block_hold :
forall ptcb v1 v2 v3 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m qid time ry,
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::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)::m::(Vint32 time)::(Vint32 ($ OS_STAT_SEM))::(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_sem qid) ( time), m)).
Lemma RH_CurTCB_high_block_hold_sem :
forall ptcb tcbls prio st 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_sem qid) time, m)).
Lemma RH_TCBList_ECBList_P_high_block_hold_sem :
forall ecbls tcbls pcur qid m cnt wl prio time,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (abssem cnt, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (abssem cnt, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_sem qid) time, m)) pcur.
Require Export OSQPendPure.
Require Import lab.
Open Scope code_scope.
Hint Resolve CltEnvMod.beq_refl: brel .
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 low_stat_rdy_imp_high:
forall a b c d e f g h i j st rtbl p t m,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
RL_TCBblk_P (a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
->
R_TCB_Status_P
(a
:: b
:: c
:: d
:: Vint32 e
:: Vint32 st
:: Vint32 f
:: g
:: h :: i :: j :: nil)
rtbl (p, t, m) -> Int.eq st ($ OS_STAT_RDY) = true ->
Int.eq e ($ 0) = true ->
t = rdy .
Lemma sempend_TCBListP_head_in_tcb_rdy:
forall v´51 v´52 v´22 x9 x8 i9 i8 i6 i5 i4 i3 v´33 v´50 xx rtbl,
array_type_vallist_match Int8u rtbl ->
length rtbl = ∘OS_RDY_TBL_SIZE ->
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)
rtbl v´50 ->
i9 = $ 0 ->
i8 = $ OS_STAT_RDY ->
TcbMod.get v´50 v´52 = Some ( xx, rdy, x8).
Lemma tcblist_p_node_rl_sem:
forall v´33 v´49 v´42 v´47 v´21 x10 x9 i i8 i7 i6 i5 i4 i3 i1 v´32 ,
TCBList_P (Vptr (v´49, Int.zero))
((v´47
:: v´21
:: x10
:: x9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4
:: Vint32 i3 :: Vint32 i1 :: nil) :: v´32)
v´33 v´42 ->
RL_TCBblk_P
(v´47
:: v´21
:: x10
:: x9
:: Vint32 i
:: V$OS_STAT_SEM
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: Vint32 i1 :: nil).
Lemma ECBList_P_high_tcb_block_hold_sem:
forall ectrl head tail msgql ecbls tcbls ptcb prio m qid time,
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_sem 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 : 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_SEM :: 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_SEM
:: 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_sem l) time, m))
.
Lemma TCBList_P_tcb_block_hold :
forall ptcb v1 v2 v3 v5 v6 v8 v9 v10 v11 rtbl vl
tcbls prio st m qid time ry,
TCBList_P (Vptr ptcb) ((v1::v2::v3::m::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)::m::(Vint32 time)::(Vint32 ($ OS_STAT_SEM))::(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_sem qid) ( time), m)).
Lemma RH_CurTCB_high_block_hold_sem :
forall ptcb tcbls prio st 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_sem qid) time, m)).
Lemma RH_TCBList_ECBList_P_high_block_hold_sem :
forall ecbls tcbls pcur qid m cnt wl prio time,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (abssem cnt, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (abssem cnt, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_sem qid) time, m)) pcur.