Library pif_theory

Require Import include.
Require Import baseTac.
Require Import Classical.
Require Import ucert.

Definition priority := int32.

Parameter taskid: Type.

Parameter State : Type.

Parameter WaitRel: taskid -> taskid -> State -> Prop.

Parameter IsWt: taskid -> State -> Prop.

Parameter IsRdy: taskid -> State -> Prop.

Parameter CurPr: taskid -> State -> option priority.

Parameter OldPr: taskid -> State -> option priority.

Parameter IsOwner: taskid -> State -> Prop.

Definition PrioLt a b := Int.ltu a b = true.
Definition PrioLe a b := (Int.ltu a b = true \/ Int.eq a b = true).

Parameter IsCur: taskid -> State -> Prop.

Parameter TaskEx: taskid -> State -> Prop.

Inductive WaitChain: taskid -> taskid -> State -> Prop :=
| waitO : forall t t´ S, WaitRel t t´ S -> t <> t´ -> WaitChain t t´ S
| waitS : forall t t´ t´´ S,
            WaitRel t t´ S ->
            t <> t´ ->
            WaitChain t´ t´´ S ->
            WaitChain t t´´ S.

Definition PI S := exists t t´ p p´, WaitChain t t´ S /\ CurPr t S = Some p /\ CurPr t´ S = Some p´ /\ PrioLt p´ p.

Definition PIF S := ~ PI S.

Definition Preemptive S :=
  forall t p,
    IsCur t S ->
    CurPr t S = Some p ->
    IsRdy t S /\
    forall t´ p´, t´ <> t -> CurPr t´ S = Some p´ -> IsRdy t´ S -> PrioLe p´ p.

Definition NoDeadLock S := forall t, IsWt t S -> exists t´, WaitChain t t´ S /\ IsRdy t´ S.

Definition PrioLift S:= (forall t po p, OldPr t S = Some po -> CurPr t S = Some p -> PrioLe po p /\ ((~ IsOwner t S) -> po = p)).

Definition StatProp S:= forall t, TaskEx t S -> IsRdy t S \/ IsWt t S.

Definition AuxProps S:=
  (forall t, TaskEx t S -> exists p po, CurPr t S = Some p /\ OldPr t S = Some po) /\
  (forall t p, CurPr t S = Some p -> TaskEx t S) /\
  (forall t p, OldPr t S = Some p -> TaskEx t S) /\
  (forall t, IsRdy t S -> TaskEx t S).

Definition UPIF S:=
  forall t tc p pc,
    t <> tc ->
    IsCur tc S ->
    OldPr t S = Some p ->
    ~ IsOwner tc S ->
    IsWt t S ->
    OldPr tc S = Some pc ->
    PrioLe p pc.

Theorem rel_pif_upif:
  forall S,
    AuxProps S ->
    NoDeadLock S ->
    PrioLift S ->
    Preemptive S ->
    StatProp S ->
    PIF S ->
    UPIF S.