Library rt.restructuring.analysis.abstract.core.run_to_completion_threshold
From rt.util Require Import epsilon sum tactics search_arg.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.analysis.basic_facts Require Import completion.
From rt.restructuring.model Require Import job task preemption.preemption_model.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Run-to-completion threshold
In this file, we provide definition and properties of run-to-completion-threshold-compilant schedules.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
In addition, we assume existence of a function
maping jobs to theirs preemption points ...
...and a function mapping tasks to theirs
run-to-completion threshold.
Consider any kind of processor state model, ...
... any job arrival sequence, ...
... and any given schedule.
In this section we define the notion of a run-to-completion threshold for a job.
We define the notion of job's run-to-completion threshold: run-to-completion threshold
is the amount of service after which a job cannot be preempted until its completion.
Definition runs_to_completion_from (j : Job) (ρ : duration) :=
all (fun (δ : duration) ⇒ ~~ job_preemptable j δ) (index_iota ρ (job_cost j)).
all (fun (δ : duration) ⇒ ~~ job_preemptable j δ) (index_iota ρ (job_cost j)).
Note that a run-to-completion threshold exists for any job.
We define run-to-completion threshold of a job as the minimal progress
the job should reach to become non-preemptive until completion.
Definition job_run_to_completion_threshold (j : Job) : duration :=
ex_minn (eventually_runs_to_completion j).
ex_minn (eventually_runs_to_completion j).
In this section we prove a few simple lemmas
about run-to-completion threshold for a job.
Assume that the preemption model is valid.
Consider an arbitrary job j from the arrival sequence.
First, we prove that a job cannot be preempted
during execution of the last segment.
Lemma job_cannot_be_preempted_within_last_segment:
∀ (ρ : duration),
job_run_to_completion_threshold j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
∀ (ρ : duration),
job_run_to_completion_threshold j ≤ ρ < job_cost j →
~~ job_preemptable j ρ.
We prove that the run-to-completion threshold is positive for any job. I.e., in order
to become non-preemptive a job must receive at least one unit of service.
Lemma job_run_to_completion_threshold_positive:
job_cost_positive j →
0 < job_run_to_completion_threshold j.
job_cost_positive j →
0 < job_run_to_completion_threshold j.
Next we show that the run-to-completion threshold
is at most the cost of a job.
Lemma job_run_to_completion_threshold_le_job_cost:
job_cost_positive j →
job_run_to_completion_threshold j ≤ job_cost j.
job_cost_positive j →
job_run_to_completion_threshold j ≤ job_cost j.
In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion.
Lemma job_nonpreemptive_after_run_to_completion_threshold:
∀ t t',
t ≤ t' →
job_run_to_completion_threshold j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
End Lemmas.
End JobRunToCompletionThreshold.
∀ t t',
t ≤ t' →
job_run_to_completion_threshold j ≤ service sched j t →
~~ completed_by sched j t' →
scheduled_at sched j t'.
End Lemmas.
End JobRunToCompletionThreshold.
Since a task model may not provide exact information about preemption point of
a task run-to-completion, task's run-to-completion threshold cannot be defined in
terms of preemption points of a task (unlike job's run-to-completion threshold).
Therefore, one can assume the existence of a function that maps a task to
its run-to-completion threshold. In this section we define the notion
of a valid run-to-completion threshold of a task.
A task's run-to-completion threshold should be at most the cost of the task.
Definition task_run_to_completion_threshold_le_task_cost tsk :=
task_run_to_completion_threshold tsk ≤ task_cost tsk.
task_run_to_completion_threshold tsk ≤ task_cost tsk.
We say that the run-to-completion threshold of a task tsk
bounds the job run-to-completionthreshold iff for any job j
of task tsk the job run-to-completion threshold is less than
or equal to the task run-to-completion threshold.
Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_run_to_completion_threshold j ≤ task_run_to_completion_threshold tsk.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_run_to_completion_threshold j ≤ task_run_to_completion_threshold tsk.
We say that task_run_to_completion_threshold is a valid task run-to-completion
threshold for a task tsk iff task_run_to_completion_threshold tsk is (1) no
bigger than tsk's cost, (2) for any job of task tsk job_run_to_completion_threshold
is bounded by task_run_to_completion_threshold.