Library prosa.analysis.facts.model.scheduled

Require Export prosa.model.schedule.scheduled.
Require Export prosa.analysis.definitions.service.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.util.tactics.

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 valid arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

... 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.
NB: We do not use valid_schedule here to avoid introducing a dependency on a readiness mode.
  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.

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.

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

We restate the previous claim for convenience.
  Corollary not_scheduled_when_idle :
    ∀ j t,
      is_idle arr_seq sched t → ~~ scheduled_at sched j t.

The Job Scheduled on an Ideal Progress Processor

In this section, we prove a simple fact about the relation between scheduled_at and served_at.
  Section IdealProgress.

Assume a scheduled job always receives some positive service.
    Hypothesis H_ideal_progress_model : ideal_progress_proc_model PState.

We prove that if a job j is scheduled at time t, then j is in the set of jobs that are served at time t.
    Lemma scheduled_at_implies_in_served_at :
      ∀ j t,
        scheduled_at sched j t →
        j \in served_jobs_at arr_seq sched t.

  End IdealProgress.

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 clearly there is at most one job scheduled at any time t.
    Corollary scheduled_jobs_at_seq1 :
      ∀ t,
        size (scheduled_jobs_at arr_seq sched t) ≤ 1.

For convenience, we restate the fact that there is at most one job as a case analysis.
    Corollary scheduled_jobs_at_uni_cases :
      ∀ t,
        scheduled_jobs_at arr_seq sched t == [::]
        ∨ ∃ j, scheduled_jobs_at arr_seq sched t == [:: j].

We note the obvious relationship between scheduled_jobs_at and scheduled_job_at ...
    Lemma scheduled_jobs_at_uni :
      ∀ j t,
        (scheduled_jobs_at arr_seq sched t == [::j])
        = (scheduled_job_at arr_seq sched t == Some j).

... and observe that scheduled_job_at t behaves as expected: it yields some job j if and only if j is scheduled at time t.
    Corollary scheduled_job_at_scheduled_at :
      ∀ j t,
        (scheduled_job_at arr_seq sched t == Some j) = scheduled_at sched j t.

Similarly to scheduled_job_at_scheduled_at, we relate scheduled_jobs_at to scheduled_at.
    Corollary scheduled_jobs_at_scheduled_at :
      ∀ j t,
        (scheduled_jobs_at arr_seq sched t == [:: j])
        = scheduled_at sched j t.

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

For convenience, we state a similar observation also for the is_idle wrapper, both for the idle case ...
    Corollary is_idle_iff :
      ∀ t,
        is_idle arr_seq sched t = (scheduled_job_at arr_seq sched t == None).

... and the non-idle case.
    Corollary is_nonidle_iff :
      ∀ t,
        ~~ is_idle arr_seq sched t ↔ ∃ j, scheduled_at sched j t.

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

For ease of porting, we restate the above case analysis in a form closer to what was used in earlier versions of Prosa.
  Corollary scheduled_at_cases :
    ∀ t,
      is_idle arr_seq sched t ∨ ∃ j, scheduled_at sched j t.

End ScheduledJobs.