Library rt.model.priority

Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.

(* Definitions of FP, JLFP and JLDP priority relations. *)
Module Priority.

  Import SporadicTaskset ArrivalSequence.

  Section PriorityDefs.

    Variable Task: eqType.
    Variable Job: eqType.

    (* We define an FP policy as a relation between tasks, ... *)
    Definition FP_policy := rel Task.

    (* ...JLFP policy as a relation between jobs, ... *)
    Definition JLFP_policy := rel Job.

    (* ...and JLDP as any time-dependent relation between jobs. *)
    Definition JLDP_policy := time rel Job.

  End PriorityDefs.

  (* Since FP policies are also JLFP and JLDP policies, we define
     next conversion functions to do the generalization. *)

  Section Generalization.

    (* Consider any arrival sequence of jobs spawned by tasks. *)
    Context {Task: eqType}.
    Context {Job: eqType}.
    Variable job_task: Job Task.

    (* We show how to convert FP to JLFP,... *)
    Definition FP_to_JLFP (task_hp: FP_policy Task) :=
      fun (jhigh jlow: Job) ⇒
        task_hp (job_task jhigh) (job_task jlow).

    (* ...FP to JLDP, ... *)
    Definition FP_to_JLDP (task_hp: FP_policy Task) :=
      fun (t: time) ⇒ FP_to_JLFP task_hp.

    (* ...and JLFP to JLDP. *)
    Definition JLFP_to_JLDP (job_hp: JLFP_policy Job) :=
      fun (t: time) ⇒ job_hp.

  End Generalization.

  (* Next we define properties of an FP policy. *)
  Section PropertiesFP.

    (* Assume that jobs are spawned by tasks. *)
    Context {Job: eqType}.
    Context {Task: eqType}.
    Variable job_task: Job Task.

    (* Let task_priority be any FP policy. *)
    Variable task_priority: FP_policy Task.

    (* Now we define the properties. *)

    (* Whether the FP policy is reflexive. *)
    Definition FP_is_reflexive := reflexive task_priority.

    (* Whether the FP policy is irreflexive. *)
    Definition FP_is_irreflexive := irreflexive task_priority.

    (* Whether the FP policy is transitive. *)
    Definition FP_is_transitive := transitive task_priority.

    Section Antisymmetry.

      (* Consider any task set ts. *)
      Variable ts: seq Task.

      (* First we define whether task set ts is totally ordered with
         the priority. *)

      Definition FP_is_total_over_task_set :=
        total_over_list task_priority ts.

      (* Then we define whether an FP policy is antisymmetric over task set ts, i.e.,
         whether the task set has unique priorities. *)

      Definition FP_is_antisymmetric_over_task_set :=
        antisymmetric_over_list task_priority ts.

    End Antisymmetry.

  End PropertiesFP.

  (* Next, we define properties of a JLFP policy. *)
  Section PropertiesJLFP.

    (* Consider any JLFP policy. *)
    Context {Job: eqType}.
    Variable arr_seq: arrival_sequence Job.

    Variable job_priority: JLFP_policy Job.

    (* Now we define the properties. *)

    (* Whether the JLFP policy is reflexive. *)
    Definition JLFP_is_reflexive := reflexive job_priority.

    (* Whether the JLFP policy is irreflexive. *)
    Definition JLFP_is_irreflexive := irreflexive job_priority.

    (* Whether the JLFP policy is transitive. *)
    Definition JLFP_is_transitive := transitive job_priority.

    (* Whether the JLFP policy is total over the arrival sequence. *)
    Definition JLFP_is_total :=
       j1 j2,
        arrives_in arr_seq j1
        arrives_in arr_seq j2
        job_priority j1 j2 || job_priority j2 j1.

  End PropertiesJLFP.

  (* Next, we define properties of a JLDP policy. *)
  Section PropertiesJLDP.

    (* Consider any JLDP policy. *)
    Context {Job: eqType}.
    Variable arr_seq: arrival_sequence Job.

    Variable job_priority: JLDP_policy Job.

    (* Now we define the properties. *)

    (* Whether the JLDP policy is reflexive. *)
    Definition JLDP_is_reflexive :=
       t, reflexive (job_priority t).

    (* Whether the JLDP policy is irreflexive. *)
    Definition JLDP_is_irreflexive :=
       t, irreflexive (job_priority t).

    (* Whether the JLDP policy is transitive. *)
    Definition JLDP_is_transitive :=
       t, transitive (job_priority t).

    (* Whether the JLDP policy is total. *)
    Definition JLDP_is_total :=
       j1 j2 t,
        arrives_in arr_seq j1
        arrives_in arr_seq j2
        job_priority t j1 j2 || job_priority t j2 j1.

  End PropertiesJLDP.

  (* Next we define some known FP policies. *)
  Section KnownFPPolicies.

    Context {Job: eqType}.
    Context {Task: eqType}.
    Variable task_period: Task time.
    Variable task_deadline: Task time.
    Variable job_task: Job Task.

    (* Rate-monotonic orders tasks by smaller periods. *)
    Definition RM (tsk1 tsk2: Task) :=
      task_period tsk1 task_period tsk2.

    (* Deadline-monotonic orders tasks by smaller relative deadlines. *)
    Definition DM (tsk1 tsk2: Task) :=
      task_deadline tsk1 task_deadline tsk2.

    Section Properties.

      (* RM is reflexive. *)
      Lemma RM_is_reflexive : FP_is_reflexive RM.

      (* RM is transitive. *)
      Lemma RM_is_transitive : FP_is_transitive RM.

      (* DM is reflexive. *)
      Lemma DM_is_reflexive : FP_is_reflexive DM.

      (* DM is transitive. *)
      Lemma DM_is_transitive : FP_is_transitive DM.

    End Properties.

  End KnownFPPolicies.

  (* In this section, we define known JLFP policies. *)
  Section KnownJLFPPolicies.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_deadline: Job time.

    Variable arr_seq: arrival_sequence Job.

    (* We define earliest deadline first (EDF) as ordering jobs by absolute deadlines. *)
    Definition EDF (j1 j2: Job) :=
      job_arrival j1 + job_deadline j1 job_arrival j2 + job_deadline j2.

    Section Properties.

      (* EDF is reflexive. *)
      Lemma EDF_is_reflexive : JLFP_is_reflexive EDF.

      (* EDF is transitive. *)
      Lemma EDF_is_transitive : JLFP_is_transitive EDF.

      (* EDF is total. *)
      Lemma EDF_is_total : JLFP_is_total arr_seq EDF.

    End Properties.

  End KnownJLFPPolicies.

  (* In this section, we define the notion of a possible interfering task. *)
  Section PossibleInterferingTasks.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_period: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Section FP.

      (* Assume an FP policy. *)
      Variable higher_eq_priority: FP_policy sporadic_task.

      (* Let tsk be the task to be analyzed ... *)
      Variable tsk: sporadic_task.

      (* ...and let tsk_other be another task. *)
      Variable tsk_other: sporadic_task.

      (* Under FP scheduling with constrained deadlines, tsk_other can only interfere
         with tsk if it is a different task with higher priority. *)

      Definition higher_priority_task :=
        higher_eq_priority tsk_other tsk &&
        (tsk_other != tsk).

    End FP.

    Section JLFP.

      (* Let tsk be the task to be analyzed ... *)
      Variable tsk: sporadic_task.

      (* ...and let tsk_other be another task. *)
      Variable tsk_other: sporadic_task.

      (* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
         with tsk if it is a different task. *)

      Definition different_task := tsk_other != tsk.

    End JLFP.

  End PossibleInterferingTasks.

End Priority.