Library prosa.analysis.facts.blocking_bound.elf
Require Export prosa.analysis.definitions.blocking_bound.elf.
Require Export prosa.analysis.facts.busy_interval.pi.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Import prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.priority.elf.
Require Export prosa.analysis.facts.busy_interval.pi.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.facts.model.arrival_curves.
Require Import prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.priority.elf.
Lower-Priority Non-Preemptive Segment is Bounded
In this file, we prove that, under the ELF scheduling policy, the length of the maximum non-preemptive segment of a lower-priority job (w.r.t. a job of a task tsk) is bounded by blocking_bound.
Consider any type of tasks, each characterized by a WCET
task_cost, an arrival curve max_arrivals, a relative
deadline task_deadline, a bound on the the task's longest
non-preemptive segment task_max_nonpreemptive_segment and
relative priority points, ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
Context `{PriorityPoint Task}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{TaskMaxNonpreemptiveSegment Task}.
Context `{PriorityPoint Task}.
... and any type of jobs associated with these tasks, where each
job has a task job_task, a cost job_cost, and an arrival
time job_arrival.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
Consider any kind of processor state model.
Consider any valid arrival sequence ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any schedule of this arrival sequence.
We further require that a job's cost cannot exceed its task's stated WCET ...
... and assume that jobs have bounded non-preemptive segments.
Context `{JobPreemptable Job}.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
Consider an arbitrary task set ts, ...
... assume that all jobs come from the task set, ...
Let max_arrivals be a family of arrival curves.
Consider an FP policy that indicates a higher-or-equal priority
relation, and assume that the relation is reflexive, transitive
and total.
Context (FP : FP_policy Task).
Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
Hypothesis H_transitive_priorities : transitive_task_priorities FP.
Hypothesis H_total_priorities : total_task_priorities FP.
Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
Hypothesis H_transitive_priorities : transitive_task_priorities FP.
Hypothesis H_total_priorities : total_task_priorities FP.
Then, the maximum length of a nonpreemptive segment among all
lower-priority jobs (w.r.t. the given job j) arrived so far is
bounded by blocking_bound.