From 266c9014884ede6888d56e141b6a1c222ac4f5b1 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Wed, 2 Mar 2016 00:03:28 +0100
Subject: [PATCH] Replace nat with time + clean-up code
---
Makefile | 4 +-
analysis/basic/bertogna_edf_comp.v | 37 +++++------
analysis/basic/bertogna_edf_theory.v | 44 ++++++-------
analysis/basic/bertogna_fp_comp.v | 34 +++++-----
analysis/basic/bertogna_fp_theory.v | 36 +++++------
analysis/basic/interference_bound.v | 6 +-
analysis/basic/interference_bound_edf.v | 43 ++++++-------
analysis/basic/interference_bound_fp.v | 6 +-
analysis/basic/workload_bound.v | 32 ++++-----
analysis/jitter/bertogna_edf_comp.v | 28 ++++----
analysis/jitter/bertogna_edf_theory.v | 26 ++++----
analysis/jitter/bertogna_fp_comp.v | 22 +++----
analysis/jitter/bertogna_fp_theory.v | 14 ++--
analysis/jitter/interference_bound.v | 8 +--
analysis/jitter/interference_bound_edf.v | 38 +++++------
analysis/jitter/interference_bound_fp.v | 8 +--
analysis/jitter/workload_bound.v | 75 ++++------------------
analysis/parallel/bertogna_edf_comp.v | 24 +++----
analysis/parallel/bertogna_edf_theory.v | 22 +++----
analysis/parallel/bertogna_fp_comp.v | 18 +++---
analysis/parallel/bertogna_fp_theory.v | 10 +--
analysis/parallel/interference_bound.v | 6 +-
analysis/parallel/interference_bound_edf.v | 28 ++++----
analysis/parallel/interference_bound_fp.v | 6 +-
analysis/parallel/workload_bound.v | 18 +++---
implementation/basic/arrival_sequence.v | 4 +-
implementation/basic/job.v | 7 +-
implementation/basic/schedule.v | 4 +-
implementation/basic/task.v | 10 +--
implementation/jitter/arrival_sequence.v | 4 +-
implementation/jitter/schedule.v | 8 +--
model/basic/arrival_sequence.v | 13 ++--
model/basic/interference.v | 21 +++---
model/basic/interference_edf.v | 8 +--
model/basic/job.v | 18 +++---
model/basic/platform.v | 14 ++--
model/basic/platform_fp.v | 24 +++----
model/basic/priority.v | 6 +-
model/basic/response_time.v | 4 +-
model/basic/schedulability.v | 14 ++--
model/basic/schedule.v | 16 ++---
model/basic/task.v | 17 +++--
model/basic/task_arrival.v | 2 +-
model/basic/time.v | 6 ++
model/basic/workload.v | 2 +-
model/jitter/interference.v | 8 +--
model/jitter/interference_edf.v | 6 +-
model/jitter/job.v | 15 +++--
model/jitter/platform.v | 12 ++--
model/jitter/platform_fp.v | 12 ++--
model/jitter/priority.v | 3 +-
model/jitter/schedule.v | 2 +-
model/jitter/time.v | 4 ++
53 files changed, 412 insertions(+), 445 deletions(-)
create mode 100644 model/basic/time.v
create mode 100644 model/jitter/time.v
diff --git a/Makefile b/Makefile
index 7f42c68ba..f44402392 100644
--- a/Makefile
+++ b/Makefile
@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
-# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
+# coq_makefile -R . rt ./util/ssromega.v ./util/lemmas.v ./util/Vbase.v ./util/divround.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/interference_bound_edf.v ./analysis/basic/interference_bound_fp.v ./analysis/basic/interference_bound.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/basic/workload_bound.v ./analysis/parallel/bertogna_fp_theory.v ./analysis/parallel/interference_bound_edf.v ./analysis/parallel/interference_bound_fp.v ./analysis/parallel/interference_bound.v ./analysis/parallel/bertogna_edf_comp.v ./analysis/parallel/bertogna_fp_comp.v ./analysis/parallel/bertogna_edf_theory.v ./analysis/parallel/workload_bound.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/interference_bound_edf.v ./analysis/jitter/interference_bound_fp.v ./analysis/jitter/interference_bound.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./analysis/jitter/workload_bound.v ./model/basic/time.v ./model/basic/schedulability.v ./model/basic/task.v ./model/basic/task_arrival.v ./model/basic/platform.v ./model/basic/schedule.v ./model/basic/priority.v ./model/basic/interference_edf.v ./model/basic/interference.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.v ./model/basic/platform_fp.v ./model/jitter/time.v ./model/jitter/schedulability.v ./model/jitter/task.v ./model/jitter/task_arrival.v ./model/jitter/platform.v ./model/jitter/schedule.v ./model/jitter/priority.v ./model/jitter/interference_edf.v ./model/jitter/interference.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/jitter/platform_fp.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -118,6 +118,7 @@ VFILES:=util/ssromega.v\
analysis/jitter/bertogna_fp_comp.v\
analysis/jitter/bertogna_edf_theory.v\
analysis/jitter/workload_bound.v\
+ model/basic/time.v\
model/basic/schedulability.v\
model/basic/task.v\
model/basic/task_arrival.v\
@@ -131,6 +132,7 @@ VFILES:=util/ssromega.v\
model/basic/arrival_sequence.v\
model/basic/response_time.v\
model/basic/platform_fp.v\
+ model/jitter/time.v\
model/jitter/schedulability.v\
model/jitter/task.v\
model/jitter/task_arrival.v\
diff --git a/analysis/basic/bertogna_edf_comp.v b/analysis/basic/bertogna_edf_comp.v
index bf08cf899..1746da564 100755
--- a/analysis/basic/bertogna_edf_comp.v
+++ b/analysis/basic/bertogna_edf_comp.v
@@ -7,22 +7,22 @@ Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
- (* In this section, we define the algorithm of Bertogna and Cirinei's
+ (* In this section, we define the algorithm for Bertogna and Cirinei's
response-time analysis for EDF scheduling. *)
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
- (* During the iterations of the algorithm, we pass around pairs
+ (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors. *)
@@ -66,16 +66,15 @@ Module ResponseTimeIterationEDF.
Definition edf_rta_iteration (rt_bounds: seq task_with_response_time) :=
map (update_bound rt_bounds) rt_bounds.
- (* To ensure that the procedure converges, we run the iteration a
- "sufficient" number of times: task_deadline tsk - task_cost tsk + 1.
- This corresponds to the time complexity of the procedure. *)
+ (* To ensure that the procedure converges, we stop the iteration
+ after a "sufficient" number of times, which corresponds to
+ the time complexity of the procedure. *)
Let max_steps (ts: taskset_of sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
- (* This yields the following definition for the RTA. At the end of
- the iteration, we check if all computed response-time bounds
- are less than or equal to the deadline, in which case they are
- valid. *)
+ (* This yields the following definition for the RTA. At the end
+ we check if all computed response-time bounds are less than
+ or equal to the deadline, in which case they are valid. *)
Definition edf_claimed_bounds (ts: taskset_of sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
@@ -368,7 +367,7 @@ Module ResponseTimeIterationEDF.
rewrite (nth_map p0);
last by rewrite size_zip 2!size_map SIZE minnn in LTi.
unfold update_bound, edf_response_time_bound; desf; simpl.
- rename s into tsk_i, s0 into tsk_i', n into R_i, n0 into R_i', Heq into EQ, Heq0 into EQ'.
+ rename s into tsk_i, s0 into tsk_i', t into R_i, t0 into R_i', Heq into EQ, Heq0 into EQ'.
assert (EQtsk: tsk_i = tsk_i').
{
destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
@@ -481,7 +480,9 @@ Module ResponseTimeIterationEDF.
by rewrite in_cons; apply/orP; right; rewrite mem_nth.
}
unfold is_valid_sporadic_task in *.
- destruct (nth elem x1' j) as [tsk_j R_j], (nth elem x2' j) as [tsk_j' R_j'].
+ destruct (nth elem x1' j) as [tsk_j R_j] eqn:SUBST1,
+ (nth elem x2' j) as [tsk_j' R_j'] eqn:SUBST2.
+ rewrite SUBST1 SUBST2 in LEj; clear SUBST1 SUBST2.
simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
by apply interference_bound_edf_monotonic.
}
@@ -658,7 +659,7 @@ Module ResponseTimeIterationEDF.
unfold update_bound; destruct i; simpl.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
- by rewrite iterS; apply/mapP; exists (s, n).
+ by rewrite iterS; apply/mapP; exists (s, t).
}
rewrite -2!big_seq_cond.
diff --git a/analysis/basic/bertogna_edf_theory.v b/analysis/basic/bertogna_edf_theory.v
index 8926eb424..5fff07bc4 100644
--- a/analysis/basic/bertogna_edf_theory.v
+++ b/analysis/basic/bertogna_edf_theory.v
@@ -18,13 +18,13 @@ Module ResponseTimeAnalysisEDF.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
@@ -56,28 +56,30 @@ Module ResponseTimeAnalysisEDF.
num_cpus > 0.
(* Assume that we have a task set where all tasks have valid
- parameters and restricted deadlines. *)
+ parameters and restricted deadlines, ... *)
Variable ts: taskset_of sporadic_task.
- Hypothesis H_all_jobs_from_taskset:
- forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_restricted_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
+ (* ... and that all jobs in the arrival sequence come from the task set. *)
+ Hypothesis H_all_jobs_from_taskset:
+ forall (j: JobIn arr_seq), job_task j \in ts.
+
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
- (* Assume a known response-time bound R is known... *)
+ (* Assume that a response-time bound R is known... *)
Let task_with_response_time := (sporadic_task * time)%type.
Variable rt_bounds: seq task_with_response_time.
- (* ...for any task in the task set. *)
+ (* ...for any task in the task set, ... *)
Hypothesis H_rt_bounds_contains_all_tasks: unzip1 rt_bounds = ts.
- (* Also, assume that R is a fixed-point of the response-time recurrence, ... *)
+ (* ... such that R is a fixed-point of the response-time recurrence, ... *)
Let I (tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Hypothesis H_response_time_is_fixed_point :
@@ -94,10 +96,9 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
- (* Assume that the task set has no duplicates. Otherwise, counting
- the number of tasks that have some property does not make sense
- (for example, for stating the global scheduling invariant as
- using number of scheduled interfering tasks = number of cpus). *)
+ (* Assume that the task set has no duplicates. This is required to
+ avoid problems when counting tasks (for example, when stating
+ that the number of interfering tasks is at most num_cpus). *)
Hypothesis H_ts_is_a_set : uniq ts.
(* In order to prove that R is a response-time bound, we first present some lemmas. *)
@@ -108,14 +109,14 @@ Module ResponseTimeAnalysisEDF.
Variable R: time.
Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.
- (* Consider any job j of tsk. *)
+ (* Consider any job j of tsk ... *)
Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk.
- (* Assume that job j did not complete on time, ... *)
+ (* ... that did not complete on time, ... *)
Hypothesis H_j_not_completed: ~~ completed job_cost sched j (job_arrival j + R).
- (* and that it is the first job not to satisfy its response-time bound. *)
+ (* ... and that is the first job not to satisfy its response-time bound. *)
Hypothesis H_all_previous_jobs_completed_on_time :
forall (j_other: JobIn arr_seq) tsk_other R_other,
job_task j_other = tsk_other ->
@@ -154,13 +155,13 @@ Module ResponseTimeAnalysisEDF.
Variable R_other: time.
Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in rt_bounds.
- (* Note that tsk_other is in task set ts ...*)
+ (* Note that tsk_other is in the task set, ...*)
Lemma bertogna_edf_tsk_other_in_ts: tsk_other \in ts.
Proof.
by rewrite -H_rt_bounds_contains_all_tasks; apply/mapP; exists (tsk_other, R_other).
Qed.
- (* Also, R_other is larger than the cost of tsk_other. *)
+ (* ... and R_other is larger than the cost of tsk_other. *)
Lemma bertogna_edf_R_other_ge_cost :
R_other >= task_cost tsk_other.
Proof.
@@ -193,7 +194,7 @@ Module ResponseTimeAnalysisEDF.
| by ins; apply BEFOREok with (tsk_other := tsk_other)].
Qed.
- (* Recall that the edf-specific interference bound also holds. *)
+ (* Recall that the edf-specific interference bound also holds for tsk_other. *)
Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
@@ -210,7 +211,6 @@ Module ResponseTimeAnalysisEDF.
(* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction.
-
(* 0) Since job j did not complete by its response time bound, it follows that
the total interference X >= R - e_k + 1. *)
Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
diff --git a/analysis/basic/bertogna_fp_comp.v b/analysis/basic/bertogna_fp_comp.v
index f88f6eb50..d5a4de3e7 100644
--- a/analysis/basic/bertogna_fp_comp.v
+++ b/analysis/basic/bertogna_fp_comp.v
@@ -12,17 +12,17 @@ Module ResponseTimeIterationFP.
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
- (* During the iterations of the algorithm, we pass around pairs
+ (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors, ... *)
@@ -177,7 +177,7 @@ Module ResponseTimeIterationFP.
Qed.
(* If the analysis suceeds, the computed response-time bounds are no larger
- than the deadline. *)
+ than the deadlines ... *)
Lemma fp_claimed_bounds_le_deadline :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
@@ -215,8 +215,7 @@ Module ResponseTimeIterationFP.
}
Qed.
- (* If the analysis succeeds, the computed response-time bounds are no smaller
- than the task cost. *)
+ (* ... and no smaller than the task costs. *)
Lemma fp_claimed_bounds_ge_cost :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
@@ -412,7 +411,7 @@ Module ResponseTimeIterationFP.
}
Qed.
- (* If the iteration converged at an earlier step, then it remains stable. *)
+ (* If the iteration converged at an earlier step, it remains as a fixed point. *)
Lemma bertogna_fp_comp_f_converges_early :
(exists k, k <= max_steps tsk /\ f k = f k.+1) ->
f (max_steps tsk) = f (max_steps tsk).+1.
@@ -517,10 +516,9 @@ Module ResponseTimeIterationFP.
Variable ts: taskset_of sporadic_task.
(* Assume that higher_priority is a total strict order (<).
- TODO: it doesn't have to be total over the entire domain, but
- only within the task set.
- But to weaken the hypothesis, we need to re-prove some lemmas
- from ssreflect. *)
+ TODO: it doesn't have to be total over the universe of tasks,
+ but only within the task set. However, to weaken this hypothesis
+ we need to re-prove some lemmas from ssreflect. *)
Hypothesis H_irreflexive: irreflexive higher_priority.
Hypothesis H_transitive: transitive higher_priority.
Hypothesis H_unique_priorities: antisymmetric higher_priority.
@@ -547,7 +545,7 @@ Module ResponseTimeIterationFP.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
- (* ...they have valid parameters,...*)
+ (* ...jobs have valid parameters,...*)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
@@ -587,8 +585,8 @@ Module ResponseTimeIterationFP.
(* In the following theorem, we prove that any response-time bound contained
in fp_claimed_bounds is safe. The proof follows by induction on the task set:
- Induction hypothesis: all higher-priority tasks have safe response-time bounds.
- Inductive step: We prove that the response-time bound of the current task is safe.
+ Induction hypothesis: assume all higher-priority tasks have safe response-time bounds.
+ Inductive step: we prove that the response-time bound of the current task is safe.
Note that the inductive step is a direct application of the main Theorem from
bertogna_fp_theory.v. *)
diff --git a/analysis/basic/bertogna_fp_theory.v b/analysis/basic/bertogna_fp_theory.v
index 70dbe9235..d0677e4c1 100644
--- a/analysis/basic/bertogna_fp_theory.v
+++ b/analysis/basic/bertogna_fp_theory.v
@@ -15,13 +15,13 @@ Module ResponseTimeAnalysisFP.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
@@ -52,8 +52,9 @@ Module ResponseTimeAnalysisFP.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
- (* Assume that we have a task set (with no duplicates) where all jobs
- come from the task set and all tasks have valid parameters and restricted deadlines. *)
+ (* Consider a task set ts with no duplicates where all jobs
+ come from the task set and all tasks have valid parameters
+ and restricted deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_ts_is_a_set: uniq ts.
Hypothesis H_all_jobs_from_taskset:
@@ -72,24 +73,21 @@ Module ResponseTimeAnalysisFP.
Let is_response_time_bound (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
- (* Assume a known response-time bound for any interfering task *)
- Let task_with_response_time := (sporadic_task * time)%type.
- Variable hp_bounds: seq task_with_response_time.
-
- (* For FP scheduling, assume there exists a fixed task priority. *)
+ (* Assume a given FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
-
Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.
-
- (* Assume that hp_bounds has exactly the tasks that interfere with tsk,... *)
- Hypothesis H_hp_bounds_has_interfering_tasks:
- [seq tsk_hp <- ts | can_interfere_with_tsk tsk_hp] = unzip1 hp_bounds.
- (* ...and that all values in the pairs contain valid response-time bounds *)
+ (* Assume a response-time bound is known... *)
+ Let task_with_response_time := (sporadic_task * time)%type.
+ Variable hp_bounds: seq task_with_response_time.
Hypothesis H_response_time_of_interfering_tasks_is_known:
forall hp_tsk R,
(hp_tsk, R) \in hp_bounds ->
is_response_time_bound_of_task job_cost job_task hp_tsk sched R.
+
+ (* ... for any task in ts that interferes with tsk. *)
+ Hypothesis H_hp_bounds_has_interfering_tasks:
+ [seq tsk_hp <- ts | can_interfere_with_tsk tsk_hp] = unzip1 hp_bounds.
(* Assume that the response-time bounds are larger than task costs. *)
Hypothesis H_response_time_bounds_ge_cost:
@@ -169,7 +167,7 @@ Module ResponseTimeAnalysisFP.
by apply/mapP; exists (tsk_other, R_other).
Qed.
- (*... and interferes with task tsk. *)
+ (*... and interferes with tsk. *)
Lemma bertogna_fp_tsk_other_interferes: can_interfere_with_tsk tsk_other.
Proof.
rename H_hp_bounds_has_interfering_tasks into UNZIP,
diff --git a/analysis/basic/interference_bound.v b/analysis/basic/interference_bound.v
index ff252c3b0..cee67ea8e 100644
--- a/analysis/basic/interference_bound.v
+++ b/analysis/basic/interference_bound.v
@@ -11,9 +11,9 @@ Module InterferenceBoundGeneric.
Import Schedule WorkloadBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/basic/interference_bound_edf.v b/analysis/basic/interference_bound_edf.v
index fd1d6876c..b56b2da2e 100644
--- a/analysis/basic/interference_bound_edf.v
+++ b/analysis/basic/interference_bound_edf.v
@@ -19,9 +19,9 @@ Module InterferenceBoundEDF.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -29,7 +29,7 @@ Module InterferenceBoundEDF.
(* Consider the interference incurred by tsk in a window of length delta... *)
Variable delta: time.
- (* due to a different task tsk_other, with response-time bound R_other. *)
+ (* ... due to a different task tsk_other, with response-time bound R_other. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
@@ -50,9 +50,9 @@ Module InterferenceBoundEDF.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -78,7 +78,7 @@ Module InterferenceBoundEDF.
(* ... with and EDF-specific interference bound, ... *)
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
- (* Bertogna and Cirinei define the following interference bound
+ (* ... Bertogna and Cirinei define the following interference bound
under EDF scheduling. *)
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
@@ -105,13 +105,13 @@ Module InterferenceBoundEDF.
Import Schedule Interference Platform SporadicTaskset.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
@@ -142,8 +142,8 @@ Module InterferenceBoundEDF.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
- (* Assume that we have a task set where all tasks have valid
- parameters and restricted deadlines. *)
+ (* Consider a task set ts where all jobs come from the task set
+ and tasks have valid parameters and restricted deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
@@ -166,7 +166,7 @@ Module InterferenceBoundEDF.
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
- (* and j_i one of its jobs. *)
+ (* ... and j_i one of its jobs. *)
Variable j_i: JobIn arr_seq.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
@@ -224,8 +224,7 @@ Module InterferenceBoundEDF.
Let earlier_arrival := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
Let sorted_jobs := (sort earlier_arrival interfering_jobs).
- (* Now we proceed with the proof.
- The first step consists in simplifying the sum corresponding to the workload. *)
+ (* Now we proceed with the proof. The first step consists in simplifying the sum corresponding to the workload. *)
Section SimplifyJobSequence.
(* Use the alternative definition of task interference, based on
@@ -292,7 +291,7 @@ Module InterferenceBoundEDF.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.
- (* Also, for any job of task tsk_k, the interference is bounded by the task cost. *)
+ (* Finally, for any job of task tsk_k, the interference is bounded by the task cost. *)
Lemma interference_bound_edf_interference_le_task_cost :
forall j,
j \in interfering_jobs ->
@@ -1122,9 +1121,9 @@ Module InterferenceBoundEDF.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
diff --git a/analysis/basic/interference_bound_fp.v b/analysis/basic/interference_bound_fp.v
index aab131355..6e1887a86 100644
--- a/analysis/basic/interference_bound_fp.v
+++ b/analysis/basic/interference_bound_fp.v
@@ -13,9 +13,9 @@ Module InterferenceBoundFP.
Section Definitions.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/basic/workload_bound.v b/analysis/basic/workload_bound.v
index 65fc799c4..5ef65e4cf 100644
--- a/analysis/basic/workload_bound.v
+++ b/analysis/basic/workload_bound.v
@@ -12,18 +12,20 @@ Module WorkloadBound.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
-
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+
+ (* Consider any task tsk with response-time bound R_tsk,
+ that is scheduled in an interval of length delta. *)
Variable tsk: sporadic_task.
- Variable R_tsk: time. (* Known response-time bound for the task *)
- Variable delta: time. (* Length of the interval *)
+ Variable R_tsk: time.
+ Variable delta: time.
- (* Bound on the number of jobs that execute completely in the interval *)
+ (* Based on the number of jobs that execute completely in the interval, ... *)
Definition max_jobs :=
div_floor (delta + R_tsk - task_cost tsk) (task_period tsk).
- (* Bertogna and Cirinei's bound on the workload of a task in an interval of length delta *)
+ (* ... Bertogna and Cirinei's workload bound is defined as follows. *)
Definition W :=
let e_k := (task_cost tsk) in
let p_k := (task_period tsk) in
@@ -34,13 +36,13 @@ Module WorkloadBound.
Section BasicLemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
(* Let tsk be any task...*)
Variable tsk: sporadic_task.
- (* ...with period > 0. *)
+ (* ... with period > 0. *)
Hypothesis H_period_positive: task_period tsk > 0.
(* Let R1 <= R2 be two response-time bounds that
@@ -115,14 +117,14 @@ Module WorkloadBound.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_deadline: Job -> nat.
+ Variable job_deadline: Job -> time.
Variable arr_seq: arrival_sequence Job.
diff --git a/analysis/jitter/bertogna_edf_comp.v b/analysis/jitter/bertogna_edf_comp.v
index 157b3c3dd..e5f19c9f2 100755
--- a/analysis/jitter/bertogna_edf_comp.v
+++ b/analysis/jitter/bertogna_edf_comp.v
@@ -7,25 +7,25 @@ Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDFJitter.
- (* In this section, we define the algorithm of Bertogna and Cirinei's
+ (* In this section, we define the algorithm for Bertogna and Cirinei's
response-time analysis for EDF scheduling. *)
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
- (* During the iterations of the algorithm, we pass around pairs
+ (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Consider a platform with num_cpus processors. *)
Variable num_cpus: nat.
@@ -421,7 +421,7 @@ Module ResponseTimeIterationEDF.
rewrite (nth_map p0);
last by rewrite size_zip 2!size_map SIZE minnn in LTi.
unfold update_bound, edf_response_time_bound; desf; simpl.
- rename s into tsk_i, s0 into tsk_i', n into R_i, n0 into R_i', Heq into EQ, Heq0 into EQ'.
+ rename s into tsk_i, s0 into tsk_i', t into R_i, t0 into R_i', Heq into EQ, Heq0 into EQ'.
assert (EQtsk: tsk_i = tsk_i').
{
destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
@@ -535,7 +535,9 @@ Module ResponseTimeIterationEDF.
by rewrite in_cons; apply/orP; right; rewrite mem_nth.
}
unfold is_valid_sporadic_task in *.
- destruct (nth elem x1' j) as [tsk_j R_j], (nth elem x2' j) as [tsk_j' R_j'].
+ destruct (nth elem x1' j) as [tsk_j R_j] eqn:SIMPL1,
+ (nth elem x2' j) as [tsk_j' R_j'] eqn:SIMPL2.
+ rewrite SIMPL1 SIMPL2 in LEj.
simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
by apply interference_bound_edf_monotonic.
}
@@ -712,7 +714,7 @@ Module ResponseTimeIterationEDF.
unfold update_bound; destruct i; simpl.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
- by rewrite iterS; apply/mapP; exists (s, n).
+ by rewrite iterS; apply/mapP; exists (s, t).
}
rewrite -2!big_seq_cond.
diff --git a/analysis/jitter/bertogna_edf_theory.v b/analysis/jitter/bertogna_edf_theory.v
index 078b02faf..834c6b633 100644
--- a/analysis/jitter/bertogna_edf_theory.v
+++ b/analysis/jitter/bertogna_edf_theory.v
@@ -19,16 +19,16 @@ Module ResponseTimeAnalysisEDFJitter.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
@@ -59,8 +59,9 @@ Module ResponseTimeAnalysisEDFJitter.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
- (* Assume that we have a task set where all tasks have valid
- parameters and restricted deadlines. *)
+ (* Assume that we have a task set ts, such that all jobs come
+ from the task set, and all tasks have valid parameters and
+ restricted deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
@@ -99,10 +100,9 @@ Module ResponseTimeAnalysisEDFJitter.
Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).
- (* Assume that the task set has no duplicates. Otherwise, counting
- the number of tasks that have some property does not make sense
- (for example, for stating the global scheduling invariant as
- using number of scheduled interfering tasks = number of cpus). *)
+ (* Assume that the task set has no duplicates. This is required to
+ avoid problems when counting tasks (for example, when stating
+ that the number of interfering tasks is at most num_cpus). *)
Hypothesis H_ts_is_a_set : uniq ts.
(* In order to prove that R is a response-time bound, we first present some lemmas. *)
diff --git a/analysis/jitter/bertogna_fp_comp.v b/analysis/jitter/bertogna_fp_comp.v
index f190d36d3..9098c969a 100644
--- a/analysis/jitter/bertogna_fp_comp.v
+++ b/analysis/jitter/bertogna_fp_comp.v
@@ -12,20 +12,20 @@ Module ResponseTimeIterationFP.
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* During the iterations of the algorithm, we pass around pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Consider a platform with num_cpus processors, ... *)
Variable num_cpus: nat.
@@ -179,7 +179,7 @@ Module ResponseTimeIterationFP.
Qed.
(* If the analysis suceeds, the computed response-time bounds are no larger
- than the deadline. *)
+ than the deadlines... *)
Lemma fp_claimed_bounds_le_deadline :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
@@ -217,8 +217,8 @@ Module ResponseTimeIterationFP.
}
Qed.
- (* If the analysis succeeds, the computed response-time bounds are no smaller
- than the task cost. *)
+ (* ... and the computed response-time bounds are no smaller
+ than the task costs. *)
Lemma fp_claimed_bounds_ge_cost :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
diff --git a/analysis/jitter/bertogna_fp_theory.v b/analysis/jitter/bertogna_fp_theory.v
index 171bd5421..7df3938f8 100644
--- a/analysis/jitter/bertogna_fp_theory.v
+++ b/analysis/jitter/bertogna_fp_theory.v
@@ -16,16 +16,16 @@ Module ResponseTimeAnalysisFP.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
diff --git a/analysis/jitter/interference_bound.v b/analysis/jitter/interference_bound.v
index a56e762ac..7e2dfb6cd 100644
--- a/analysis/jitter/interference_bound.v
+++ b/analysis/jitter/interference_bound.v
@@ -12,10 +12,10 @@ Module InterferenceBoundJitter.
Section Definitions.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/jitter/interference_bound_edf.v b/analysis/jitter/interference_bound_edf.v
index ce7fea420..0b0857420 100644
--- a/analysis/jitter/interference_bound_edf.v
+++ b/analysis/jitter/interference_bound_edf.v
@@ -18,10 +18,10 @@ Module InterferenceBoundEDFJitter.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -51,10 +51,10 @@ Module InterferenceBoundEDFJitter.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -107,16 +107,16 @@ Module InterferenceBoundEDFJitter.
Import ScheduleWithJitter Interference Platform SporadicTaskset.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
@@ -1214,10 +1214,10 @@ Module InterferenceBoundEDFJitter.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
diff --git a/analysis/jitter/interference_bound_fp.v b/analysis/jitter/interference_bound_fp.v
index ae11e1809..29a891261 100644
--- a/analysis/jitter/interference_bound_fp.v
+++ b/analysis/jitter/interference_bound_fp.v
@@ -13,10 +13,10 @@ Module InterferenceBoundFP.
Section Definitions.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/jitter/workload_bound.v b/analysis/jitter/workload_bound.v
index b8c731a56..e866ffe50 100644
--- a/analysis/jitter/workload_bound.v
+++ b/analysis/jitter/workload_bound.v
@@ -13,9 +13,9 @@ Module WorkloadBoundJitter.
Section WorkloadBoundJitterDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Variable tsk: sporadic_task.
Variable R_tsk: time. (* Known response-time bound for the task *)
@@ -36,9 +36,9 @@ Module WorkloadBoundJitter.
Section BasicLemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
(* Let tsk be any task...*)
Variable tsk: sporadic_task.
@@ -118,16 +118,16 @@ Module WorkloadBoundJitter.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_deadline: Job -> nat.
- Variable job_jitter: Job -> nat.
+ Variable job_deadline: Job -> time.
+ Variable job_jitter: Job -> time.
Variable arr_seq: arrival_sequence Job.
@@ -567,55 +567,6 @@ Module WorkloadBoundJitter.
by rewrite subh3 // addnC; move: INnth => /eqP INnth; rewrite -INnth.
Qed.
- (* Now, we prove an auxiliary lemma for the next result.
- The statement is not meaningful, since it's part of a proof
- by contradiction. *)
- (*Lemma workload_bound_helper_lemma :
- job_arrival j_fst + task_period tsk + delta <= job_arrival j_lst ->
- t1 <= job_arrival j_fst + task_deadline tsk.
- Proof.
- intros LE.
- rename H_jobs_have_valid_parameters into PARAMS,
- H_completed_jobs_dont_execute into EXEC,
- H_no_deadline_misses_during_interval into NOMISS.
- unfold task_misses_no_deadline_before, valid_sporadic_job,
- job_misses_no_deadline, completed in *; des.
- exploit workload_bound_all_jobs_from_tsk.
- {
- apply mem_nth; instantiate (1 := 0).
- apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
- }
- instantiate (1 := elem); move => [FSTtsk [/eqP FSTserv FSTin]].
- exploit (NOMISS j_fst FSTtsk); last intros COMP.
- {
- (* Prove that arr_fst + d_k <= t2 *)
- apply leq_ltn_trans with (n := job_arrival j_lst);
- last by apply workload_bound_last_job_arrives_before_end_of_interval.
- apply leq_trans with (n := job_arrival j_fst + task_period tsk + delta); last by done.
- rewrite -addnA leq_add2l -[job_deadline _]addn0.
- apply leq_add; last by ins.
- specialize (PARAMS j_fst); des.
- by rewrite PARAMS1 FSTtsk H_restricted_deadline.
- }
- rewrite leqNgt; apply/negP; unfold not; intro LTt1.
- (* Now we assume that (job_arrival j_fst + d_k < t1) and reach a contradiction.
- Since j_fst doesn't miss deadlines, then the service it receives between t1 and t2
- equals 0, which contradicts the previous assumption that j_fst interferes in
- the scheduling window. *)
- apply FSTserv.
- {
- unfold service_during; apply/eqP; rewrite -leqn0.
- rewrite <- leq_add2l with (p := job_cost j_fst); rewrite addn0.
- move: COMP => /eqP COMP; unfold service in COMP; rewrite -{1}COMP.
- apply leq_trans with (n := service sched j_fst t2); last by apply EXEC.
- unfold service; rewrite -> big_cat_nat with (m := 0) (p := t2) (n := t1);
- [rewrite leq_add2r /= | by ins | by apply leq_addr].
- rewrite -> big_cat_nat with (p := t1) (n := job_arrival j_fst + job_deadline j_fst);
- [by rewrite /= -{1}[\sum_(_ <= _ < _) _]addn0 leq_add2l | by ins | ].
- by apply ltnW; specialize (PARAMS j_fst); des; rewrite PARAMS1 FSTtsk.
- }
- Qed.*)
-
(* Prove that n_k is at least the number of the middle jobs *)
Lemma workload_bound_n_k_covers_middle_jobs :
n_k >= num_mid_jobs.
diff --git a/analysis/parallel/bertogna_edf_comp.v b/analysis/parallel/bertogna_edf_comp.v
index ca57b3471..201ccdf88 100755
--- a/analysis/parallel/bertogna_edf_comp.v
+++ b/analysis/parallel/bertogna_edf_comp.v
@@ -7,22 +7,22 @@ Module ResponseTimeIterationEDF.
Import ResponseTimeAnalysisEDF.
- (* In this section, we define the algorithm of Bertogna and Cirinei's
+ (* In this section, we define the algorithm for Bertogna and Cirinei's
response-time analysis for EDF scheduling. *)
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
- (* During the iterations of the algorithm, we pass around pairs
+ (* As input for each iteration of the algorithm, we consider pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors. *)
@@ -368,7 +368,7 @@ Module ResponseTimeIterationEDF.
rewrite (nth_map p0);
last by rewrite size_zip 2!size_map SIZE minnn in LTi.
unfold update_bound, edf_response_time_bound; desf; simpl.
- rename s into tsk_i, s0 into tsk_i', n into R_i, n0 into R_i', Heq into EQ, Heq0 into EQ'.
+ rename s into tsk_i, s0 into tsk_i', t into R_i, t0 into R_i', Heq into EQ, Heq0 into EQ'.
assert (EQtsk: tsk_i = tsk_i').
{
destruct p0 as [tsk0 R0], p0' as [tsk0' R0']; simpl in H2; subst.
@@ -481,7 +481,9 @@ Module ResponseTimeIterationEDF.
by rewrite in_cons; apply/orP; right; rewrite mem_nth.
}
unfold is_valid_sporadic_task in *.
- destruct (nth elem x1' j) as [tsk_j R_j], (nth elem x2' j) as [tsk_j' R_j'].
+ destruct (nth elem x1' j) as [tsk_j R_j] eqn:SUBST1,
+ (nth elem x2' j) as [tsk_j' R_j'] eqn:SUBST2.
+ rewrite SUBST1 SUBST2 in LEj.
simpl in FSTeq; rewrite -FSTeq; simpl in LEj; simpl in VALIDj; des.
by apply interference_bound_edf_monotonic.
}
@@ -658,7 +660,7 @@ Module ResponseTimeIterationEDF.
unfold update_bound; destruct i; simpl.
rewrite subh1; first by rewrite -addnBA // subnn addn0.
apply (edf_claimed_bounds_ge_cost ts step.+1).
- by rewrite iterS; apply/mapP; exists (s, n).
+ by rewrite iterS; apply/mapP; exists (s, t).
}
rewrite -2!big_seq_cond.
diff --git a/analysis/parallel/bertogna_edf_theory.v b/analysis/parallel/bertogna_edf_theory.v
index c43712be3..ace04e2b3 100644
--- a/analysis/parallel/bertogna_edf_theory.v
+++ b/analysis/parallel/bertogna_edf_theory.v
@@ -18,13 +18,13 @@ Module ResponseTimeAnalysisEDF.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
@@ -52,8 +52,9 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_at_least_one_cpu :
num_cpus > 0.
- (* Assume that we have a task set where all tasks have valid
- parameters and restricted deadlines. *)
+ (* Assume that we have a task set ts such that all jobs come from
+ the task set, and all tasks have valid parameters and
+ restricted deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
@@ -91,10 +92,9 @@ Module ResponseTimeAnalysisEDF.
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).
- (* Assume that the task set has no duplicates. Otherwise, counting
- the number of tasks that have some property does not make sense
- (for example, for stating the global scheduling invariant as
- using number of scheduled interfering tasks = number of cpus). *)
+ (* Assume that the task set has no duplicates. This is required to
+ avoid problems when counting tasks (for example, when stating
+ that the number of interfering tasks is at most num_cpus). *)
Hypothesis H_ts_is_a_set : uniq ts.
(* In order to prove that R is a response-time bound, we first present some lemmas. *)
diff --git a/analysis/parallel/bertogna_fp_comp.v b/analysis/parallel/bertogna_fp_comp.v
index 824d2855f..d38f68d65 100644
--- a/analysis/parallel/bertogna_fp_comp.v
+++ b/analysis/parallel/bertogna_fp_comp.v
@@ -12,17 +12,17 @@ Module ResponseTimeIterationFP.
Section Analysis.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* During the iterations of the algorithm, we pass around pairs
of tasks and computed response-time bounds. *)
- Let task_with_response_time := (sporadic_task * nat)%type.
+ Let task_with_response_time := (sporadic_task * time)%type.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Consider a platform with num_cpus processors, ... *)
@@ -177,7 +177,7 @@ Module ResponseTimeIterationFP.
Qed.
(* If the analysis suceeds, the computed response-time bounds are no larger
- than the deadline. *)
+ than the deadline... *)
Lemma fp_claimed_bounds_le_deadline :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
@@ -215,8 +215,8 @@ Module ResponseTimeIterationFP.
}
Qed.
- (* If the analysis succeeds, the computed response-time bounds are no smaller
- than the task cost. *)
+ (* ... and the computed response-time bounds are no smaller than
+ the task costs. *)
Lemma fp_claimed_bounds_ge_cost :
forall ts' rt_bounds tsk R,
fp_claimed_bounds ts' = Some rt_bounds ->
diff --git a/analysis/parallel/bertogna_fp_theory.v b/analysis/parallel/bertogna_fp_theory.v
index 719ccb555..aeaf7730f 100644
--- a/analysis/parallel/bertogna_fp_theory.v
+++ b/analysis/parallel/bertogna_fp_theory.v
@@ -15,13 +15,13 @@ Module ResponseTimeAnalysisFP.
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
diff --git a/analysis/parallel/interference_bound.v b/analysis/parallel/interference_bound.v
index 8b2c0f1f6..0bd5d4567 100644
--- a/analysis/parallel/interference_bound.v
+++ b/analysis/parallel/interference_bound.v
@@ -11,9 +11,9 @@ Module InterferenceBoundGeneric.
Import Schedule WorkloadBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/parallel/interference_bound_edf.v b/analysis/parallel/interference_bound_edf.v
index d38b48efc..e2148326c 100644
--- a/analysis/parallel/interference_bound_edf.v
+++ b/analysis/parallel/interference_bound_edf.v
@@ -19,9 +19,9 @@ Module InterferenceBoundEDF.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -49,9 +49,9 @@ Module InterferenceBoundEDF.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
@@ -104,13 +104,13 @@ Module InterferenceBoundEDF.
Import Schedule Interference Platform SporadicTaskset.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
@@ -774,9 +774,9 @@ Module InterferenceBoundEDF.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
diff --git a/analysis/parallel/interference_bound_fp.v b/analysis/parallel/interference_bound_fp.v
index 061d1dc52..0760ecf0a 100644
--- a/analysis/parallel/interference_bound_fp.v
+++ b/analysis/parallel/interference_bound_fp.v
@@ -13,9 +13,9 @@ Module InterferenceBoundFP.
Section Definitions.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
diff --git a/analysis/parallel/workload_bound.v b/analysis/parallel/workload_bound.v
index abec94d01..5309d07da 100644
--- a/analysis/parallel/workload_bound.v
+++ b/analysis/parallel/workload_bound.v
@@ -12,8 +12,8 @@ Module WorkloadBound.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
Variable tsk: sporadic_task.
Variable R_tsk: time. (* Known response-time bound for the task *)
@@ -31,8 +31,8 @@ Module WorkloadBound.
Section BasicLemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
(* Let tsk be any task...*)
Variable tsk: sporadic_task.
@@ -65,14 +65,14 @@ Module WorkloadBound.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_deadline: Job -> nat.
+ Variable job_deadline: Job -> time.
Variable arr_seq: arrival_sequence Job.
diff --git a/implementation/basic/arrival_sequence.v b/implementation/basic/arrival_sequence.v
index 723f77487..0682bec69 100644
--- a/implementation/basic/arrival_sequence.v
+++ b/implementation/basic/arrival_sequence.v
@@ -37,11 +37,9 @@ Module ConcreteArrivalSequence.
Let arr_seq := periodic_arrival_sequence ts.
(* ... every job comes from the task set, ... *)
- (* TODO: It's supposed to be job_task j, but I don't know yet how to
- fix the coercion. *)
Theorem periodic_arrivals_all_jobs_from_taskset:
forall (j: JobIn arr_seq),
- job_task (_job_in arr_seq j) \in ts.
+ job_task (_job_in arr_seq j) \in ts. (* TODO: fix coercion. *)
Proof.
intros j.
destruct j as [j arr ARRj]; simpl.
diff --git a/implementation/basic/job.v b/implementation/basic/job.v
index ba32c5366..dfc61354b 100644
--- a/implementation/basic/job.v
+++ b/implementation/basic/job.v
@@ -1,10 +1,11 @@
Add LoadPath "../../" as rt.
-Require Import rt.util.Vbase.
+Require Import rt.model.basic.time rt.util.Vbase.
Require Import rt.implementation.basic.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteJob.
+ Import Time.
Import ConcreteTask.
Section Defs.
@@ -13,8 +14,8 @@ Module ConcreteJob.
Record concrete_job :=
{
job_id: nat;
- job_cost: nat;
- job_deadline: nat;
+ job_cost: time;
+ job_deadline: time;
job_task: concrete_task_eqType
}.
diff --git a/implementation/basic/schedule.v b/implementation/basic/schedule.v
index 0a546122e..d39bb5544 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/basic/schedule.v
@@ -11,7 +11,7 @@ Module ConcreteScheduler.
Section Implementation.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
(* Let num_cpus denote the number of processors, ...*)
Variable num_cpus: nat.
@@ -60,7 +60,7 @@ Module ConcreteScheduler.
Section Proofs.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
(* Assume a positive number of processors. *)
Variable num_cpus: nat.
diff --git a/implementation/basic/task.v b/implementation/basic/task.v
index 30c7a8965..a8f9c7aa9 100644
--- a/implementation/basic/task.v
+++ b/implementation/basic/task.v
@@ -1,11 +1,11 @@
Add LoadPath "../../" as rt.
-Require Import rt.util.Vbase.
+Require Import rt.model.basic.time rt.util.Vbase.
Require Import rt.model.basic.task.
Require Import ssreflect ssrbool ssrnat eqtype seq.
Module ConcreteTask.
- Import SporadicTaskset.
+ Import Time SporadicTaskset.
Section Defs.
@@ -13,9 +13,9 @@ Module ConcreteTask.
Record concrete_task :=
{
task_id: nat; (* for uniqueness *)
- task_cost: nat;
- task_period: nat;
- task_deadline: nat
+ task_cost: time;
+ task_period: time;
+ task_deadline: time
}.
(* To make it compatible with ssreflect, we define a decidable
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/jitter/arrival_sequence.v
index e50701dc8..58d9fa4f4 100644
--- a/implementation/jitter/arrival_sequence.v
+++ b/implementation/jitter/arrival_sequence.v
@@ -37,11 +37,9 @@ Module ConcreteArrivalSequence.
Let arr_seq := periodic_arrival_sequence ts.
(* ... every job comes from the task set, ... *)
- (* TODO: It's supposed to be job_task j, but I don't know yet how to
- fix the coercion. *)
Theorem periodic_arrivals_all_jobs_from_taskset:
forall (j: JobIn arr_seq),
- job_task (_job_in arr_seq j) \in ts.
+ job_task (_job_in arr_seq j) \in ts. (* TODO: fix coercion *)
Proof.
intros j.
destruct j as [j arr ARRj]; simpl.
diff --git a/implementation/jitter/schedule.v b/implementation/jitter/schedule.v
index 72a593d1b..851c48943 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/jitter/schedule.v
@@ -11,8 +11,8 @@ Module ConcreteScheduler.
Section Implementation.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_jitter: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_jitter: Job -> time.
(* Let num_cpus denote the number of processors, ...*)
Variable num_cpus: nat.
@@ -61,8 +61,8 @@ Module ConcreteScheduler.
Section Proofs.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_jitter: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_jitter: Job -> time.
(* Assume a positive number of processors. *)
Variable num_cpus: nat.
diff --git a/model/basic/arrival_sequence.v b/model/basic/arrival_sequence.v
index 92fc92817..890358650 100644
--- a/model/basic/arrival_sequence.v
+++ b/model/basic/arrival_sequence.v
@@ -1,13 +1,12 @@
Add LoadPath "../../" as rt.
-Require Import rt.util.Vbase rt.util.lemmas rt.model.basic.job rt.model.basic.task.
+Require Import rt.util.Vbase rt.util.lemmas rt.model.basic.job rt.model.basic.task rt.model.basic.time.
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(* Definitions and properties of job arrival sequences. *)
Module ArrivalSequence.
- (* Let time be the set of natural numbers. *)
- Definition time := nat.
-
+ Export Time.
+
(* Next, we define a job arrival sequence (can be infinite). *)
Section ArrivalSequenceDef.
@@ -77,13 +76,13 @@ Module ArrivalSequence.
Variable j: JobIn arr_seq.
(* A job has arrived at time t iff it arrives at some time t_0, with 0 <= t_0 <= t. *)
- Definition has_arrived (t: nat) := job_arrival j <= t.
+ Definition has_arrived (t: time) := job_arrival j <= t.
(* A job arrived before t iff it arrives at some time t_0, with 0 <= t_0 < t. *)
- Definition arrived_before (t: nat) := job_arrival j < t.
+ Definition arrived_before (t: time) := job_arrival j < t.
(* A job arrives between t1 and t2 iff it arrives at some time t with t1 <= t < t2. *)
- Definition arrived_between (t1 t2: nat) := t1 <= job_arrival j < t2.
+ Definition arrived_between (t1 t2: time) := t1 <= job_arrival j < t2.
End ArrivingJobs.
diff --git a/model/basic/interference.v b/model/basic/interference.v
index a5c8c218f..a65c3ce54 100644
--- a/model/basic/interference.v
+++ b/model/basic/interference.v
@@ -11,16 +11,16 @@ Module Interference.
Section PossibleInterferingTasks.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Section FP.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
- (* Under constrained dealdines, tsk_other can only interfere with tsk
+ (* Under constrained deadlines, tsk_other can only interfere with tsk
if it's a different task with higher or equal priority. *)
Definition fp_can_interfere_with (tsk tsk_other: sporadic_task) :=
higher_eq_priority tsk_other tsk && (tsk_other != tsk).
@@ -42,7 +42,7 @@ Module Interference.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence...*)
@@ -110,8 +110,8 @@ Module Interference.
Definition task_is_scheduled (t: time) :=
[exists cpu in processor num_cpus, schedules_job_of_task cpu t].
- (* We define the total interference incurred by tsk during [t1, t2)
- as the cumulative time while tsk is scheduled. *)
+ (* We define the total interference caused by tsk during [t1, t2) as the
+ cumulative time in which j is backlogged while tsk is scheduled. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
\sum_(cpu < num_cpus)
@@ -124,8 +124,9 @@ Module Interference.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
- (* If jobs are sequential, we define the total interference incurred by tsk
- during [t1, t2) as the cumulative time in which tsk is scheduled. *)
+ (* If jobs are sequential, we define the total interference caused by
+ tsk during [t1, t2) as the cumulative time in which j is backlogged
+ while tsk is scheduled. *)
Definition task_interference_sequential (t1 t2: time) :=
\sum_(t1 <= t < t2)
(job_is_backlogged t && task_is_scheduled tsk_other t).
@@ -282,7 +283,7 @@ Module Interference.
Hypothesis job_is_not_complete :
~~ completed job_cost sched j t2.
- (* then the service received by j during [t1, t2) equals
+ (* ... then the service received by j during [t1, t2) equals
the cumulative time in which it did not incur interference. *)
Lemma complement_of_interf_equals_service :
\sum_(t1 <= t < t2) service_at sched j t =
diff --git a/model/basic/interference_edf.v b/model/basic/interference_edf.v
index d1c91f5b4..1c97066f1 100644
--- a/model/basic/interference_edf.v
+++ b/model/basic/interference_edf.v
@@ -12,8 +12,8 @@ Module InterferenceEDF.
Section Lemmas.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
@@ -28,7 +28,7 @@ Module InterferenceEDF.
Hypothesis H_scheduler_uses_EDF:
enforces_JLDP_policy job_cost sched (EDF job_deadline).
- (* Under EDF scheduling, a job only causes interference if its deadline
+ (* Under EDF scheduling, a job only causes sequential interference if its deadline
is not larger than the deadline of the analyzed job. *)
Lemma interference_seq_under_edf_implies_shorter_deadlines :
forall (j j': JobIn arr_seq) t1 t2,
@@ -55,7 +55,7 @@ Module InterferenceEDF.
}
Qed.
- (* Under EDF scheduling, a job only causes interference if its deadline
+ (* Under EDF scheduling, a job only causes (parallel) interference if its deadline
is not larger than the deadline of the analyzed job. *)
Lemma interference_under_edf_implies_shorter_deadlines :
forall (j j': JobIn arr_seq) t1 t2,
diff --git a/model/basic/job.v b/model/basic/job.v
index 7e5a94468..60bc26b69 100644
--- a/model/basic/job.v
+++ b/model/basic/job.v
@@ -1,15 +1,17 @@
Add LoadPath "../../" as rt.
-Require Import rt.model.basic.task rt.util.lemmas.
+Require Import rt.model.basic.time rt.model.basic.task rt.util.lemmas.
Require Import ssrnat ssrbool eqtype.
(* Properties of different types of job: *)
Module Job.
+ Import Time.
+
(* 1) Basic Job *)
Section ValidJob.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable j: Job.
@@ -22,8 +24,8 @@ Module Job.
Section ValidRealtimeJob.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable j: Job.
@@ -42,12 +44,12 @@ Module Job.
Section ValidSporadicTaskJob.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
Variable j: Job.
diff --git a/model/basic/platform.v b/model/basic/platform.v
index 06b058308..3467c661e 100644
--- a/model/basic/platform.v
+++ b/model/basic/platform.v
@@ -11,19 +11,19 @@ Module Platform.
Section SchedulingInvariants.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- (* Assume any job arrival sequence... *)
+ (* Consider any job arrival sequence ... *)
Context {arr_seq: arrival_sequence Job}.
- (* Consider any schedule. *)
+ (* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
diff --git a/model/basic/platform_fp.v b/model/basic/platform_fp.v
index 161b76a57..3b789bb42 100644
--- a/model/basic/platform_fp.v
+++ b/model/basic/platform_fp.v
@@ -12,23 +12,23 @@ Module PlatformFP.
Section Lemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- (* Assume any job arrival sequence... *)
+ (* Consider any job arrival sequence ... *)
Context {arr_seq: arrival_sequence Job}.
- (* Consider any schedule. *)
+ (* ... and any schedule of this arrival sequence. *)
Context {num_cpus: nat}.
Variable sched: schedule num_cpus arr_seq.
- (* Assume all jobs have valid parameters, ...*)
+ (* Assume that all jobs have valid parameters. *)
Hypothesis H_valid_job_parameters:
forall (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
@@ -41,12 +41,12 @@ Module PlatformFP.
Hypothesis H_enforces_JLDP_policy:
enforces_FP_policy job_cost job_task sched higher_eq_priority.
- (* Consider task set ts. *)
+ (* Consider any task set ts ... *)
Variable ts: taskset_of sporadic_task.
- (* Assume the task set has no duplicates, ... *)
+ (* ... that has no duplicate tasks ... *)
Hypothesis H_ts_is_a_set: uniq ts.
- (* ... and all jobs come from the taskset. *)
+ (* ... and such that all jobs come from the taskset. *)
Hypothesis H_all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
@@ -60,7 +60,7 @@ Module PlatformFP.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
- (* Assume that the schedule satisfies the sporadic task model ...*)
+ (* Assume that jobs arrive sporadically. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
diff --git a/model/basic/priority.v b/model/basic/priority.v
index 9819609d3..869fd889b 100644
--- a/model/basic/priority.v
+++ b/model/basic/priority.v
@@ -93,8 +93,8 @@ Module Priority.
Section RateDeadlineMonotonic.
Context {sporadic_task: eqType}.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
(* Rate-Monotonic and Deadline-Monotonic as priority order *)
Definition RM (tsk1 tsk2: sporadic_task) := task_period tsk1 <= task_period tsk2.
@@ -180,7 +180,7 @@ Module Priority.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
- Variable job_deadline: Job -> nat.
+ Variable job_deadline: Job -> time.
Definition EDF (t: time) (j1 j2: JobIn arr_seq) :=
job_arrival j1 + job_deadline j1 <= job_arrival j2 + job_deadline j2.
diff --git a/model/basic/response_time.v b/model/basic/response_time.v
index 422d96b83..471501ebf 100644
--- a/model/basic/response_time.v
+++ b/model/basic/response_time.v
@@ -14,7 +14,7 @@ Module ResponseTime.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Context {arr_seq: arrival_sequence Job}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Given a task ...*)
@@ -42,7 +42,7 @@ Module ResponseTime.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
Context {arr_seq: arrival_sequence Job}.
diff --git a/model/basic/schedulability.v b/model/basic/schedulability.v
index e0da35e9f..1d60e1230 100644
--- a/model/basic/schedulability.v
+++ b/model/basic/schedulability.v
@@ -13,8 +13,8 @@ Module Schedulability.
(* 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.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Section ScheduleOfJobs.
@@ -62,13 +62,13 @@ Module Schedulability.
Section BasicLemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
Context {arr_seq: arrival_sequence Job}.
diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index 7ac133079..af20beea8 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -34,7 +34,7 @@ Module Schedule.
(* Given an arrival sequence, ... *)
Context {arr_seq: arrival_sequence Job}.
- Variable job_cost: Job -> nat. (* ... a job cost function, ... *)
+ Variable job_cost: Job -> time. (* ... a job cost function, ... *)
(* ... and the number of processors, ...*)
Context {num_cpus: nat}.
@@ -102,7 +102,7 @@ Module Schedule.
Context {Job: eqType}. (* Assume a job type with decidable equality, ...*)
Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*)
- Variable job_cost: Job -> nat. (* ... a cost function, .... *)
+ Variable job_cost: Job -> time. (* ... a cost function, .... *)
(* ... and a schedule. *)
Context {num_cpus: nat}.
@@ -131,7 +131,7 @@ Module Schedule.
Context {arr_seq: arrival_sequence Job}.
(* ... a job cost function, ...*)
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
(* ..., and a particular schedule. *)
Context {num_cpus: nat}.
@@ -553,7 +553,7 @@ Module ScheduleOfSporadicTask.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Consider any schedule. *)
@@ -580,12 +580,12 @@ Module ScheduleOfSporadicTask.
(* Assume the job cost and task are known. *)
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Then, in a valid schedule of sporadic tasks ...*)
diff --git a/model/basic/task.v b/model/basic/task.v
index d3d55d80f..38e5e8e43 100644
--- a/model/basic/task.v
+++ b/model/basic/task.v
@@ -1,15 +1,17 @@
Add LoadPath "../../" as rt.
-Require Import rt.util.Vbase rt.util.lemmas.
+Require Import rt.model.basic.time rt.util.Vbase rt.util.lemmas.
Require Import ssrnat ssrbool eqtype fintype seq.
(* Attributes of a valid sporadic task. *)
Module SporadicTask.
+ Import Time.
+
Section BasicTask.
Context {Task: eqType}.
- Variable task_cost: Task -> nat.
- Variable task_period: Task -> nat.
- Variable task_deadline: Task -> nat.
+ Variable task_cost: Task -> time.
+ Variable task_period: Task -> time.
+ Variable task_deadline: Task -> time.
Section ValidParameters.
Variable tsk: Task.
@@ -35,6 +37,7 @@ End SporadicTask.
(* Definition and properties of a task set. *)
Module SporadicTaskset.
+ Import Time.
Export SporadicTask.
Section TasksetDefs.
@@ -46,9 +49,9 @@ Module SporadicTaskset.
Section TasksetProperties.
Context {Task: eqType}.
- Variable task_cost: Task -> nat.
- Variable task_period: Task -> nat.
- Variable task_deadline: Task -> nat.
+ Variable task_cost: Task -> time.
+ Variable task_period: Task -> time.
+ Variable task_deadline: Task -> time.
Let is_valid_task :=
is_valid_sporadic_task task_cost task_period task_deadline.
diff --git a/model/basic/task_arrival.v b/model/basic/task_arrival.v
index 3501c62b3..b70d4b77f 100644
--- a/model/basic/task_arrival.v
+++ b/model/basic/task_arrival.v
@@ -12,7 +12,7 @@ Import SporadicTaskset Schedule.
(* Assume the task period is known. *)
Context {sporadic_task: eqType}.
- Variable task_period: sporadic_task -> nat.
+ Variable task_period: sporadic_task -> time.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
diff --git a/model/basic/time.v b/model/basic/time.v
new file mode 100644
index 000000000..6c5adab3d
--- /dev/null
+++ b/model/basic/time.v
@@ -0,0 +1,6 @@
+Module Time.
+
+ (* Time is defined as a natural number. *)
+ Definition time := nat.
+
+End Time.
\ No newline at end of file
diff --git a/model/basic/workload.v b/model/basic/workload.v
index 332021e9c..fd6bc3816 100644
--- a/model/basic/workload.v
+++ b/model/basic/workload.v
@@ -26,7 +26,7 @@ Module Workload.
(* First, we define a function that returns the amount of service
received by this task in a particular processor. *)
Definition service_of_task (cpu: processor num_cpus)
- (j: option (JobIn arr_seq)) : nat :=
+ (j: option (JobIn arr_seq)) : time :=
match j with
| Some j' => (job_task j' == tsk)
| None => 0
diff --git a/model/jitter/interference.v b/model/jitter/interference.v
index 6c6fedc5d..f0aa7caee 100644
--- a/model/jitter/interference.v
+++ b/model/jitter/interference.v
@@ -19,9 +19,9 @@ Module Interference.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence...*)
Context {arr_seq: arrival_sequence Job}.
@@ -74,8 +74,8 @@ Module Interference.
Definition task_is_scheduled (t: time) :=
[exists cpu in processor num_cpus, schedules_job_of_tsk cpu t].
- (* We define the total interference incurred by tsk during [t1, t2)
- as the cumulative time in which tsk is scheduled. *)
+ (* We define the total interference caused by tsk during [t1, t2) as
+ the cumulative time in which j is backlogged while tsk is scheduled. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 <= t < t2)
(job_is_backlogged t && task_is_scheduled t).
diff --git a/model/jitter/interference_edf.v b/model/jitter/interference_edf.v
index a7128532f..6b1fd7a50 100644
--- a/model/jitter/interference_edf.v
+++ b/model/jitter/interference_edf.v
@@ -12,9 +12,9 @@ Module InterferenceEDF.
Section Lemmas.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
- Variable job_jitter: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
diff --git a/model/jitter/job.v b/model/jitter/job.v
index a33e716ff..abf424493 100644
--- a/model/jitter/job.v
+++ b/model/jitter/job.v
@@ -1,5 +1,5 @@
Add LoadPath "../../" as rt.
-Require Import rt.model.basic.task.
+Require Import rt.model.jitter.time rt.model.jitter.task.
Require Import ssrnat ssrbool eqtype.
Require Export rt.model.basic.job.
@@ -7,21 +7,22 @@ Require Export rt.model.basic.job.
(* Properties of different types of job: *)
Module JobWithJitter.
+ Import Time.
Export Job.
(* 4) Job of sporadic task with jitter *)
Section ValidSporadicTaskJobWithJitter.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
- Variable task_jitter: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
+ Variable task_jitter: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
Variable j: Job.
diff --git a/model/jitter/platform.v b/model/jitter/platform.v
index 01886afe3..ee3bc7502 100644
--- a/model/jitter/platform.v
+++ b/model/jitter/platform.v
@@ -11,15 +11,15 @@ Module Platform.
Section SchedulingInvariants.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
diff --git a/model/jitter/platform_fp.v b/model/jitter/platform_fp.v
index a36124660..dd208730c 100644
--- a/model/jitter/platform_fp.v
+++ b/model/jitter/platform_fp.v
@@ -13,15 +13,15 @@ Module PlatformFP.
Section Lemmas.
Context {sporadic_task: eqType}.
- Variable task_cost: sporadic_task -> nat.
- Variable task_period: sporadic_task -> nat.
- Variable task_deadline: sporadic_task -> nat.
+ Variable task_cost: sporadic_task -> time.
+ Variable task_period: sporadic_task -> time.
+ Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
- Variable job_deadline: Job -> nat.
+ Variable job_cost: Job -> time.
+ Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
- Variable job_jitter: Job -> nat.
+ Variable job_jitter: Job -> time.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
diff --git a/model/jitter/priority.v b/model/jitter/priority.v
index c7a7cac54..c2f5a4aec 100644
--- a/model/jitter/priority.v
+++ b/model/jitter/priority.v
@@ -1,5 +1,4 @@
Add LoadPath "../../" as rt.
-(* Because we define EDF using the *original job arrivals*, we can safely import the
- definitions. *)
+(* Because we define EDF using the *actual job arrivals*, we can safely import the original of priority. *)
Require Export rt.model.basic.priority.
\ No newline at end of file
diff --git a/model/jitter/schedule.v b/model/jitter/schedule.v
index 3ddd451d7..eba9cf87b 100644
--- a/model/jitter/schedule.v
+++ b/model/jitter/schedule.v
@@ -14,7 +14,7 @@ Module ScheduleWithJitter.
Section ArrivalDependentProperties.
Context {Job: eqType}.
- Variable job_cost: Job -> nat.
+ Variable job_cost: Job -> time.
Variable job_jitter: Job -> time.
(* Given an arrival sequence, ... *)
diff --git a/model/jitter/time.v b/model/jitter/time.v
new file mode 100644
index 000000000..603a1f76e
--- /dev/null
+++ b/model/jitter/time.v
@@ -0,0 +1,4 @@
+Add LoadPath "../../" as rt.
+
+(* The definition of time is the same. *)
+Require Export rt.model.basic.time.
\ No newline at end of file
--
GitLab