Library OSTCBInvDef


This file defines the specification for the key data structure OSTCBList in uC/OS-II, which is used to record the basic information of each task for controlling the tasks. The specification also spells out the relationships between the low-level concrete concrete datas and the high-level abstract datas.


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.

the operations for calculating the fields of nodes in TCBList.

Definition V_OSTCBNext (vl:vallist) := nth_val 0 vl.
Definition V_OSTCBPrev (vl:vallist) := nth_val 1 vl.
Definition V_OSTCBEventPtr (vl:vallist) := nth_val 2 vl.
Definition V_OSTCBMsg (vl:vallist) := nth_val 3 vl.
Definition V_OSTCBDly (vl:vallist) := nth_val 4 vl.
Definition V_OSTCBStat (vl:vallist) := nth_val 5 vl.
Definition V_OSTCBPrio (vl:vallist) := nth_val 6 vl.
Definition V_OSTCBX (vl:vallist) := nth_val 7 vl.
Definition V_OSTCBY (vl:vallist) := nth_val 8 vl.
Definition V_OSTCBBitX (vl:vallist) := nth_val 9 vl.
Definition V_OSTCBBitY (vl:vallist) := nth_val 10 vl.
Definition V_OSTCBMutexOwn (vl:vallist) := nth_val 11 vl.

Open Scope Z_scope.
Open Scope int_scope.

the following properties should hold for each TCB block: (1) the probity of each task should be in the range of 0,64) (2) prio & 7 = x (3) prio >> 3 = y (4) 1 << x = bitx (5) 1 << y = bity (6) the status of each task should be OS_STAT_RDY, OS_STAT_SEM, OS_STAT_Q, OS_STAT_MBOX, or OS_STAT_MUTEX.

Definition RL_TCBblk_P vl :=
  exists prio x y bitx bity stat,
    V_OSTCBPrio vl = Some (Vint32 prio) /\
    V_OSTCBX vl = Some (Vint32 x) /\ V_OSTCBY vl = Some (Vint32 y) /\
    V_OSTCBBitX vl = Some (Vint32 bitx) /\ V_OSTCBBitY vl = Some (Vint32 bity) /\
    V_OSTCBStat vl = Some (Vint32 stat) /\
    0 <= Int.unsigned prio < 64 /\
    prio & ($ 7) = x /\
    Int.shru prio ($ 3) = y /\
    ($ 1) << x = bitx /\ ($ 1) << y = bity /\
    (
      (stat = ($ OS_STAT_RDY) \/ stat = ($ OS_STAT_SEM) \/ stat = ($ OS_STAT_Q) \/
       stat = ($ OS_STAT_MBOX) \/ stat = ($ OS_STAT_MUTEX)) /\
      exists eptr, V_OSTCBEventPtr vl = Some eptr /\ (stat = ($ OS_STAT_RDY) -> eptr = Vnull)
    ) .

the low-level relation specifies that a task with a priority "prio" is in the ready table "tbl", which is a bitmap. If "prio_in_tbl prio tbl" holds then the task with the priority "prio" is ready.
Definition prio_in_tbl (prio:int32) (tbl:vallist) :=
  forall x y z,
    x = prio & ($ 7) -> y = Int.shru prio ($ 3) ->
    nth_val (nat_of_Z (Int.unsigned y)) tbl = Some (Vint32 z) ->
    z & (($ 1) << x) = (($ 1) << x).

If "prio_not_in_tbl prio tbl" holds then the task with the priority "prio" is not ready.
Definition prio_not_in_tbl (prio:int32) (tbl:vallist) :=
  forall x y z,
    x = prio & ($ 7) -> y = Int.shru prio ($ 3) ->
    nth_val (nat_of_Z (Int.unsigned y)) tbl = Some (Vint32 z) ->
    z & (($ 1) << x) = $ 0.

the task with the priority "prio" is ready
Definition RdyTCBblk vl rtbl (prio : priority) :=
  V_OSTCBPrio vl = Some (Vint32 prio) /\ prio_in_tbl prio rtbl .


the task is ready at the low level implies it is ready at the high level.
Definition RLH_RdyI_P vl rtbl abstcb:=
  forall prio , RdyTCBblk vl rtbl prio ->
                V_OSTCBStat vl = Some (V$ OS_STAT_RDY) /\
                V_OSTCBDly vl = Some (V$ 0) /\
                exists (m:msg), abstcb = (prio,rdy,m).

the task is ready at the high level implies it is ready at the low level.
Definition RHL_RdyI_P vl rtbl abstcb :=
  forall prio (m:msg), abstcb = (prio,rdy,m)->
                (RdyTCBblk vl rtbl prio/\
                 V_OSTCBStat vl = Some (V$ OS_STAT_RDY)/\
                 V_OSTCBDly vl = Some (V$ 0)).

the task with the priority "prio" is waiting
Definition WaitTCBblk vl rtbl (prio : priority) t:=
  V_OSTCBPrio vl = Some (Vint32 prio) /\ prio_not_in_tbl prio rtbl /\
  V_OSTCBDly vl = Some (Vint32 t).

the task is delayed for the time "t" at the low level implies it is also delayed for "t" at the high level.
Definition RLH_Wait_P vl rtbl abstcb :=
  forall prio t, WaitTCBblk vl rtbl prio t ->
                  V_OSTCBStat vl = Some (V$ OS_STAT_RDY) ->
                  Int.ltu Int.zero t = true /\
                  exists (m:msg), abstcb = (prio,wait os_stat_time t,m).

the task is delayed for the time "t" at the high level implies it is also delayed for "t" at the low level.
Definition RHL_Wait_P vl rtbl abstcb :=
  forall prio t (m:msg), abstcb = (prio,wait os_stat_time t,m)->
                         WaitTCBblk vl rtbl prio t /\
                         Int.ltu Int.zero t = true /\
                         V_OSTCBStat vl = Some (V$ OS_STAT_RDY).

the task is waiting for the semaphore "eid" at the low level implies it is is waiting for the semaphore "eid" at the high level.
Definition RLH_WaitS_P vl rtbl abstcb :=
  forall prio t eid,
    WaitTCBblk vl rtbl prio t ->
    V_OSTCBStat vl = Some (V$ OS_STAT_SEM) ->
    V_OSTCBEventPtr vl = Some (Vptr eid) ->
    exists (m:msg), abstcb = (prio,(wait (os_stat_sem eid) t),m).

the task is waiting for the semaphore "eid" at the high level implies it is is waiting for the semaphore "eid" at the low level.
Definition RHL_WaitS_P vl rtbl abstcb :=
  forall prio eid t (m:msg), abstcb = (prio,wait (os_stat_sem eid) t,m)->
                             (WaitTCBblk vl rtbl prio t /\
                              V_OSTCBEventPtr vl = Some (Vptr eid)/\
                              V_OSTCBStat vl = Some (V$ OS_STAT_SEM)).

the task is waiting for the message queue "eid" at the low level implies it is is waiting for the message queue "eid" at the high level.
Definition RLH_WaitQ_P vl rtbl abstcb :=
  forall prio t eid,
    WaitTCBblk vl rtbl prio t ->
    V_OSTCBStat vl = Some (V$ OS_STAT_Q) ->
    V_OSTCBEventPtr vl = Some (Vptr eid) ->
    exists (m:msg), abstcb = (prio,wait (os_stat_q eid) t,m).

the task is waiting for the message queue "eid" at the high level implies it is is waiting for the message queue "eid" at the low level.
Definition RHL_WaitQ_P vl rtbl abstcb :=
  forall prio eid t (m:msg),
    abstcb = (prio,wait (os_stat_q eid) t,m)->
    (WaitTCBblk vl rtbl prio t /\
     V_OSTCBEventPtr vl = Some (Vptr eid)/\
     V_OSTCBStat vl = Some (V$ OS_STAT_Q)).


the similar relation when waiting for the mail box between the low level and the high level
Definition RLH_WaitMB_P vl rtbl abstcb :=
  forall prio t eid,
    WaitTCBblk vl rtbl prio t ->
    V_OSTCBStat vl = Some (V$ OS_STAT_MBOX) ->
    V_OSTCBEventPtr vl = Some (Vptr eid) ->
    exists (m:msg), abstcb = (prio,wait (os_stat_mbox eid) t,m).

Definition RHL_WaitMB_P vl rtbl abstcb :=
  forall prio eid t (m:msg),
    abstcb = (prio,wait (os_stat_mbox eid) t,m)->
    (WaitTCBblk vl rtbl prio t /\
     V_OSTCBEventPtr vl = Some (Vptr eid)/\
     V_OSTCBStat vl = Some (V$ OS_STAT_MBOX)).

the similar relation when waiting for the mutex between the low level and the high level
Definition RLH_WaitMS_P vl rtbl abstcb :=
  forall prio t eid,
    WaitTCBblk vl rtbl prio t ->
    V_OSTCBStat vl = Some (V$ OS_STAT_MUTEX) ->
    V_OSTCBEventPtr vl = Some (Vptr eid) ->
    exists (m:msg), abstcb = (prio,wait (os_stat_mutexsem eid) t,m).

Definition RHL_WaitMS_P vl rtbl abstcb :=
  forall prio eid t (m:msg),
    abstcb = (prio,wait (os_stat_mutexsem eid) t,m)->
    (WaitTCBblk vl rtbl prio t /\
     V_OSTCBEventPtr vl = Some (Vptr eid)/\
     V_OSTCBStat vl = Some (V$ OS_STAT_MUTEX)).

the relationship of TCB status between the low-level concrete TCB blocks and the high-level abstract TCBs.
Definition RLH_TCB_Status_Wait_P vl rtbl abstcb :=
  RLH_Wait_P vl rtbl abstcb /\
  RLH_WaitS_P vl rtbl abstcb /\
  RLH_WaitQ_P vl rtbl abstcb /\
  RLH_WaitMB_P vl rtbl abstcb /\
  RLH_WaitMS_P vl rtbl abstcb
.

Definition RHL_TCB_Status_Wait_P vl rtbl abstcb :=
  RHL_Wait_P vl rtbl abstcb /\
  RHL_WaitS_P vl rtbl abstcb /\
  RHL_WaitQ_P vl rtbl abstcb /\
  RHL_WaitMB_P vl rtbl abstcb /\
  RHL_WaitMS_P vl rtbl abstcb.

Definition R_TCB_Status_P vl rtbl abstcb :=
  RLH_RdyI_P vl rtbl abstcb /\
  RHL_RdyI_P vl rtbl abstcb /\
  RLH_TCB_Status_Wait_P vl rtbl abstcb /\
  RHL_TCB_Status_Wait_P vl rtbl abstcb.

the full proposition for specifying properties of TCB nodes
Definition TCBNode_P vl (rtbl : vallist) (abstcb:priority * taskstatus * msg):=
  match abstcb with
    |(p,st,m) =>
     V_OSTCBMsg vl = Some m /\ V_OSTCBPrio vl = Some (Vint32 p) /\
     RL_TCBblk_P vl /\ R_TCB_Status_P vl rtbl abstcb
  end.

Definition TcbJoin tid abstcb tcbls´ tcbls :=
  TcbMod.join (TcbMod.sig tid abstcb) tcbls´ tcbls.

the following assertion is used to specify the spatial parts of TCBList, which is a double linked list.
Definition tcbdllseg (head headprev tail tailnext : val) (l : list vallist) :=
               dllseg head headprev tail tailnext l OS_TCB V_OSTCBPrev V_OSTCBNext .

the pure proposition for TCBList, it specifies the relationship between the entire low-level concrete TCBList and the high-level abstract TCBList.
Fixpoint TCBList_P (v: val) (l:list vallist) (rtbl : vallist) (tcbls : TcbMod.map)
         {struct l} : Prop :=
  match l with
    | nil => tcbls =TcbMod.emp
    | vl :: l´ => exists tid v´ tcbls´ abstcb,
                      v = Vptr tid /\
                      V_OSTCBNext vl = Some v´ /\
                      TcbJoin tid abstcb tcbls´ tcbls/\
                      TCBNode_P vl rtbl abstcb /\
                      TCBList_P v´ l´ rtbl tcbls´
  end.

the full relational assertion for TCBList, which contains both the spatial part specified by the inductive predicate "tcbdllseg" and the pure proposition "TCBList_P". "OSTCBCur" points to the current TCB block
Definition AOSTCBList (p1 p2: val) (l1 l2:list vallist) (rtbl : vallist)
           (hcurt:addrval)(tcbls : TcbMod.map) :=
  EX tail1 tail2 tcbls1 tcbls2,
  (GV OSTCBList @ (Tptr OS_TCB) |-> p1) **
                                        tcbdllseg p1 Vnull tail1 p2 l1 **
                                        (GV OSTCBCur @ (Tptr OS_TCB) |-> p2) **
                                        tcbdllseg p2 tail1 tail2 Vnull l2 **
                                        [|p1 <> Vnull /\ p2 = Vptr hcurt|] **
                                        [|TcbMod.join tcbls1 tcbls2 tcbls|] **
                                        [| TCBList_P p1 l1 rtbl tcbls1 |]**
                                        [| TCBList_P p2 l2 rtbl tcbls2 |].

the following assertion specifies the single linked list pointed by the global variable "OSTCBFreeList" The list is used to store the free TCB blocks for the task creation.
Definition AOSTCBFreeList (p:val) (l:list vallist) :=
  (GV OSTCBFreeList @ (Tptr OS_TCB) |-> p) ** sll p l OS_TCB V_OSTCBNext.

the assertion specifies the ready table, which is a 8*8 bitmap implemented with a length-8 array.
Definition AOSRdyTbl (vl:vallist) :=
  GAarray OSRdyTbl (Tarray Tint8 (nat_of_Z OS_RDY_TBL_SIZE)) vl
          ** [| array_type_vallist_match Tint8 vl /\ length vl = (nat_of_Z OS_RDY_TBL_SIZE)|].

the assertion specifies the ready group, which is implemented with a 8-bit integer. It is an auxiliary data structure used in uC/OS-II to accelerate the task scheduling.
Definition AOSRdyGrp (v:val) := GV OSRdyGrp @ Tint8 |-> v ** [| rule_type_val_match Tint8 v = true |].

the following two constant tables are used to calculate the task with the highest priority in the ready table.
Definition OSMapVallist :=
  V$1::V$2::V$4::V$8::V$16::V$32::V$64::V$128::nil.

Definition AOSMapTbl :=
  GAarray OSMapTbl (Tarray Tint8 8) OSMapVallist.

Definition OSUnMapVallist :=
  V$0::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$5::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$6::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$5::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$7::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$5::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$6::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$5::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::
   V$4::V$0::V$1::V$0::V$2::V$0::V$1::V$0::V$3::V$0::V$1::V$0::V$2::V$0::V$1::V$0::nil.

Definition AOSUnMapTbl :=
  GAarray OSUnMapTbl (Tarray Tint8 256) OSUnMapVallist.

the relation between the ready table "rtbl" and the priority table "ptbl". It says, if the priority "p" is in the ready table then we must be able to get a task with the priority "p" from the priority table. Here the priority table maps priorities to the corresponding tasks.
Definition RL_RTbl_PrioTbl_P rtbl ptbl vhold:=
  forall p,
    0 <= Int.unsigned p < 64 ->
    prio_in_tbl p rtbl ->
    exists tid,
      nth_val (Z.to_nat (Int.unsigned p)) ptbl = Some (Vptr tid) /\ tid <> vhold.

the predicate requires tasks should have different priorities.
Definition R_Prio_No_Dup (tcbls : TcbMod.map) :=
  forall tid tid´ prio st m prio´ st´ m´,
    tid <> tid´ ->
    TcbMod.get tcbls tid = Some (prio, st, m) ->
    TcbMod.get tcbls tid´ = Some (prio´,st´,m´) ->
    prio <> prio´.

the relationship between the low-level priority table and the high-level abstract TCBList.
Definition R_PrioTbl_P (ptbl : vallist) (tcbls : TcbMod.map) (vhold:addrval):=
  (forall prio tcbid,
     (0<=Int.unsigned prio<64) ->
     nth_val (nat_of_Z (Int.unsigned prio)) ptbl = Some (Vptr tcbid) ->
     tcbid <> vhold ->
     exists st m,TcbMod.get tcbls tcbid = Some (prio,st,m)) /\
  (forall tcbid prio st m,
     TcbMod.get tcbls tcbid = Some (prio,st,m) ->
     nth_val (nat_of_Z (Int.unsigned prio)) ptbl = Some (Vptr tcbid) /\ tcbid <> vhold) /\
  R_Prio_No_Dup tcbls.

the assertion for specifying the priority table, which is a length-64 array. It is indexed with the priority and maps priorities to pointers pointing to TCB blocks.

Definition AOSTCBPrioTbl (vl:vallist) (rtbl:vallist) (tcbls:TcbMod.map) (vhold:addrval):=
  GAarray OSTCBPrioTbl (Tarray (Tptr OS_TCB) 64) vl **
  (G& OSPlaceHolder @ Tint8 == vhold ** (EX v, Aptrmapsto vhold Tint8 v)) **
  [| array_type_vallist_match (Tptr OS_TCB) vl /\ length vl = 64%nat |] **
  [|RL_RTbl_PrioTbl_P rtbl vl vhold|] ** [| R_PrioTbl_P vl tcbls vhold|].

the global variable "OSTime"
Definition AOSTime (t:val) := GV OSTime @ Tint32 |-> t.

the global variable " OSIntNesting"
Definition AOSIntNesting := EX v,GV OSIntNesting @ Tint32 |-> Vint32 v.


Definition RL_Tbl_Grp_P (tbl:vallist) (grp:val):=
  (forall n v v´, (0<=n<8)%nat -> nth_val n tbl = Some (Vint32 v) -> grp = Vint32 v´ ->
                 ((v´ & (($ 1) << ($ (Z_of_nat n))) = $0 <-> v = $0) /\
                  (v´ & (($ 1) << ($ (Z_of_nat n))) = (($ 1) << ($ (Z_of_nat n))) <->
                   Int.ltu ($ 0) v = true ))) .

the assertion for specifying the ready table and the group table
Definition AOSRdyTblGrp (vl:vallist) (v:val) :=
  AOSRdyTbl vl ** AOSRdyGrp v ** [|RL_Tbl_Grp_P vl v /\ prio_in_tbl (Int.repr OS_IDLE_PRIO) vl|].

the assertion for specifying the high-level abstract TCBList
Notation HTCBList tcbls:= (Aabsdata abstcblsid (abstcblist tcbls)).

the assertion for specifying the high-level abstract time
Notation HTime t := (Aabsdata ostmid (ostm t)).

the assertion for specifying the current task identifier at the high level
Notation HCurTCB tid:= (Aabsdata curtid (oscurt tid)).

the assertion for specifying the high-level abstract ECBList
Notation HECBList ecbls:= (Aabsdata absecblsid (absecblist ecbls)).

the assertion for specifying the global variables
Definition AGVars:=
  (GV OSRunning @ (Tint8) |-> Vint32 (Int.repr 1))
    ** (EX v, GV OSPrioHighRdy @ (Tint8) |-> Vint32 v
                 ** [| Int.unsigned v <= 63 |])
    ** (EX v, GV OSCtxSwCtr @ (Tint32) |-> Vint32 v)
    ** (EX v,GV OSTCBHighRdy @ (Tptr OS_TCB) |-> Vptr v)
    ** (EX v, GV OSPrioCur @ (Tint8) |-> Vint32 v
                  ** [| Int.unsigned v <= 63 |])
    ** (EX v, GV OSIntExitY @ (Tint8) |-> Vint32 v).

Definition RH_CurTCB ct tcbls:= exists p st msg, TcbMod.get tcbls ct = Some (p,st,msg).

Close Scope int_scope.
Close Scope Z_scope.