Library InternalFunSpec
This file contains the specification of the uC/OS-II internal functions.
Internal functions are used by the uC/OS-II kernel to implement some
recurring functionalities inside the kernel itself.
The internal functions specified in this file correspond to those defined
in 'os_core.v', and are used in the APIs we are verifying. Internal
functions are not intended to be used by the application programmer.
In our framework, the assertions used to specify the pre and post conditions
of an internal function must obey some syntactic restrictions. We use the
definition 'GoodFunAsrt' to impose this restriction on the pre and post
conditions we defined for the various internal functions.
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 Export OSTCBInvDef.
Require Export OSQInvDef.
Require Import absop.
Require Import simulation.
Require Import os_core.
Require Import os_code_notations.
Require Import auxdef.
Require Import inv_prop.
Open Scope Z_scope.
Open Scope int_scope.
Require Import List.
Open Scope code_scope.
A solver for checking the syntax restriction on internal
function pre & post conditions defined in this file, with
some supporting lemmas.
Lemma GoodFunAsrt_Astruct´ :
forall vl v d, GoodFunAsrt(Astruct´ v d vl).
Lemma GoodFunAsrt_Astruct :
forall v t vl, GoodFunAsrt(Astruct v t vl).
Lemma GoodFunAsrt_Aarray´ :
forall vl n t l, GoodFunAsrt (Aarray´ l n t vl).
Lemma GoodFunAsrt_Aarray :
forall l t vl, GoodFunAsrt(Aarray l t vl).
Lemma GoodFunAsrt_AOSEvent :
forall v osevent etbl,
GoodFunAsrt (AOSEvent v osevent etbl).
Lemma GoodFunAsrt_AEventData :
forall osevent d,
GoodFunAsrt (AEventData osevent d).
Lemma GoodFunAstr_AEventNode :
forall v osevent etbl d,
GoodFunAsrt (AEventNode v osevent etbl d).
Lemma GoodFunAsrt_evsllseg :
forall vl head tailnext ecbls,
GoodFunAsrt (evsllseg head tailnext vl ecbls).
Lemma GoodFunAsrt_dllseg :
forall l head headprev tail tailnext t pre next,
GoodFunAsrt(dllseg head headprev tail tailnext l t pre next).
Lemma GoodFunAsrt_tcbdllseg :
forall head headprev tail tailnext l,
GoodFunAsrt (tcbdllseg head headprev tail tailnext l).
Lemma GoodFunAsrt_qblkf_sllseg :
forall l head tailnext t next,
GoodFunAsrt (qblkf_sllseg head tailnext l t next).
Lemma GoodFunAsrt_qblkf_sll :
forall head l t next,
GoodFunAsrt (qblkf_sll head l t next).
Lemma GoodFunAsrt_ecbf_sllseg :
forall l head tailnext t next,
GoodFunAsrt (ecbf_sllseg head tailnext l t next).
Lemma GoodFunAsrt_ecbf_sll :
forall head l t next,
GoodFunAsrt (ecbf_sllseg head Vnull l t next).
Lemma GoodFunAsrt_sllseg :
forall l head tailnext t next,
GoodFunAsrt (sllseg head tailnext l t next).
Lemma GoodFunAsrt_sll :
forall head l t next,
GoodFunAsrt(sll head l t next).
Definition invlth_isr´ (I:Inv) l h:=
match leb l h with
| true => atoy_inv´
| false => Aemp
end.
Lemma GoodFunAsrt_invlth_isr´ :
forall x l h,
GoodFunAsrt (invlth_isr´ x l h).
Ltac GoodFunAsrt_solver :=
repeat (split;
try (apply GoodFunAsrt_Aarray);
try (apply GoodFunAsrt_Astruct);
try (apply GoodFunAsrt_AEventData);
try (apply GoodFunAsrt_evsllseg);
try (apply GoodFunAsrt_tcbdllseg);
try (apply GoodFunAsrt_dllseg);
try (apply GoodFunAsrt_ecbf_sll);
try (apply GoodFunAsrt_sll);
try (apply GoodFunAsrt_qblkf_sll);
try (apply GoodFunAsrt_invlth_isr´);
auto).
Specification for internal function OS_EventWaitListInit.
This function is used to initialize the wait table and the wait group
of an event.
Pre condition
Note: The parameter 'vl' is the list of argument values passed to the function
on invocation. The parameter 'logicl' is used to preserve the identities of some
logic variables before and after the function invocation, see the corresponding
inference rules for more information. These are the same for all the specs defined
in this file.
Before the function invocation, we should have the event control block we want to
initialize in the resource, the event table is described by a separate array
structure in our invariant definition.
Assertion of the pre condition.
Definition OS_EventWaitListInitPre´ (vl:vallist) (logicl:list logicvar):=
EX b i1 i0 i2 x2 x3 v´22 v´24 s,
Aisr empisr ** Aie false ** Ais nil ** Acs (true :: nil) **
Astruct (b, Int.zero) OS_EVENT
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´22 :: nil) **
Aarray (b, Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ($ 1+ᵢInt.zero)))))
(Tarray Int8u ∘OS_EVENT_TBL_SIZE) v´24 ** A_isr_is_prop ** <||s||> **
[| nth_val 0 vl = Some (Vptr (b, Int.zero)) /\ Int.unsigned i1 <= 255/\Int.unsigned i0 <= 255/\Int.unsigned i2 <= 65535 /\
isptr x2 /\ isptr v´22 /\ logicl = logic_code s :: nil|].
EX b i1 i0 i2 x2 x3 v´22 v´24 s,
Aisr empisr ** Aie false ** Ais nil ** Acs (true :: nil) **
Astruct (b, Int.zero) OS_EVENT
(Vint32 i1 :: Vint32 i0 :: Vint32 i2 :: x2 :: x3 :: v´22 :: nil) **
Aarray (b, Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ($ 1+ᵢInt.zero)))))
(Tarray Int8u ∘OS_EVENT_TBL_SIZE) v´24 ** A_isr_is_prop ** <||s||> **
[| nth_val 0 vl = Some (Vptr (b, Int.zero)) /\ Int.unsigned i1 <= 255/\Int.unsigned i0 <= 255/\Int.unsigned i2 <= 65535 /\
isptr x2 /\ isptr v´22 /\ logicl = logic_code s :: nil|].
syntax restriction
Theorem OS_EventWaitListInitPreGood (vl:vallist) (logicl:list logicvar):
GoodFunAsrt (OS_EventWaitListInitPre´ vl logicl).
GoodFunAsrt (OS_EventWaitListInitPre´ vl logicl).
combine the assertion and the syntax property into the final pre condition definition.
Definition OS_EventWaitListInitPre : fpre :=
fun vl ll => mkfunasrt (OS_EventWaitListInitPreGood vl ll).
fun vl ll => mkfunasrt (OS_EventWaitListInitPreGood vl ll).
Post condition
Notation INIT_EVENT_TBL :=
(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).
(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).
Assertion of the post condition.
Note: The parameter v represents the return value of the function invocation.
The wait table and wait group has been initialized, e.g. each table row and the group are set to 0.
Definition OS_EventWaitListInitPost´ (vl:vallist) (v:option val) (logicl:list logicvar):=
EX b i1 i2 x2 x3 v´22 s,
Aisr empisr ** Aie false ** Ais nil ** Acs (true :: nil) **
Astruct (b, Int.zero) OS_EVENT
(Vint32 i1 :: Vint32 Int.zero ::
Vint32 i2 :: x2 :: x3 :: v´22 :: nil) **
Aarray (b, Int.zero+ᵢ($ 4+ᵢ($ 2+ᵢ($ 1+ᵢ($ 1+ᵢInt.zero)))))
(Tarray Int8u ∘OS_EVENT_TBL_SIZE) INIT_EVENT_TBL ** A_isr_is_prop ** <||s||> **
[| nth_val 0 vl = Some (Vptr (b, Int.zero)) /\ Int.unsigned i1 <= 255/\
Int.unsigned i2 <= 65535 /\
isptr x2 /\ isptr v´22 /\ v = None/\ logicl = logic_code s :: nil|].
Theorem OS_EventWaitListInitPostGood (vl:vallist) (v:option val) (logicl:list logicvar):
GoodFunAsrt (OS_EventWaitListInitPost´ vl v logicl).
Definition OS_EventWaitListInitPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventWaitListInitPostGood vl v ll).
Specification for internal function OS_EventSearch.
We maintained a list of all the kernel events created in the current version
in order to distinguish whether a pointer passed by the user to an API points
to a valid event control block.
This function searches the event list for a particular event.
Assertion for the pre condition
Before the function invocation, we should have the event list in the resource,
and also some other resources from the invariant which maybe useful during the
reasoning of the implementation code.
Definition OS_EventSearchPre´ (vl:vallist) (logicl:list logicvar):=
EX msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
AECBList ectrl msgql mqls tcbls **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct **
A_isr_is_prop ** <||s||> **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| RH_CurTCB ct tcbls |] ** [|logicl = logic_code s::nil|].
Theorem OS_EventSearchPreGood (vl:vallist) logicl:
GoodFunAsrt (OS_EventSearchPre´ vl logicl).
Definition OS_EventSearchPre : fpre :=
fun vl ll=> mkfunasrt (OS_EventSearchPreGood vl ll).
EX msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
AECBList ectrl msgql mqls tcbls **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct **
A_isr_is_prop ** <||s||> **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| RH_CurTCB ct tcbls |] ** [|logicl = logic_code s::nil|].
Theorem OS_EventSearchPreGood (vl:vallist) logicl:
GoodFunAsrt (OS_EventSearchPre´ vl logicl).
Definition OS_EventSearchPre : fpre :=
fun vl ll=> mkfunasrt (OS_EventSearchPreGood vl ll).
Assertion for the post condition.
We have either successfully found the event in the list (the first part of the disjunction),
and we got the return value 1. The event node corresponds to the event we are searching for
has been split out from the list. Or the search has failed and we got the return value 0, the
resources remained intacted.
Definition OS_EventSearchPost´ (vl:vallist) (v:option val) (logicl:list logicvar):=
(EX msgqls ectrl1 ectrl2 msgqls1 msgqls2 ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct p a b msgq vn mqls1 mqls2 mqls´ mq vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ (Tptr OS_EVENT) |-> p **
AEventNode (Vptr qid) a b msgq **
evsllseg p (Vptr qid) ectrl1 msgqls1 **
evsllseg vn Vnull ectrl2 msgqls2 **
A_isr_is_prop **
[|ECBList_P p Vnull ectrl msgqls mqls tcbls|] **
[|ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls|] **
[|ECBList_P vn Vnull ectrl2 msgqls2 mqls2 tcbls|] **
[| RLH_ECBData_P msgq mq |] **
[| R_ECB_ETbl_P qid (a,b) tcbls |] **
[| EcbMod.joinsig qid mq mqls2 mqls´/\ EcbMod.join mqls1 mqls´ mqls |] **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct ** <||s ||> **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| RH_CurTCB ct tcbls |] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| ectrl = ectrl1 ++ ((a,b)::nil) ++ ectrl2 |] **
[| msgqls = msgqls1 ++ (msgq::nil) ++msgqls2|] **
[|length ectrl1 = length msgqls1 |] **
[|V_OSEventListPtr a = Some vn|] **
[| v = Some (V$1) |] ** [|logicl = logic_code s :: nil|]) \\//
(EX msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
AECBList ectrl msgql mqls tcbls **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct ** <||s ||> **
A_isr_is_prop **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| RH_CurTCB ct tcbls |] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| (v = Some (V$0) /\ EcbMod.get mqls qid = None) |]
** [|logicl = logic_code s :: nil|]).
Theorem OS_EventSearchPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventSearchPost´ vl v ll).
Definition OS_EventSearchPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventSearchPostGood vl v ll).
Fixpoint get_eid_ecbls (ecbls:list EventCtr):=
match ecbls with
| nil => nil
| (a,b)::ecbls´ => (nth_val´ 5 a) :: (get_eid_ecbls ecbls´)
end.
Definition get_eidls eid ecbls := eid::(List.removelast (get_eid_ecbls ecbls)).
(EX msgqls ectrl1 ectrl2 msgqls1 msgqls2 ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct p a b msgq vn mqls1 mqls2 mqls´ mq vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ (Tptr OS_EVENT) |-> p **
AEventNode (Vptr qid) a b msgq **
evsllseg p (Vptr qid) ectrl1 msgqls1 **
evsllseg vn Vnull ectrl2 msgqls2 **
A_isr_is_prop **
[|ECBList_P p Vnull ectrl msgqls mqls tcbls|] **
[|ECBList_P p (Vptr qid) ectrl1 msgqls1 mqls1 tcbls|] **
[|ECBList_P vn Vnull ectrl2 msgqls2 mqls2 tcbls|] **
[| RLH_ECBData_P msgq mq |] **
[| R_ECB_ETbl_P qid (a,b) tcbls |] **
[| EcbMod.joinsig qid mq mqls2 mqls´/\ EcbMod.join mqls1 mqls´ mqls |] **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct ** <||s ||> **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| RH_CurTCB ct tcbls |] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| ectrl = ectrl1 ++ ((a,b)::nil) ++ ectrl2 |] **
[| msgqls = msgqls1 ++ (msgq::nil) ++msgqls2|] **
[|length ectrl1 = length msgqls1 |] **
[|V_OSEventListPtr a = Some vn|] **
[| v = Some (V$1) |] ** [|logicl = logic_code s :: nil|]) \\//
(EX msgql ectrl ptbl p1 p2 tcbl1 tcbcur tcbl2 rtbl rgrp mqls tcbls qid ct vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
AECBList ectrl msgql mqls tcbls **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp ** AOSTCBPrioTbl ptbl rtbl tcbls vhold**
HECBList mqls ** HTCBList tcbls ** HCurTCB ct ** <||s ||> **
A_isr_is_prop **
[| RH_TCBList_ECBList_P mqls tcbls ct|] **
[| RH_CurTCB ct tcbls |] **
[| nth_val 0 vl = Some (Vptr qid)|] **
[| (v = Some (V$0) /\ EcbMod.get mqls qid = None) |]
** [|logicl = logic_code s :: nil|]).
Theorem OS_EventSearchPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventSearchPost´ vl v ll).
Definition OS_EventSearchPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventSearchPostGood vl v ll).
Fixpoint get_eid_ecbls (ecbls:list EventCtr):=
match ecbls with
| nil => nil
| (a,b)::ecbls´ => (nth_val´ 5 a) :: (get_eid_ecbls ecbls´)
end.
Definition get_eidls eid ecbls := eid::(List.removelast (get_eid_ecbls ecbls)).
Specification for internal function OS_EventRemove.
This function removes a particular event from the event list mention above.
Definition get_last_ptr (els : list EventCtr) :=
match(last els (nil,nil)) with
| (a,b) => V_OSEventListPtr a
end.
match(last els (nil,nil)) with
| (a,b) => V_OSEventListPtr a
end.
Assertion for the pre condition
The resource should contain the event list before the function invocation.
Also this function is always called after 'OS_EventSearch' successfully finds
the event in the event list, so the node we would like to remove is guaranteed
to be inside the list in the pre condition, which resides at the head node of
the 2nd segment of the value list, e.g. 'ectrl2'.
Definition OS_EventRemovePre´ (vl:vallist) (logicl:list logicvar):=
EX (msgql1 msgql2 : list EventData)
(ectrl1 ectrl2 : list EventCtr)
p qid s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ Tptr OS_EVENT |-> p **
evsllseg p Vnull (ectrl1 ++ ectrl2) (msgql1 ++ msgql2) **
A_isr_is_prop ** <||s||> **
[|nth_val 0 vl = Some (Vptr qid) |] **
[| length ectrl1 = length msgql1 |] **
[| (ectrl1 = nil -> Vptr qid = p)
/\ (ectrl1 <> nil -> Some (Vptr qid) = get_last_ptr ectrl1)|] **
[| logicl = logic_val p :: logic_leventc ectrl1 ::
logic_leventc ectrl2 :: logic_leventd msgql1 ::
logic_leventd msgql2 :: logic_code s ::
nil|].
Theorem OS_EventRemovePreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventRemovePre´ vl ll).
Definition OS_EventRemovePre : fpre :=
fun vl => fun ll=> mkfunasrt (OS_EventRemovePreGood vl ll).
EX (msgql1 msgql2 : list EventData)
(ectrl1 ectrl2 : list EventCtr)
p qid s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ Tptr OS_EVENT |-> p **
evsllseg p Vnull (ectrl1 ++ ectrl2) (msgql1 ++ msgql2) **
A_isr_is_prop ** <||s||> **
[|nth_val 0 vl = Some (Vptr qid) |] **
[| length ectrl1 = length msgql1 |] **
[| (ectrl1 = nil -> Vptr qid = p)
/\ (ectrl1 <> nil -> Some (Vptr qid) = get_last_ptr ectrl1)|] **
[| logicl = logic_val p :: logic_leventc ectrl1 ::
logic_leventc ectrl2 :: logic_leventd msgql1 ::
logic_leventd msgql2 :: logic_code s ::
nil|].
Theorem OS_EventRemovePreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventRemovePre´ vl ll).
Definition OS_EventRemovePre : fpre :=
fun vl => fun ll=> mkfunasrt (OS_EventRemovePreGood vl ll).
some definitions for the post condition
Fixpoint update_nth (t : Type ) (n : nat) (vl : list t) (v : t) {struct vl} : list t :=
match vl with
| nil => nil
| v´ :: vl´ =>
match n with
| 0%nat => v :: vl´
| S n´ => v´ :: update_nth t n´ vl´ v
end
end.
Definition update_ectr (x : EventCtr) (v : val) :=
match x with
| (a , b) => (update_nth _ 5%nat a v, b)
end.
Fixpoint update_nth_ectrls (els : list EventCtr) (n: nat) (v:val) :=
match els with
| nil => nil
| v´ :: vl´ =>
match n with
| 0%nat => (update_ectr v´ v) :: vl´
| S n´ => v´ :: update_nth_ectrls vl´ n´ v
end
end.
Definition upd_last_ectrls (els : list EventCtr) (v:val) :=
update_nth_ectrls els (length els - 1)%nat v.
match vl with
| nil => nil
| v´ :: vl´ =>
match n with
| 0%nat => v :: vl´
| S n´ => v´ :: update_nth t n´ vl´ v
end
end.
Definition update_ectr (x : EventCtr) (v : val) :=
match x with
| (a , b) => (update_nth _ 5%nat a v, b)
end.
Fixpoint update_nth_ectrls (els : list EventCtr) (n: nat) (v:val) :=
match els with
| nil => nil
| v´ :: vl´ =>
match n with
| 0%nat => (update_ectr v´ v) :: vl´
| S n´ => v´ :: update_nth_ectrls vl´ n´ v
end
end.
Definition upd_last_ectrls (els : list EventCtr) (v:val) :=
update_nth_ectrls els (length els - 1)%nat v.
Assertion for the post condition
The event node at the head of 'ectrl2' in the pre condition has been removed.
The head ptr of the event list is reset if the node removed is the head node
of the original event list.
Definition OS_EventPtrRemovePost´ (vl:vallist) (v:option val) (logicl:list logicvar):=
(EX (msgql1 msgql2 : list EventData)
(ectrl1 ectrl2 ectrl1´: list EventCtr)
p p´ next ectr msgq osevent etbl qid s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ Tptr OS_EVENT |-> p´ **
evsllseg p´ Vnull (ectrl1´++ectrl2) (msgql1++msgql2) **
AEventNode (Vptr qid) osevent etbl msgq **
A_isr_is_prop ** <||s||> **
[| logicl = logic_val p :: logic_leventc ectrl1 ::
logic_leventc (ectr::ectrl2) :: logic_leventd msgql1 ::
logic_leventd (msgq::msgql2) ::logic_code s ::
nil|]**
[| nth_val 0 vl = Some (Vptr qid) |] **
[| ectr = (osevent,etbl) |] **
[| length ectrl1 = length msgql1 |] **
[| Some next = V_OSEventListPtr osevent |] **
[| (ectrl1 = nil -> (Vptr qid = p /\ p´ = next /\ ectrl1´ = nil))
/\ (ectrl1 <> nil -> (p´ = p /\ Some (Vptr qid) = get_last_ptr ectrl1 /\
ectrl1´ = upd_last_ectrls ectrl1 next))|]
).
Theorem OS_EventPtrRemovePostGood (vl:vallist) (v:option val) ll :
GoodFunAsrt (OS_EventPtrRemovePost´ vl v ll).
Definition OS_EventRemovePost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventPtrRemovePostGood vl v ll).
(EX (msgql1 msgql2 : list EventData)
(ectrl1 ectrl2 ectrl1´: list EventCtr)
p p´ next ectr msgq osevent etbl qid s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSEventList @ Tptr OS_EVENT |-> p´ **
evsllseg p´ Vnull (ectrl1´++ectrl2) (msgql1++msgql2) **
AEventNode (Vptr qid) osevent etbl msgq **
A_isr_is_prop ** <||s||> **
[| logicl = logic_val p :: logic_leventc ectrl1 ::
logic_leventc (ectr::ectrl2) :: logic_leventd msgql1 ::
logic_leventd (msgq::msgql2) ::logic_code s ::
nil|]**
[| nth_val 0 vl = Some (Vptr qid) |] **
[| ectr = (osevent,etbl) |] **
[| length ectrl1 = length msgql1 |] **
[| Some next = V_OSEventListPtr osevent |] **
[| (ectrl1 = nil -> (Vptr qid = p /\ p´ = next /\ ectrl1´ = nil))
/\ (ectrl1 <> nil -> (p´ = p /\ Some (Vptr qid) = get_last_ptr ectrl1 /\
ectrl1´ = upd_last_ectrls ectrl1 next))|]
).
Theorem OS_EventPtrRemovePostGood (vl:vallist) (v:option val) ll :
GoodFunAsrt (OS_EventPtrRemovePost´ vl v ll).
Definition OS_EventRemovePost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventPtrRemovePostGood vl v ll).
Specification for internal function OS_EventTaskRdy.
This function readies the task with the highest priority in the waiting list
of the event passed as the argument.
Assertion for pre condition
The operation of 'OS_EventTaskRdy' touches the priority table, the task ready
table and the task ready group, the TCB list, the event node of that event, also
in order to convert between the priority value and its bit representation, it
should also have access to the map and unmap tables.
The pre condition should describe these resources, and also some pure relations
between relevant structures that we need in the reasoning of the implement code.
Definition OS_EventTaskRdyPre´ (vl:vallist) (logicl:list logicvar):=
EX ptbl tcbl1 tcbcur tcbl2 rtbl rgrp
tcbls egrp
qid p1 p2 ct osevent etbl d vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr ** A_isr_is_prop **
AEventNode (Vptr qid) osevent etbl d ** <||s||> **
[| R_ECB_ETbl_P qid (osevent,etbl) tcbls |] **
AOSUnMapTbl **
AOSMapTbl **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp **
AOSTCBPrioTbl ptbl rtbl tcbls vhold**
[| nth_val 0 vl = Some (Vptr qid) |] **
[| V_OSEventGrp osevent = Some (Vint32 egrp) /\ egrp <> Int.zero |] **
[| logicl = logic_lv ptbl :: logic_lv tcbcur ::
logic_llv tcbl1 :: logic_llv tcbl2 ::
logic_lv rtbl :: logic_val rgrp :: logic_abstcb tcbls ::
logic_val p1 :: logic_val p2 ::
logic_val (Vptr ct) :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s::
nil |].
Theorem OS_EventTaskRdyPreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventTaskRdyPre´ vl ll).
Definition OS_EventTaskRdyPre : fpre :=
fun vl => fun ll => mkfunasrt (OS_EventTaskRdyPreGood vl ll).
Definition get_highest_prio grp tbl:=
match nth_val´ (Z.to_nat (Int.unsigned grp)) OSUnMapVallist with
| Vint32 x =>
match nth_val´ (Z.to_nat (Int.unsigned x)) tbl with
| Vint32 i0 =>
match nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist with
| Vint32 y => Some ((x<<$ 3) +ᵢ y)
| _ => None
end
| _ => None
end
| _ => None
end.
Definition get_highest_tcb ptbl x:= nth_val´ (Z.to_nat (Int.unsigned x)) ptbl.
Require Import symbolic_execution.
Require Import List.
Open Scope code_scope.
Definition get_last_tcb_ptr (l: list vallist) (x : val) :=
match l with
| nil => Some x
| _ => V_OSTCBNext (last l nil)
end.
EX ptbl tcbl1 tcbcur tcbl2 rtbl rgrp
tcbls egrp
qid p1 p2 ct osevent etbl d vhold s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr ** A_isr_is_prop **
AEventNode (Vptr qid) osevent etbl d ** <||s||> **
[| R_ECB_ETbl_P qid (osevent,etbl) tcbls |] **
AOSUnMapTbl **
AOSMapTbl **
AOSTCBList p1 p2 tcbl1 (tcbcur :: tcbl2) rtbl ct tcbls **
AOSRdyTblGrp rtbl rgrp **
AOSTCBPrioTbl ptbl rtbl tcbls vhold**
[| nth_val 0 vl = Some (Vptr qid) |] **
[| V_OSEventGrp osevent = Some (Vint32 egrp) /\ egrp <> Int.zero |] **
[| logicl = logic_lv ptbl :: logic_lv tcbcur ::
logic_llv tcbl1 :: logic_llv tcbl2 ::
logic_lv rtbl :: logic_val rgrp :: logic_abstcb tcbls ::
logic_val p1 :: logic_val p2 ::
logic_val (Vptr ct) :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s::
nil |].
Theorem OS_EventTaskRdyPreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventTaskRdyPre´ vl ll).
Definition OS_EventTaskRdyPre : fpre :=
fun vl => fun ll => mkfunasrt (OS_EventTaskRdyPreGood vl ll).
Definition get_highest_prio grp tbl:=
match nth_val´ (Z.to_nat (Int.unsigned grp)) OSUnMapVallist with
| Vint32 x =>
match nth_val´ (Z.to_nat (Int.unsigned x)) tbl with
| Vint32 i0 =>
match nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist with
| Vint32 y => Some ((x<<$ 3) +ᵢ y)
| _ => None
end
| _ => None
end
| _ => None
end.
Definition get_highest_tcb ptbl x:= nth_val´ (Z.to_nat (Int.unsigned x)) ptbl.
Require Import symbolic_execution.
Require Import List.
Open Scope code_scope.
Definition get_last_tcb_ptr (l: list vallist) (x : val) :=
match l with
| nil => Some x
| _ => V_OSTCBNext (last l nil)
end.
Assertion for post condition
The post condition for 'OS_EventTaskRdy' consists of 12 disjunctive cases.
The definition of the TCB list in current version of our framework is split as
'list1 ++ current_tcb :: list2', the task readied by 'OS_EventTaskRdy' may on
any of the three parts of this splitting. In each case, the bit in the event
group corresponding to the readied task may or maynot be unset depending on
whether this task is the last waiting task in that particular group. And also,
the task may or may not be set to the 'ready' state depending on if it is in
the 'suspended' state. If it is suspended, then the task ready table and task
ready group remain intact, else, the bit in the ready table and ready group
correspond to this task is set accordingly. So there are totally 3*2*2=12
disjunctive case in this post condition.
These 12 cases are some what ugly, and produced negative consequences for our
reasoning of the implementation code and API code using this internal function.
Its presentation is due to some historical issue during the development of our
verification framework and API code verification, we will get rid of it in the
next version of our project.
case1: task on first segment of tcb list, set to ready, event ready group bit cleared.
Definition event_rdy_post1 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil)
:: logic_code s :: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post2 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] ** <||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post3 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post4 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold |] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl**
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
case5: task is the current task, set to ready, event ready group bit cleared.
Definition event_rdy_post5 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post6 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post1´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post2´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post3´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold |] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x))rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post4´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post5´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post6´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold |] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition OS_EventTaskRdyPost_fold´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
(event_rdy_post1 vl v logicl \\// event_rdy_post2 vl v logicl \\// event_rdy_post3 vl v logicl \\// event_rdy_post4 vl v logicl \\// event_rdy_post5 vl v logicl \\// event_rdy_post6 vl v logicl \\// event_rdy_post1´ vl v logicl \\// event_rdy_post2´ vl v logicl \\// event_rdy_post3´ vl v logicl \\// event_rdy_post4´ vl v logicl \\// event_rdy_post5´ vl v logicl \\// event_rdy_post6´ vl v logicl) **
Aie false **
Ais nil **
Acs (true :: nil) **
Aisr empisr ** A_isr_is_prop.
Close Scope code_scope.
Definition OS_EventTaskRdyPost´ := OS_EventTaskRdyPost_fold´.
Theorem OS_EventTaskRdyPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventTaskRdyPost´ vl v ll).
Definition OS_EventTaskRdyPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventTaskRdyPostGood vl v ll).
Definition OS_EventTaskWaitPre´ (vl:vallist) (logicl:list logicvar):=
EX ct tcbcur rtbl rgrp qid osevent etbl d s,
<||s||> ** Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSTCBCur @ Tptr OS_TCB |-> (Vptr ct) **
node (Vptr ct) tcbcur OS_TCB **
[| RL_TCBblk_P tcbcur |] **
AOSRdyTblGrp rtbl rgrp ** AEventNode (Vptr qid) osevent etbl d **
[| logicl = logic_val (Vptr ct) :: logic_lv rtbl :: logic_val rgrp :: logic_lv tcbcur :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s :: nil |] **
[| nth_val 0 vl = Some (Vptr qid) /\ (exists p,V_OSTCBPrio tcbcur = Some (Vint32 p) /\ Int.eq p ($ OS_IDLE_PRIO) = false) |].
Theorem OS_EventTaskWaitPreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventTaskWaitPre´ vl ll).
Definition OS_EventTaskWaitPre : fpre :=
fun vl => fun ll => mkfunasrt (OS_EventTaskWaitPreGood vl ll).
Definition OS_EventTaskWaitPost´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
(EX ct tcbcur rtbl rgrp qid osevent etbl d
tcbcur´ rtbl´ rgrp´ osevent´ etbl´
y bitx bity ry ey egrp s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSTCBCur @ Tptr OS_TCB |-> (Vptr ct) **
node (Vptr ct) tcbcur´ OS_TCB **
AOSRdyTblGrp rtbl´ (Vint32 rgrp´) ** AEventNode (Vptr qid) osevent´ etbl´ d **
<||s||> **
[| logicl = logic_val (Vptr ct) :: logic_lv rtbl :: logic_val (Vint32 rgrp) :: logic_lv tcbcur :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s :: nil |] **
[| nth_val 0 vl = Some (Vptr qid) |] **
[| tcbcur´ = update_nth_val 2 tcbcur (Vptr qid) /\
V_OSTCBY tcbcur = Some (Vint32 y) /\
V_OSTCBBitX tcbcur = Some (Vint32 bitx) /\
V_OSTCBBitY tcbcur = Some (Vint32 bity) /\
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) /\
rtbl´ = update_nth_val (nat_of_Z (Int.unsigned y)) rtbl (Vint32 (Int.and ry (Int.not bitx))) /\
nth_val (nat_of_Z (Int.unsigned y)) etbl = Some (Vint32 ey) /\
etbl´ = update_nth_val (nat_of_Z (Int.unsigned y)) etbl (Vint32 (Int.or ey bitx)) /\
V_OSEventGrp osevent = Some (Vint32 egrp) /\
osevent´ = update_nth_val 1 osevent (Vint32 (Int.or egrp bity)) |]).
Theorem OS_EventTaskWaitPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventTaskWaitPost´ vl v ll).
Definition OS_EventTaskWaitPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventTaskWaitPostGood vl v ll).
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post6 (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = true |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 (ergrp&Int.not x3) :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post1´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post2´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´8 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_llv v´8
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P (Vptr v´16) (v´7 :: v´8) rtbl v´23 |] **
[| TCBList_P v´14 v´24 rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´21 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P v´14
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil) :: v´26)
rtbl v´21 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´24 v´14 = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´13 (Vptr v´16) v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´15 (Vptr (v´29, Int.zero)) v´24 **
tcbdllseg (Vptr v´16) v´13 v´17 Vnull (v´7 :: v´8) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post3´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold |] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x))rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post4´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´16 v´7 v´6 x16 x15 i9 i8 i7 i6 i5 i4 i3 v´15 v´29 x8 x9 x10 v´28 v´27 v´24 v´26 x11 v´13 v´17 v´19 vhold s vholdx,
[| logicl = (logic_lv ptbl
:: logic_lv v´7
:: logic_llv v´6
:: logic_llv
(v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26)
:: logic_lv rtbl
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr v´16)
:: logic_val (Vptr v´16)
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil) |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| TCBList_P (Vptr v´16) (v´7::v´24) rtbl v´27 |] **
[| TcbMod.join v´27 v´28 v´23 |] **
[| isptr x16 |] **
[| isptr x15 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´15 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´29, Int.zero) |] **
[| v´16 <> (v´29, Int.zero) |] **
[| TCBList_P x8 v´26 rtbl x9 |] **
[| TcbJoin (v´29, Int.zero) x10 x9 v´28 |] **
[| TcbJoin (v´29, Int.zero) x10 x11 tcbls |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| isptr x8 |] **
[| TCBList_P (Vptr v´16)
(v´7
:: v´24 ++
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: v´26) rtbl v´23 |] **
[| TCBNode_P
(x8
:: v´15
:: x16
:: x15
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr (v´7::v´24) (Vptr v´16) = Some (Vptr (v´29,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´29, Int.zero) OS_TCB
(x8
:: v´15
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´29, Int.zero)) v´17 Vnull v´26 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
tcbdllseg v´14 Vnull v´13 (Vptr v´16) v´6 **
tcbdllseg (Vptr v´16) v´13 v´15 (Vptr (v´29, Int.zero)) (v´7 :: v´24) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr v´16 **
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post5´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold|] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = true |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) rtbl
(val_inj
(or (nth_val´ (Z.to_nat (Int.unsigned x)) rtbl) (Vint32 x2)))) **
GV OSRdyGrp @ Int8u |-> Vint32 (Int.or rgrp x3) **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition event_rdy_post6´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX msk x0 ertbl i1 i2 x4 x6 ergrp v´22 v´20 x5 tcbls x i0 x1 x2 x3 ptbl rtbl rgrp v´14 v´21 v´23 v´6 x15 i9 i8 i7 i6 i5 i4 i3 x8 x9 x10 v´24 v´13 v´17 v´19 x14 v´8 v´9 vhold s vholdx,
[| logicl = logic_lv ptbl
:: logic_lv
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5
:: Vint32 i4 :: Vint32 i3 :: nil)
:: logic_llv v´6
:: logic_llv v´8
:: logic_lv v´9
:: logic_val (Vint32 rgrp)
:: logic_abstcb tcbls
:: logic_val v´14
:: logic_val (Vptr (v´24, Int.zero))
:: logic_val (Vptr (v´24, Int.zero))
:: logic_lv
(Vint32 i1
:: Vint32 ergrp
:: Vint32 i2
:: x4 :: x5 :: x6 :: nil)
:: logic_lv ertbl
:: logic_leventd (v´19 :: nil) :: logic_code s
:: nil |] **
[| Int.unsigned msk <= 255 |] **
[| isptr x0 |] **
[| array_type_vallist_match Int8u ertbl |] **
[| length ertbl = ∘OS_EVENT_TBL_SIZE |] **
[| Int.unsigned i1 <= 255 |] **
[| Int.unsigned i2 <= 65535 |] **
[| isptr x4 |] **
[| isptr x6 |] **
[| Int.unsigned ergrp <= 255 |] **
[| RL_Tbl_Grp_P ertbl (Vint32 ergrp) |] **
[| id_addrval´ (Vptr (v´22, Int.zero)) OSEventTbl OS_EVENT = Some v´20 |] **
[| R_ECB_ETbl_P (v´22, Int.zero)
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil,
ertbl) tcbls |] **
[| nth_val´ (Z.to_nat (Int.unsigned ergrp)) OSUnMapVallist = Vint32 x |] **
[| Int.unsigned x <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) ertbl = Vint32 i0 |] **
[| Int.unsigned i0 <= 255 |] **
[| nth_val´ (Z.to_nat (Int.unsigned i0)) OSUnMapVallist = Vint32 x1 |] **
[| Int.unsigned x1 <= 7 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x1)) OSMapVallist = Vint32 x2 |] **
[| Int.unsigned x2 <= 128 |] **
[| nth_val´ (Z.to_nat (Int.unsigned x)) OSMapVallist = Vint32 x3 |] **
[| Int.unsigned x3 <= 128 |] **
[| array_type_vallist_match OS_TCB ∗ ptbl |] **
[| length ptbl = 64%nat |] **
[| RL_RTbl_PrioTbl_P rtbl ptbl vhold|] **
[| R_PrioTbl_P ptbl tcbls vhold |] **
[| Int.eq (i0&Int.not x2) ($0) = false |] **
[| Int.eq (i8&Int.not msk) ($ OS_STAT_RDY) = false |] **
[| length
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) = ∘OS_EVENT_TBL_SIZE |] **
[| RL_RTbl_PrioTbl_P ertbl ptbl vhold|] **
[| prio_in_tbl ((x<<$ 3)+ᵢx1) ertbl |] **
[| v´14 <> Vnull |] **
[| TcbMod.join v´21 v´23 tcbls |] **
[| TCBList_P v´14 v´6 rtbl v´21 |] **
[| isptr x15 |] **
[| isptr x14 |] **
[| Int.unsigned i9 <= 65535 |] **
[| Int.unsigned i8 <= 255 |] **
[| Int.unsigned i7 <= 255 |] **
[| Int.unsigned i6 <= 255 |] **
[| Int.unsigned i5 <= 255 |] **
[| Int.unsigned i4 <= 255 |] **
[| Int.unsigned i3 <= 255 |] **
[| isptr v´13 |] **
[| nth_val´ (Z.to_nat (Int.unsigned ((x<<$ 3)+ᵢx1))) ptbl =
Vptr (v´24, Int.zero) |] **
[| TCBList_P x8 v´8 rtbl x9 |] **
[| TcbJoin (v´24, Int.zero) x10 x9 v´23 |] **
[| isptr x8 |] **
[| TCBNode_P
(x8
:: v´13
:: x15
:: x14
:: Vint32 i9
:: Vint32 i8
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil)
rtbl x10 |] **
[| array_type_vallist_match Int8u rtbl |] **
[| length rtbl = ∘OS_RDY_TBL_SIZE |] **
[| Int.unsigned rgrp <= 255 |] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl |] **
[| RL_Tbl_Grp_P rtbl (Vint32 rgrp) |] **
[| nth_val 0%nat vl = Some (Vptr (v´22, Int.zero)) |] **
[| nth_val 1%nat vl = Some x0 |] **
[| nth_val 2%nat vl = Some (Vint32 msk) |] **
[| get_last_tcb_ptr v´6 v´14 = Some (Vptr (v´24,Int.zero)) |] **
[| v = Some (Vint32 ((x<<$ 3)+ᵢx1)) |] **
<||s||> **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl **
GV OSRdyGrp @ Int8u |-> Vint32 rgrp **
Astruct (v´24, Int.zero) OS_TCB
(x8
:: v´13
:: Vnull
:: x0
:: V$0
:: Vint32 (i8&Int.not msk)
:: Vint32 i7
:: Vint32 i6
:: Vint32 i5 :: Vint32 i4 :: Vint32 i3 :: nil) **
dllseg x8 (Vptr (v´24, Int.zero)) v´17 Vnull v´8 OS_TCB
(fun vl : vallist => nth_val 1 vl) (fun vl : vallist => nth_val 0 vl) **
GV OSTCBList @ OS_TCB ∗ |-> v´14 **
tcbdllseg v´14 Vnull v´13 (Vptr (v´24, Int.zero)) v´6 **
GV OSTCBCur @ OS_TCB ∗ |-> Vptr (v´24, Int.zero)**
Aarray v´20 (Tarray Int8u ∘OS_EVENT_TBL_SIZE)
(update_nth_val (Z.to_nat (Int.unsigned x)) ertbl
(Vint32 (i0&Int.not x2))) **
Astruct (v´22, Int.zero) OS_EVENT
(Vint32 i1
:: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) **
AEventData
(Vint32 i1 :: Vint32 ergrp :: Vint32 i2 :: x4 :: x5 :: x6 :: nil) v´19 **
GAarray OSUnMapTbl (Tarray Int8u 256) OSUnMapVallist **
GAarray OSMapTbl (Tarray Int8u 8) OSMapVallist **
GAarray OSTCBPrioTbl (Tarray OS_TCB ∗ 64) ptbl **
G&OSPlaceHolder @ Int8u == vhold **
PV vhold @ Int8u |-> vholdx.
Definition OS_EventTaskRdyPost_fold´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
(event_rdy_post1 vl v logicl \\// event_rdy_post2 vl v logicl \\// event_rdy_post3 vl v logicl \\// event_rdy_post4 vl v logicl \\// event_rdy_post5 vl v logicl \\// event_rdy_post6 vl v logicl \\// event_rdy_post1´ vl v logicl \\// event_rdy_post2´ vl v logicl \\// event_rdy_post3´ vl v logicl \\// event_rdy_post4´ vl v logicl \\// event_rdy_post5´ vl v logicl \\// event_rdy_post6´ vl v logicl) **
Aie false **
Ais nil **
Acs (true :: nil) **
Aisr empisr ** A_isr_is_prop.
Close Scope code_scope.
Definition OS_EventTaskRdyPost´ := OS_EventTaskRdyPost_fold´.
Theorem OS_EventTaskRdyPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventTaskRdyPost´ vl v ll).
Definition OS_EventTaskRdyPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventTaskRdyPostGood vl v ll).
Definition OS_EventTaskWaitPre´ (vl:vallist) (logicl:list logicvar):=
EX ct tcbcur rtbl rgrp qid osevent etbl d s,
<||s||> ** Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSTCBCur @ Tptr OS_TCB |-> (Vptr ct) **
node (Vptr ct) tcbcur OS_TCB **
[| RL_TCBblk_P tcbcur |] **
AOSRdyTblGrp rtbl rgrp ** AEventNode (Vptr qid) osevent etbl d **
[| logicl = logic_val (Vptr ct) :: logic_lv rtbl :: logic_val rgrp :: logic_lv tcbcur :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s :: nil |] **
[| nth_val 0 vl = Some (Vptr qid) /\ (exists p,V_OSTCBPrio tcbcur = Some (Vint32 p) /\ Int.eq p ($ OS_IDLE_PRIO) = false) |].
Theorem OS_EventTaskWaitPreGood (vl:vallist) ll:
GoodFunAsrt (OS_EventTaskWaitPre´ vl ll).
Definition OS_EventTaskWaitPre : fpre :=
fun vl => fun ll => mkfunasrt (OS_EventTaskWaitPreGood vl ll).
Definition OS_EventTaskWaitPost´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
(EX ct tcbcur rtbl rgrp qid osevent etbl d
tcbcur´ rtbl´ rgrp´ osevent´ etbl´
y bitx bity ry ey egrp s,
Aie false ** Ais nil ** Acs (true::nil) ** Aisr empisr **
GV OSTCBCur @ Tptr OS_TCB |-> (Vptr ct) **
node (Vptr ct) tcbcur´ OS_TCB **
AOSRdyTblGrp rtbl´ (Vint32 rgrp´) ** AEventNode (Vptr qid) osevent´ etbl´ d **
<||s||> **
[| logicl = logic_val (Vptr ct) :: logic_lv rtbl :: logic_val (Vint32 rgrp) :: logic_lv tcbcur :: logic_lv osevent ::
logic_lv etbl :: logic_leventd (d::nil) :: logic_code s :: nil |] **
[| nth_val 0 vl = Some (Vptr qid) |] **
[| tcbcur´ = update_nth_val 2 tcbcur (Vptr qid) /\
V_OSTCBY tcbcur = Some (Vint32 y) /\
V_OSTCBBitX tcbcur = Some (Vint32 bitx) /\
V_OSTCBBitY tcbcur = Some (Vint32 bity) /\
nth_val (nat_of_Z (Int.unsigned y)) rtbl = Some (Vint32 ry) /\
rtbl´ = update_nth_val (nat_of_Z (Int.unsigned y)) rtbl (Vint32 (Int.and ry (Int.not bitx))) /\
nth_val (nat_of_Z (Int.unsigned y)) etbl = Some (Vint32 ey) /\
etbl´ = update_nth_val (nat_of_Z (Int.unsigned y)) etbl (Vint32 (Int.or ey bitx)) /\
V_OSEventGrp osevent = Some (Vint32 egrp) /\
osevent´ = update_nth_val 1 osevent (Vint32 (Int.or egrp bity)) |]).
Theorem OS_EventTaskWaitPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_EventTaskWaitPost´ vl v ll).
Definition OS_EventTaskWaitPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_EventTaskWaitPostGood vl v ll).
Specification of internal function 'OS_Sched'
This function determines whether a task with higher priority
has been made ready to run, and do the context switch in such
a case.
pre condition
This function enters and exits critical region in its implementation code,
so we don't need to specify the resources used by it in the pre and post
conditions. The pre condition specifies that the high level code at this
point should be a schedule action.
Definition OS_SchedPre´ (vl:vallist) (logicl:list logicvar) :=
EX s, Aie true ** Ais nil ** Acs nil ** Aisr empisr **
<||isched;;s||> ** [|logicl = logic_code s :: nil|].
EX s, Aie true ** Ais nil ** Acs nil ** Aisr empisr **
<||isched;;s||> ** [|logicl = logic_code s :: nil|].
post condition
After the invocation, the high level schedule action has been consumed.
Definition OS_SchedPost´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX s, Aie true ** Ais nil ** Acs nil ** Aisr empisr **
<||s||> ** [|logicl = logic_code s :: nil|].
Theorem OS_SchedPreGood (vl:vallist) ll:
GoodFunAsrt (OS_SchedPre´ vl ll).
Theorem OS_SchedPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_SchedPost´ vl v ll).
Definition OS_SchedPre : fpre :=
fun vl=> fun ll => mkfunasrt (OS_SchedPreGood vl ll).
Definition OS_SchedPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_SchedPostGood vl v ll).
EX s, Aie true ** Ais nil ** Acs nil ** Aisr empisr **
<||s||> ** [|logicl = logic_code s :: nil|].
Theorem OS_SchedPreGood (vl:vallist) ll:
GoodFunAsrt (OS_SchedPre´ vl ll).
Theorem OS_SchedPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OS_SchedPost´ vl v ll).
Definition OS_SchedPre : fpre :=
fun vl=> fun ll => mkfunasrt (OS_SchedPreGood vl ll).
Definition OS_SchedPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OS_SchedPostGood vl v ll).
Specification for internal function 'OSIntExit'
This function is used to notify uC/OS-II that you have completed
serving an ISR. When the last nested ISR has completed, uC/OS-II
will call the scheduler to determine whether a new, high-priority
task, is ready to run.
Definition fx is (O : osabst) := is_nest is = false.
Definition nfx is (O : osabst) := is_nest is = true.
Definition OSIntExitPre´ (vl:vallist) (logicl:list logicvar):=
EX ir ie si i, [|logicl= (logic_isr ir) :: (logic_ie ie) ::
(logic_is si) :: (logic_hid i) :: nil |] ** Aisr (isrupd ir i%nat false) **
Aie ie **
Ais (i%nat :: si) **
Acs nil ** <|| (isched;; END None ?? END None)||> **
[| isr_is_prop (isrupd ir i%nat false) (i%nat :: si) |] **
[| (i <= INUM)%nat /\ (forall j : nat, (0 <= j < i)%nat -> (isrupd ir i%nat false) j = false) |] **
((
(EX (eventl osql qblkl : list vallist) (msgql : list EventData)
(ectrl : list EventCtr) (ptbl : vallist) (p1 p2 : val)
(tcbl1 : list vallist) (tcbcur : vallist) (tcbl2 : list vallist)
(rtbl : vallist) (rgrp : val) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (t : int32) (ct : addrval) pf lf vhold,
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 pf lf **
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|] ) ** invlth_isr´ I 1%nat i%nat ** [| ie = false |])\\//[|ie=true|]).
Definition OSIntExitPost´ (vl:vallist) (v:option val) (logicl:list logicvar):=
EX ir ie si i, [|logicl= (logic_isr ir) :: (logic_ie ie)
:: (logic_is si) :: (logic_hid i) ::nil |] ** Aisr (isrupd ir i%nat false)**
Aie ie **
Ais (i%nat :: si) **
Acs nil ** <||END None||> **
[| isr_is_prop (isrupd ir i%nat false) (i%nat :: si) |] **
[| (i<=INUM)%nat |] **
((
(EX (eventl osql qblkl : list vallist) (msgql : list EventData)
(ectrl : list EventCtr) (ptbl : vallist) (p1 p2 : val)
(tcbl1 : list vallist) (tcbcur : vallist) (tcbl2 : list vallist)
(rtbl : vallist) (rgrp : val) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (t : int32) (ct : addrval) pf lf vhold,
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 pf lf **
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|] ) ** invlth_isr´ I 1%nat i%nat ** [| ie = false |]) \\// [|ie = true |]).
Theorem OSIntExitPreGood (vl:vallist) ll:
GoodFunAsrt (OSIntExitPre´ vl ll).
Theorem OSIntExitPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OSIntExitPost´ vl v ll).
Definition OSIntExitPre : fpre :=
fun vl=> fun ll => mkfunasrt (OSIntExitPreGood vl ll).
Definition OSIntExitPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OSIntExitPostGood vl v ll).
Open Scope code_scope.
Definition OSTimeTickPre´ (vl:vallist) (logicl:list logicvar):=
EX isrr si v´5 v´6 v´7, EX v´8 v´9 v´10 v´11 v´14 v´17 v´18 tcbls tcbls1 tcbls2 v´3 v´2 v´12 v´15 s,
[|logicl = (logic_isr isrr) :: (logic_is si) ::
logic_val (Vint32 v´14) :: (logic_val (Vptr v´5)) ::
(logic_val v´6) :: (logic_val (Vptr v´5)) :: (logic_llv v´7) ::
(logic_lv v´8) :: (logic_llv v´9) :: (logic_lv v´10) :: (logic_val v´11) ::
(logic_val v´17) :: (logic_val v´18) :: (logic_abstcb tcbls) ::
(logic_abstcb tcbls1) :: (logic_abstcb tcbls2) :: (logic_leventc v´3) :: (logic_leventd v´2) ::
(logic_absecb v´12):: logic_code s :: nil|] **
Aisr (isrupd isrr 0%nat false) **
Aie false **
Ais (0%nat :: si) **
Acs nil **
<||s||> **
GV OSTCBList @ OS_TCB ∗ |-> (Vptr v´5) **
tcbdllseg (Vptr v´5) Vnull v´17 v´6 v´7 **
GV OSTCBCur @ OS_TCB ∗ |-> v´6 **
tcbdllseg v´6 v´17 v´18 Vnull (v´8 :: v´9) **
[|TcbMod.join tcbls1 tcbls2 tcbls|] **
[|TCBList_P (Vptr v´5) v´7 v´10 tcbls1|] ** [|TCBList_P v´6 (v´8::v´9) v´10 tcbls2|] **
AOSRdyTblGrp v´10 v´11 **
GV OSTime @ Int32u |-> (Vint32 v´14)**
AECBList v´3 v´2 v´12 tcbls **
[| RH_TCBList_ECBList_P v´12 tcbls v´15 |].
Definition tmdly_sub_1 (vl:vallist):=
match nth_val 4%nat vl with
| Some (Vint32 v) => Some (update_nth_val 5%nat vl (Vint32 (Int.sub v Int.one)))
| _ => None
end.
Definition set_rdy_grp tcbbity rgrp := bop_eval rgrp tcbbity Tint8 Tint8 obitor.
Definition nth_val_vallist tcby rtbl:=
match tcby with
| Vint32 v => nth_val (Z.to_nat (Int.unsigned v)) rtbl
| _ => None
end.
Definition set_rdy_tbl tcbbitx tcby rtbl:=
match tcby with
| Vint32 vi =>
match nth_val (Z.to_nat (Int.unsigned vi)) rtbl with
| Some v => match bop_eval v tcbbitx Tint8 Tint8 obitor with
| Some v´ => Some (update_nth_val (Z.to_nat (Int.unsigned vi)) rtbl v´)
| None => None
end
| None => None
end
| _ => None
end.
Definition add_option_first (vl:vallist) (tri: option ((list vallist)*vallist*val*(list EventCtr))):=
match tri with
| Some (a,b,c,d) => Some (vl::a,b,c,d)
| _ => None
end.
Definition set_rdy (vl:vallist):=
update_nth_val 3%nat (update_nth_val 6%nat vl (Vint32 (Int.repr OS_STAT_RDY))) Vnull.
Definition beq_addrval :=
fun n m : addrval =>
let (b, i) := n in let (b´, i´) := m in beq_pos b b´ && Int.eq i i´.
Definition rdy_ectr (vl:vallist) (ectr:EventCtr) :option EventCtr:=
match ectr with
| (v1::Vint32 v2::v3::v4::v5::v6::nil,etbl) =>
match V_OSTCBY vl, (V_OSTCBBitX vl), (V_OSTCBBitY vl) with
| Some (Vint32 y),Some (Vint32 bitx),Some (Vint32 bity) =>
match nth_val´ (Z.to_nat (Int.unsigned y)) etbl with
| Vint32 xx =>
match Int.eq (xx&Int.not bitx) ($ 0) with
| true => Some (v1::Vint32 (v2&Int.not bity)::v3::v4::v5::v6::nil,
update_nth_val (Z.to_nat (Int.unsigned y)) etbl (Vint32 (xx&Int.not bitx)))
| false => Some (v1::Vint32 v2::v3::v4::v5::v6::nil,
update_nth_val (Z.to_nat (Int.unsigned y)) etbl (Vint32 (xx&Int.not bitx)))
end
| _ => None
end
| _,_,_ => None
end
| _ => None
end.
Fixpoint tick_rdy_ectr´ (e:addrval) (vl:vallist) (head:val) (ectrl:list EventCtr) :=
match head with
| (Vptr e´) =>
match ectrl with
|(osevent, etbl)::vll =>
match beq_addrval e e´ with
| true => match (rdy_ectr vl (osevent, etbl)) with
| Some x => Some (x :: vll)
| None => None
end
| false => match V_OSEventListPtr osevent with
| Some vn => match (tick_rdy_ectr´ e vl vn vll) with
| Some x => Some ((osevent, etbl)::x)
| None => None
end
| _ => None
end
end
| _ => Some ectrl
end
| Vnull => Some ectrl
| _=> None
end.
Definition tick_rdy_ectr (vl:vallist) (head:val) (ectrl:list EventCtr) :=
match nth_val 2%nat vl with
| Some (Vptr eid) => tick_rdy_ectr´ eid vl head ectrl
| Some (Vnull) => Some ectrl
| _ => None
end.
Fixpoint tcbls_rtbl_timetci_update (vll:list vallist) (rtbl:vallist) (rgrp:val) (head:val) (ectrl:list EventCtr) :=
match vll with
| nil => Some ((nil:list vallist),rtbl,rgrp,ectrl)
| vl::vll´ =>
match vl with
| (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) =>
match Int.eq vdly Int.zero with
| true => add_option_first vl (tcbls_rtbl_timetci_update vll´ rtbl rgrp head ectrl)
| false =>
match Int.eq (Int.sub vdly Int.one) Int.zero with
| true =>
match set_rdy_grp (Vint32 vbity) rgrp with
| Some (Vint32 rgrp´) =>
match set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl with
| Some rtbl´ =>
match eid with
| Vnull =>
add_option_first
(vnext :: vprev ::
eid :: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl´ (Vint32 rgrp´) head ectrl)
| Vptr eptr =>
match (tick_rdy_ectr vl head ectrl) with
| Some x => add_option_first
(vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl´ (Vint32 rgrp´) head x)
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| false => add_option_first
(vnext :: vprev ::
eid :: msg :: Vint32 (Int.sub vdly Int.one) ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl rgrp head ectrl)
end
end
| _ => None
end
end.
Inductive tickchange_l: vallist -> vallist -> val -> val -> list EventCtr -> vallist -> vallist -> val -> list EventCtr -> Prop:=
| rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity l rtbl rgrp head ectr,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = true ->
tickchange_l l rtbl rgrp head ectr l rtbl rgrp ectr
| wait_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity l l´ rtbl rgrp head ectr,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = false ->
l´ = (vnext :: vprev ::
eid:: msg :: Vint32 (Int.sub vdly Int.one) ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)->
tickchange_l l rtbl rgrp head ectr l´ rtbl rgrp ectr
| wait_rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity
l l´ rtbl rgrp head ectr rgrp´ rtbl´,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = true ->
l´ = (vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
eid = Vnull ->
set_rdy_grp (Vint32 vbity) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl = Some rtbl´ ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr
| waite_rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity
l l´ rtbl rgrp head ectr rgrp´ rtbl´ eptr ectr´,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = true ->
l´ = (vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
eid = Vptr eptr ->
set_rdy_grp (Vint32 vbity) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl = Some rtbl´ ->
tick_rdy_ectr l head ectr = Some ectr´ ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´.
Inductive tickstep_l: list vallist -> vallist -> val -> val -> list EventCtr -> list vallist -> vallist -> val -> list EventCtr -> Prop :=
| emp_update: forall rtbl rgrp head ectr,
tickstep_l nil rtbl rgrp head ectr nil rtbl rgrp ectr
| tl_update: forall l ll rtbl rgrp head ectr l´ ll´ rtbl´ rgrp´ ectr´ rtbl´´ rgrp´´ ectr´´,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
tickstep_l ll rtbl´ rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´ ->
tickstep_l (l::ll) rtbl rgrp head ectr (l´::ll´) rtbl´´ rgrp´´ ectr´´.
Definition OSTimeTickPost´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX isrr si v´5 v´6 v´7, EX v´8 v´9 v´10 v´11 v´14 v´17 v´18 rtbl´ rgrp´ v´15 tcbls tcbls1 tcbls2 i v´20 v´3 v´2 ectrl´ v´12 s,
[|logicl = (logic_isr isrr) :: (logic_is si) :: (logic_val (Vint32 v´14)) ::
(logic_val (Vptr v´5)) :: (logic_val v´6) :: (logic_val (Vptr v´5)) ::
(logic_llv v´7) :: (logic_lv v´8) :: (logic_llv v´9) :: (logic_lv v´10) ::
(logic_val v´11) :: (logic_val v´17) :: (logic_val v´18) :: (logic_abstcb tcbls) ::
(logic_abstcb tcbls1) :: (logic_abstcb tcbls2) :: (logic_leventc v´3) :: (logic_leventd v´2) ::
(logic_absecb v´12)::logic_code s :: nil|] **
[| array_type_vallist_match Int8u v´10|] **
[| length v´10 = ∘OS_RDY_TBL_SIZE |] **
[| v´11 = Vint32 i|] ** [| Int.unsigned i <= 255 |] **
[| RL_Tbl_Grp_P v´10 v´11 |] **
[| v´7 = nil /\ v´6 = Vptr v´5 \/
(exists vl, v´7 <> nil /\ last v´7 nil = vl /\ nth_val 0 vl = Some v´6) |] **
Aisr (isrupd isrr 0%nat false) **
Aie false **
Ais (0%nat :: si) **
Acs nil **
<||s||> **
GV OSTCBList @ OS_TCB ∗ |-> (Vptr v´5) **
GV OSEventList @ OS_EVENT ∗ |-> v´20 **
evsllseg v´20 Vnull ectrl´ v´2 **
tcbdllseg (Vptr v´5) Vnull v´18 Vnull v´15 **
[|TcbMod.join tcbls1 tcbls2 tcbls|] **
[|TCBList_P (Vptr v´5) v´7 v´10 tcbls1|] ** [|TCBList_P v´6 (v´8::v´9) v´10 tcbls2|] **
[|ECBList_P v´20 Vnull v´3 v´2 v´12 tcbls|] **
GV OSTCBCur @ OS_TCB ∗ |-> v´6 **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl´ **
GV OSRdyGrp @ Int8u |-> rgrp´ **
GV OSTime @ Int32u |-> Vint32 (Int.add v´14 Int.one) **
[| tcbls_rtbl_timetci_update (v´7++(v´8::v´9)) v´10 v´11 v´20 v´3= Some (v´15,rtbl´,rgrp´,ectrl´)|] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl´|]
.
Theorem OSTimeTickPreGood (vl:vallist) ll:
GoodFunAsrt (OSTimeTickPre´ vl ll).
Theorem OSTimeTickPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OSTimeTickPost´ vl v ll).
Definition OSTimeTickPre : fpre :=
fun vl ll=> mkfunasrt (OSTimeTickPreGood vl ll).
Definition OSTimeTickPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OSTimeTickPostGood vl v ll).
Open Scope list_scope.
Definition OS_Sched_spec : fspec:= (OS_SchedPre,OS_SchedPost,(Tvoid,nil)).
Definition OSIntExit_spec : fspec:= (OSIntExitPre,OSIntExitPost,(Tvoid,nil)).
Definition OSTimeTick_spec : fspec:= (OSTimeTickPre,OSTimeTickPost,(Tvoid,nil)).
Definition OS_EventSearch_spec : fspec :=(OS_EventSearchPre, OS_EventSearchPost, (Tint8, (Tptr OS_EVENT) :: nil)).
Definition OS_EventRemove_spec : fspec :=(OS_EventRemovePre, OS_EventRemovePost, (Tvoid, (Tptr OS_EVENT) :: nil)).
Definition OS_EventTaskRdy_spec : fspec :=(OS_EventTaskRdyPre, OS_EventTaskRdyPost, (Tint8, (Tptr OS_EVENT) :: (Tptr Tvoid) :: Tint8 :: nil)).
Definition OS_EventTaskWait_spec : fspec :=(OS_EventTaskWaitPre, OS_EventTaskWaitPost, (Tvoid, (Tptr OS_EVENT) :: nil)).
Definition OS_EventWaitListInit_spec : fspec :=
(OS_EventWaitListInitPre, OS_EventWaitListInitPost,
(Tvoid, (Tptr OS_EVENT)::nil)).
Definition osq_spec_list :=
(OS_EventSearch, OS_EventSearch_spec) ::
(OS_EventRemove, OS_EventRemove_spec) ::
(OS_EventTaskRdy, OS_EventTaskRdy_spec) ::
(OS_EventTaskWait, OS_EventTaskWait_spec) ::
(OS_Sched, OS_Sched_spec) ::
(OSIntExit, OSIntExit_spec) ::
(OSTimeTick, OSTimeTick_spec)::
(OS_EventWaitListInit,OS_EventWaitListInit_spec) ::
nil.
Fixpoint convert_spec (ls : list (fid * fspec)) : fid -> option fspec :=
match ls with
| nil => fun _ => None
| (id,spec) :: ls´ =>
fun (id´ : fid) =>
if Zeq_bool id id´ then
Some spec else convert_spec ls´ id´
end.
Definition OSQ_spec := convert_spec osq_spec_list.
Close Scope list_scope.
Definition nfx is (O : osabst) := is_nest is = true.
Definition OSIntExitPre´ (vl:vallist) (logicl:list logicvar):=
EX ir ie si i, [|logicl= (logic_isr ir) :: (logic_ie ie) ::
(logic_is si) :: (logic_hid i) :: nil |] ** Aisr (isrupd ir i%nat false) **
Aie ie **
Ais (i%nat :: si) **
Acs nil ** <|| (isched;; END None ?? END None)||> **
[| isr_is_prop (isrupd ir i%nat false) (i%nat :: si) |] **
[| (i <= INUM)%nat /\ (forall j : nat, (0 <= j < i)%nat -> (isrupd ir i%nat false) j = false) |] **
((
(EX (eventl osql qblkl : list vallist) (msgql : list EventData)
(ectrl : list EventCtr) (ptbl : vallist) (p1 p2 : val)
(tcbl1 : list vallist) (tcbcur : vallist) (tcbl2 : list vallist)
(rtbl : vallist) (rgrp : val) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (t : int32) (ct : addrval) pf lf vhold,
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 pf lf **
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|] ) ** invlth_isr´ I 1%nat i%nat ** [| ie = false |])\\//[|ie=true|]).
Definition OSIntExitPost´ (vl:vallist) (v:option val) (logicl:list logicvar):=
EX ir ie si i, [|logicl= (logic_isr ir) :: (logic_ie ie)
:: (logic_is si) :: (logic_hid i) ::nil |] ** Aisr (isrupd ir i%nat false)**
Aie ie **
Ais (i%nat :: si) **
Acs nil ** <||END None||> **
[| isr_is_prop (isrupd ir i%nat false) (i%nat :: si) |] **
[| (i<=INUM)%nat |] **
((
(EX (eventl osql qblkl : list vallist) (msgql : list EventData)
(ectrl : list EventCtr) (ptbl : vallist) (p1 p2 : val)
(tcbl1 : list vallist) (tcbcur : vallist) (tcbl2 : list vallist)
(rtbl : vallist) (rgrp : val) (ecbls : EcbMod.map)
(tcbls : TcbMod.map) (t : int32) (ct : addrval) pf lf vhold,
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 pf lf **
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|] ) ** invlth_isr´ I 1%nat i%nat ** [| ie = false |]) \\// [|ie = true |]).
Theorem OSIntExitPreGood (vl:vallist) ll:
GoodFunAsrt (OSIntExitPre´ vl ll).
Theorem OSIntExitPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OSIntExitPost´ vl v ll).
Definition OSIntExitPre : fpre :=
fun vl=> fun ll => mkfunasrt (OSIntExitPreGood vl ll).
Definition OSIntExitPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OSIntExitPostGood vl v ll).
Open Scope code_scope.
Definition OSTimeTickPre´ (vl:vallist) (logicl:list logicvar):=
EX isrr si v´5 v´6 v´7, EX v´8 v´9 v´10 v´11 v´14 v´17 v´18 tcbls tcbls1 tcbls2 v´3 v´2 v´12 v´15 s,
[|logicl = (logic_isr isrr) :: (logic_is si) ::
logic_val (Vint32 v´14) :: (logic_val (Vptr v´5)) ::
(logic_val v´6) :: (logic_val (Vptr v´5)) :: (logic_llv v´7) ::
(logic_lv v´8) :: (logic_llv v´9) :: (logic_lv v´10) :: (logic_val v´11) ::
(logic_val v´17) :: (logic_val v´18) :: (logic_abstcb tcbls) ::
(logic_abstcb tcbls1) :: (logic_abstcb tcbls2) :: (logic_leventc v´3) :: (logic_leventd v´2) ::
(logic_absecb v´12):: logic_code s :: nil|] **
Aisr (isrupd isrr 0%nat false) **
Aie false **
Ais (0%nat :: si) **
Acs nil **
<||s||> **
GV OSTCBList @ OS_TCB ∗ |-> (Vptr v´5) **
tcbdllseg (Vptr v´5) Vnull v´17 v´6 v´7 **
GV OSTCBCur @ OS_TCB ∗ |-> v´6 **
tcbdllseg v´6 v´17 v´18 Vnull (v´8 :: v´9) **
[|TcbMod.join tcbls1 tcbls2 tcbls|] **
[|TCBList_P (Vptr v´5) v´7 v´10 tcbls1|] ** [|TCBList_P v´6 (v´8::v´9) v´10 tcbls2|] **
AOSRdyTblGrp v´10 v´11 **
GV OSTime @ Int32u |-> (Vint32 v´14)**
AECBList v´3 v´2 v´12 tcbls **
[| RH_TCBList_ECBList_P v´12 tcbls v´15 |].
Definition tmdly_sub_1 (vl:vallist):=
match nth_val 4%nat vl with
| Some (Vint32 v) => Some (update_nth_val 5%nat vl (Vint32 (Int.sub v Int.one)))
| _ => None
end.
Definition set_rdy_grp tcbbity rgrp := bop_eval rgrp tcbbity Tint8 Tint8 obitor.
Definition nth_val_vallist tcby rtbl:=
match tcby with
| Vint32 v => nth_val (Z.to_nat (Int.unsigned v)) rtbl
| _ => None
end.
Definition set_rdy_tbl tcbbitx tcby rtbl:=
match tcby with
| Vint32 vi =>
match nth_val (Z.to_nat (Int.unsigned vi)) rtbl with
| Some v => match bop_eval v tcbbitx Tint8 Tint8 obitor with
| Some v´ => Some (update_nth_val (Z.to_nat (Int.unsigned vi)) rtbl v´)
| None => None
end
| None => None
end
| _ => None
end.
Definition add_option_first (vl:vallist) (tri: option ((list vallist)*vallist*val*(list EventCtr))):=
match tri with
| Some (a,b,c,d) => Some (vl::a,b,c,d)
| _ => None
end.
Definition set_rdy (vl:vallist):=
update_nth_val 3%nat (update_nth_val 6%nat vl (Vint32 (Int.repr OS_STAT_RDY))) Vnull.
Definition beq_addrval :=
fun n m : addrval =>
let (b, i) := n in let (b´, i´) := m in beq_pos b b´ && Int.eq i i´.
Definition rdy_ectr (vl:vallist) (ectr:EventCtr) :option EventCtr:=
match ectr with
| (v1::Vint32 v2::v3::v4::v5::v6::nil,etbl) =>
match V_OSTCBY vl, (V_OSTCBBitX vl), (V_OSTCBBitY vl) with
| Some (Vint32 y),Some (Vint32 bitx),Some (Vint32 bity) =>
match nth_val´ (Z.to_nat (Int.unsigned y)) etbl with
| Vint32 xx =>
match Int.eq (xx&Int.not bitx) ($ 0) with
| true => Some (v1::Vint32 (v2&Int.not bity)::v3::v4::v5::v6::nil,
update_nth_val (Z.to_nat (Int.unsigned y)) etbl (Vint32 (xx&Int.not bitx)))
| false => Some (v1::Vint32 v2::v3::v4::v5::v6::nil,
update_nth_val (Z.to_nat (Int.unsigned y)) etbl (Vint32 (xx&Int.not bitx)))
end
| _ => None
end
| _,_,_ => None
end
| _ => None
end.
Fixpoint tick_rdy_ectr´ (e:addrval) (vl:vallist) (head:val) (ectrl:list EventCtr) :=
match head with
| (Vptr e´) =>
match ectrl with
|(osevent, etbl)::vll =>
match beq_addrval e e´ with
| true => match (rdy_ectr vl (osevent, etbl)) with
| Some x => Some (x :: vll)
| None => None
end
| false => match V_OSEventListPtr osevent with
| Some vn => match (tick_rdy_ectr´ e vl vn vll) with
| Some x => Some ((osevent, etbl)::x)
| None => None
end
| _ => None
end
end
| _ => Some ectrl
end
| Vnull => Some ectrl
| _=> None
end.
Definition tick_rdy_ectr (vl:vallist) (head:val) (ectrl:list EventCtr) :=
match nth_val 2%nat vl with
| Some (Vptr eid) => tick_rdy_ectr´ eid vl head ectrl
| Some (Vnull) => Some ectrl
| _ => None
end.
Fixpoint tcbls_rtbl_timetci_update (vll:list vallist) (rtbl:vallist) (rgrp:val) (head:val) (ectrl:list EventCtr) :=
match vll with
| nil => Some ((nil:list vallist),rtbl,rgrp,ectrl)
| vl::vll´ =>
match vl with
| (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) =>
match Int.eq vdly Int.zero with
| true => add_option_first vl (tcbls_rtbl_timetci_update vll´ rtbl rgrp head ectrl)
| false =>
match Int.eq (Int.sub vdly Int.one) Int.zero with
| true =>
match set_rdy_grp (Vint32 vbity) rgrp with
| Some (Vint32 rgrp´) =>
match set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl with
| Some rtbl´ =>
match eid with
| Vnull =>
add_option_first
(vnext :: vprev ::
eid :: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl´ (Vint32 rgrp´) head ectrl)
| Vptr eptr =>
match (tick_rdy_ectr vl head ectrl) with
| Some x => add_option_first
(vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl´ (Vint32 rgrp´) head x)
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| false => add_option_first
(vnext :: vprev ::
eid :: msg :: Vint32 (Int.sub vdly Int.one) ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)
(tcbls_rtbl_timetci_update vll´ rtbl rgrp head ectrl)
end
end
| _ => None
end
end.
Inductive tickchange_l: vallist -> vallist -> val -> val -> list EventCtr -> vallist -> vallist -> val -> list EventCtr -> Prop:=
| rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity l rtbl rgrp head ectr,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = true ->
tickchange_l l rtbl rgrp head ectr l rtbl rgrp ectr
| wait_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity l l´ rtbl rgrp head ectr,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = false ->
l´ = (vnext :: vprev ::
eid:: msg :: Vint32 (Int.sub vdly Int.one) ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil)->
tickchange_l l rtbl rgrp head ectr l´ rtbl rgrp ectr
| wait_rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity
l l´ rtbl rgrp head ectr rgrp´ rtbl´,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = true ->
l´ = (vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
eid = Vnull ->
set_rdy_grp (Vint32 vbity) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl = Some rtbl´ ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr
| waite_rdy_change_l: forall vnext vprev eid msg vdly stat prio vx vy vbitx vbity
l l´ rtbl rgrp head ectr rgrp´ rtbl´ eptr ectr´,
l = (vnext :: vprev ::
eid :: msg :: Vint32 vdly ::
stat :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
Int.eq vdly Int.zero = false ->
Int.eq (Int.sub vdly Int.one) Int.zero = true ->
l´ = (vnext :: vprev ::
Vnull:: msg :: Vint32 (Int.sub vdly Int.one) ::
(Vint32 (Int.repr OS_STAT_RDY)) :: (Vint32 prio) ::
(Vint32 vx) :: (Vint32 vy) ::
(Vint32 vbitx) :: (Vint32 vbity) :: nil) ->
eid = Vptr eptr ->
set_rdy_grp (Vint32 vbity) rgrp = Some rgrp´ ->
set_rdy_tbl (Vint32 vbitx) (Vint32 vy) rtbl = Some rtbl´ ->
tick_rdy_ectr l head ectr = Some ectr´ ->
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´.
Inductive tickstep_l: list vallist -> vallist -> val -> val -> list EventCtr -> list vallist -> vallist -> val -> list EventCtr -> Prop :=
| emp_update: forall rtbl rgrp head ectr,
tickstep_l nil rtbl rgrp head ectr nil rtbl rgrp ectr
| tl_update: forall l ll rtbl rgrp head ectr l´ ll´ rtbl´ rgrp´ ectr´ rtbl´´ rgrp´´ ectr´´,
tickchange_l l rtbl rgrp head ectr l´ rtbl´ rgrp´ ectr´ ->
tickstep_l ll rtbl´ rgrp´ head ectr´ ll´ rtbl´´ rgrp´´ ectr´´ ->
tickstep_l (l::ll) rtbl rgrp head ectr (l´::ll´) rtbl´´ rgrp´´ ectr´´.
Definition OSTimeTickPost´ (vl:vallist) (v:option val) (logicl:list logicvar) :=
EX isrr si v´5 v´6 v´7, EX v´8 v´9 v´10 v´11 v´14 v´17 v´18 rtbl´ rgrp´ v´15 tcbls tcbls1 tcbls2 i v´20 v´3 v´2 ectrl´ v´12 s,
[|logicl = (logic_isr isrr) :: (logic_is si) :: (logic_val (Vint32 v´14)) ::
(logic_val (Vptr v´5)) :: (logic_val v´6) :: (logic_val (Vptr v´5)) ::
(logic_llv v´7) :: (logic_lv v´8) :: (logic_llv v´9) :: (logic_lv v´10) ::
(logic_val v´11) :: (logic_val v´17) :: (logic_val v´18) :: (logic_abstcb tcbls) ::
(logic_abstcb tcbls1) :: (logic_abstcb tcbls2) :: (logic_leventc v´3) :: (logic_leventd v´2) ::
(logic_absecb v´12)::logic_code s :: nil|] **
[| array_type_vallist_match Int8u v´10|] **
[| length v´10 = ∘OS_RDY_TBL_SIZE |] **
[| v´11 = Vint32 i|] ** [| Int.unsigned i <= 255 |] **
[| RL_Tbl_Grp_P v´10 v´11 |] **
[| v´7 = nil /\ v´6 = Vptr v´5 \/
(exists vl, v´7 <> nil /\ last v´7 nil = vl /\ nth_val 0 vl = Some v´6) |] **
Aisr (isrupd isrr 0%nat false) **
Aie false **
Ais (0%nat :: si) **
Acs nil **
<||s||> **
GV OSTCBList @ OS_TCB ∗ |-> (Vptr v´5) **
GV OSEventList @ OS_EVENT ∗ |-> v´20 **
evsllseg v´20 Vnull ectrl´ v´2 **
tcbdllseg (Vptr v´5) Vnull v´18 Vnull v´15 **
[|TcbMod.join tcbls1 tcbls2 tcbls|] **
[|TCBList_P (Vptr v´5) v´7 v´10 tcbls1|] ** [|TCBList_P v´6 (v´8::v´9) v´10 tcbls2|] **
[|ECBList_P v´20 Vnull v´3 v´2 v´12 tcbls|] **
GV OSTCBCur @ OS_TCB ∗ |-> v´6 **
GAarray OSRdyTbl (Tarray Int8u ∘OS_RDY_TBL_SIZE) rtbl´ **
GV OSRdyGrp @ Int8u |-> rgrp´ **
GV OSTime @ Int32u |-> Vint32 (Int.add v´14 Int.one) **
[| tcbls_rtbl_timetci_update (v´7++(v´8::v´9)) v´10 v´11 v´20 v´3= Some (v´15,rtbl´,rgrp´,ectrl´)|] **
[| prio_in_tbl ($ OS_IDLE_PRIO) rtbl´|]
.
Theorem OSTimeTickPreGood (vl:vallist) ll:
GoodFunAsrt (OSTimeTickPre´ vl ll).
Theorem OSTimeTickPostGood (vl:vallist) (v:option val) ll:
GoodFunAsrt (OSTimeTickPost´ vl v ll).
Definition OSTimeTickPre : fpre :=
fun vl ll=> mkfunasrt (OSTimeTickPreGood vl ll).
Definition OSTimeTickPost : fpost :=
fun vl => fun v => fun ll => mkfunasrt (OSTimeTickPostGood vl v ll).
Open Scope list_scope.
Definition OS_Sched_spec : fspec:= (OS_SchedPre,OS_SchedPost,(Tvoid,nil)).
Definition OSIntExit_spec : fspec:= (OSIntExitPre,OSIntExitPost,(Tvoid,nil)).
Definition OSTimeTick_spec : fspec:= (OSTimeTickPre,OSTimeTickPost,(Tvoid,nil)).
Definition OS_EventSearch_spec : fspec :=(OS_EventSearchPre, OS_EventSearchPost, (Tint8, (Tptr OS_EVENT) :: nil)).
Definition OS_EventRemove_spec : fspec :=(OS_EventRemovePre, OS_EventRemovePost, (Tvoid, (Tptr OS_EVENT) :: nil)).
Definition OS_EventTaskRdy_spec : fspec :=(OS_EventTaskRdyPre, OS_EventTaskRdyPost, (Tint8, (Tptr OS_EVENT) :: (Tptr Tvoid) :: Tint8 :: nil)).
Definition OS_EventTaskWait_spec : fspec :=(OS_EventTaskWaitPre, OS_EventTaskWaitPost, (Tvoid, (Tptr OS_EVENT) :: nil)).
Definition OS_EventWaitListInit_spec : fspec :=
(OS_EventWaitListInitPre, OS_EventWaitListInitPost,
(Tvoid, (Tptr OS_EVENT)::nil)).
Definition osq_spec_list :=
(OS_EventSearch, OS_EventSearch_spec) ::
(OS_EventRemove, OS_EventRemove_spec) ::
(OS_EventTaskRdy, OS_EventTaskRdy_spec) ::
(OS_EventTaskWait, OS_EventTaskWait_spec) ::
(OS_Sched, OS_Sched_spec) ::
(OSIntExit, OSIntExit_spec) ::
(OSTimeTick, OSTimeTick_spec)::
(OS_EventWaitListInit,OS_EventWaitListInit_spec) ::
nil.
Fixpoint convert_spec (ls : list (fid * fspec)) : fid -> option fspec :=
match ls with
| nil => fun _ => None
| (id,spec) :: ls´ =>
fun (id´ : fid) =>
if Zeq_bool id id´ then
Some spec else convert_spec ls´ id´
end.
Definition OSQ_spec := convert_spec osq_spec_list.
Close Scope list_scope.