Library prosa.model.task.sequentiality


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

Welcome to Coq 8.11.2 (June 2020)

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


Require Export prosa.model.task.concept.

In this module, we give a precise definition of the common notion of "sequential tasks", which is commonly understood to mean that the jobs of a sequential task execute in sequence and in a non-overlapping fashion.
Consider any type of jobs stemming from 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 model.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

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

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

We say that the tasks execute sequentially if each task's jobs are executed in arrival order and in a non-overlapping fashion.
  Definition sequential_tasks :=
     (j1 j2 : Job) (t : instant),
      arrives_in arr_seq j1
      arrives_in arr_seq j2
      same_task j1 j2
      job_arrival j1 < job_arrival j2
      scheduled_at sched j2 t
      completed_by sched j1 t.

End PropertyOfSequentiality.