Library prosa.analysis.facts.behavior.deadlines


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

Welcome to Coq 8.11.2 (June 2020)

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


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}.

We begin with 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...
...and scheduled jobs always receive service.
We observe that, if a job is known to meet its deadline, then its deadline must be later than any point at which it is scheduled. That is, if a job that meets its deadline is scheduled at time t, we may conclude that 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 53)
  
  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.
      movej t.

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

1 subgoal (ID 55)
  
  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
  ============================
  job_meets_deadline sched j -> scheduled_at sched j t -> t < job_deadline j

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


      rewrite /job_meets_deadlineCOMP SCHED.

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

1 subgoal (ID 64)
  
  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
  COMP : completed_by sched j (job_deadline j)
  SCHED : scheduled_at sched j t
  ============================
  t < job_deadline j

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


      case: (boolP (t < job_deadline j)) ⇒ //.

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

1 subgoal (ID 82)
  
  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
  COMP : completed_by sched j (job_deadline j)
  SCHED : scheduled_at sched j t
  ============================
  ~~ (t < job_deadline j) -> false

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


      rewrite -leqNgtAFTER_DL.

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

1 subgoal (ID 112)
  
  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
  COMP : completed_by sched j (job_deadline j)
  SCHED : scheduled_at sched j t
  AFTER_DL : job_deadline j <= t
  ============================
  false

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


      apply completion_monotonic with (t' := t) in COMP ⇒ //.

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

1 subgoal (ID 117)
  
  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
  COMP : completed_by sched j t
  SCHED : scheduled_at sched j t
  AFTER_DL : job_deadline j <= t
  ============================
  false

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


      apply scheduled_implies_not_completed in SCHED ⇒ //.

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

1 subgoal (ID 146)
  
  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
  COMP : completed_by sched j t
  SCHED : ~~ completed_by sched j t
  AFTER_DL : job_deadline j <= t
  ============================
  false

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


      move/negP in SCHED.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 217)
  
  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
  COMP : completed_by sched j t
  AFTER_DL : job_deadline j <= t
  SCHED : ~ completed_by sched j t
  ============================
  false

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


contradiction.

(* ----------------------------------[ 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 61)
  
  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.
      movej SERVICE.

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

1 subgoal (ID 63)
  
  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.