Library OSMutexPendPure1
Require Import sem_common.
Require Import sempend_pure.
Require Import os_mutex.
Require Import OSMutex_common.
Require Import OSEventTaskRdyPure.
Require Import OSQPendPure.
Require Import OSQPostPure.
Require Import mathlib.
Open Scope code_scope.
Lemma aux_trivial:
forall x, Int.unsigned x < 64 -> Int.unsigned (x>>ᵢ$ 3) < 8.
Lemma and7_lt8:
forall x, Int.unsigned x < 64 -> Int.unsigned (x & $ 7) < 8.
Section lzh_join.
Lemma mund_disj_sub_l:
forall ma mb ma´,
TcbMod.disj ma mb ->
TcbMod.sub ma´ ma ->
TcbMod.disj ma´ mb.
Hint Resolve mund_disj_sub_l.
Lemma mund_disj_sub_r:
forall ma mb mb´,
TcbMod.disj ma mb ->
TcbMod.sub mb´ mb ->
TcbMod.disj ma mb´.
Hint Resolve mund_disj_sub_r.
Lemma mund_disj_sub_w:
forall ma mb ma´ mb´,
TcbMod.disj ma mb ->
TcbMod.sub ma´ ma ->
TcbMod.sub mb´ mb ->
TcbMod.disj ma´ mb´.
Hint Resolve mund_disj_sub_w.
Lemma join_prop_mutexpend:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join x2 (TcbMod.sig (ptcb_addr, Int.zero) p_st)
(TcbMod.merge (TcbMod.sig (ptcb_addr, Int.zero) p_st) x2)
.
Hint Resolve TcbMod.get_sig_some.
Hint Resolve TcbMod.join_sub_l.
Hint Resolve TcbMod.join_sub_r.
Hint Resolve TcbMod.sub_sig.
Hint Resolve TcbMod.meq_merge_sym.
Hint Resolve TcbMod.compat_sym.
Lemma rtbl_remove_RL_RTbl_PrioTbl_P_hold´´:
forall (prio : Z) (y bitx : int32) (rtbl : vallist)
(ry : int32) (ptbl : vallist) (av : addrval),
0 <= prio < 64 ->
y = $ prio>>ᵢ$ 3 ->
bitx = $ 1<<($ 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)))
(update_nth_val (∘prio) ptbl (Vptr av))
av.
Lemma join_prop_mutexpend´:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52 y,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join (TcbMod.set tcbls_l (ptcb_addr, Int.zero) y)
(TcbMod.sig (v´38, Int.zero) cur_st)
(TcbMod.merge (TcbMod.sig (v´38, Int.zero) cur_st)
(TcbMod.set tcbls_l (ptcb_addr, Int.zero) y)).
Lemma join_mutexpend´:
forall x y x1 y1 y1´ y´ l1 l2 l3 L L´,
TcbJoin x y´ L´ L ->
TcbMod.join l3 l2 L´ ->
TcbMod.joinsig x1 y1´ l1 l2 ->
TcbJoin x y (TcbMod.set L´ x1 y1) (TcbMod.set (TcbMod.set L x y) x1 y1).
Hint Resolve TcbMod.get_indom.
Hint Resolve tcbmod_joinsig_get.
Lemma join_prop_mutexpend´´:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52 y z,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join (TcbMod.set tcbls_l (ptcb_addr, Int.zero) z)
(TcbMod.set tcbls_r (v´38, Int.zero)
y)
(TcbMod.set
(TcbMod.set tcbls (v´38, Int.zero)
y)
(ptcb_addr, Int.zero) z).
Hint Resolve TcbMod.get_indom.
Lemma join_prop_mutexpend´´´:
forall x y m n b c,
m <> x ->
TcbMod.join (TcbMod.sig m n) b c ->
TcbMod.join (TcbMod.sig m n) (TcbMod.set b x y) (TcbMod.merge (TcbMod.sig m n) (TcbMod.set b x y)).
Lemma join_prop_mutexpend´´´´:
forall a b c x y b´,
TcbMod.join a b c ->
TcbJoin x y b´ b ->
TcbMod.join b´ (TcbMod.merge a (TcbMod.sig x y)) c.
End lzh_join.
Lemma evsllseg_aux:
forall l1 s a b l2 P,
s |= evsllseg a b l1 l2 ** P ->
(a = b /\ l1 = nil \/ get_last_ptr l1 = Some b) /\ length l1 = length l2.
Lemma prio_neq_cur_set:
forall tcbls_l v´38 cur_prio x xm ptcb_addr ptcb_prio,
prio_neq_cur tcbls_l (v´38, Int.zero) cur_prio ->
TcbMod.get tcbls_l (ptcb_addr, Int.zero) =
Some (ptcb_prio, rdy, xm) ->
Int.ltu x cur_prio = true ->
prio_neq_cur (TcbMod.set tcbls_l (ptcb_addr, Int.zero) (x, rdy, xm))
(v´38, Int.zero) cur_prio.
Lemma RL_RTbl_PrioTbl_P_set_vhold:
forall v´45 v´43 x11 xm x y ptcb_prio i8 ptcb_tcby ptcb_bitx ptcb_bity v´53 os_rdy_tbl v0 v´32,
RL_TCBblk_P
(v´45
:: v´43
:: x11
:: xm
:: x
:: y
:: Vint32 ptcb_prio
:: Vint32 i8
:: Vint32 ptcb_tcby
:: Vint32 ptcb_bitx
:: Vint32 ptcb_bity :: nil) ->
(Z.to_nat (Int.unsigned (ptcb_prio>>ᵢ$ 3)) < length os_rdy_tbl)%nat ->
nth_val´ (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl =
Vint32 v0 ->
RL_RTbl_PrioTbl_P os_rdy_tbl v´32 v´53 ->
RL_RTbl_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_prio)) v´32 (Vptr v´53))
v´53.
Lemma R_PrioTbl_Pend_lift:
forall ptcb_addr v´38 x v´53 v´32 tcbls cur_prio ptcb_prio xm v´46 i,
(length v´32 = 64)%nat ->
Int.unsigned cur_prio < 64 ->
Int.unsigned (x>>ᵢ$ 8) < 64 ->
Int.unsigned ptcb_prio < 64 ->
(ptcb_addr,Int.zero) <> (v´38,Int.zero) ->
(nth_val´ (Z.to_nat (Int.unsigned (x>>ᵢ$ 8))) v´32) = (Vptr v´53) ->
R_PrioTbl_P v´32 tcbls v´53 ->
TcbMod.get tcbls (v´38, Int.zero) = Some (cur_prio, rdy, Vnull) ->
TcbMod.get tcbls (ptcb_addr, Int.zero) = Some (ptcb_prio, rdy, xm) ->
R_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned (x>>ᵢ$ 8)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_prio)) v´32 (Vptr v´53))
(Vptr (ptcb_addr, Int.zero)))
(TcbMod.set
(TcbMod.set tcbls (v´38, Int.zero)
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull))
(ptcb_addr, Int.zero) (x>>ᵢ$ 8, rdy, xm)) v´53.
Ltac simpl_vqm :=
repeat
match goal with
| H: ?f _ = Some _ |- _ => simpl in H;inverts H
| _ => idtac
end.
Lemma neg_priointbl_prionotintbl:
forall p tbl,
Int.unsigned p < 64 ->
array_type_vallist_match Int8u tbl ->
length tbl = ∘OS_RDY_TBL_SIZE ->
~ prio_in_tbl p tbl -> prio_not_in_tbl p tbl.
Lemma R_TCB_Status_mutexpend_lift:
forall cur_prio ptcb_prio prio_lift x0 v´26 x12 i5 v´64 v´65 i1 v´45 v´43 x11 xm i8
ptcb_tcby ptcb_bitx ptcb_bity v´46 v´67 x5 v0 os_rdy_tbl i,
length os_rdy_tbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u
(update_nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx)))
(val_inj
(or
(nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx))))
(Vint32 ($ 1<<(prio_lift&$ 7))))))
(Vint32 (v´67&Int.not v´65))) ->
cur_prio <> ptcb_prio ->
ptcb_prio <> prio_lift ->
nth_val´ (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl = Vint32 v0 ->
nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx))) = Vint32 x5 ->
Int.unsigned prio_lift < 64 ->
TCBNode_P
(x0
:: v´26
:: x12
:: Vnull
:: V$0
:: V$OS_STAT_RDY
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64
:: Vint32 v´65 :: Vint32 i1 :: nil)
os_rdy_tbl (cur_prio, rdy, Vnull) ->
RL_TCBblk_P
(v´45
:: v´43
:: x11
:: xm
:: V$0
:: V$OS_STAT_RDY
:: Vint32 ptcb_prio
:: Vint32 i8
:: Vint32 ptcb_tcby
:: Vint32 ptcb_bitx
:: Vint32 ptcb_bity :: nil) ->
Int.ltu prio_lift cur_prio = true ->
nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(val_inj
(or
(nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx))))
(Vint32 ($ 1<<(prio_lift&$ 7)))))) =
Some (Vint32 v´67) ->
R_TCB_Status_P
(x0
:: v´26
:: Vptr (v´46, Int.zero)
:: Vnull
:: Vint32 i
:: V$OS_STAT_MUTEX
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64 :: Vint32 v´65 :: Vint32 i1 :: nil)
(update_nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(Vint32 (Int.or x5 ($ 1<<(prio_lift&$ 7)))))
(Vint32 (v´67&Int.not v´65)))
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull).
Lemma absinfer_mutex_pend_lift_is_rdy_block:
forall P mqls qid v wl p m t ct tls tid opr pr m´ p´,
ct <>tid ->
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmutexsem pr (Some (tid, p´)), wl) ->
TcbMod.get tls ct = Some (p, rdy, m) ->
TcbMod.get tls tid = Some (opr, rdy, m´) ->
Int.eq opr pr = false ->
Int.ltu p p´ = true ->
Int.ltu pr p = true ->
absinfer
( <|| mutexpend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| isched;;
(mutexpend_to (|Vptr qid :: Vint32 v :: nil|) ??
mutexpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList ( EcbMod.set mqls qid (absmutexsem pr (Some (tid, p´)), ct :: wl) ) **
HTCBList (TcbMod.set
(TcbMod.set tls
ct (p,wait (os_stat_mutexsem qid) v, m))
tid (pr, rdy, m´)) **
HTime t **
HCurTCB ct ** P).
Lemma tcbdllseg_cons:
forall s tid h p´ tail tailnext l P pre,
struct_type_vallist_match OS_TCB h ->
s |= Astruct (tid,Int.zero) OS_TCB h **
tcbdllseg p´ (Vptr (tid,Int.zero)) tail tailnext l ** P ->
V_OSTCBNext h = Some p´ ->
V_OSTCBPrev h = Some pre ->
s |= tcbdllseg (Vptr (tid,Int.zero)) pre tail tailnext (h::l) ** P.
Lemma tcbdllseg_l_not_nil:
forall head l rtbl tcbls tid v,
TCBList_P head l rtbl tcbls ->
TcbMod.get tcbls tid = Some v ->
exists h l´, l = h :: l´.
Lemma dllseg_compose:
forall (s : RstateOP) (P : asrt) (h hp t1 tn1 t2 tn2 : val)
(l1 l2 : list vallist),
s |= dllseg h hp t1 tn1 l1 OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl) ** dllseg tn1 t1 t2 tn2 l2 OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl)** P ->
s |= dllseg h hp t2 tn2 (l1 ++ l2) OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl) ** P.
Lemma mutexpend_block_no_lift_step:
forall P els tls tm ct i eid els´ tls´ t´ pt m m´ px p´ wl p,
can_change_aop P ->
EcbMod.get els eid = Some (absmutexsem p (Some (t´, p´)), wl) ->
TcbMod.get tls ct = Some (pt, rdy, m) ->
TcbMod.get tls t´ = Some (px, rdy, m´) ->
(Int.eq px p <> false \/ Int.ltu p´ pt = true) ->
els´ = EcbMod.set els eid (absmutexsem p (Some (t´, p´)), ct :: wl) ->
tls´ = TcbMod.set tls ct (pt, wait (os_stat_mutexsem eid) i, Vnull) ->
Int.ltu p pt = true ->
absinfer (<|| mutexpend (Vptr eid :: Vint32 i :: nil) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| isched;;(mutexpend_to (| Vptr eid :: Vint32 i :: nil |) ?? mutexpend_block_get (|Vptr eid :: Vint32 i :: nil|)) ||> **
HECBList els´ **
HTCBList tls´ **
HTime tm **
HCurTCB ct ** P).
Lemma mutexpend_block_timeout_step:
forall P els tls tm ct i eid st pt,
can_change_aop P ->
TcbMod.get tls ct = Some (pt, st, Vnull) ->
absinfer (<||
mutexpend_to (|Vptr eid :: Vint32 i :: nil|)
?? mutexpend_block_get
(|Vptr eid :: Vint32 i :: nil|) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT))) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P).
Lemma mutexpend_block_get_step:
forall P els tls tm ct i eid st pt m,
can_change_aop P ->
TcbMod.get tls ct = Some (pt, st, m) ->
m <> Vnull ->
absinfer (<||
mutexpend_to (|Vptr eid :: Vint32 i :: nil|)
?? mutexpend_block_get
(|Vptr eid :: Vint32 i :: nil|) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P).
Lemma ECBList_P_high_tcb_block_hold_mutex
: forall (ectrl : list EventCtr) (head tail : val)
(msgql : list EventData) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (ptcb : tidspec.A) (prio : priority)
(m : msg) (qid : tidspec.A) (time : int32),
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_mutexsem qid) time, m)).
Lemma R_ECB_ETbl_P_high_tcb_block_hold_mutex:
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_MUTEX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil,
etbl) tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = prio>>ᵢ$ 3 ->
bity = $ 1<<y ->
bitx = $ 1<<(prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MUTEX
:: 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_mutexsem l) time, m)).
Lemma TCBList_P_tcb_block_hold_mutex:
forall (ptcb : addrval) (v1 v2 v3 v4 v5 : val) (v6 : int32)
(v8 : val) (v9 v10 : int32) (v11 : val) (rtbl : vallist)
(vl : list (list val)) (tcbls : TcbMod.map) (prio : int32)
(st : taskstatus) (m : msg) (qid : addrval) (time ry : int32),
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 ∘(Int.unsigned v9) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb)
((v1
:: v2
:: Vptr qid
:: Vnull
:: Vint32 time
:: V$OS_STAT_MUTEX
:: Vint32 prio
:: v8 :: Vint32 v9 :: Vint32 v10 :: v11 :: nil) :: vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (ry&Int.not v10)))
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mutexsem qid) time, Vnull)).
Lemma RH_CurTCB_high_block_hold_mutex:
forall (ptcb : tidspec.A) (tcbls : TcbMod.map) (prio : priority)
(st : taskstatus) (qid : ecbid) (time : int32)
(m : msg),
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mutexsem qid) time, m)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mutexsem:
forall (ecbls : EcbMod.map) (tcbls : TcbMod.map)
(pcur : tid) (qid : tidspec.A) (m : msg) (cnt : int32)
(wl : waitset) (prio : priority) (time : int32) x,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmutexsem cnt x, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmutexsem cnt x, pcur :: wl))
(TcbMod.set tcbls pcur (prio, wait (os_stat_mutexsem qid) time, m)) pcur.
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_MUTEX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil, etbl)
tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = prio>>ᵢ$ 3 ->
bity = $ 1<<y ->
bitx = $ 1<<(prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MUTEX
:: 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_mutexsem l) time, m´)).
Lemma ecblist_p_mutexpend:
forall v´57 v´69 v´38 v´46 x ptcb_addr wls x3 v´48 v´28 v´30 v´40 tcbls v´44 v´27 v´29 cur_prio v´66 v´65 v´68 v´64 i os_rdy_tbl x0 v´26 x12 i5 ptbl vhold,
((v´44 = Vptr (v´46, Int.zero) /\ v´27 = nil)\/ get_last_ptr v´27 = Some (Vptr (v´46, Int.zero))) /\ (length v´27 = length v´29)->
R_PrioTbl_P ptbl tcbls vhold ->
TCBNode_P
(x0
:: v´26
:: x12
:: Vnull
:: V$0
:: V$OS_STAT_RDY
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64
:: Vint32 v´65 :: Vint32 v´66 :: nil)
os_rdy_tbl (cur_prio, rdy, Vnull) ->
array_type_vallist_match Int8u v´57 ->
RL_Tbl_Grp_P v´57 (Vint32 v´69) ->
nth_val ∘(Int.unsigned v´64) v´57 = Some (Vint32 v´68) ->
TcbMod.get tcbls (v´38, Int.zero) = Some (cur_prio, rdy, Vnull) ->
EcbMod.get v´40 (v´46, Int.zero) =
Some
(absmutexsem (x>>ᵢ$ 8)
(Some (ptcb_addr, Int.zero, x&$ OS_MUTEX_KEEP_LOWER_8)), wls) ->
ECBList_P v´44 Vnull
(v´27 ++
((V$OS_EVENT_TYPE_MUTEX
:: Vint32 v´69
:: Vint32 x :: Vptr (ptcb_addr, Int.zero) :: x3 :: v´48 :: nil,
v´57) :: nil) ++ v´28)
(v´29 ++
(DMutex (Vint32 x) (Vptr (ptcb_addr, Int.zero)) :: nil) ++ v´30)
v´40 tcbls ->
ECBList_P v´44 Vnull
(v´27 ++
((V$OS_EVENT_TYPE_MUTEX
:: Vint32 (Int.or v´69 v´66)
:: Vint32 x :: Vptr (ptcb_addr, Int.zero) :: x3 :: v´48 :: nil,
update_nth_val ∘(Int.unsigned v´64) v´57 (Vint32 (Int.or v´68 v´65)))
:: nil) ++ v´28)
(v´29 ++ (DMutex (Vint32 x) (Vptr (ptcb_addr, Int.zero)) :: nil) ++ v´30)
(EcbMod.set v´40 (v´46, Int.zero)
(absmutexsem (x>>ᵢ$ 8)
(Some (ptcb_addr, Int.zero, x&$ OS_MUTEX_KEEP_LOWER_8)),
(v´38, Int.zero) :: wls))
(TcbMod.set tcbls (v´38, Int.zero)
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mutex:
forall (ecbls : EcbMod.map) (tcbls : TcbMod.map)
(pcur : tid) (qid : tidspec.A) (m : msg) cnt x
(wl : waitset) (prio : priority) (time : int32),
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmutexsem cnt x, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmutexsem cnt x, pcur :: wl))
(TcbMod.set tcbls pcur (prio, wait (os_stat_mutexsem qid) time, m)) pcur.
Close Scope code_scope.
Require Import sempend_pure.
Require Import os_mutex.
Require Import OSMutex_common.
Require Import OSEventTaskRdyPure.
Require Import OSQPendPure.
Require Import OSQPostPure.
Require Import mathlib.
Open Scope code_scope.
Lemma aux_trivial:
forall x, Int.unsigned x < 64 -> Int.unsigned (x>>ᵢ$ 3) < 8.
Lemma and7_lt8:
forall x, Int.unsigned x < 64 -> Int.unsigned (x & $ 7) < 8.
Section lzh_join.
Lemma mund_disj_sub_l:
forall ma mb ma´,
TcbMod.disj ma mb ->
TcbMod.sub ma´ ma ->
TcbMod.disj ma´ mb.
Hint Resolve mund_disj_sub_l.
Lemma mund_disj_sub_r:
forall ma mb mb´,
TcbMod.disj ma mb ->
TcbMod.sub mb´ mb ->
TcbMod.disj ma mb´.
Hint Resolve mund_disj_sub_r.
Lemma mund_disj_sub_w:
forall ma mb ma´ mb´,
TcbMod.disj ma mb ->
TcbMod.sub ma´ ma ->
TcbMod.sub mb´ mb ->
TcbMod.disj ma´ mb´.
Hint Resolve mund_disj_sub_w.
Lemma join_prop_mutexpend:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join x2 (TcbMod.sig (ptcb_addr, Int.zero) p_st)
(TcbMod.merge (TcbMod.sig (ptcb_addr, Int.zero) p_st) x2)
.
Hint Resolve TcbMod.get_sig_some.
Hint Resolve TcbMod.join_sub_l.
Hint Resolve TcbMod.join_sub_r.
Hint Resolve TcbMod.sub_sig.
Hint Resolve TcbMod.meq_merge_sym.
Hint Resolve TcbMod.compat_sym.
Lemma rtbl_remove_RL_RTbl_PrioTbl_P_hold´´:
forall (prio : Z) (y bitx : int32) (rtbl : vallist)
(ry : int32) (ptbl : vallist) (av : addrval),
0 <= prio < 64 ->
y = $ prio>>ᵢ$ 3 ->
bitx = $ 1<<($ 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)))
(update_nth_val (∘prio) ptbl (Vptr av))
av.
Lemma join_prop_mutexpend´:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52 y,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join (TcbMod.set tcbls_l (ptcb_addr, Int.zero) y)
(TcbMod.sig (v´38, Int.zero) cur_st)
(TcbMod.merge (TcbMod.sig (v´38, Int.zero) cur_st)
(TcbMod.set tcbls_l (ptcb_addr, Int.zero) y)).
Lemma join_mutexpend´:
forall x y x1 y1 y1´ y´ l1 l2 l3 L L´,
TcbJoin x y´ L´ L ->
TcbMod.join l3 l2 L´ ->
TcbMod.joinsig x1 y1´ l1 l2 ->
TcbJoin x y (TcbMod.set L´ x1 y1) (TcbMod.set (TcbMod.set L x y) x1 y1).
Hint Resolve TcbMod.get_indom.
Hint Resolve tcbmod_joinsig_get.
Lemma join_prop_mutexpend´´:
forall cur_st x2 tcbls tcbls_l tcbls_r tcbls_sub_l tcbls_sub_r p_st v´38 ptcb_addr v´52 y z,
TcbJoin (v´38, Int.zero) cur_st x2 tcbls_r ->
TcbMod.joinsig (ptcb_addr, Int.zero)
p_st tcbls_sub_r v´52 ->
TcbMod.join tcbls_sub_l v´52 tcbls_l ->
TcbMod.join tcbls_l tcbls_r tcbls ->
TcbMod.join (TcbMod.set tcbls_l (ptcb_addr, Int.zero) z)
(TcbMod.set tcbls_r (v´38, Int.zero)
y)
(TcbMod.set
(TcbMod.set tcbls (v´38, Int.zero)
y)
(ptcb_addr, Int.zero) z).
Hint Resolve TcbMod.get_indom.
Lemma join_prop_mutexpend´´´:
forall x y m n b c,
m <> x ->
TcbMod.join (TcbMod.sig m n) b c ->
TcbMod.join (TcbMod.sig m n) (TcbMod.set b x y) (TcbMod.merge (TcbMod.sig m n) (TcbMod.set b x y)).
Lemma join_prop_mutexpend´´´´:
forall a b c x y b´,
TcbMod.join a b c ->
TcbJoin x y b´ b ->
TcbMod.join b´ (TcbMod.merge a (TcbMod.sig x y)) c.
End lzh_join.
Lemma evsllseg_aux:
forall l1 s a b l2 P,
s |= evsllseg a b l1 l2 ** P ->
(a = b /\ l1 = nil \/ get_last_ptr l1 = Some b) /\ length l1 = length l2.
Lemma prio_neq_cur_set:
forall tcbls_l v´38 cur_prio x xm ptcb_addr ptcb_prio,
prio_neq_cur tcbls_l (v´38, Int.zero) cur_prio ->
TcbMod.get tcbls_l (ptcb_addr, Int.zero) =
Some (ptcb_prio, rdy, xm) ->
Int.ltu x cur_prio = true ->
prio_neq_cur (TcbMod.set tcbls_l (ptcb_addr, Int.zero) (x, rdy, xm))
(v´38, Int.zero) cur_prio.
Lemma RL_RTbl_PrioTbl_P_set_vhold:
forall v´45 v´43 x11 xm x y ptcb_prio i8 ptcb_tcby ptcb_bitx ptcb_bity v´53 os_rdy_tbl v0 v´32,
RL_TCBblk_P
(v´45
:: v´43
:: x11
:: xm
:: x
:: y
:: Vint32 ptcb_prio
:: Vint32 i8
:: Vint32 ptcb_tcby
:: Vint32 ptcb_bitx
:: Vint32 ptcb_bity :: nil) ->
(Z.to_nat (Int.unsigned (ptcb_prio>>ᵢ$ 3)) < length os_rdy_tbl)%nat ->
nth_val´ (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl =
Vint32 v0 ->
RL_RTbl_PrioTbl_P os_rdy_tbl v´32 v´53 ->
RL_RTbl_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_prio)) v´32 (Vptr v´53))
v´53.
Lemma R_PrioTbl_Pend_lift:
forall ptcb_addr v´38 x v´53 v´32 tcbls cur_prio ptcb_prio xm v´46 i,
(length v´32 = 64)%nat ->
Int.unsigned cur_prio < 64 ->
Int.unsigned (x>>ᵢ$ 8) < 64 ->
Int.unsigned ptcb_prio < 64 ->
(ptcb_addr,Int.zero) <> (v´38,Int.zero) ->
(nth_val´ (Z.to_nat (Int.unsigned (x>>ᵢ$ 8))) v´32) = (Vptr v´53) ->
R_PrioTbl_P v´32 tcbls v´53 ->
TcbMod.get tcbls (v´38, Int.zero) = Some (cur_prio, rdy, Vnull) ->
TcbMod.get tcbls (ptcb_addr, Int.zero) = Some (ptcb_prio, rdy, xm) ->
R_PrioTbl_P
(update_nth_val (Z.to_nat (Int.unsigned (x>>ᵢ$ 8)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_prio)) v´32 (Vptr v´53))
(Vptr (ptcb_addr, Int.zero)))
(TcbMod.set
(TcbMod.set tcbls (v´38, Int.zero)
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull))
(ptcb_addr, Int.zero) (x>>ᵢ$ 8, rdy, xm)) v´53.
Ltac simpl_vqm :=
repeat
match goal with
| H: ?f _ = Some _ |- _ => simpl in H;inverts H
| _ => idtac
end.
Lemma neg_priointbl_prionotintbl:
forall p tbl,
Int.unsigned p < 64 ->
array_type_vallist_match Int8u tbl ->
length tbl = ∘OS_RDY_TBL_SIZE ->
~ prio_in_tbl p tbl -> prio_not_in_tbl p tbl.
Lemma R_TCB_Status_mutexpend_lift:
forall cur_prio ptcb_prio prio_lift x0 v´26 x12 i5 v´64 v´65 i1 v´45 v´43 x11 xm i8
ptcb_tcby ptcb_bitx ptcb_bity v´46 v´67 x5 v0 os_rdy_tbl i,
length os_rdy_tbl = ∘OS_RDY_TBL_SIZE ->
array_type_vallist_match Int8u
(update_nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx)))
(val_inj
(or
(nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx))))
(Vint32 ($ 1<<(prio_lift&$ 7))))))
(Vint32 (v´67&Int.not v´65))) ->
cur_prio <> ptcb_prio ->
ptcb_prio <> prio_lift ->
nth_val´ (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl = Vint32 v0 ->
nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx))) = Vint32 x5 ->
Int.unsigned prio_lift < 64 ->
TCBNode_P
(x0
:: v´26
:: x12
:: Vnull
:: V$0
:: V$OS_STAT_RDY
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64
:: Vint32 v´65 :: Vint32 i1 :: nil)
os_rdy_tbl (cur_prio, rdy, Vnull) ->
RL_TCBblk_P
(v´45
:: v´43
:: x11
:: xm
:: V$0
:: V$OS_STAT_RDY
:: Vint32 ptcb_prio
:: Vint32 i8
:: Vint32 ptcb_tcby
:: Vint32 ptcb_bitx
:: Vint32 ptcb_bity :: nil) ->
Int.ltu prio_lift cur_prio = true ->
nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(val_inj
(or
(nth_val´ (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby))
os_rdy_tbl (Vint32 (v0&Int.not ptcb_bitx))))
(Vint32 ($ 1<<(prio_lift&$ 7)))))) =
Some (Vint32 v´67) ->
R_TCB_Status_P
(x0
:: v´26
:: Vptr (v´46, Int.zero)
:: Vnull
:: Vint32 i
:: V$OS_STAT_MUTEX
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64 :: Vint32 v´65 :: Vint32 i1 :: nil)
(update_nth_val ∘(Int.unsigned v´64)
(update_nth_val (Z.to_nat (Int.unsigned (prio_lift>>ᵢ$ 3)))
(update_nth_val (Z.to_nat (Int.unsigned ptcb_tcby)) os_rdy_tbl
(Vint32 (v0&Int.not ptcb_bitx)))
(Vint32 (Int.or x5 ($ 1<<(prio_lift&$ 7)))))
(Vint32 (v´67&Int.not v´65)))
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull).
Lemma absinfer_mutex_pend_lift_is_rdy_block:
forall P mqls qid v wl p m t ct tls tid opr pr m´ p´,
ct <>tid ->
Int.unsigned v <= 65535 ->
can_change_aop P ->
EcbMod.get mqls qid = Some (absmutexsem pr (Some (tid, p´)), wl) ->
TcbMod.get tls ct = Some (p, rdy, m) ->
TcbMod.get tls tid = Some (opr, rdy, m´) ->
Int.eq opr pr = false ->
Int.ltu p p´ = true ->
Int.ltu pr p = true ->
absinfer
( <|| mutexpend (Vptr qid :: Vint32 v :: nil) ||> **
HECBList mqls **
HTCBList tls **
HTime t **
HCurTCB ct ** P)
(<|| isched;;
(mutexpend_to (|Vptr qid :: Vint32 v :: nil|) ??
mutexpend_block_get (|Vptr qid :: Vint32 v :: nil|)) ||> **
HECBList ( EcbMod.set mqls qid (absmutexsem pr (Some (tid, p´)), ct :: wl) ) **
HTCBList (TcbMod.set
(TcbMod.set tls
ct (p,wait (os_stat_mutexsem qid) v, m))
tid (pr, rdy, m´)) **
HTime t **
HCurTCB ct ** P).
Lemma tcbdllseg_cons:
forall s tid h p´ tail tailnext l P pre,
struct_type_vallist_match OS_TCB h ->
s |= Astruct (tid,Int.zero) OS_TCB h **
tcbdllseg p´ (Vptr (tid,Int.zero)) tail tailnext l ** P ->
V_OSTCBNext h = Some p´ ->
V_OSTCBPrev h = Some pre ->
s |= tcbdllseg (Vptr (tid,Int.zero)) pre tail tailnext (h::l) ** P.
Lemma tcbdllseg_l_not_nil:
forall head l rtbl tcbls tid v,
TCBList_P head l rtbl tcbls ->
TcbMod.get tcbls tid = Some v ->
exists h l´, l = h :: l´.
Lemma dllseg_compose:
forall (s : RstateOP) (P : asrt) (h hp t1 tn1 t2 tn2 : val)
(l1 l2 : list vallist),
s |= dllseg h hp t1 tn1 l1 OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl) ** dllseg tn1 t1 t2 tn2 l2 OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl)** P ->
s |= dllseg h hp t2 tn2 (l1 ++ l2) OS_TCB
(fun vl : vallist => nth_val 1 vl)
(fun vl : vallist => nth_val 0 vl) ** P.
Lemma mutexpend_block_no_lift_step:
forall P els tls tm ct i eid els´ tls´ t´ pt m m´ px p´ wl p,
can_change_aop P ->
EcbMod.get els eid = Some (absmutexsem p (Some (t´, p´)), wl) ->
TcbMod.get tls ct = Some (pt, rdy, m) ->
TcbMod.get tls t´ = Some (px, rdy, m´) ->
(Int.eq px p <> false \/ Int.ltu p´ pt = true) ->
els´ = EcbMod.set els eid (absmutexsem p (Some (t´, p´)), ct :: wl) ->
tls´ = TcbMod.set tls ct (pt, wait (os_stat_mutexsem eid) i, Vnull) ->
Int.ltu p pt = true ->
absinfer (<|| mutexpend (Vptr eid :: Vint32 i :: nil) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| isched;;(mutexpend_to (| Vptr eid :: Vint32 i :: nil |) ?? mutexpend_block_get (|Vptr eid :: Vint32 i :: nil|)) ||> **
HECBList els´ **
HTCBList tls´ **
HTime tm **
HCurTCB ct ** P).
Lemma mutexpend_block_timeout_step:
forall P els tls tm ct i eid st pt,
can_change_aop P ->
TcbMod.get tls ct = Some (pt, st, Vnull) ->
absinfer (<||
mutexpend_to (|Vptr eid :: Vint32 i :: nil|)
?? mutexpend_block_get
(|Vptr eid :: Vint32 i :: nil|) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr TIME_OUT))) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P).
Lemma mutexpend_block_get_step:
forall P els tls tm ct i eid st pt m,
can_change_aop P ->
TcbMod.get tls ct = Some (pt, st, m) ->
m <> Vnull ->
absinfer (<||
mutexpend_to (|Vptr eid :: Vint32 i :: nil|)
?? mutexpend_block_get
(|Vptr eid :: Vint32 i :: nil|) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P)
(<|| END (Some (Vint32 (Int.repr OS_NO_ERR))) ||> **
HECBList els **
HTCBList tls **
HTime tm **
HCurTCB ct ** P).
Lemma ECBList_P_high_tcb_block_hold_mutex
: forall (ectrl : list EventCtr) (head tail : val)
(msgql : list EventData) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (ptcb : tidspec.A) (prio : priority)
(m : msg) (qid : tidspec.A) (time : int32),
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_mutexsem qid) time, m)).
Lemma R_ECB_ETbl_P_high_tcb_block_hold_mutex:
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_MUTEX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil,
etbl) tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = prio>>ᵢ$ 3 ->
bity = $ 1<<y ->
bitx = $ 1<<(prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MUTEX
:: 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_mutexsem l) time, m)).
Lemma TCBList_P_tcb_block_hold_mutex:
forall (ptcb : addrval) (v1 v2 v3 v4 v5 : val) (v6 : int32)
(v8 : val) (v9 v10 : int32) (v11 : val) (rtbl : vallist)
(vl : list (list val)) (tcbls : TcbMod.map) (prio : int32)
(st : taskstatus) (m : msg) (qid : addrval) (time ry : int32),
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 ∘(Int.unsigned v9) rtbl = Some (Vint32 ry) ->
TCBList_P (Vptr ptcb)
((v1
:: v2
:: Vptr qid
:: Vnull
:: Vint32 time
:: V$OS_STAT_MUTEX
:: Vint32 prio
:: v8 :: Vint32 v9 :: Vint32 v10 :: v11 :: nil) :: vl)
(update_nth_val ∘(Int.unsigned v9) rtbl (Vint32 (ry&Int.not v10)))
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mutexsem qid) time, Vnull)).
Lemma RH_CurTCB_high_block_hold_mutex:
forall (ptcb : tidspec.A) (tcbls : TcbMod.map) (prio : priority)
(st : taskstatus) (qid : ecbid) (time : int32)
(m : msg),
RH_CurTCB ptcb tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
RH_CurTCB ptcb
(TcbMod.set tcbls ptcb (prio, wait (os_stat_mutexsem qid) time, m)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mutexsem:
forall (ecbls : EcbMod.map) (tcbls : TcbMod.map)
(pcur : tid) (qid : tidspec.A) (m : msg) (cnt : int32)
(wl : waitset) (prio : priority) (time : int32) x,
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmutexsem cnt x, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmutexsem cnt x, pcur :: wl))
(TcbMod.set tcbls pcur (prio, wait (os_stat_mutexsem qid) time, m)) pcur.
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_MUTEX :: Vint32 egrp :: v2 :: v3 :: v4 :: v5 :: nil, etbl)
tcbls ->
TcbMod.get tcbls ptcb = Some (prio, st, m) ->
y = prio>>ᵢ$ 3 ->
bity = $ 1<<y ->
bitx = $ 1<<(prio&$ 7) ->
nth_val ∘(Int.unsigned y) etbl = Some (Vint32 ey) ->
R_ECB_ETbl_P l
(V$OS_EVENT_TYPE_MUTEX
:: 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_mutexsem l) time, m´)).
Lemma ecblist_p_mutexpend:
forall v´57 v´69 v´38 v´46 x ptcb_addr wls x3 v´48 v´28 v´30 v´40 tcbls v´44 v´27 v´29 cur_prio v´66 v´65 v´68 v´64 i os_rdy_tbl x0 v´26 x12 i5 ptbl vhold,
((v´44 = Vptr (v´46, Int.zero) /\ v´27 = nil)\/ get_last_ptr v´27 = Some (Vptr (v´46, Int.zero))) /\ (length v´27 = length v´29)->
R_PrioTbl_P ptbl tcbls vhold ->
TCBNode_P
(x0
:: v´26
:: x12
:: Vnull
:: V$0
:: V$OS_STAT_RDY
:: Vint32 cur_prio
:: Vint32 i5
:: Vint32 v´64
:: Vint32 v´65 :: Vint32 v´66 :: nil)
os_rdy_tbl (cur_prio, rdy, Vnull) ->
array_type_vallist_match Int8u v´57 ->
RL_Tbl_Grp_P v´57 (Vint32 v´69) ->
nth_val ∘(Int.unsigned v´64) v´57 = Some (Vint32 v´68) ->
TcbMod.get tcbls (v´38, Int.zero) = Some (cur_prio, rdy, Vnull) ->
EcbMod.get v´40 (v´46, Int.zero) =
Some
(absmutexsem (x>>ᵢ$ 8)
(Some (ptcb_addr, Int.zero, x&$ OS_MUTEX_KEEP_LOWER_8)), wls) ->
ECBList_P v´44 Vnull
(v´27 ++
((V$OS_EVENT_TYPE_MUTEX
:: Vint32 v´69
:: Vint32 x :: Vptr (ptcb_addr, Int.zero) :: x3 :: v´48 :: nil,
v´57) :: nil) ++ v´28)
(v´29 ++
(DMutex (Vint32 x) (Vptr (ptcb_addr, Int.zero)) :: nil) ++ v´30)
v´40 tcbls ->
ECBList_P v´44 Vnull
(v´27 ++
((V$OS_EVENT_TYPE_MUTEX
:: Vint32 (Int.or v´69 v´66)
:: Vint32 x :: Vptr (ptcb_addr, Int.zero) :: x3 :: v´48 :: nil,
update_nth_val ∘(Int.unsigned v´64) v´57 (Vint32 (Int.or v´68 v´65)))
:: nil) ++ v´28)
(v´29 ++ (DMutex (Vint32 x) (Vptr (ptcb_addr, Int.zero)) :: nil) ++ v´30)
(EcbMod.set v´40 (v´46, Int.zero)
(absmutexsem (x>>ᵢ$ 8)
(Some (ptcb_addr, Int.zero, x&$ OS_MUTEX_KEEP_LOWER_8)),
(v´38, Int.zero) :: wls))
(TcbMod.set tcbls (v´38, Int.zero)
(cur_prio, wait (os_stat_mutexsem (v´46, Int.zero)) i, Vnull)).
Lemma RH_TCBList_ECBList_P_high_block_hold_mutex:
forall (ecbls : EcbMod.map) (tcbls : TcbMod.map)
(pcur : tid) (qid : tidspec.A) (m : msg) cnt x
(wl : waitset) (prio : priority) (time : int32),
RH_TCBList_ECBList_P ecbls tcbls pcur ->
EcbMod.get ecbls qid = Some (absmutexsem cnt x, wl) ->
TcbMod.get tcbls pcur = Some (prio, rdy, m) ->
RH_TCBList_ECBList_P (EcbMod.set ecbls qid (absmutexsem cnt x, pcur :: wl))
(TcbMod.set tcbls pcur (prio, wait (os_stat_mutexsem qid) time, m)) pcur.
Close Scope code_scope.