Library PIF_def

'WAIT_CHAIN' says that there exists a waiting chain between two tasks. 'IS_OWNER t _ _' means there exist semaphores owned by a task 't'. 'IS_OWNER_P t _ p' means there exist semaphores owned by a task 't' with priority 'p'. 'IS_WAITING t' means 't' is waiting for some resource. 'IS_WAINTG_E t eid ' means the 't' is waiting for the event 'eid'. 'NO_NEST_PENDING_O _ _' specifies no nested use of mutexes by requiring that an owner will not be waiting for a mutex semaphore or owns other mutex semaphore. 'HighestRdy _ t' means 't' is the highest ready task. 'init_st' means the initial high-level state. 'GET_OP' is a function to get the original priority.

'UPIF' is the our new definition for the unbounded priority-inversion-freedom, which means that if current task 't' is not a owner, and there exists a task 't' and a waiting chain between 't' and ' t' ', then ' t' ' must have a lower original priority (corresponding to Def. 5.1 in our paper).

Require Import lemmasfortoptheo.
Require Import ucert.
Require Import auxdef.
Require Import etraceref.

Definition WAIT_OWNER t t_owner tls els:=
  exists qid p v m p_owner wl p_q,
    TcbMod.get tls t = Some (p,wait (os_stat_mutexsem qid) v,m) /\
    EcbMod.get els qid = Some (absmutexsem p_q (Some (t_owner ,p_owner)),wl).

Inductive WAIT_CHAIN: tid -> tid -> TcbMod.map -> EcbMod.map -> Prop :=
| wait_O: forall t t_owner tls els, WAIT_OWNER t t_owner tls els /\ t <> t_owner ->
                     WAIT_CHAIN t t_owner tls els
| wait_S: forall t t_owner tls els t´, WAIT_OWNER t t´ tls els -> WAIT_CHAIN t´ t_owner tls els ->
                     WAIT_CHAIN t t_owner tls els.

Definition IS_OWNER t_owner qid els :=
  exists p_q p_owner wl, EcbMod.get els qid = Some (absmutexsem p_q (Some (t_owner ,p_owner)),wl).

Definition IS_OWNER_P t_owner qid els p_owner:=
  exists p_q wl, EcbMod.get els qid = Some (absmutexsem p_q (Some (t_owner ,p_owner )),wl).

Definition IS_WAITING t els:=
  exists qid p_q owner wl, EcbMod.get els qid = Some (absmutexsem p_q owner,wl) /\ In t wl.

Definition IS_WAITING_E t eid els:=
  exists p_q owner wl, EcbMod.get els eid = Some (absmutexsem p_q owner,wl) /\ In t wl.

Definition NO_NEST_PENDING tls els:=
  forall t qid,
    TcbMod.get tls t <> None ->
    IS_OWNER t qid els ->
    (~ IS_WAITING t els /\ ~ exists qid´, qid <> qid´ /\ IS_OWNER t qid´ els).

Definition NO_NEST_PENDING_O O:=
  forall els tls,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    NO_NEST_PENDING tls els.

Definition GET_OP t tls els p :=
  TcbMod.get tls t <> None ->
  (exists qid, IS_OWNER_P t qid els p ) \/
  ((~ exists qid, IS_OWNER t qid els ) /\ exists st msg, TcbMod.get tls t = Some (p ,st,msg)).

Definition HighestRdy tls t :=
  exists prio msg0,
    TcbMod.get tls t = Some (prio, rdy , msg0) /\
    (forall (i : tid) (prio´ : priority) (msg´ : msg),
       i <> t ->
       TcbMod.get tls i = Some (prio´, rdy , msg´) ->
       Int.ltu prio prio´ = true ).

Definition PREEMP O :=
  forall ct tls ,
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    OSAbstMod.get O curtid = Some (oscurt ct) ->
    HighestRdy tls ct.

Definition init_st O:=
  exists tls,
    OSAbstMod.get O absecblsid = Some (absecblist EcbMod.emp) /\
    OSAbstMod.get O abstcblsid = Some (abstcblist tls) /\
    forall t, exists p msg, TcbMod.get tls t = Some (p,rdy ,msg).

Definition PIF (O:osabst) :=
  forall els tls ct p_ct,
    OSAbstMod.get O absecblsid = Some (absecblist els) ->
    OSAbstMod.get O abtcblsid = Some (abstcblist tls) ->
    OSAbstMod.get O curtid = Some (oscurt ct) ->
    GET_OP ct tls els p_ct ->
    ~ (exists eid, IS_OWNER ct eid els ) ->
    forall t p_t,
      t <> ct ->
      TcbMod.get tls t <> None ->
      GET_OP t tls els p_t ->
      (exists t´, WAIT_CHAIN t t´ tls els) ->
      Int.ltu p_ct p_t = true \/ Int.eq p_ct p_t = true.