Library prosa.analysis.facts.model.scheduled

Require Export prosa.model.schedule.scheduled.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.arrivals.

Correctness of the Scheduled Job(s)

In this file, we establish the correctness of the computable definition of the (set of) scheduled job(s) and a useful case-analysis lemma.

Section ScheduledJobs.

Consider any type of jobs with arrival times.

Context {Job : JobType}.
Context `{JobArrival Job}.

Next, consider any kind of processor state model, ...

Context {PState : ProcessorState Job}.

... any arrival sequence, ...

Variable arr_seq : arrival_sequence Job.

... and any schedule.

Variable sched : schedule PState.

Now we establish the validity conditions under which these definitions yield the expected results: all jobs must come from the arrival sequence and do not execute before their arrival.

  Hypothesis H_jobs_come_from_arrival_sequence :
    jobs_come_from_arrival_sequence sched arr_seq.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

The Set of Jobs Scheduled at a Given Time

Under these assumptions, scheduled_jobs_at is correct: a job is included in the sequence if and only if it scheduled.

  Lemma scheduled_jobs_at_iff :
    ∀ j t,
      j \in scheduled_jobs_at arr_seq sched t ↔ scheduled_at sched j t.
  Proof.
    move⇒ j t
      ; split ⇒ [|SCHED]
      ; rewrite /scheduled_jobs_at mem_filter
      ; first by move⇒ /andP [SCHED _].
    apply /andP; split; first exact: SCHED.
    apply: arrivals_before_scheduled_at; rt_eauto.
    by rewrite /ε; lia.
  Qed.

Conversely, if no jobs are in the sequence, then no job is scheduled.

  Lemma scheduled_jobs_at_nil :
    ∀ t,
      nilp (scheduled_jobs_at arr_seq sched t)
      ↔ (∀ j, ~~ scheduled_at sched j t ).
  Proof.
    move⇒ t; split ⇒ [/nilP NIL j|NS].
    { apply: contraT ⇒ /negbNE.
      by rewrite -scheduled_jobs_at_iff NIL in_nil. }
    { apply /nilP.
      case NN: (scheduled_jobs_at _) ⇒ [//|j js].
      exfalso.
      have: scheduled_at sched j t; last by move: (NS j) ⇒ /negP.
      rewrite -scheduled_jobs_at_iff NN.
      exact: mem_head. }
  Qed.

The Job Scheduled on a Uniprocessor

For convenience, we note similar rewriting rules for uniprocessors.

Section Uniprocessors.

Suppose we are looking at a uniprocessor.

Hypothesis H_uni : uniprocessor_model PState.

Then scheduled_job_at t is correct: it yields some job j if and only if j is scheduled at time t.

    Corollary scheduled_job_at_iff :
      ∀ j t,
        scheduled_job_at arr_seq sched t = Some j ↔ scheduled_at sched j t.
    Proof.
      move⇒ j t
        ; rewrite /scheduled_job_at /ohead
        ; split ⇒ [|SCHED]
        ; case SJA: (scheduled_jobs_at _) ⇒ [//|j' js].
      { rewrite -scheduled_jobs_at_iff SJA.
        by move⇒ []->; exact: mem_head. }
      { by move: SCHED; rewrite -scheduled_jobs_at_iff SJA. }
      { rewrite (H_uni j j' sched t) // -scheduled_jobs_at_iff SJA.
        exact: mem_head. }
    Qed.

Conversely, if scheduled_job_at t returns None, then no job is scheduled at time t.

    Corollary scheduled_job_at_none :
      ∀ t,
        scheduled_job_at arr_seq sched t = None
        ↔ (∀ j, ~~ scheduled_at sched j t ).
    Proof.
      move⇒ t. rewrite /scheduled_job_at -scheduled_jobs_at_nil.
      by case: (scheduled_jobs_at arr_seq sched t).
    Qed.

  End Uniprocessors.

Case Analysis: a Scheduled Job Exists or no Job is Scheduled

Last but not least, We note a case analysis that results from the above considerations: at any point in time, either some job is scheduled, or it holds that all jobs are not scheduled.

  Lemma scheduled_at_dec :
    ∀ t,
      {∃ j , scheduled_at sched j t } + {∀ j, ~~ scheduled_at sched j t }.
  Proof.
    move⇒ t.
    case SJA: (scheduled_jobs_at arr_seq sched t) ⇒ [|j js].
    - by right; rewrite -scheduled_jobs_at_nil SJA.
    - left; ∃ j.
      rewrite -scheduled_jobs_at_iff SJA.
      exact: mem_head.
  Qed.

End ScheduledJobs.