Library OSQPendPure
Require Export mathlib.
Require Export OSQAcceptPure.
Require Export OSTimeDlyPure.
Lemma OSQOut_elim :
forall osq b,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
exists iout,
(V_OSQOut osq = Some (Vptr (b, iout)) /\
4 <= Int.unsigned iout /\
4 * ((Int.unsigned iout - 4) / 4) = Int.unsigned iout - 4 /\
(Int.unsigned iout - 4) / 4 < OS_MAX_Q_SIZE).
Lemma OSQEnd_elim :
forall osq b qsize,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
V_OSQSize osq = Some (Vint32 qsize) ->
V_OSQEnd osq = Some (Vptr (b, Int.mul qsize ($ 4) +ᵢ ($ 4))).
Lemma OSQStart_elim :
forall osq b qsize,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
V_OSQSize osq = Some (Vint32 qsize) ->
V_OSQStart osq = Some (Vptr (b, ($ 4))).
Lemma RLH_ECBData_P_impl_high_ecb_msg_nil :
forall (qptr qst qend qin qout : val) (size : int32)
(qblk : addrval) (mblk ml : vallist) (A : absecb.B)
(l : val),
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: qout ::Vint32 size :: Vint32 Int.zero :: Vptr qblk :: nil)
mblk ml) A -> exists qmax wl, A = (absmsgq nil qmax, wl).
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_Some´ :
forall tcbls tcur tcurl tcblist rtbl prio,
TCBList_P (Vptr tcur) (tcurl::tcblist) rtbl tcbls ->
V_OSTCBPrio tcurl = Some (Vint32 prio) ->
exists st m, TcbMod.get tcbls tcur = Some (prio, st, m).
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.
Lemma R_ECB_ETbl_P_high_tcb_get_msg_hold :
forall l ecb tcbls ptcb prio st m m´,
R_ECB_ETbl_P l ecb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
R_ECB_ETbl_P l ecb (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma R_ECB_ETbl_P_high_tcb_block_hold :
forall l vl egrp v2 v3 v4 v5 etbl tcbls ptcb prio st m m´ y bity bitx ey time av,
Int.unsigned prio < 64 ->
R_PrioTbl_P vl tcbls av->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_Q
:: Vint32 egrp
:: v2 :: v3 :: v4 :: v5 :: nil,
etbl) tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = Int.shru (prio) ($ 3) ->
bity = ($ 1) << y ->
bitx = ($ 1) << (Int.and (prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_Q
:: 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_q l) time, m´)).
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 ECBList_P_high_tcb_block_hold:
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_q qid) time, 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 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 rtbl_remove_RL_RTbl_PrioTbl_P_hold :
forall prio y bitx rtbl ry ptbl av,
0 <= prio < 64 ->
y = Int.shru ($ prio) ($ 3) ->
bitx = ($ 1) << (Int.and ($ prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) rtbl = Some (Vint32 ry) ->
RL_RTbl_PrioTbl_P rtbl ptbl av->
RL_RTbl_PrioTbl_P
(update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (ry&Int.not bitx))) ptbl av.
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_Q))::(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_q qid) ( time), Vnull)).
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 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 RH_CurTCB_high_block_hold :
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_q qid) time, m´)).
Lemma RH_TCBList_ECBList_P_high_get_msg_hold :
forall ecbls tcbls pcur qid m ml max wl prio m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmsgq (m::ml) max, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m´) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmsgq ml max, wl)) (TcbMod.set tcbls pcur (prio, rdy, m)) pcur.
Require Import Mbox_common.
Lemma RH_TCBList_ECBList_P_high_block_hold :
forall ecbls tcbls pcur qid m ml max wl prio time m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmsgq ml max, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmsgq ml max, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_q qid) time, m´)) pcur.
Lemma tcblist_p_node_rl:
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_Q
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil).
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 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_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).
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 m, TcbMod.get tcbls tcur = Some (i8, rdy, m).
Lemma qpend_absinfer_null:
forall P vl,
can_change_aop P ->
absinfer
( <|| qpend (Vnull :: vl) ||> **
P) (<|| END (Some (V$OS_ERR_PEVENT_NULL)) ||> **
P).
Lemma qpend_absinfer_no_q:
forall P mqls x v,
Int.unsigned v <= 65535 ->
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer
( <|| qpend (Vptr x :: Vint32 v :: nil) ||> **
HECBList mqls ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR))) ||> ** HECBList mqls ** P).
Lemma qpend_absinfer_get:
forall P mqls x v msg ml p m t ct tls n wl,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq (msg::ml) n, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| qpend (Vptr x :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmsgq ml n,wl)) ** HTCBList (TcbMod.set tls ct (p,rdy, msg) ) ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_block:
forall P mqls qid v wl p m t ct tls n,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmsgq nil n, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| qpend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched ;; (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> ** HECBList (EcbMod.set mqls qid (absmsgq nil n,ct::wl)) ** HTCBList (TcbMod.set tls ct (p,wait (os_stat_q qid) v, Vnull) ) ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_to:
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
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_block_get:
forall P mqls qid v p t ct tls m st,
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p,st,m) ->
m<>Vnull ->
absinfer
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma OSQPend_high_step_null :
forall qid timeout P,
qid = Vnull ->
Int.unsigned timeout <= 65535 ->
can_change_aop P ->
absinfer ( <|| qpend (qid :: Vint32 timeout :: nil) ||> ** P)
( <|| END Some (V$OS_ERR_PEVENT_NULL) ||> ** P).
Lemma OSQPend_high_step_get_succ :
forall qid timeout msg ml n wl ecbls tls t tcur prio m P,
Int.unsigned timeout <= 65535 ->
EcbMod.get ecbls qid = Some (absmsgq (msg :: ml) n, wl) ->
TcbMod.get tls tcur = Some (prio, rdy, m)->
can_change_aop P ->
absinfer ( <|| qpend (Vptr qid :: Vint32 timeout :: nil) ||> **
HECBList ecbls ** HTCBList tls ** HTime t ** HCurTCB tcur ** P)
(<|| END (Some (V$NO_ERR)) ||> **
Aabsdata absecblsid (absecblist (EcbMod.set ecbls qid (absmsgq ml n, wl))) **
Aabsdata abtcblsid (abstcblist (TcbMod.set tls tcur (prio, rdy, msg))) **
HTime t ** HCurTCB tcur ** P).
Lemma OSQPend_high_step_block :
forall qid timeout wl n ecbls tls t tcur prio m P,
Int.unsigned timeout <= 65535 ->
EcbMod.get ecbls qid = Some (absmsgq nil n, wl) ->
TcbMod.get tls tcur = Some (prio, rdy, m)->
can_change_aop P ->
absinfer ( <|| qpend (Vptr qid :: Vint32 timeout :: nil) ||> **
HECBList ecbls ** HTCBList tls ** HTime t ** HCurTCB tcur ** P)
(<|| isched ;; (qpend_to (|Vptr qid :: Vint32 timeout :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 timeout :: nil|)) ||> **
Aabsdata absecblsid (absecblist (EcbMod.set ecbls qid (absmsgq nil n, tcur::wl))) **
Aabsdata abtcblsid (abstcblist (TcbMod.set tls tcur (prio, wait (os_stat_q qid) timeout, Vnull))) **
HTime t ** HCurTCB tcur ** P).
Lemma OSQPend_high_step_to :
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
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma OSQPend_high_step_block_get :
forall P mqls qid v p t ct tls m st,
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p,st,m) ->
m<>Vnull ->
absinfer
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_idle :
forall P ecbls tcbls t ct st msg v x,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (Int.repr OS_IDLE_PRIO, st, msg) ->
can_change_aop P ->
absinfer (<|| qpend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absimp_stat_err :
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 (<|| qpend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma event_type_n_match:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DSem i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma xx:forall x16,isptr x16 -> val_inj (notint (val_inj (val_eq x16 Vnull))) = Vint32 Int.zero -> x16=Vnull.
Lemma xx´:forall x16,isptr x16 -> val_inj (notint (val_inj (val_eq x16 Vnull))) = Vnull -> False.
Require Export OSQAcceptPure.
Require Export OSTimeDlyPure.
Lemma OSQOut_elim :
forall osq b,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
exists iout,
(V_OSQOut osq = Some (Vptr (b, iout)) /\
4 <= Int.unsigned iout /\
4 * ((Int.unsigned iout - 4) / 4) = Int.unsigned iout - 4 /\
(Int.unsigned iout - 4) / 4 < OS_MAX_Q_SIZE).
Lemma OSQEnd_elim :
forall osq b qsize,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
V_OSQSize osq = Some (Vint32 qsize) ->
V_OSQEnd osq = Some (Vptr (b, Int.mul qsize ($ 4) +ᵢ ($ 4))).
Lemma OSQStart_elim :
forall osq b qsize,
WellformedOSQ osq ->
V_qfreeblk osq = Some (Vptr (b, Int.zero)) ->
V_OSQSize osq = Some (Vint32 qsize) ->
V_OSQStart osq = Some (Vptr (b, ($ 4))).
Lemma RLH_ECBData_P_impl_high_ecb_msg_nil :
forall (qptr qst qend qin qout : val) (size : int32)
(qblk : addrval) (mblk ml : vallist) (A : absecb.B)
(l : val),
RLH_ECBData_P
(DMsgQ l
(qptr
:: qst
:: qend
:: qin
:: qout ::Vint32 size :: Vint32 Int.zero :: Vptr qblk :: nil)
mblk ml) A -> exists qmax wl, A = (absmsgq nil qmax, wl).
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_Some´ :
forall tcbls tcur tcurl tcblist rtbl prio,
TCBList_P (Vptr tcur) (tcurl::tcblist) rtbl tcbls ->
V_OSTCBPrio tcurl = Some (Vint32 prio) ->
exists st m, TcbMod.get tcbls tcur = Some (prio, st, m).
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.
Lemma R_ECB_ETbl_P_high_tcb_get_msg_hold :
forall l ecb tcbls ptcb prio st m m´,
R_ECB_ETbl_P l ecb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
R_ECB_ETbl_P l ecb (TcbMod.set tcbls ptcb (prio, st, m´)).
Lemma R_ECB_ETbl_P_high_tcb_block_hold :
forall l vl egrp v2 v3 v4 v5 etbl tcbls ptcb prio st m m´ y bity bitx ey time av,
Int.unsigned prio < 64 ->
R_PrioTbl_P vl tcbls av->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_Q
:: Vint32 egrp
:: v2 :: v3 :: v4 :: v5 :: nil,
etbl) tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = Int.shru (prio) ($ 3) ->
bity = ($ 1) << y ->
bitx = ($ 1) << (Int.and (prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_Q
:: 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_q l) time, m´)).
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 ECBList_P_high_tcb_block_hold:
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_q qid) time, 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 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 rtbl_remove_RL_RTbl_PrioTbl_P_hold :
forall prio y bitx rtbl ry ptbl av,
0 <= prio < 64 ->
y = Int.shru ($ prio) ($ 3) ->
bitx = ($ 1) << (Int.and ($ prio) ($ 7)) ->
nth_val ∘(Int.unsigned y) rtbl = Some (Vint32 ry) ->
RL_RTbl_PrioTbl_P rtbl ptbl av->
RL_RTbl_PrioTbl_P
(update_nth_val ∘(Int.unsigned y) rtbl (Vint32 (ry&Int.not bitx))) ptbl av.
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_Q))::(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_q qid) ( time), Vnull)).
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 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 RH_CurTCB_high_block_hold :
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_q qid) time, m´)).
Lemma RH_TCBList_ECBList_P_high_get_msg_hold :
forall ecbls tcbls pcur qid m ml max wl prio m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmsgq (m::ml) max, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m´) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmsgq ml max, wl)) (TcbMod.set tcbls pcur (prio, rdy, m)) pcur.
Require Import Mbox_common.
Lemma RH_TCBList_ECBList_P_high_block_hold :
forall ecbls tcbls pcur qid m ml max wl prio time m´,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmsgq ml max, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmsgq ml max, pcur::wl)) (TcbMod.set tcbls pcur (prio, wait (os_stat_q qid) time, m´)) pcur.
Lemma tcblist_p_node_rl:
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_Q
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6 :: Vint32 i5 :: Vint32 i1 :: nil).
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 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_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).
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 m, TcbMod.get tcbls tcur = Some (i8, rdy, m).
Lemma qpend_absinfer_null:
forall P vl,
can_change_aop P ->
absinfer
( <|| qpend (Vnull :: vl) ||> **
P) (<|| END (Some (V$OS_ERR_PEVENT_NULL)) ||> **
P).
Lemma qpend_absinfer_no_q:
forall P mqls x v,
Int.unsigned v <= 65535 ->
can_change_aop P ->
(~ exists a b wl,EcbMod.get mqls x = Some (absmsgq a b,wl)) ->
absinfer
( <|| qpend (Vptr x :: Vint32 v :: nil) ||> **
HECBList mqls ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR))) ||> ** HECBList mqls ** P).
Lemma qpend_absinfer_get:
forall P mqls x v msg ml p m t ct tls n wl,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls x = Some (absmsgq (msg::ml) n, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| qpend (Vptr x :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR))) ||> ** HECBList (EcbMod.set mqls x (absmsgq ml n,wl)) ** HTCBList (TcbMod.set tls ct (p,rdy, msg) ) ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_block:
forall P mqls qid v wl p m t ct tls n,
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmsgq nil n, wl) ->
TcbMod.get tls ct = Some (p,rdy,m) ->
absinfer
( <|| qpend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| isched ;; (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> ** HECBList (EcbMod.set mqls qid (absmsgq nil n,ct::wl)) ** HTCBList (TcbMod.set tls ct (p,wait (os_stat_q qid) v, Vnull) ) ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_to:
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
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_block_get:
forall P mqls qid v p t ct tls m st,
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p,st,m) ->
m<>Vnull ->
absinfer
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma OSQPend_high_step_null :
forall qid timeout P,
qid = Vnull ->
Int.unsigned timeout <= 65535 ->
can_change_aop P ->
absinfer ( <|| qpend (qid :: Vint32 timeout :: nil) ||> ** P)
( <|| END Some (V$OS_ERR_PEVENT_NULL) ||> ** P).
Lemma OSQPend_high_step_get_succ :
forall qid timeout msg ml n wl ecbls tls t tcur prio m P,
Int.unsigned timeout <= 65535 ->
EcbMod.get ecbls qid = Some (absmsgq (msg :: ml) n, wl) ->
TcbMod.get tls tcur = Some (prio, rdy, m)->
can_change_aop P ->
absinfer ( <|| qpend (Vptr qid :: Vint32 timeout :: nil) ||> **
HECBList ecbls ** HTCBList tls ** HTime t ** HCurTCB tcur ** P)
(<|| END (Some (V$NO_ERR)) ||> **
Aabsdata absecblsid (absecblist (EcbMod.set ecbls qid (absmsgq ml n, wl))) **
Aabsdata abtcblsid (abstcblist (TcbMod.set tls tcur (prio, rdy, msg))) **
HTime t ** HCurTCB tcur ** P).
Lemma OSQPend_high_step_block :
forall qid timeout wl n ecbls tls t tcur prio m P,
Int.unsigned timeout <= 65535 ->
EcbMod.get ecbls qid = Some (absmsgq nil n, wl) ->
TcbMod.get tls tcur = Some (prio, rdy, m)->
can_change_aop P ->
absinfer ( <|| qpend (Vptr qid :: Vint32 timeout :: nil) ||> **
HECBList ecbls ** HTCBList tls ** HTime t ** HCurTCB tcur ** P)
(<|| isched ;; (qpend_to (|Vptr qid :: Vint32 timeout :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 timeout :: nil|)) ||> **
Aabsdata absecblsid (absecblist (EcbMod.set ecbls qid (absmsgq nil n, tcur::wl))) **
Aabsdata abtcblsid (abstcblist (TcbMod.set tls tcur (prio, wait (os_stat_q qid) timeout, Vnull))) **
HTime t ** HCurTCB tcur ** P).
Lemma OSQPend_high_step_to :
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
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma OSQPend_high_step_block_get :
forall P mqls qid v p t ct tls m st,
Int.unsigned v <= 65535 ->
can_change_aop P ->
TcbMod.get tls ct = Some (p,st,m) ->
m<>Vnull ->
absinfer
( <|| (qpend_to (|Vptr qid :: Vint32 v :: nil|) ?? qpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr NO_ERR)))||> ** HECBList mqls ** HTCBList tls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absinfer_idle :
forall P ecbls tcbls t ct st msg v x,
Int.unsigned v <= 65535 ->
TcbMod.get tcbls ct = Some (Int.repr OS_IDLE_PRIO, st, msg) ->
can_change_aop P ->
absinfer (<|| qpend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma qpend_absimp_stat_err :
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 (<|| qpend (Vptr x :: Vint32 v :: nil) ||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr MSGQ_NULL_ERR)))||> ** HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct ** P).
Lemma event_type_n_match:
forall s P i1 i0 i2 x2 x3 v´42 i10,
s|= AEventData
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´42 :: nil)
(DSem i10) ** P ->
Int.eq i1 ($ OS_EVENT_TYPE_Q) = true ->
False.
Lemma xx:forall x16,isptr x16 -> val_inj (notint (val_inj (val_eq x16 Vnull))) = Vint32 Int.zero -> x16=Vnull.
Lemma xx´:forall x16,isptr x16 -> val_inj (notint (val_inj (val_eq x16 Vnull))) = Vnull -> False.