Library prosa.analysis.facts.model.sequential

Require Export prosa.model.task.sequentiality.

Section ExecutionOrder.

Consider any type of job associated with any type of tasks...
  Context {Job: JobType}.
  Context {Task: TaskType}.
  Context `{JobTask Job Task}.

... with arrival times and costs ...
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... and any kind of processor state model.
  Context {PState: ProcessorState Job}.

Trivially, same_task is symmetric.
  Remark same_task_sym :
    ∀ j1 j2,
      same_task j1 j2 = same_task j2 j1.

Consider any arrival sequence ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule of this arrival sequence ...
  Variable sched : schedule PState.

... in which the sequential tasks hypothesis holds.
  Hypothesis H_sequential_tasks: sequential_tasks arr_seq sched.

A simple corollary of this hypothesis is that the scheduler executes a job with the earliest arrival time.
  Corollary scheduler_executes_job_with_earliest_arrival:
    ∀ j1 j2 t,
      arrives_in arr_seq j1 →
      arrives_in arr_seq j2 →
      same_task j1 j2 →
      ~~ completed_by sched j2 t →
      scheduled_at sched j1 t →
      job_arrival j1 ≤ job_arrival j2.

Likewise, if we see an earlier-arrived incomplete job j1 while another job j2 is scheduled, then j1 and j2 must stem from different tasks.
  Corollary sequential_tasks_different_tasks :
    ∀ j1 j2 t,
      arrives_in arr_seq j1 →
      arrives_in arr_seq j2 →
      job_arrival j1 < job_arrival j2 →
      ~~ completed_by sched j1 t →
      scheduled_at sched j2 t →
      ~~ same_task j1 j2.

End ExecutionOrder.