Library prosa.analysis.facts.behavior.deadlines


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.13.0 (January 2021)

----------------------------------------------------------------------------- *)

Require Export prosa.analysis.facts.behavior.completion.

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: eqType}.
  Context `{ProcessorState Job PState}.

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:
      ∀ j t,
        job_meets_deadline sched j →
        ~~ completed_by sched j t →
        t < job_deadline j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 34)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  sched : schedule PState
  ============================
  forall (j : Job) (t : instant),
  job_meets_deadline sched j ->
  ~~ completed_by sched j t -> t < job_deadline j

----------------------------------------------------------------------------- *)

    Proof.
      move⇒ j t MET INCOMP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 38)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  MET : job_meets_deadline sched j
  INCOMP : ~~ completed_by sched j t
  ============================
  t < job_deadline j

----------------------------------------------------------------------------- *)

      apply contraT; rewrite -leqNgt ⇒ PAST_DL.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 44)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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 DL_MISS: ~~ completed_by sched j (job_deadline j)
        by apply incompletion_monotonic with (t' := t) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 59)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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
  DL_MISS : ~~ completed_by sched j (job_deadline j)
  ============================
  false

----------------------------------------------------------------------------- *)

      by move: DL_MISS ⇒ /negP.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t,
        job_meets_deadline sched j →
        ~~ completed_by sched j t →
        ∃ t', t ≤ t' < job_deadline j ∧ scheduled_at sched j t'.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 57)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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.
      move⇒ j t MET INCOMP.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 61)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 105)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 120)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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 by (apply ltnW; apply incomplete_implies_later_deadline).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 133)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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)

----------------------------------------------------------------------------- *)

      apply ltn_leq_trans with (n := job_cost j);
        first by rewrite less_service_than_cost_is_incomplete.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 141)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  sched : schedule PState
  j : Job
  t : instant
  MET : job_meets_deadline sched j
  INCOMP : ~~ completed_by sched j t
  ============================
  job_cost j <= service sched j (job_deadline j)

----------------------------------------------------------------------------- *)

      by apply MET.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j t,
        job_meets_deadline sched j →
        scheduled_at sched j t →
        t < job_deadline j.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 39)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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.
      move⇒ j t MET SCHED_AT.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 43)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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) ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 45)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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

----------------------------------------------------------------------------- *)

      by apply scheduled_implies_not_completed.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    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:
      ∀ j,
        service sched j (job_deadline j) = service sched' j (job_deadline j) →
        (job_meets_deadline sched j ↔ job_meets_deadline sched' j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 46)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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.
      move⇒ j SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 48)
  
  Job : JobType
  H : JobCost Job
  H0 : JobDeadline Job
  PState : eqType
  H1 : ProcessorState Job PState
  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

----------------------------------------------------------------------------- *)

      split;
        by rewrite /job_meets_deadline /completed_by -SERVICE.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    Qed.

  End EqualProgress.

End DeadlineFacts.