Library prosa.model.task.sequentiality
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.13.0 (January 2021)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.concept.
Require Export prosa.model.task.arrivals.
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 ...
... with arrival times and costs ...
... and any kind of processor model.
Consider any arrival sequence ...
... and any schedule of this arrival sequence.
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.
(* Given a job [j] and a time instant [t], we say that all prior
jobs are completed if any job [j_tsk] of task [job_task j] that
arrives before time [job_arrival j] is completed by time [t]. *)
Definition prior_jobs_complete (j : Job) (t : instant) :=
all
(fun j_tsk ⇒ completed_by sched j_tsk t)
(task_arrivals_before arr_seq (job_task j) (job_arrival j)).
End PropertyOfSequentiality.
∀ (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.
(* Given a job [j] and a time instant [t], we say that all prior
jobs are completed if any job [j_tsk] of task [job_task j] that
arrives before time [job_arrival j] is completed by time [t]. *)
Definition prior_jobs_complete (j : Job) (t : instant) :=
all
(fun j_tsk ⇒ completed_by sched j_tsk t)
(task_arrivals_before arr_seq (job_task j) (job_arrival j)).
End PropertyOfSequentiality.