Library rt.restructuring.analysis.schedulability
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Export task job_deadline.
From rt.restructuring.analysis.basic_facts Require Export completion.
From rt.util Require Export seqset.
Section Task.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Consider any job arrival sequence...
...and any schedule of these jobs.
Let tsk be any task that is to be analyzed.
Then, we say that R is a response-time bound of tsk in this schedule ...
... iff any job j of tsk in this arrival sequence has
completed by (job_arrival j + R).
Definition task_response_time_bound :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_response_time_bound sched j R.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_response_time_bound sched j R.
We say that a task is schedulable if all its jobs meet their deadline
Definition schedulable_task :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_meets_deadline sched j.
End Task.
Section TaskSet.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable ts : {set Task}.
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_meets_deadline sched j.
End Task.
Section TaskSet.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Variable ts : {set Task}.
Consider any job arrival sequence...
...and any schedule of these jobs.
We say that a task set is schedulable if all its tasks are schedulable
Definition schedulable_taskset :=
∀ tsk, tsk \in ts → schedulable_task arr_seq sched tsk.
End TaskSet.
Section Schedulability.
∀ tsk, tsk \in ts → schedulable_task arr_seq sched tsk.
End TaskSet.
Section Schedulability.
We can infer schedulability from a response-time bound of a task.
Context {Task : TaskType}.
Context {Job: JobType}.
Context `{TaskDeadline Task}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
Consider any job arrival sequence...
...and any schedule of these jobs.
Assume that jobs don't execute after completion.
Let tsk be any task that is to be analyzed.
Given a response-time bound of tsk in this schedule no larger than its deadline, ...
Variable R: duration.
Hypothesis H_R_le_deadline: R ≤ task_deadline tsk.
Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.
Hypothesis H_R_le_deadline: R ≤ task_deadline tsk.
Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.
...then tsk is schedulable.
Lemma schedulability_from_response_time_bound:
schedulable_task arr_seq sched tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
============================
schedulable_task arr_seq sched tsk
----------------------------------------------------------------------------- *)
Proof.
intros j ARRj JOBtsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
job_meets_deadline sched j
----------------------------------------------------------------------------- *)
rewrite /job_meets_deadline.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
completed_by sched j (job_deadline j)
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t := job_arrival j + R);
[ | by apply H_response_time_bounded].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
job_arrival j + R <= job_deadline j
----------------------------------------------------------------------------- *)
rewrite /job_deadline leq_add2l JOBtsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
R <= task_deadline tsk
----------------------------------------------------------------------------- *)
by erewrite leq_trans; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Schedulability.
schedulable_task arr_seq sched tsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 56)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
============================
schedulable_task arr_seq sched tsk
----------------------------------------------------------------------------- *)
Proof.
intros j ARRj JOBtsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
job_meets_deadline sched j
----------------------------------------------------------------------------- *)
rewrite /job_meets_deadline.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 67)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
completed_by sched j (job_deadline j)
----------------------------------------------------------------------------- *)
apply completion_monotonic with (t := job_arrival j + R);
[ | by apply H_response_time_bounded].
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 74)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
job_arrival j + R <= job_deadline j
----------------------------------------------------------------------------- *)
rewrite /job_deadline leq_add2l JOBtsk.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 89)
Task : TaskType
Job : JobType
H : TaskDeadline Task
H0 : JobArrival Job
H1 : JobCost Job
H2 : JobTask Job Task
PState : Type
H3 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
H_completed_jobs_dont_execute : completed_jobs_dont_execute sched
tsk : Task
R : duration
H_R_le_deadline : R <= task_deadline tsk
H_response_time_bounded : task_response_time_bound arr_seq sched tsk R
j : Job
ARRj : arrives_in arr_seq j
JOBtsk : job_task j = tsk
============================
R <= task_deadline tsk
----------------------------------------------------------------------------- *)
by erewrite leq_trans; eauto.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End Schedulability.
We further define two notions of "all deadlines met" that do not
depend on a task abstraction: one w.r.t. all scheduled jobs in a
given schedule and one w.r.t. all jobs that arrive in a given
arrival sequence.
Consider any given type of jobs...
... any given type of processor states.
We say that all deadlines are met if every job scheduled at some
point in the schedule meets its deadline. Note that this is a
relatively weak definition since an "empty" schedule that is idle
at all times trivially satisfies it (since the definition does
not require any kind of work conservation).
Definition all_deadlines_met (sched: schedule PState) :=
∀ j t,
scheduled_at sched j t →
job_meets_deadline sched j.
∀ j t,
scheduled_at sched j t →
job_meets_deadline sched j.
To augment the preceding definition, we also define an alternate
notion of "all deadlines met" based on all jobs included in a
given arrival sequence.
Given an arbitrary job arrival sequence ...
... we say that all arrivals meet their deadline if every job
that arrives at some point in time meets its deadline. Note
that this definition does not preclude the existence of jobs in
a schedule that miss their deadline (e.g., if they stem from
another arrival sequence).
Definition all_deadlines_of_arrivals_met (sched: schedule PState) :=
∀ j,
arrives_in arr_seq j →
job_meets_deadline sched j.
End DeadlinesOfArrivals.
∀ j,
arrives_in arr_seq j →
job_meets_deadline sched j.
End DeadlinesOfArrivals.
We observe that the latter definition, assuming a schedule in
which all jobs come from the arrival sequence, implies the former
definition.
Lemma all_deadlines_met_in_valid_schedule:
∀ arr_seq sched,
jobs_come_from_arrival_sequence sched arr_seq →
all_deadlines_of_arrivals_met arr_seq sched →
all_deadlines_met sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
============================
forall (arr_seq : arrival_sequence Job) (sched : schedule PState),
jobs_come_from_arrival_sequence sched arr_seq ->
all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_met sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ arr_seq sched FROM_ARR DL_ARR_MET j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
FROM_ARR : jobs_come_from_arrival_sequence sched arr_seq
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
job_meets_deadline sched j
----------------------------------------------------------------------------- *)
apply DL_ARR_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
FROM_ARR : jobs_come_from_arrival_sequence sched arr_seq
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
arrives_in arr_seq j
----------------------------------------------------------------------------- *)
by apply (FROM_ARR _ t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AllDeadlinesMet.
∀ arr_seq sched,
jobs_come_from_arrival_sequence sched arr_seq →
all_deadlines_of_arrivals_met arr_seq sched →
all_deadlines_met sched.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 51)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
============================
forall (arr_seq : arrival_sequence Job) (sched : schedule PState),
jobs_come_from_arrival_sequence sched arr_seq ->
all_deadlines_of_arrivals_met arr_seq sched -> all_deadlines_met sched
----------------------------------------------------------------------------- *)
Proof.
move⇒ arr_seq sched FROM_ARR DL_ARR_MET j t SCHED.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 59)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
FROM_ARR : jobs_come_from_arrival_sequence sched arr_seq
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
job_meets_deadline sched j
----------------------------------------------------------------------------- *)
apply DL_ARR_MET.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 60)
Job : JobType
H : JobCost Job
H0 : JobDeadline Job
H1 : JobArrival Job
PState : eqType
H2 : ProcessorState Job PState
arr_seq : arrival_sequence Job
sched : schedule PState
FROM_ARR : jobs_come_from_arrival_sequence sched arr_seq
DL_ARR_MET : all_deadlines_of_arrivals_met arr_seq sched
j : Job
t : instant
SCHED : scheduled_at sched j t
============================
arrives_in arr_seq j
----------------------------------------------------------------------------- *)
by apply (FROM_ARR _ t).
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End AllDeadlinesMet.