Library prosa.analysis.facts.readiness.sequential
Require Export prosa.analysis.definitions.readiness.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.task_arrivals.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.facts.model.task_arrivals.
Throughout this file, we assume the sequential task readiness model.
In this section, we show some useful properties of the sequential
task readiness model.
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}.
... and any kind of processor state.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(* As it was mentioned in the beginning of this file,
we assume the sequential task readiness model. *)
Instance sequential_ready_instance : JobReady Job PState :=
sequential.sequential_ready_instance arr_seq.
(* Consider any valid schedule of arr_seq. *)
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
(* As it was mentioned in the beginning of this file,
we assume the sequential task readiness model. *)
Instance sequential_ready_instance : JobReady Job PState :=
sequential.sequential_ready_instance arr_seq.
(* Consider any valid schedule of arr_seq. *)
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Consider an FP policy that indicates a reflexive
higher-or-equal priority relation.
First, we show that the sequential readiness model is non-clairvoyant.
Next, we show that the sequential readiness model ensures that
tasks are sequential. That is, that jobs of the same task
execute in order of their arrival.
Lemma sequential_readiness_implies_sequential_tasks :
sequential_tasks arr_seq sched.
(* Finally, we show that the sequential readiness model is a
work-bearing readiness model. That is, if a job j is pending
but not ready at a time instant t, then there exists another
(earlier) job of the same task that is pending and ready at time
t. *)
Lemma sequential_readiness_implies_work_bearing_readiness :
work_bearing_readiness arr_seq sched.
End SequentialTasksReadiness.
sequential_tasks arr_seq sched.
(* Finally, we show that the sequential readiness model is a
work-bearing readiness model. That is, if a job j is pending
but not ready at a time instant t, then there exists another
(earlier) job of the same task that is pending and ready at time
t. *)
Lemma sequential_readiness_implies_work_bearing_readiness :
work_bearing_readiness arr_seq sched.
End SequentialTasksReadiness.