Require Export prosa.analysis.facts.behavior.completion.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Import prosa.model.task.absolute_deadline.

(** * Schedulability *)

(** In the following section we define the notion of schedulable
    task. *)
Section Task.
  
  (** Consider any type of tasks, ... *)
  Context {Task : TaskType}.

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

  (** ... and any kind of processor state. *)
  Context {PState : ProcessorState Job}.

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

  (** ...and any schedule of these jobs. *)
  Variable sched: schedule PState.

  (** Let [tsk] be any task that is to be analyzed. *)
  Variable tsk: Task.

  (** Then, we say that R is a response-time bound of [tsk] in this schedule ... *)
  Variable R: duration.

  (** ... iff any job [j] of [tsk] in this arrival sequence has
         completed by [job_arrival j + R]. *)
  Definition task_response_time_bound :=
    forall j,
      arrives_in arr_seq j ->
      job_of_task tsk j ->
      job_response_time_bound sched j R.

  (** We say that a task is schedulable if all its jobs meet their deadline *)
  Definition schedulable_task :=
    forall j,
      arrives_in arr_seq j ->
      job_of_task tsk j ->
      job_meets_deadline sched j.
  
End Task.

(** In this section we infer schedulability from a response-time bound
    of a task. *)
Section Schedulability.  

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

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

  (** ... and any kind of processor state. *)
  Context {PState : ProcessorState Job}.
  
  (** Consider any job arrival sequence... *)
  Variable arr_seq: arrival_sequence Job.

  (** ...and any schedule of these jobs. *)
  Variable sched: schedule PState.

  (** Assume that jobs don't execute after completion. *)
  Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.

  (** Let [tsk] be any task that is to be analyzed. *)
  Variable tsk: Task.

  (** Given  a response-time bound of [tsk] in this schedule no larger than its deadline, ... *)
  Variable R: duration.

  Hypothesis H_R_le_deadline: R <= task_deadline tsk.
  Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.

  (** ...then [tsk] is schedulable. *)
  Lemma schedulability_from_response_time_bound:
    schedulable_task arr_seq sched tsk.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
schedulable_task arr_seq sched tsk
  Proof.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
schedulable_task arr_seq sched tsk
    intros j ARRj JOBtsk.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
j: Job
ARRj: arrives_in arr_seq j
JOBtsk: job_of_task tsk j
job_meets_deadline sched j
    rewrite /job_meets_deadline.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
j: Job
ARRj: arrives_in arr_seq j
JOBtsk: job_of_task tsk j
completed_by sched j (job_deadline j)
    apply completion_monotonic with (t := job_arrival j + R);
      [ | by apply H_response_time_bounded].
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
j: Job
ARRj: arrives_in arr_seq j
JOBtsk: job_of_task tsk j
job_arrival j + R <= job_deadline j
    rewrite /job_deadline leq_add2l.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
j: Job
ARRj: arrives_in arr_seq j
JOBtsk: job_of_task tsk j
R <= task_deadline (job_task j)
    move: JOBtsk => /eqP ->.
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobArrival Job
H1: JobCost Job
H2: JobTask Job Task
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
H_completed_jobs_dont_execute: completed_jobs_dont_execute
  sched
tsk: Task
R: duration
H_R_le_deadline: R <= task_deadline tsk
H_response_time_bounded: task_response_time_bound
  arr_seq sched tsk R
j: Job
ARRj: arrives_in arr_seq j
R <= task_deadline tsk
    by erewrite leq_trans; eauto.
  Qed.

End Schedulability.


(** We further define two notions of "all deadlines met" that do not
    depend on a task abstraction: one w.r.t. all scheduled jobs in a
    given schedule and one w.r.t. all jobs that arrive in a given
    arrival sequence. *)
Section AllDeadlinesMet.
  
  (** Consider any given type of jobs... *)
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.

  (** ... any given type of processor states. *)
  Context {PState: ProcessorState Job}.

  (** We say that all deadlines are met if every job scheduled at some
     point in the schedule meets its deadline. Note that this is a
     relatively weak definition since an "empty" schedule that is idle
     at all times trivially satisfies it (since the definition does
     not require any kind of work conservation). *)
  Definition all_deadlines_met (sched: schedule PState) :=
    forall j t,
      scheduled_at sched j t ->
      job_meets_deadline sched j.

  (** To augment the preceding definition, we also define an alternate
     notion of "all deadlines met" based on all jobs included in a
     given arrival sequence.  *)
  Section DeadlinesOfArrivals.

    (** Given an arbitrary job arrival sequence ... *)
    Variable arr_seq: arrival_sequence Job.  

    (** ... we say that all arrivals meet their deadline if every job
       that arrives at some point in time meets its deadline. Note
       that this definition does not preclude the existence of jobs in
       a schedule that miss their deadline (e.g., if they stem from
       another arrival sequence). *)
    Definition all_deadlines_of_arrivals_met (sched: schedule PState) :=
      forall j,
        arrives_in arr_seq j ->
        job_meets_deadline sched j.

  End DeadlinesOfArrivals.

  (** We observe that the latter definition, assuming a schedule in
      which all jobs come from the arrival sequence, implies the
      former definition. *)
  Lemma all_deadlines_met_in_valid_schedule:
    forall arr_seq sched,
      jobs_come_from_arrival_sequence sched arr_seq ->
      all_deadlines_of_arrivals_met arr_seq sched ->
      all_deadlines_met sched.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
PState: ProcessorState Job
forall (arr_seq : arrival_sequence Job)
  (sched : schedule PState),
jobs_come_from_arrival_sequence sched arr_seq ->
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_met sched
  Proof.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
PState: ProcessorState Job
forall (arr_seq : arrival_sequence Job)
  (sched : schedule PState),
jobs_come_from_arrival_sequence sched arr_seq ->
all_deadlines_of_arrivals_met arr_seq sched ->
all_deadlines_met sched
    move=> arr_seq sched FROM_ARR DL_ARR_MET j t SCHED.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FROM_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
DL_ARR_MET: all_deadlines_of_arrivals_met arr_seq
  sched
j: Job
t: instant
SCHED: scheduled_at sched j t
job_meets_deadline sched j
    apply DL_ARR_MET.
Job: JobType
H: JobArrival Job
H0: JobCost Job
H1: JobDeadline Job
PState: ProcessorState Job
arr_seq: arrival_sequence Job
sched: schedule PState
FROM_ARR: jobs_come_from_arrival_sequence sched
  arr_seq
DL_ARR_MET: all_deadlines_of_arrivals_met arr_seq
  sched
j: Job
t: instant
SCHED: scheduled_at sched j t
arrives_in arr_seq j
    by apply (FROM_ARR _ t).
  Qed.
    
End AllDeadlinesMet.