diff --git a/response_time.v b/response_time.v
index 349f083d09314a81ba037cb58edad50a18e5a78f..02d697bb4b7e665c684e1bd53e3eab905ba36c98 100644
--- a/response_time.v
+++ b/response_time.v
@@ -1,10 +1,11 @@
Require Import Vbase task job task_arrival schedule util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+(* Definition of response-time bound and some simple lemmas. *)
Module ResponseTime.
Import Schedule SporadicTaskset SporadicTaskArrival.
-
+
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
@@ -57,16 +58,16 @@ Module ResponseTime.
Section SpecificJob.
- (* Consider any job ...*)
+ (* Then, for any job j ...*)
Variable j: JobIn arr_seq.
- (* ...with response-time bound R in this schedule. *)
+ (* ...with response-time bound R in this schedule, ... *)
Variable R: time.
Hypothesis response_time_bound:
job_has_completed_by j (job_arrival j + R).
- (* The service at any time t' after the response time is 0. *)
- Lemma service_at_after_job_rt_zero :
+ (* the service received by j at any time t' after its response time is 0. *)
+ Lemma service_after_job_rt_zero :
forall t',
t' >= job_arrival j + R ->
service_at rate sched j t' = 0.
@@ -86,8 +87,8 @@ Module ResponseTime.
by rewrite big_nat_recr // /=; apply leq_addl.
Qed.
- (* The cumulative service after the response time is 0. *)
- Lemma sum_service_after_job_rt_zero :
+ (* The same applies for the cumulative service of job j. *)
+ Lemma cumulative_service_after_job_rt_zero :
forall t' t'',
t' >= job_arrival j + R ->
\sum_(t' <= t < t'') service_at rate sched j t = 0.
@@ -96,7 +97,7 @@ Module ResponseTime.
rewrite big_nat_cond; rewrite -> eq_bigr with (F2 := fun i => 0);
first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
intro i; rewrite andbT; move => /andP [LE _].
- by rewrite service_at_after_job_rt_zero;
+ by rewrite service_after_job_rt_zero;
[by ins | by apply leq_trans with (n := t')].
Qed.
@@ -104,33 +105,35 @@ Module ResponseTime.
Section AllJobs.
- (* Assume a task tsk ...*)
+ (* Consider any task tsk ...*)
Variable tsk: sporadic_task.
- (* ...and that R is a response-time bound of tsk in this schedule. *)
+ (* ... for which a response-time bound R is known. *)
Variable R: time.
Hypothesis response_time_bound:
is_response_time_bound_of_task job_cost job_task tsk rate sched R.
+ (* Then, for any job j of this task, ...*)
Variable j: JobIn arr_seq.
Hypothesis H_job_of_task: job_task j = tsk.
- (* The service at any time t' after the response time is 0. *)
- Lemma service_at_after_rt_zero :
+ (* the service received by job j at any time t' after the response time is 0. *)
+ Lemma service_after_task_rt_zero :
forall t',
t' >= job_arrival j + R ->
service_at rate sched j t' = 0.
Proof.
- by ins; apply service_at_after_job_rt_zero with (R := R); [apply response_time_bound |].
+ by ins; apply service_after_job_rt_zero with (R := R); [apply response_time_bound |].
Qed.
- (* The cumulative service after the response time is 0. *)
- Lemma sum_service_after_rt_zero :
+ (* The same applies for the cumulative service of job j. *)
+ Lemma cumulative_service_after_task_rt_zero :
forall t' t'',
t' >= job_arrival j + R ->
\sum_(t' <= t < t'') service_at rate sched j t = 0.
Proof.
- by ins; apply sum_service_after_job_rt_zero with (R := R); [apply response_time_bound |].
+ by ins; apply cumulative_service_after_job_rt_zero with (R := R);
+ first by apply response_time_bound.
Qed.
End AllJobs.
diff --git a/schedulability.v b/schedulability.v
index dbdedb2aca20fb11ac9ae6cfd77a085033bd4680..800bc70a96d1094a3699019759e413006fd37dbf 100644
--- a/schedulability.v
+++ b/schedulability.v
@@ -1,12 +1,14 @@
-Require Import Vbase task schedule
- ssreflect eqtype ssrbool ssrnat seq.
+Require Import Vbase job task schedule util_lemmas
+ ssreflect eqtype ssrbool ssrnat seq bigop.
+(* Definitions of deadline miss. *)
Module Schedulability.
- Import Schedule SporadicTaskset.
+ Import Schedule SporadicTaskset Job.
Section SchedulableDefs.
-
+
+ (* Assume that the cost and deadline of a job is known. *)
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
Variable job_cost: Job -> nat.
@@ -14,13 +16,14 @@ Module Schedulability.
Section ScheduleOfJobs.
+ (* For any job j in schedule sched, ...*)
Context {num_cpus: nat}.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
Variable j: JobIn arr_seq.
- (* Job won't miss its deadline if it is completed by its arrival time plus its (relative) deadline. *)
+ (* job j misses no deadline in sched if it completed by its absolute deadline. *)
Definition job_misses_no_deadline :=
completed job_cost rate sched j (job_arrival j + job_deadline j).
@@ -35,19 +38,20 @@ Module Schedulability.
Variable rate: Job -> processor num_cpus -> nat.
Variable sched: schedule num_cpus arr_seq.
- Variable ts: taskset_of sporadic_task.
+ (* Consider any task tsk. *)
Variable tsk: sporadic_task.
- (* A task doesn't miss its deadline iff all of its jobs don't miss their deadline. *)
+ (* Task tsk doesn't miss its deadline iff all of its jobs don't miss their deadline. *)
Definition task_misses_no_deadline :=
forall (j: JobIn arr_seq),
- job_task j == tsk ->
+ job_task j = tsk ->
job_misses_no_deadline rate sched j.
- (* Whether a task misses a deadline before a particular time. *)
+ (* Task tsk doesn't miss its deadline before time t' iff all of its jobs don't miss
+ their deadline by that time. *)
Definition task_misses_no_deadline_before (t': time) :=
forall (j: JobIn arr_seq),
- job_task j == tsk ->
+ job_task j = tsk ->
job_arrival j + job_deadline j < t' ->
job_misses_no_deadline rate sched j.
@@ -55,4 +59,113 @@ Module Schedulability.
End SchedulableDefs.
+ Section BasicLemmas.
+
+ Context {sporadic_task: eqType}.
+ Variable task_cost: sporadic_task -> nat.
+ Variable task_period: sporadic_task -> nat.
+ Variable task_deadline: sporadic_task -> nat.
+
+ Context {Job: eqType}.
+ Variable job_cost: Job -> nat.
+ Variable job_deadline: Job -> nat.
+ Variable job_task: Job -> sporadic_task.
+
+ Context {arr_seq: arrival_sequence Job}.
+
+ (* Consider any valid schedule... *)
+ Context {num_cpus : nat}.
+ Variable sched: schedule num_cpus arr_seq.
+ Variable rate: Job -> processor num_cpus -> nat.
+
+ (* ... where jobs dont execute after completion. *)
+ Hypothesis H_completed_jobs_dont_execute:
+ completed_jobs_dont_execute job_cost rate sched.
+
+ Section SpecificJob.
+
+ (* Then, for any job j ...*)
+ Variable j: JobIn arr_seq.
+
+ (* ...that doesn't miss a deadline in this schedule, ... *)
+ Hypothesis no_deadline_miss:
+ job_misses_no_deadline job_cost job_deadline rate sched j.
+
+ (* the service received by j at any time t' after its deadline is 0. *)
+ Lemma service_after_job_deadline_zero :
+ forall t',
+ t' >= job_arrival j + job_deadline j ->
+ service_at rate sched j t' = 0.
+ Proof.
+ intros t' LE.
+ rename no_deadline_miss into NOMISS,
+ H_completed_jobs_dont_execute into EXEC.
+ unfold job_misses_no_deadline, completed, completed_jobs_dont_execute in *.
+ apply/eqP; rewrite -leqn0.
+ rewrite <- leq_add2l with (p := job_cost j).
+ move: NOMISS => /eqP NOMISS; rewrite -{1}NOMISS addn0.
+ apply leq_trans with (n := service rate sched j t'.+1); last by apply EXEC.
+ unfold service; rewrite -> big_cat_nat with
+ (p := t'.+1) (n := job_arrival j + job_deadline j);
+ [rewrite leq_add2l /= | by ins | by apply ltnW].
+ by rewrite big_nat_recr // /=; apply leq_addl.
+ Qed.
+
+ (* The same applies for the cumulative service of job j. *)
+ Lemma cumulative_service_after_job_deadline_zero :
+ forall t' t'',
+ t' >= job_arrival j + job_deadline j ->
+ \sum_(t' <= t < t'') service_at rate sched j t = 0.
+ Proof.
+ ins; apply/eqP; rewrite -leqn0.
+ rewrite big_nat_cond; rewrite -> eq_bigr with (F2 := fun i => 0);
+ first by rewrite big_const_seq iter_addn mul0n addn0 leqnn.
+ intro i; rewrite andbT; move => /andP [LE _].
+ by rewrite service_after_job_deadline_zero;
+ [by ins | by apply leq_trans with (n := t')].
+ Qed.
+
+ End SpecificJob.
+
+ Section AllJobs.
+
+ (* Consider any task tsk ...*)
+ Variable tsk: sporadic_task.
+
+ (* ... that doesn't miss any deadline. *)
+ Hypothesis no_deadline_misses:
+ task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
+
+ (* Then, for any valid job j of this task, ...*)
+ Variable j: JobIn arr_seq.
+ Hypothesis H_job_of_task: job_task j = tsk.
+ Hypothesis H_valid_job:
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+
+ (* the service received by job j at any time t' after the deadline is 0. *)
+ Lemma service_after_task_deadline_zero :
+ forall t',
+ t' >= job_arrival j + task_deadline tsk ->
+ service_at rate sched j t' = 0.
+ Proof.
+ rename H_valid_job into PARAMS; unfold valid_sporadic_job in *; des; intros t'.
+ rewrite -H_job_of_task -PARAMS1.
+ by apply service_after_job_deadline_zero, no_deadline_misses.
+ Qed.
+
+ (* The same applies for the cumulative service of job j. *)
+ Lemma cumulative_service_after_task_deadline_zero :
+ forall t' t'',
+ t' >= job_arrival j + task_deadline tsk ->
+ \sum_(t' <= t < t'') service_at rate sched j t = 0.
+ Proof.
+ rename H_valid_job into PARAMS; unfold valid_sporadic_job in *; des; intros t' t''.
+ rewrite -H_job_of_task -PARAMS1.
+ by apply cumulative_service_after_job_deadline_zero, no_deadline_misses.
+ Qed.
+
+ End AllJobs.
+
+ End BasicLemmas.
+
End Schedulability.
\ No newline at end of file
diff --git a/task_arrival.v b/task_arrival.v
index dd35207290a574a6fcc16410ce702b5fca4e30fb..33b59d2278d6874b0e981f6574aeeb0d83e478d6 100644
--- a/task_arrival.v
+++ b/task_arrival.v
@@ -1,12 +1,14 @@
Require Import Vbase task job schedule util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+(* Properties of the job arrival. *)
Module SporadicTaskArrival.
Import SporadicTaskset Schedule.
Section ArrivalModels.
+ (* Assume the task period is known. *)
Context {sporadic_task: eqType}.
Variable task_period: sporadic_task -> nat.
@@ -14,13 +16,14 @@ Import SporadicTaskset Schedule.
Variable arr_seq: arrival_sequence Job.
Variable job_task: Job -> sporadic_task.
- (* We define the sporadic task model *)
+ (* Then, we define the sporadic task model as follows.*)
+
Definition sporadic_task_model :=
forall (j j': JobIn arr_seq),
- j <> j' -> (* Given two different jobs j and j' such that ... *)
- job_task j = job_task j' -> (* ...they are from the same task ... *)
- job_arrival j <= job_arrival j' -> (* ...and arr <= arr'... *)
- (* then the next jobs arrives 'period' time units later. *)
+ j <> j' -> (* Given two different jobs j and j' ... *)
+ job_task j = job_task j' -> (* ... of the same task, ... *)
+ job_arrival j <= job_arrival j' -> (* ... if the arrival of j precedes the arrival of j' ..., *)
+ (* then the arrival of j and the arrival of j' are separated by at least one period. *)
job_arrival j' >= job_arrival j + task_period (job_task j).
End ArrivalModels.