edf.v

Require Import prosa.model.priority.edf.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Import prosa.model.task.absolute_deadline.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Import prosa.model.task.preemption.parameters.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
     
(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.

  (** Consider any type of tasks with relative deadlines ... *)
  Context {Task : TaskType}.
  Context `{TaskDeadline Task}.

  (**  ... and any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.

  (** EDF respects sequential tasks hypothesis. *)
  Lemma EDF_respects_sequential_tasks:
    policy_respects_sequential_tasks.Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
policy_respects_sequential_tasks
  Proof.Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
policy_respects_sequential_tasks
    move => j1 j2 /eqP TSK ARR.Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2
hep_job j1 j2
    rewrite /hep_job /EDF /job_deadline /job_deadline_from_task_deadline TSK.Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
    by lia.
  Qed.

End PropertiesOfEDF.

(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
    will be able to apply it automatically. *)
Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.


Require Export prosa.model.task.sequentiality.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.busy_interval.priority_inversion.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.priority.sequential.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]

(** In this section, we prove that EDF priority policy 
    implies that tasks are sequential. *)
Section SequentialEDF.  

  (** Consider any type of tasks ... *)
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskDeadline Task}.

  (** ... with a bound on the maximum non-preemptive segment length.
      The bound is needed to ensure that, at any instant, it always 
      exists a subsequent preemption time in which the scheduler can, 
      if needed, switch to another higher-priority job. *)
  Context `{TaskMaxNonpreemptiveSegment Task}.
  
  (** Further, consider any type of jobs associated with these tasks. *)
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.

  (** Consider any arrival sequence. *)
  Variable arr_seq : arrival_sequence Job.
  
  (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
  Variable sched : schedule (ideal.processor_state Job).
  
  (** ... allow for any work-bearing notion of job readiness, ... *)
  Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.
  Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

  (** ... and assume that the schedule is valid. *)
  Hypothesis H_sched_valid : valid_schedule sched arr_seq.
  
  (** In addition, we assume the existence of a function mapping jobs
      to their preemption points ... *)
  Context `{JobPreemptable Job}.

  (** ... and assume that it defines a valid preemption model with
      bounded non-preemptive segments. *)
  Hypothesis H_valid_preemption_model:
    valid_preemption_model arr_seq sched.

  (** Next, we assume that the schedule respects the scheduling policy at every preemption point. *)
  Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).

  (** To prove sequentiality, we use lemma
      [early_hep_job_is_scheduled]. Clearly, under the EDF priority
      policy, jobs satisfy the conditions described by the lemma
      (i.e., given two jobs [j1] and [j2] from the same task, if [j1]
      arrives earlier than [j2], then [j1] always has a higher
      priority than job [j2], and hence completes before [j2]);
      therefore EDF implies sequential tasks. *)
  Lemma EDF_implies_sequential_tasks:
    sequential_tasks arr_seq sched.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
sequential_tasks arr_seq sched
  Proof.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
sequential_tasks arr_seq sched
    move => j1 j2 t ARR1 ARR2 /eqP SAME LT.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
scheduled_at sched j2 t -> completed_by sched j1 t
    eapply early_hep_job_is_scheduled => //; rt_eauto => t'.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant
hep_job_at t' j1 j2 && ~~ hep_job_at t' j2 j1
    rewrite /hep_job_at  /JLFP_to_JLDP /hep_job /EDF /job_deadline
      /absolute_deadline.job_deadline_from_task_deadline SAME.Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model
  arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point
  arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant
(job_arrival j1 + task_deadline (job_task j2) <=
 job_arrival j2 + task_deadline (job_task j2)) &&
~~
(job_arrival j2 + task_deadline (job_task j2) <=
 job_arrival j1 + task_deadline (job_task j2))
    by lia.
  Qed.

End SequentialEDF.