Library prosa.analysis.facts.model.sequential
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.model.task.sequentiality.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.facts.model.task_arrivals.
Section ExecutionOrder.
Require Export prosa.model.task.sequentiality.
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.facts.model.task_arrivals.
Section ExecutionOrder.
Consider any type of job associated with any type of tasks...
... with arrival times and costs ...
... and any kind of processor state model.
Consider any arrival sequence.
... and any schedule of this arrival sequence ...
... in which the sequential tasks hypothesis holds.
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.
∀ 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.
∀ 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.
In the following section, we connect sequential_readiness with
sequential_tasks, showing that the latter follows from the former.
Consider any type of job associated with any type of tasks ...
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
... any kind of processor state, ...
... and any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
If we have a sequential readiness model, ...
... then in any valid schedule of the arrival sequence ...
... all tasks execute sequentially.