Library prosa.classic.model.schedule.uni.schedulability
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Schedulability.
Import Job SporadicTaskset ArrivalSequence UniprocessorSchedule ResponseTime.
Section DeadlineMisses.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Context {Task: eqType}.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_completed_by := completed_by job_cost sched.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Section Definitions.
Section JobLevel.
Variable j: Job.
Definition job_misses_no_deadline :=
job_completed_by j (job_arrival j + job_deadline j).
End JobLevel.
Section TaskLevel.
Variable tsk: Task.
Definition task_misses_no_deadline :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_misses_no_deadline j.
End TaskLevel.
Section TaskSetLevel.
Variable ts: seq Task.
Definition taskset_misses_no_deadline :=
∀ tsk,
tsk \in ts →
task_misses_no_deadline tsk.
End TaskSetLevel.
End Definitions.
Section Lemmas.
Variable task_cost: Task → time.
Variable task_deadline: Task → time.
Section ResponseTimeIsBounded.
Hypothesis H_job_deadline_eq_task_deadline:
∀ j,
arrives_in arr_seq j →
job_deadline_eq_task_deadline task_deadline job_deadline job_task j.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Variable tsk: Task.
Variable R: time.
Hypothesis H_R_le_deadline: R ≤ task_deadline tsk.
Hypothesis H_response_time_bounded: response_time_bounded_by tsk R.
Lemma task_completes_before_deadline:
task_misses_no_deadline tsk.
End ResponseTimeIsBounded.
End Lemmas.
End DeadlineMisses.
End Schedulability.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.response_time.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Schedulability.
Import Job SporadicTaskset ArrivalSequence UniprocessorSchedule ResponseTime.
Section DeadlineMisses.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Context {Task: eqType}.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Variable sched: schedule Job.
Let job_completed_by := completed_by job_cost sched.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Section Definitions.
Section JobLevel.
Variable j: Job.
Definition job_misses_no_deadline :=
job_completed_by j (job_arrival j + job_deadline j).
End JobLevel.
Section TaskLevel.
Variable tsk: Task.
Definition task_misses_no_deadline :=
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_misses_no_deadline j.
End TaskLevel.
Section TaskSetLevel.
Variable ts: seq Task.
Definition taskset_misses_no_deadline :=
∀ tsk,
tsk \in ts →
task_misses_no_deadline tsk.
End TaskSetLevel.
End Definitions.
Section Lemmas.
Variable task_cost: Task → time.
Variable task_deadline: Task → time.
Section ResponseTimeIsBounded.
Hypothesis H_job_deadline_eq_task_deadline:
∀ j,
arrives_in arr_seq j →
job_deadline_eq_task_deadline task_deadline job_deadline job_task j.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Variable tsk: Task.
Variable R: time.
Hypothesis H_R_le_deadline: R ≤ task_deadline tsk.
Hypothesis H_response_time_bounded: response_time_bounded_by tsk R.
Lemma task_completes_before_deadline:
task_misses_no_deadline tsk.
End ResponseTimeIsBounded.
End Lemmas.
End DeadlineMisses.
End Schedulability.