Library OSQInvDef
Require Import include.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import BaseAsrtDef.
Require Import OSTCBInvDef.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.
Require Import os_code_defs.
Require Import os_ucos_h.
Require Import BaseAsrtDef.
Require Import OSTCBInvDef.
This file contains the relational assertion for specifying the OS event list and
the full invariant for specifying interleavings between interrupt handlers and
non-handler code.
Definitions for returning the value of the struct OS_EVENT
Definition V_OSEventType (vl:vallist) := nth_val 0 vl.
Definition V_OSEventGrp (vl:vallist) := nth_val 1 vl.
Definition V_OSEventCnt (vl:vallist) := nth_val 2 vl.
Definition V_OSEventPtr (vl:vallist) := nth_val 3 vl.
Definition V_OSEventListPtr (vl:vallist) := nth_val 5 vl.
Definition V_OSEventGrp (vl:vallist) := nth_val 1 vl.
Definition V_OSEventCnt (vl:vallist) := nth_val 2 vl.
Definition V_OSEventPtr (vl:vallist) := nth_val 3 vl.
Definition V_OSEventListPtr (vl:vallist) := nth_val 5 vl.
Definitions for returning the value of the struct OS_Q
Definition V_OSQPtr (vl:vallist) := nth_val 0 vl.
Definition V_OSQStart (vl:vallist) := nth_val 1 vl.
Definition V_OSQEnd (vl:vallist) := nth_val 2 vl.
Definition V_OSQIn (vl:vallist) := nth_val 3 vl.
Definition V_OSQOut (vl:vallist) := nth_val 4 vl.
Definition V_OSQSize (vl:vallist) := nth_val 5 vl.
Definition V_OSQEntries (vl:vallist) := nth_val 6 vl.
Definition V_qfreeblk (vl:vallist) := nth_val 7 vl.
Definition V_OSQStart (vl:vallist) := nth_val 1 vl.
Definition V_OSQEnd (vl:vallist) := nth_val 2 vl.
Definition V_OSQIn (vl:vallist) := nth_val 3 vl.
Definition V_OSQOut (vl:vallist) := nth_val 4 vl.
Definition V_OSQSize (vl:vallist) := nth_val 5 vl.
Definition V_OSQEntries (vl:vallist) := nth_val 6 vl.
Definition V_qfreeblk (vl:vallist) := nth_val 7 vl.
Definitions for returning the value of the struct OS_Q_FREEBLK
Definitions for returning the value of the struct OS_Q_PTR
Definition V_next (vl:vallist) := nth_val 0 vl.
Definition V_qeventptr (vl:vallist) := nth_val 1 vl.
Open Scope int_scope.
Definition EVENT_TBL_INIT_VL:=
Vint32 (Int.zero) ::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::nil.
Definition id_addrval´ (v : val) (id :var) (t : type):=
match v with
| Vptr av => id_addrval av id t
| _ => None
end.
Fixpoint ecbf_sllseg (head tailnext : val) (l:list vallist) (t:type) (next: vallist -> option val):=
match l with
| nil => [| head = tailnext |]
| vl::l´ => EX vn ltbl vla,
[|next vl = Some vn|] **
node head vl t **
[| id_addrval´ head OSEventTbl OS_EVENT = Some ltbl |]**
Aarray ltbl (Tarray Tint8 (nat_of_Z OS_EVENT_TBL_SIZE)) vla**
ecbf_sllseg vn tailnext l´ t next
end.
Definition ecbf_sll :=
fun (head : val) (l : list vallist) (t : type) (next : vallist -> option val) =>
ecbf_sllseg head Vnull l t next.
Definition sll head l t next := sllseg head Vnull l t next.
Definition V_qeventptr (vl:vallist) := nth_val 1 vl.
Open Scope int_scope.
Definition EVENT_TBL_INIT_VL:=
Vint32 (Int.zero) ::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::
Vint32 (Int.zero)::nil.
Definition id_addrval´ (v : val) (id :var) (t : type):=
match v with
| Vptr av => id_addrval av id t
| _ => None
end.
Fixpoint ecbf_sllseg (head tailnext : val) (l:list vallist) (t:type) (next: vallist -> option val):=
match l with
| nil => [| head = tailnext |]
| vl::l´ => EX vn ltbl vla,
[|next vl = Some vn|] **
node head vl t **
[| id_addrval´ head OSEventTbl OS_EVENT = Some ltbl |]**
Aarray ltbl (Tarray Tint8 (nat_of_Z OS_EVENT_TBL_SIZE)) vla**
ecbf_sllseg vn tailnext l´ t next
end.
Definition ecbf_sll :=
fun (head : val) (l : list vallist) (t : type) (next : vallist -> option val) =>
ecbf_sllseg head Vnull l t next.
Definition sll head l t next := sllseg head Vnull l t next.
The assertion specifies the free list of OS event blocks.
Definition AOSEventFreeList (l:list vallist) :=
EX p,(GV OSEventFreeList @ (Tptr OS_EVENT) |-> p) **
ecbf_sll p l OS_EVENT V_OSEventListPtr.
EX p,(GV OSEventFreeList @ (Tptr OS_EVENT) |-> p) **
ecbf_sll p l OS_EVENT V_OSEventListPtr.
The assertion specifies the free list of message queues.
Definition AOSQFreeList (l:list vallist):=
EX p,(GV OSQFreeList @ (Tptr OS_Q) |-> p) ** sll p l OS_Q V_OSQPtr.
Fixpoint qblkf_sllseg (head tailnext : val) (l:list vallist) (t:type) (next: vallist -> option val):=
match l with
| nil => [| head = tailnext |]
| vl::l´ => EX vn ltbl vla,
[|next vl = Some vn|] **
node head vl t **
[| id_addrval´ head msgqueuetbl OS_Q_FREEBLK = Some ltbl |]**
Aarray ltbl (Tarray (Tptr Tvoid) (nat_of_Z OS_MAX_Q_SIZE)) vla**
qblkf_sllseg vn tailnext l´ t next
end.
Definition qblkf_sll :=
fun (head : val) (l : list vallist) (t : type) (next : vallist -> option val) =>
qblkf_sllseg head Vnull l t next.
Definition AOSQFreeBlk (l:list vallist):=
EX p,(GV OSQFreeBlk @ (Tptr OS_Q_FREEBLK) |-> p)
** qblkf_sll p l OS_Q_FREEBLK V_nextblk.
Open Scope Z_scope.
Open Scope int_scope.
Definition ptr_minus (l1 l2:addrval) (t:type) :=
let (b1,i1):=l1 in
let (b2,i2):=l2 in
if (b1=? b2)%positive then
Some (nat_of_Z (Int.unsigned (Int.divu (Int.sub i1 i2) (Int.repr (Z_of_nat (typelen t))))))
else None.
Definition ptr_offset_right (l1 l2:addrval) (t:type) :=
let (b1,i1):=l1 in
let (b2,i2):=l2 in
if (b1=? b2)%positive then
Int.ltu i1 i2 = false /\
Int.modu (Int.sub i1 i2) ($ (Z_of_nat (typelen t))) = $ 0
else False.
Definition qend_right qend qtbl qsize :=
snd qtbl = Int.repr 4 /\
ptr_offset_right qend qtbl (Tptr Tvoid) /\
ptr_minus qend qtbl (Tptr Tvoid) = Some (nat_of_Z (Int.unsigned qsize)).
Definition arrayelem_addr_right p qtbl qsize :=
exists n, ptr_offset_right p qtbl (Tptr Tvoid) /\
ptr_minus p qtbl (Tptr Tvoid) = Some n /\
(n < (nat_of_Z (Int.unsigned qsize)))%nat.
EX p,(GV OSQFreeList @ (Tptr OS_Q) |-> p) ** sll p l OS_Q V_OSQPtr.
Fixpoint qblkf_sllseg (head tailnext : val) (l:list vallist) (t:type) (next: vallist -> option val):=
match l with
| nil => [| head = tailnext |]
| vl::l´ => EX vn ltbl vla,
[|next vl = Some vn|] **
node head vl t **
[| id_addrval´ head msgqueuetbl OS_Q_FREEBLK = Some ltbl |]**
Aarray ltbl (Tarray (Tptr Tvoid) (nat_of_Z OS_MAX_Q_SIZE)) vla**
qblkf_sllseg vn tailnext l´ t next
end.
Definition qblkf_sll :=
fun (head : val) (l : list vallist) (t : type) (next : vallist -> option val) =>
qblkf_sllseg head Vnull l t next.
Definition AOSQFreeBlk (l:list vallist):=
EX p,(GV OSQFreeBlk @ (Tptr OS_Q_FREEBLK) |-> p)
** qblkf_sll p l OS_Q_FREEBLK V_nextblk.
Open Scope Z_scope.
Open Scope int_scope.
Definition ptr_minus (l1 l2:addrval) (t:type) :=
let (b1,i1):=l1 in
let (b2,i2):=l2 in
if (b1=? b2)%positive then
Some (nat_of_Z (Int.unsigned (Int.divu (Int.sub i1 i2) (Int.repr (Z_of_nat (typelen t))))))
else None.
Definition ptr_offset_right (l1 l2:addrval) (t:type) :=
let (b1,i1):=l1 in
let (b2,i2):=l2 in
if (b1=? b2)%positive then
Int.ltu i1 i2 = false /\
Int.modu (Int.sub i1 i2) ($ (Z_of_nat (typelen t))) = $ 0
else False.
Definition qend_right qend qtbl qsize :=
snd qtbl = Int.repr 4 /\
ptr_offset_right qend qtbl (Tptr Tvoid) /\
ptr_minus qend qtbl (Tptr Tvoid) = Some (nat_of_Z (Int.unsigned qsize)).
Definition arrayelem_addr_right p qtbl qsize :=
exists n, ptr_offset_right p qtbl (Tptr Tvoid) /\
ptr_minus p qtbl (Tptr Tvoid) = Some n /\
(n < (nat_of_Z (Int.unsigned qsize)))%nat.
A good message queue should satisfy the following property
Definition WellformedOSQ (osq:vallist):=
exists qstart qend qin qout qsize qtbl qblk,
V_OSQStart osq = Some (Vptr qstart) /\
V_OSQEnd osq = Some (Vptr qend) /\
V_OSQIn osq = Some (Vptr qin) /\
V_OSQOut osq = Some (Vptr qout) /\
V_OSQSize osq = Some (Vint32 qsize) /\
V_qfreeblk osq = Some (Vptr qblk) /\
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some qtbl /\
0 < Int.unsigned qsize <= OS_MAX_Q_SIZE /\ qstart = qtbl /\
qend_right qend qtbl qsize /\
arrayelem_addr_right qin qtbl qsize /\
arrayelem_addr_right qout qtbl qsize.
Close Scope Z_scope.
Definition EventCtr:=( vallist * vallist).
Open Scope Z_scope.
Definition RH_ECB_P (msgq : absecb.B) :=
match msgq with
|(ed,waitset) =>
match ed with
| absmsgq msgl qsize =>
(msgl <> nil -> waitset = nil) /\
(waitset <> nil -> msgl = nil)
| abssem z =>
(Int.ltu Int.zero z = true -> waitset = nil) /\
(waitset <> nil -> Int.eq Int.zero z = true)
| absmbox msg=>
(msg <> Vnull -> waitset = nil) /\
(waitset <> nil -> msg = Vnull)
| absmutexsem pr owner =>
(owner = None -> waitset = nil) /\
(forall tid opr,
owner = Some (tid,opr) ->
Int.ltu pr opr = true /\ Int.unsigned opr < 64) /\
(waitset <> nil -> owner <> None) /\ (Int.unsigned pr < 64)
end
end.
Definition offset_zero (l:addrval) := exists b, l = (b,Int.zero).
Definition AOSEventTbl letbl etbl :=
Aarray letbl (Tarray Tint8 (nat_of_Z OS_EVENT_TBL_SIZE)) etbl
** [| array_type_vallist_match Tint8 etbl |].
Definition AOSEvent losevent osevent etbl:=
EX letbl egrp,
node losevent osevent OS_EVENT
** AOSEventTbl letbl etbl **
[| id_addrval´ losevent OSEventTbl OS_EVENT = Some letbl |] **
[| V_OSEventGrp osevent = Some egrp |] ** [|RL_Tbl_Grp_P etbl egrp|].
Definition AOSQCtr losq osq :=
node losq osq OS_Q **
[| WellformedOSQ osq |].
Definition AOSQBlk losqblk osqblk msgtbl :=
EX lmsgtbl,
node losqblk osqblk OS_Q_FREEBLK **
[| id_addrval´ losqblk msgqueuetbl OS_Q_FREEBLK = Some lmsgtbl |] **
Aarray lmsgtbl (Tarray (Tptr Tvoid) (nat_of_Z OS_MAX_Q_SIZE)) msgtbl.
Definition distance (v1 v2:addrval) :=
Int.unsigned (Int.divu (Int.sub (snd v2) (snd v1)) (Int.repr (Z_of_nat (typelen (Tptr Tvoid))))).
Fixpoint vallist_post (first:nat) (vl:vallist) :=
match first with
| 0%nat => vl
| S n => match vl with
| nil => nil
| v::vl´ => vallist_post n vl´
end
end.
Fixpoint vallist_pre (last:nat) (vl:vallist):=
match last with
| 0%nat=> nil
| S n => match vl with
| nil => nil
| v::vl´ => v::(vallist_pre n vl´)
end
end.
Definition vallist_seg (first last:nat) (vl:vallist) :=
vallist_post first (vallist_pre last vl).
Fixpoint isptr_list vl:=
match vl with
| nil => True
| v::vl´ => isptr v /\ isptr_list vl´
end.
Definition MatchLHMsgList osq msgtbl msgl :=
exists qstart qin qout qsize d1 d2 qens,
V_OSQStart osq = Some (Vptr qstart) /\
V_OSQIn osq = Some (Vptr qin) /\
V_OSQOut osq = Some (Vptr qout) /\
V_OSQSize osq = Some (Vint32 qsize) /\
V_OSQEntries osq = Some (Vint32 qens) /\
d1 = distance qstart qout /\
d2 = distance qstart qin /\
(
( d2 > d1->
vallist_seg (nat_of_Z d1) (nat_of_Z d2) msgtbl = msgl)
/\
( d2 < d1 ->
(vallist_seg (nat_of_Z d1)
(nat_of_Z (Int.unsigned qsize)) msgtbl)++
(vallist_seg 0 (nat_of_Z d2)
msgtbl) = msgl) /\
(d2 = d1 ->
(Int.eq qens Int.zero = true /\ msgl = nil) \/
(Int.eq qens qsize = true /\
(vallist_seg (nat_of_Z d1)
(nat_of_Z (Int.unsigned qsize)) msgtbl)++
(vallist_seg 0 (nat_of_Z d2)
msgtbl) = msgl) ))
/\ isptr_list msgl.
Definition MatchLHMsgLength osq (msgl : vallist):=
exists qents,
V_OSQEntries osq = Some (Vint32 qents)/\
Int.unsigned qents = Z_of_nat (List.length msgl).
Definition MatchLHMsgSize osq qmaxlen :=
exists qsize, V_OSQSize osq = Some (Vint32 qsize) /\
qsize = ($ qmaxlen) /\ 0<=qmaxlen <= Int.max_unsigned.
Definition MatchMutexSem (x y : val) (pr : priority) (o : owner) :=
exists v op, x = Vint32 v /\ Int.unsigned v <= 65535 /\
pr = (Int.shru v ($ 8)) /\
op = (Int.and v ($ OS_MUTEX_KEEP_LOWER_8)) /\
(op = $ OS_MUTEX_AVAILABLE -> o = None /\ y = Vnull) /\
(op <> $ OS_MUTEX_AVAILABLE -> exists tid, y = Vptr tid /\ o = Some (tid, op)).
exists qstart qend qin qout qsize qtbl qblk,
V_OSQStart osq = Some (Vptr qstart) /\
V_OSQEnd osq = Some (Vptr qend) /\
V_OSQIn osq = Some (Vptr qin) /\
V_OSQOut osq = Some (Vptr qout) /\
V_OSQSize osq = Some (Vint32 qsize) /\
V_qfreeblk osq = Some (Vptr qblk) /\
id_addrval qblk msgqueuetbl OS_Q_FREEBLK = Some qtbl /\
0 < Int.unsigned qsize <= OS_MAX_Q_SIZE /\ qstart = qtbl /\
qend_right qend qtbl qsize /\
arrayelem_addr_right qin qtbl qsize /\
arrayelem_addr_right qout qtbl qsize.
Close Scope Z_scope.
Definition EventCtr:=( vallist * vallist).
Open Scope Z_scope.
Definition RH_ECB_P (msgq : absecb.B) :=
match msgq with
|(ed,waitset) =>
match ed with
| absmsgq msgl qsize =>
(msgl <> nil -> waitset = nil) /\
(waitset <> nil -> msgl = nil)
| abssem z =>
(Int.ltu Int.zero z = true -> waitset = nil) /\
(waitset <> nil -> Int.eq Int.zero z = true)
| absmbox msg=>
(msg <> Vnull -> waitset = nil) /\
(waitset <> nil -> msg = Vnull)
| absmutexsem pr owner =>
(owner = None -> waitset = nil) /\
(forall tid opr,
owner = Some (tid,opr) ->
Int.ltu pr opr = true /\ Int.unsigned opr < 64) /\
(waitset <> nil -> owner <> None) /\ (Int.unsigned pr < 64)
end
end.
Definition offset_zero (l:addrval) := exists b, l = (b,Int.zero).
Definition AOSEventTbl letbl etbl :=
Aarray letbl (Tarray Tint8 (nat_of_Z OS_EVENT_TBL_SIZE)) etbl
** [| array_type_vallist_match Tint8 etbl |].
Definition AOSEvent losevent osevent etbl:=
EX letbl egrp,
node losevent osevent OS_EVENT
** AOSEventTbl letbl etbl **
[| id_addrval´ losevent OSEventTbl OS_EVENT = Some letbl |] **
[| V_OSEventGrp osevent = Some egrp |] ** [|RL_Tbl_Grp_P etbl egrp|].
Definition AOSQCtr losq osq :=
node losq osq OS_Q **
[| WellformedOSQ osq |].
Definition AOSQBlk losqblk osqblk msgtbl :=
EX lmsgtbl,
node losqblk osqblk OS_Q_FREEBLK **
[| id_addrval´ losqblk msgqueuetbl OS_Q_FREEBLK = Some lmsgtbl |] **
Aarray lmsgtbl (Tarray (Tptr Tvoid) (nat_of_Z OS_MAX_Q_SIZE)) msgtbl.
Definition distance (v1 v2:addrval) :=
Int.unsigned (Int.divu (Int.sub (snd v2) (snd v1)) (Int.repr (Z_of_nat (typelen (Tptr Tvoid))))).
Fixpoint vallist_post (first:nat) (vl:vallist) :=
match first with
| 0%nat => vl
| S n => match vl with
| nil => nil
| v::vl´ => vallist_post n vl´
end
end.
Fixpoint vallist_pre (last:nat) (vl:vallist):=
match last with
| 0%nat=> nil
| S n => match vl with
| nil => nil
| v::vl´ => v::(vallist_pre n vl´)
end
end.
Definition vallist_seg (first last:nat) (vl:vallist) :=
vallist_post first (vallist_pre last vl).
Fixpoint isptr_list vl:=
match vl with
| nil => True
| v::vl´ => isptr v /\ isptr_list vl´
end.
Definition MatchLHMsgList osq msgtbl msgl :=
exists qstart qin qout qsize d1 d2 qens,
V_OSQStart osq = Some (Vptr qstart) /\
V_OSQIn osq = Some (Vptr qin) /\
V_OSQOut osq = Some (Vptr qout) /\
V_OSQSize osq = Some (Vint32 qsize) /\
V_OSQEntries osq = Some (Vint32 qens) /\
d1 = distance qstart qout /\
d2 = distance qstart qin /\
(
( d2 > d1->
vallist_seg (nat_of_Z d1) (nat_of_Z d2) msgtbl = msgl)
/\
( d2 < d1 ->
(vallist_seg (nat_of_Z d1)
(nat_of_Z (Int.unsigned qsize)) msgtbl)++
(vallist_seg 0 (nat_of_Z d2)
msgtbl) = msgl) /\
(d2 = d1 ->
(Int.eq qens Int.zero = true /\ msgl = nil) \/
(Int.eq qens qsize = true /\
(vallist_seg (nat_of_Z d1)
(nat_of_Z (Int.unsigned qsize)) msgtbl)++
(vallist_seg 0 (nat_of_Z d2)
msgtbl) = msgl) ))
/\ isptr_list msgl.
Definition MatchLHMsgLength osq (msgl : vallist):=
exists qents,
V_OSQEntries osq = Some (Vint32 qents)/\
Int.unsigned qents = Z_of_nat (List.length msgl).
Definition MatchLHMsgSize osq qmaxlen :=
exists qsize, V_OSQSize osq = Some (Vint32 qsize) /\
qsize = ($ qmaxlen) /\ 0<=qmaxlen <= Int.max_unsigned.
Definition MatchMutexSem (x y : val) (pr : priority) (o : owner) :=
exists v op, x = Vint32 v /\ Int.unsigned v <= 65535 /\
pr = (Int.shru v ($ 8)) /\
op = (Int.and v ($ OS_MUTEX_KEEP_LOWER_8)) /\
(op = $ OS_MUTEX_AVAILABLE -> o = None /\ y = Vnull) /\
(op <> $ OS_MUTEX_AVAILABLE -> exists tid, y = Vptr tid /\ o = Some (tid, op)).
The relation between the low-level concrete event blocks and high-level abstract events
Definition RLH_ECBData_P (lecb: EventData) (hecb:absecb.B) :=
match lecb , hecb with
| (DMsgQ a osq osqblk msgtbl), ((absmsgq msgl qmaxlen),qwaitset) =>
MatchLHMsgList osq msgtbl msgl /\
MatchLHMsgLength osq msgl/\
MatchLHMsgSize osq (Int.unsigned qmaxlen) /\ RH_ECB_P hecb
| (DSem n1), (abssem n2, waitset) =>
n1 = n2 /\ RH_ECB_P hecb
| (DMbox a), (absmbox b,waitset) =>
a = b /\ RH_ECB_P hecb
| (DMutex x y), (absmutexsem pr own, waitset) =>
MatchMutexSem x y pr own /\ RH_ECB_P hecb
| _ , _ => False
end.
Definition RH_TCBList_ECBList_Q_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid):=
(forall eid x y qwaitset tid,
(EcbMod.get ecbls eid = Some (absmsgq x y,qwaitset) /\
In tid qwaitset) ->
exists prio m n, TcbMod.get tcbls tid = Some (prio,wait (os_stat_q eid) n,m)) /\
(forall p tid eid n m,
TcbMod.get tcbls tid = Some (p,wait (os_stat_q eid) n,m)->
(exists x y qwaitset,
EcbMod.get ecbls eid = Some (absmsgq x y,qwaitset) /\
In tid qwaitset)).
Definition RH_TCBList_ECBList_SEM_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n wls tid,
(EcbMod.get ecbls eid = Some (abssem n, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_sem eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_sem eid) t, msg) ->
(exists n wls,
EcbMod.get ecbls eid = Some (abssem n, wls) /\
In tid wls)).
Definition RH_TCBList_ECBList_MBOX_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n wls tid,
(EcbMod.get ecbls eid = Some (absmbox n, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_mbox eid) t, msg) ->
(exists n wls,
EcbMod.get ecbls eid = Some (absmbox n, wls) /\
In tid wls)).
Definition RH_TCBList_ECBList_MUTEX_OWNER ecbls tcbls :=
forall eid pr wls opr tid,
(EcbMod.get ecbls eid = Some (absmutexsem pr (Some (tid, opr)), wls)) ->
(exists prio msg st,
TcbMod.get tcbls tid = Some (prio, st, msg)).
Definition RH_TCBList_ECBList_MUTEX_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n1 n2 wls tid,
(EcbMod.get ecbls eid = Some (absmutexsem n1 n2, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mutexsem eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_mutexsem eid) t, msg) ->
(exists n1 n2 wls,
EcbMod.get ecbls eid = Some (absmutexsem n1 n2, wls) /\
In tid wls)) /\
RH_TCBList_ECBList_MUTEX_OWNER ecbls tcbls.
match lecb , hecb with
| (DMsgQ a osq osqblk msgtbl), ((absmsgq msgl qmaxlen),qwaitset) =>
MatchLHMsgList osq msgtbl msgl /\
MatchLHMsgLength osq msgl/\
MatchLHMsgSize osq (Int.unsigned qmaxlen) /\ RH_ECB_P hecb
| (DSem n1), (abssem n2, waitset) =>
n1 = n2 /\ RH_ECB_P hecb
| (DMbox a), (absmbox b,waitset) =>
a = b /\ RH_ECB_P hecb
| (DMutex x y), (absmutexsem pr own, waitset) =>
MatchMutexSem x y pr own /\ RH_ECB_P hecb
| _ , _ => False
end.
Definition RH_TCBList_ECBList_Q_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid):=
(forall eid x y qwaitset tid,
(EcbMod.get ecbls eid = Some (absmsgq x y,qwaitset) /\
In tid qwaitset) ->
exists prio m n, TcbMod.get tcbls tid = Some (prio,wait (os_stat_q eid) n,m)) /\
(forall p tid eid n m,
TcbMod.get tcbls tid = Some (p,wait (os_stat_q eid) n,m)->
(exists x y qwaitset,
EcbMod.get ecbls eid = Some (absmsgq x y,qwaitset) /\
In tid qwaitset)).
Definition RH_TCBList_ECBList_SEM_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n wls tid,
(EcbMod.get ecbls eid = Some (abssem n, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_sem eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_sem eid) t, msg) ->
(exists n wls,
EcbMod.get ecbls eid = Some (abssem n, wls) /\
In tid wls)).
Definition RH_TCBList_ECBList_MBOX_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n wls tid,
(EcbMod.get ecbls eid = Some (absmbox n, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mbox eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_mbox eid) t, msg) ->
(exists n wls,
EcbMod.get ecbls eid = Some (absmbox n, wls) /\
In tid wls)).
Definition RH_TCBList_ECBList_MUTEX_OWNER ecbls tcbls :=
forall eid pr wls opr tid,
(EcbMod.get ecbls eid = Some (absmutexsem pr (Some (tid, opr)), wls)) ->
(exists prio msg st,
TcbMod.get tcbls tid = Some (prio, st, msg)).
Definition RH_TCBList_ECBList_MUTEX_P (ecbls:EcbMod.map) (tcbls:TcbMod.map) (ct:tid) :=
(forall eid n1 n2 wls tid,
(EcbMod.get ecbls eid = Some (absmutexsem n1 n2, wls) /\ In tid wls) ->
(exists prio msg t,
TcbMod.get tcbls tid = Some (prio, wait (os_stat_mutexsem eid) t, msg))) /\
(forall p tid eid t msg,
TcbMod.get tcbls tid = Some (p, wait (os_stat_mutexsem eid) t, msg) ->
(exists n1 n2 wls,
EcbMod.get ecbls eid = Some (absmutexsem n1 n2, wls) /\
In tid wls)) /\
RH_TCBList_ECBList_MUTEX_OWNER ecbls tcbls.
The relationship between the high-level abstract event list and the high-level abstract tcb list
Definition RH_TCBList_ECBList_P ecbls tcbls ct:=
RH_TCBList_ECBList_Q_P ecbls tcbls ct /\
RH_TCBList_ECBList_SEM_P ecbls tcbls ct /\
RH_TCBList_ECBList_MBOX_P ecbls tcbls ct /\
RH_TCBList_ECBList_MUTEX_P ecbls tcbls ct.
Definition AMsgData losq osq osqblk msgtbl:=
EX losqblk,
AOSQCtr losq osq **
[| V_qfreeblk osq = Some losqblk |] **
AOSQBlk losqblk osqblk msgtbl.
Definition AEventData:=
fun (osevent : vallist) (d : EventData) =>
match d with
| DMsgQ a osq osqblk msgtbl =>
[|V_OSEventPtr osevent = Some a|] **
[|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_Q)|] **
AMsgData a osq osqblk msgtbl
| DSem z => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_SEM)|] **
[| V_OSEventCnt osevent = Some (Vint32 z) |] ** [| Int.ltu z (Int.repr 65536) = true |]
| DMbox msg => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_MBOX)|] **
[| V_OSEventPtr osevent = Some msg |]
| DMutex a b => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_MUTEX)|] **
[| V_OSEventCnt osevent = Some a |] ** [| V_OSEventPtr osevent = Some b|]
end.
Definition AEventNode:=
fun (v : val) (osevent etbl : vallist) (d : EventData) =>
AOSEvent v osevent etbl ** AEventData osevent d.
Fixpoint evsllseg (head tailnext : val) (vl:list EventCtr)
(ecbls : list EventData) {struct vl}: asrt :=
match vl with
| nil => [|head = tailnext /\ ecbls = nil|]
| l::vl´=>
match ecbls with
| nil => Afalse
| enode :: ecbls´ =>
match l with
| (osevent, etbl) =>
EX vn,
[|V_OSEventListPtr osevent = Some vn|] **
AEventNode head osevent etbl enode **
evsllseg vn tailnext vl´ ecbls´
end
end
end.
Definition PrioWaitInQ prio etbl :=
exists x y z,
0<=prio<64 /\
x = Int.and ($ prio) ($ 7) /\ y = Int.shru ($ prio) ($ 3) /\
nth_val (nat_of_Z (Int.unsigned y)) etbl = Some (Vint32 z) /\
Int.and z (Int.shl Int.one x) = (Int.shl Int.one x).
Definition RLH_ECB_ETbl_Q_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_q l) n,m))
end.
Definition RLH_ECB_ETbl_SEM_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_sem l) n,m))
end.
Definition RLH_ECB_ETbl_MBOX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_mbox l) n,m))
end.
Definition RLH_ECB_ETbl_MUTEX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_mutexsem l) n,m))
end.
Definition RHL_ECB_ETbl_Q_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_q l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q))
end.
Definition RHL_ECB_ETbl_SEM_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_sem l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM))
end.
Definition RHL_ECB_ETbl_MBOX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_mbox l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX))
end.
Definition RHL_ECB_ETbl_MUTEX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_mutexsem l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX))
end.
Definition RLH_ECB_ETbl_P l ecb tcbls := RLH_ECB_ETbl_Q_P l ecb tcbls /\RLH_ECB_ETbl_SEM_P l ecb tcbls /\RLH_ECB_ETbl_MBOX_P l ecb tcbls /\RLH_ECB_ETbl_MUTEX_P l ecb tcbls.
Definition RHL_ECB_ETbl_P l ecb tcbls := RHL_ECB_ETbl_Q_P l ecb tcbls /\ RHL_ECB_ETbl_SEM_P l ecb tcbls /\ RHL_ECB_ETbl_MBOX_P l ecb tcbls /\ RHL_ECB_ETbl_MUTEX_P l ecb tcbls.
Definition Event_Type_P osevent :=
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX)).
Definition R_ECB_ETbl_P (l:addrval) (ecb : EventCtr) tcbls :=
RLH_ECB_ETbl_P l ecb tcbls /\
RHL_ECB_ETbl_P l ecb tcbls /\
Event_Type_P (fst ecb).
Fixpoint ECBList_P (v tl: val) (l:list EventCtr) (ecbls : list EventData) (mqls: EcbMod.map)
(tcbls : TcbMod.map)
{struct l} : Prop :=
match l with
| nil => ecbls=nil /\ mqls = EcbMod.emp /\ v = tl
| vl :: l´ =>
exists qid,
v = Vptr qid /\ R_ECB_ETbl_P qid vl tcbls /\
match ecbls with
| nil => False
| enode ::ecbls´ =>
match vl with
| (osevent,etbl) =>
exists absmq mqls´ v´,
V_OSEventListPtr osevent = Some v´ /\
EcbMod.joinsig qid absmq mqls´ mqls /\
RLH_ECBData_P enode absmq /\
ECBList_P v´ tl l´ ecbls´ mqls´ tcbls
end
end
end.
RH_TCBList_ECBList_Q_P ecbls tcbls ct /\
RH_TCBList_ECBList_SEM_P ecbls tcbls ct /\
RH_TCBList_ECBList_MBOX_P ecbls tcbls ct /\
RH_TCBList_ECBList_MUTEX_P ecbls tcbls ct.
Definition AMsgData losq osq osqblk msgtbl:=
EX losqblk,
AOSQCtr losq osq **
[| V_qfreeblk osq = Some losqblk |] **
AOSQBlk losqblk osqblk msgtbl.
Definition AEventData:=
fun (osevent : vallist) (d : EventData) =>
match d with
| DMsgQ a osq osqblk msgtbl =>
[|V_OSEventPtr osevent = Some a|] **
[|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_Q)|] **
AMsgData a osq osqblk msgtbl
| DSem z => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_SEM)|] **
[| V_OSEventCnt osevent = Some (Vint32 z) |] ** [| Int.ltu z (Int.repr 65536) = true |]
| DMbox msg => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_MBOX)|] **
[| V_OSEventPtr osevent = Some msg |]
| DMutex a b => [|V_OSEventType osevent = Some (V$OS_EVENT_TYPE_MUTEX)|] **
[| V_OSEventCnt osevent = Some a |] ** [| V_OSEventPtr osevent = Some b|]
end.
Definition AEventNode:=
fun (v : val) (osevent etbl : vallist) (d : EventData) =>
AOSEvent v osevent etbl ** AEventData osevent d.
Fixpoint evsllseg (head tailnext : val) (vl:list EventCtr)
(ecbls : list EventData) {struct vl}: asrt :=
match vl with
| nil => [|head = tailnext /\ ecbls = nil|]
| l::vl´=>
match ecbls with
| nil => Afalse
| enode :: ecbls´ =>
match l with
| (osevent, etbl) =>
EX vn,
[|V_OSEventListPtr osevent = Some vn|] **
AEventNode head osevent etbl enode **
evsllseg vn tailnext vl´ ecbls´
end
end
end.
Definition PrioWaitInQ prio etbl :=
exists x y z,
0<=prio<64 /\
x = Int.and ($ prio) ($ 7) /\ y = Int.shru ($ prio) ($ 3) /\
nth_val (nat_of_Z (Int.unsigned y)) etbl = Some (Vint32 z) /\
Int.and z (Int.shl Int.one x) = (Int.shl Int.one x).
Definition RLH_ECB_ETbl_Q_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_q l) n,m))
end.
Definition RLH_ECB_ETbl_SEM_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_sem l) n,m))
end.
Definition RLH_ECB_ETbl_MBOX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_mbox l) n,m))
end.
Definition RLH_ECB_ETbl_MUTEX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent,etbl) =>
forall prio, PrioWaitInQ prio etbl ->
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX)) ->
(exists tid n m,
TcbMod.get tcbls tid = Some ((Int.repr prio),wait (os_stat_mutexsem l) n,m))
end.
Definition RHL_ECB_ETbl_Q_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_q l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q))
end.
Definition RHL_ECB_ETbl_SEM_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_sem l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM))
end.
Definition RHL_ECB_ETbl_MBOX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_mbox l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX))
end.
Definition RHL_ECB_ETbl_MUTEX_P (l:addrval) (ecb : EventCtr) tcbls :=
match ecb with
| (osevent, etbl) =>
forall prio m n tid, TcbMod.get tcbls tid = Some (prio,wait (os_stat_mutexsem l) n,m) ->
PrioWaitInQ (Int.unsigned prio) etbl /\ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX))
end.
Definition RLH_ECB_ETbl_P l ecb tcbls := RLH_ECB_ETbl_Q_P l ecb tcbls /\RLH_ECB_ETbl_SEM_P l ecb tcbls /\RLH_ECB_ETbl_MBOX_P l ecb tcbls /\RLH_ECB_ETbl_MUTEX_P l ecb tcbls.
Definition RHL_ECB_ETbl_P l ecb tcbls := RHL_ECB_ETbl_Q_P l ecb tcbls /\ RHL_ECB_ETbl_SEM_P l ecb tcbls /\ RHL_ECB_ETbl_MBOX_P l ecb tcbls /\ RHL_ECB_ETbl_MUTEX_P l ecb tcbls.
Definition Event_Type_P osevent :=
V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_Q)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_SEM)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MBOX)) \/ V_OSEventType osevent = Some (Vint32 (Int.repr OS_EVENT_TYPE_MUTEX)).
Definition R_ECB_ETbl_P (l:addrval) (ecb : EventCtr) tcbls :=
RLH_ECB_ETbl_P l ecb tcbls /\
RHL_ECB_ETbl_P l ecb tcbls /\
Event_Type_P (fst ecb).
Fixpoint ECBList_P (v tl: val) (l:list EventCtr) (ecbls : list EventData) (mqls: EcbMod.map)
(tcbls : TcbMod.map)
{struct l} : Prop :=
match l with
| nil => ecbls=nil /\ mqls = EcbMod.emp /\ v = tl
| vl :: l´ =>
exists qid,
v = Vptr qid /\ R_ECB_ETbl_P qid vl tcbls /\
match ecbls with
| nil => False
| enode ::ecbls´ =>
match vl with
| (osevent,etbl) =>
exists absmq mqls´ v´,
V_OSEventListPtr osevent = Some v´ /\
EcbMod.joinsig qid absmq mqls´ mqls /\
RLH_ECBData_P enode absmq /\
ECBList_P v´ tl l´ ecbls´ mqls´ tcbls
end
end
end.
The relational assertion specifies the event list with the spatial part "evsllseg" and the pure part ECBList_P
Definition AECBList (l : list EventCtr)
(ecbls : list EventData) (els: EcbMod.map) (tcbls : TcbMod.map)
: asrt :=
(EX p, (GV OSEventList @ (Tptr OS_EVENT) |-> p **
evsllseg p Vnull l ecbls) **[| ECBList_P p Vnull l ecbls els tcbls|]).
Definition isr_is_prop isr is:=
forall (x:hid), ~(List.In x is) -> isr x =false.
(ecbls : list EventData) (els: EcbMod.map) (tcbls : TcbMod.map)
: asrt :=
(EX p, (GV OSEventList @ (Tptr OS_EVENT) |-> p **
evsllseg p Vnull l ecbls) **[| ECBList_P p Vnull l ecbls els tcbls|]).
Definition isr_is_prop isr is:=
forall (x:hid), ~(List.In x is) -> isr x =false.
The invariant conformed by "isr" and "is"
The global invariant
Definition OSInv :=
EX eventl osql qblkl msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp ecbls tcbls t ct vhold ptfree lfree,
AOSEventFreeList eventl ** AOSQFreeList osql **
AOSQFreeBlk qblkl **
AECBList ectrl msgql ecbls tcbls **
AOSMapTbl ** AOSUnMapTbl ** AOSTCBPrioTbl ptbl rtbl tcbls vhold **
AOSIntNesting **
AOSTCBList p1 p2 tcbl1 (tcbcur::tcbl2) rtbl ct tcbls **
AOSTCBFreeList ptfree lfree **
AOSRdyTblGrp rtbl rgrp ** AOSTime (Vint32 t) **
HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct **
AGVars **
[| RH_TCBList_ECBList_P ecbls tcbls ct|] ** [| RH_CurTCB ct tcbls|] ** A_isr_is_prop.
Close Scope int_scope.
Close Scope Z_scope.
EX eventl osql qblkl msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp ecbls tcbls t ct vhold ptfree lfree,
AOSEventFreeList eventl ** AOSQFreeList osql **
AOSQFreeBlk qblkl **
AECBList ectrl msgql ecbls tcbls **
AOSMapTbl ** AOSUnMapTbl ** AOSTCBPrioTbl ptbl rtbl tcbls vhold **
AOSIntNesting **
AOSTCBList p1 p2 tcbl1 (tcbcur::tcbl2) rtbl ct tcbls **
AOSTCBFreeList ptfree lfree **
AOSRdyTblGrp rtbl rgrp ** AOSTime (Vint32 t) **
HECBList ecbls ** HTCBList tcbls ** HTime t ** HCurTCB ct **
AGVars **
[| RH_TCBList_ECBList_P ecbls tcbls ct|] ** [| RH_CurTCB ct tcbls|] ** A_isr_is_prop.
Close Scope int_scope.
Close Scope Z_scope.