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]

(** * Deadlines *)

(** In this file, we observe basic properties of the behavioral job
    model w.r.t. deadlines. *)
Section DeadlineFacts.

  (** Consider any given type of jobs with costs and deadlines... *)
  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.

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

  (** First, we derive two properties from the fact that a job is incomplete at
      some point in time. *)
  Section Incompletion.

    (** Consider any given schedule. *)
    Variable sched: schedule PState.

    (** Trivially, a job that both meets its deadline and is incomplete at a
        time [t] must have a deadline later than [t]. *)
    Lemma incomplete_implies_later_deadline:
      forall j t,
        job_meets_deadline sched j ->
        ~~ completed_by sched j t ->
        t < job_deadline j.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
~~ completed_by sched j t -> t < job_deadline j
    Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
~~ completed_by sched j t -> t < job_deadline j
      move=> j t MET INCOMP; apply: contraT; rewrite -leqNgt => PAST_DL.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
PAST_DL: job_deadline j <= t
false
      have /negP// : ~~ completed_by sched j (job_deadline j).
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
PAST_DL: job_deadline j <= t
~~ completed_by sched j (job_deadline j)
      exact: incompletion_monotonic INCOMP.
    Qed.

    (** Furthermore, a job that both meets its deadline and is incomplete at a
        time [t] must be scheduled at some point between [t] and its
        deadline. *)
    Lemma incomplete_implies_scheduled_later:
      forall j t,
        job_meets_deadline sched j ->
        ~~ completed_by sched j t ->
        exists t', t <= t' < job_deadline j /\ scheduled_at sched j t'.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
~~ completed_by sched j t ->
exists t' : nat,
  t <= t' < job_deadline j /\ scheduled_at sched j t'
    Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
~~ completed_by sched j t ->
exists t' : nat,
  t <= t' < job_deadline j /\ scheduled_at sched j t'
      move=> j t MET INCOMP.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
exists t' : nat,
  t <= t' < job_deadline j /\ scheduled_at sched j t'
      apply: cumulative_service_implies_scheduled.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
0 < service_during sched j t (job_deadline j)
      rewrite -(ltn_add2l (service sched j t)) addn0.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
service sched j t <
service sched j t +
service_during sched j t (job_deadline j)
      rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
MET: job_meets_deadline sched j
INCOMP: ~~ completed_by sched j t
service sched j t < service sched j (job_deadline j)
      by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete.
    Qed.

  End Incompletion.

  (** Next, we look at schedules / processor models in which scheduled jobs
      always receive service. *)
  Section IdealProgressSchedules.

    (** Consider a given reference schedule... *)
    Variable sched: schedule PState.

    (** ...in which complete jobs don't execute... *)
    Hypothesis H_completed_jobs: completed_jobs_dont_execute sched.

    (** ...and scheduled jobs always receive service. *)
    Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

    (** We observe that if a job meets its deadline and is scheduled at time
        [t], then then its deadline is at a time later than t. *)
    Lemma scheduled_at_implies_later_deadline:
      forall j t,
        job_meets_deadline sched j ->
        scheduled_at sched j t ->
        t < job_deadline j.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model
  PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
scheduled_at sched j t -> t < job_deadline j
    Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model
  PState
forall (j : Job) (t : instant),
job_meets_deadline sched j ->
scheduled_at sched j t -> t < job_deadline j
      move=> j t MET SCHED_AT.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model
  PState
j: Job
t: instant
MET: job_meets_deadline sched j
SCHED_AT: scheduled_at sched j t
t < job_deadline j
      apply: (incomplete_implies_later_deadline sched) => //.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model
  PState
j: Job
t: instant
MET: job_meets_deadline sched j
SCHED_AT: scheduled_at sched j t
~~ completed_by sched j t
      exact: scheduled_implies_not_completed.
    Qed.

  End IdealProgressSchedules.

  (** In the following section, we observe that it is sufficient to
      establish that service is invariant across two schedules at a
      job's deadline to establish that it either meets its deadline in
      both schedules or none. *)
  Section EqualProgress.

    (** Consider any two schedules [sched] and [sched']. *)
    Variable sched sched': schedule PState.

    (** We observe that, if the service is invariant at the time of a
       job's absolute deadline, and if the job meets its deadline in one of the schedules, 
       then it meets its deadline also in the other schedule. *)
    Lemma service_invariant_implies_deadline_met:
      forall j,
        service sched j (job_deadline j) = service sched' j (job_deadline j) ->
        (job_meets_deadline sched j <-> job_meets_deadline sched' j).
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState
forall j : Job,
service sched j (job_deadline j) =
service sched' j (job_deadline j) ->
job_meets_deadline sched j <->
job_meets_deadline sched' j
    Proof.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState
forall j : Job,
service sched j (job_deadline j) =
service sched' j (job_deadline j) ->
job_meets_deadline sched j <->
job_meets_deadline sched' j
      move=> j SERVICE.
Job: JobType
H: JobCost Job
H0: JobDeadline Job
PState: ProcessorState Job
sched, sched': schedule PState
j: Job
SERVICE: service sched j (job_deadline j) =
service sched' j (job_deadline j)
job_meets_deadline sched j <->
job_meets_deadline sched' j
      by split; rewrite /job_meets_deadline /completed_by -SERVICE.
    Qed.

  End EqualProgress.

End DeadlineFacts.