From c8db68d09787c54c2f84f3af4f3db47b11b98d99 Mon Sep 17 00:00:00 2001
From: Felipe Cerqueira <felipec@mpi-sws.org>
Date: Sun, 7 Feb 2016 00:57:54 +0100
Subject: [PATCH] Add more implementations for basic/jitter
- Implemented concrete job and tasks.
- Added a periodic arrival sequence.
- Created examples of applying a schedulability
test to small task sets and concluding that
no task misses a deadline.
---
Makefile | 10 +-
implementation/basic/arrival_sequence.v | 114 +++++++++++++++
implementation/basic/bertogna_edf_example.v | 136 ++++++++++++++++++
implementation/basic/job.v | 61 ++++++++
implementation/basic/schedule.v | 4 +-
implementation/basic/task.v | 69 ++++++++++
implementation/jitter/arrival_sequence.v | 114 +++++++++++++++
implementation/jitter/bertogna_edf_example.v | 138 +++++++++++++++++++
implementation/jitter/job.v | 63 +++++++++
implementation/jitter/schedule.v | 16 +--
implementation/jitter/task.v | 71 ++++++++++
11 files changed, 784 insertions(+), 12 deletions(-)
create mode 100644 implementation/basic/arrival_sequence.v
create mode 100644 implementation/basic/bertogna_edf_example.v
create mode 100644 implementation/basic/job.v
create mode 100644 implementation/basic/task.v
create mode 100644 implementation/jitter/arrival_sequence.v
create mode 100644 implementation/jitter/bertogna_edf_example.v
create mode 100644 implementation/jitter/job.v
create mode 100644 implementation/jitter/task.v
diff --git a/Makefile b/Makefile
index 31f4cb7ec..a640af6de 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/schedule.v ./implementation/jitter/schedule.v ./analysis/basic/bertogna_fp_theory.v ./analysis/basic/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./model/basic/schedulability.v ./model/basic/interference_bound_edf.v ./model/basic/task.v ./model/basic/interference_bound_fp.v ./model/basic/task_arrival.v ./model/basic/interference_bound.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/basic/workload_bound.v ./model/jitter/schedulability.v ./model/jitter/interference_bound_edf.v ./model/jitter/task.v ./model/jitter/interference_bound_fp.v ./model/jitter/task_arrival.v ./model/jitter/interference_bound.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 ./model/jitter/workload_bound.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/bertogna_edf_comp.v ./analysis/basic/bertogna_fp_comp.v ./analysis/basic/bertogna_edf_theory.v ./analysis/jitter/bertogna_fp_theory.v ./analysis/jitter/bertogna_edf_comp.v ./analysis/jitter/bertogna_fp_comp.v ./analysis/jitter/bertogna_edf_theory.v ./model/basic/schedulability.v ./model/basic/interference_bound_edf.v ./model/basic/task.v ./model/basic/interference_bound_fp.v ./model/basic/task_arrival.v ./model/basic/interference_bound.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/basic/workload_bound.v ./model/jitter/schedulability.v ./model/jitter/interference_bound_edf.v ./model/jitter/task.v ./model/jitter/interference_bound_fp.v ./model/jitter/task_arrival.v ./model/jitter/interference_bound.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 ./model/jitter/workload_bound.v -o Makefile
#
.DEFAULT_GOAL := all
@@ -84,8 +84,16 @@ VFILES:=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/bertogna_edf_comp.v\
analysis/basic/bertogna_fp_comp.v\
diff --git a/implementation/basic/arrival_sequence.v b/implementation/basic/arrival_sequence.v
new file mode 100644
index 000000000..723f77487
--- /dev/null
+++ b/implementation/basic/arrival_sequence.v
@@ -0,0 +1,114 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.model.basic.arrival_sequence rt.model.basic.job
+ rt.model.basic.task rt.model.basic.task_arrival.
+Require Import rt.implementation.basic.task rt.implementation.basic.job.
+Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
+
+Module ConcreteArrivalSequence.
+
+ Import Job ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset SporadicTaskArrival.
+
+ Section PeriodicArrivals.
+
+ Variable ts: concrete_taskset.
+
+ (* At any time t, we release Some job of tsk if t is a multiple of the period,
+ otherwise we release None. *)
+ Definition add_job (t: time) (tsk: concrete_task) :=
+ if task_period tsk %| t then
+ Some (Build_concrete_job (t %/ task_period tsk) (task_cost tsk) (task_deadline tsk) tsk)
+ else
+ None.
+
+ (* The arrival sequence at any time t is simply the partial map of add_job. *)
+ Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.
+
+ End PeriodicArrivals.
+
+ Section Proofs.
+
+ (* Let ts be any concrete task set with valid parameters. *)
+ Variable ts: concrete_taskset.
+ Hypothesis H_valid_task_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* Regarding the periodic arrival sequence built from ts, we prove that...*)
+ 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.
+ Proof.
+ intros j.
+ destruct j as [j arr ARRj]; simpl.
+ unfold arr_seq, arrives_at, periodic_arrival_sequence in *.
+ rewrite mem_pmap in ARRj.
+ move: ARRj => /mapP ARRj; destruct ARRj as [tsk IN SOME].
+ by unfold add_job in *; desf.
+ Qed.
+
+ (* ..., jobs have valid parameters, ... *)
+ Theorem periodic_arrivals_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
+ Proof.
+ rename H_valid_task_parameters into PARAMS.
+ unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
+ intros j; destruct j as [j arr ARRj]; simpl.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in ARRj.
+ rewrite mem_pmap in ARRj; move: ARRj => /mapP [tsk IN SOME].
+ unfold add_job in SOME; desf.
+ specialize (PARAMS tsk IN); des.
+ unfold valid_sporadic_job, valid_realtime_job, job_cost_positive.
+ by repeat split; try (by done); apply leqnn.
+ Qed.
+
+ (* ... job arrivals satisfy the sporadic task model, ... *)
+ Theorem periodic_arrivals_are_sporadic:
+ sporadic_task_model task_period arr_seq job_task.
+ Proof.
+ unfold sporadic_task_model; move => j j' /eqP DIFF SAMEtsk LE.
+ destruct j as [j arr ARR], j' as [j' arr' ARR']; simpl in *.
+ rewrite eqE /= /jobin_eqdef negb_and /= in DIFF.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in *.
+ rewrite 2!mem_pmap in ARR ARR'.
+ move: ARR ARR' => /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
+ unfold add_job in *; desf; simpl in *; subst.
+ clear INj'.
+ move: Heq Heq0 => /dvdnP DIV' /dvdnP DIV; des.
+ rewrite DIV DIV' -mulSnr.
+ rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
+ {
+ move: DIFF => /orP [/eqP CASE1 | /eqP CASE2].
+ - by exfalso; apply CASE1; repeat f_equal.
+ - by rewrite EQ in CASE2.
+ }
+ rewrite leq_mul2r; apply/orP; right.
+ rewrite ltn_neqAle; apply/andP; split.
+ {
+ apply/eqP; red; intro EQ; subst.
+ by rewrite ltnn in LESS.
+ }
+ rewrite leqNgt; apply/negP; red; intro LT.
+ rewrite ltnNge in LESS; move: LESS => /negP LESS; apply LESS.
+ by subst; rewrite leq_mul2r; apply/orP; right; apply ltnW.
+ Qed.
+
+ (* ... and if the task set has no duplicates, the same applies to
+ the arrival sequence. *)
+ Theorem periodic_arrivals_is_a_set:
+ uniq ts -> arrival_sequence_is_a_set arr_seq.
+ Proof.
+ intros UNIQ t.
+ unfold arr_seq, periodic_arrival_sequence.
+ apply (pmap_uniq) with (g := job_task); last by done.
+ by unfold add_job, ocancel; intro tsk; desf.
+ Qed.
+
+ End Proofs.
+
+End ConcreteArrivalSequence.
\ No newline at end of file
diff --git a/implementation/basic/bertogna_edf_example.v b/implementation/basic/bertogna_edf_example.v
new file mode 100644
index 000000000..ad8eaa3ea
--- /dev/null
+++ b/implementation/basic/bertogna_edf_example.v
@@ -0,0 +1,136 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase rt.util.divround.
+Require Import rt.model.basic.job rt.model.basic.task
+ rt.model.basic.schedule rt.model.basic.schedulability
+ rt.model.basic.workload_bound
+ rt.model.basic.interference_bound_edf
+ rt.model.basic.priority rt.model.basic.platform
+ rt.analysis.basic.bertogna_edf_comp.
+Require Import rt.implementation.basic.job
+ rt.implementation.basic.task
+ rt.implementation.basic.schedule
+ rt.implementation.basic.arrival_sequence.
+Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Module ResponseTimeAnalysisEDF.
+
+ Import Job Schedule SporadicTaskset Priority Schedulability Platform InterferenceBoundEDF WorkloadBound ResponseTimeIterationEDF.
+ Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
+
+ Section ExampleRTA.
+
+ Let tsk1 := {| task_id := 1; task_cost := 2; task_period := 5; task_deadline := 3|}.
+ Let tsk2 := {| task_id := 2; task_cost := 4; task_period := 6; task_deadline := 5|}.
+ Let tsk3 := {| task_id := 3; task_cost := 3; task_period := 12; task_deadline := 11|}.
+
+ (* Let ts be a task set containing these three tasks. *)
+ Let ts := [:: tsk1; tsk2; tsk3].
+
+ Section FactsAboutTaskset.
+
+ Fact ts_is_a_set: uniq ts.
+ Proof.
+ by compute.
+ Qed.
+
+ Fact ts_has_valid_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
+ Qed.
+
+ Fact ts_has_constrained_deadlines:
+ forall tsk,
+ tsk \in ts ->
+ task_deadline tsk <= task_period tsk.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
+ Qed.
+
+ End FactsAboutTaskset.
+
+ (* Assume there are two processors. *)
+ Let num_cpus := 2.
+
+ (* Recall the EDF RTA schedulability test. *)
+ Let schedulability_test :=
+ edf_schedulable task_cost task_period task_deadline num_cpus.
+
+ Fact schedulability_test_succeeds :
+ schedulability_test ts = true.
+ Proof.
+ unfold schedulability_test, edf_schedulable, edf_claimed_bounds; desf.
+ apply negbT in Heq; move: Heq => /negP ALL.
+ exfalso; apply ALL; clear ALL.
+ assert (STEPS: \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1 = 11).
+ {
+ by rewrite unlock; compute.
+ } rewrite STEPS; clear STEPS.
+
+ Ltac f :=
+ unfold edf_rta_iteration; simpl;
+ unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W; simpl;
+ repeat rewrite addnE;
+ repeat rewrite big_cons; repeat rewrite big_nil;
+ repeat rewrite addnE; simpl;
+ unfold num_cpus, divn; simpl.
+
+ rewrite [edf_rta_iteration]lock; simpl.
+
+ unfold locked at 11; destruct master_key; f.
+ unfold locked at 10; destruct master_key; f.
+ unfold locked at 9; destruct master_key; f.
+ unfold locked at 8; destruct master_key; f.
+ unfold locked at 7; destruct master_key; f.
+ unfold locked at 6; destruct master_key; f.
+ unfold locked at 5; destruct master_key; f.
+ unfold locked at 4; destruct master_key; f.
+ unfold locked at 3; destruct master_key; f.
+ unfold locked at 2; destruct master_key; f.
+ by unfold locked at 1; destruct master_key; f.
+ Qed.
+
+ (* Let arr_seq be the periodic arrival sequence from ts. *)
+ Let arr_seq := periodic_arrival_sequence ts.
+
+ (* Let sched be the work-conserving EDF scheduler. *)
+ Let sched := scheduler job_cost num_cpus arr_seq (EDF job_deadline).
+
+ (* Recall the definition of deadline miss. *)
+ Let no_deadline_missed_by :=
+ task_misses_no_deadline job_cost job_deadline job_task sched.
+
+ (* Next, we prove that ts is schedulable with the result of the test. *)
+ Corollary ts_is_schedulable:
+ forall tsk,
+ tsk \in ts ->
+ no_deadline_missed_by tsk.
+ Proof.
+ intros tsk IN.
+ have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
+ have EDFVALID := @edf_valid_policy _ arr_seq job_deadline.
+ unfold valid_JLDP_policy, valid_sporadic_job, valid_realtime_job in *; des.
+ apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts).
+ - by apply ts_is_a_set.
+ - by apply ts_has_valid_parameters.
+ - by apply ts_has_constrained_deadlines.
+ - by apply periodic_arrivals_all_jobs_from_taskset.
+ - by apply periodic_arrivals_valid_job_parameters, ts_has_valid_parameters.
+ - by apply periodic_arrivals_are_sporadic.
+ - by compute.
+ - by apply scheduler_jobs_must_arrive_to_execute.
+ - apply scheduler_completed_jobs_dont_execute; intro j'.
+ -- by specialize (VALID j'); des.
+ -- by apply periodic_arrivals_is_a_set.
+ - by apply scheduler_no_parallelism, periodic_arrivals_is_a_set.
+ - by apply scheduler_work_conserving.
+ - by apply scheduler_enforces_policy; ins.
+ - by apply schedulability_test_succeeds.
+ - by apply IN.
+ Qed.
+
+ End ExampleRTA.
+
+End ResponseTimeAnalysisEDF.
\ No newline at end of file
diff --git a/implementation/basic/job.v b/implementation/basic/job.v
new file mode 100644
index 000000000..ba32c5366
--- /dev/null
+++ b/implementation/basic/job.v
@@ -0,0 +1,61 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.implementation.basic.task.
+Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteJob.
+
+ Import ConcreteTask.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_job :=
+ {
+ job_id: nat;
+ job_cost: nat;
+ job_deadline: nat;
+ job_task: concrete_task_eqType
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete jobs. *)
+ Definition job_eqdef (j1 j2: concrete_job) :=
+ (job_id j1 == job_id j2) &&
+ (job_cost j1 == job_cost j2) &&
+ (job_deadline j1 == job_deadline j2) &&
+ (job_task j1 == job_task j2).
+
+ (* Next, we prove that job_eqdef is indeed an equality, ... *)
+ Lemma eqn_job : Equality.axiom job_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (job_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT; unfold job_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/eqP ID /eqP COST] /eqP DL] /eqP TASK].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold job_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP TASK]; last by apply TASK; inversion BUG.
+ move: EQ => /orP [EQ | /eqP DL].
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID | /eqP COST].
+ by apply ID; inversion BUG.
+ by apply COST; inversion BUG.
+ by apply DL; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_job_eqMixin := EqMixin eqn_job.
+ Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.
+
+ End Defs.
+
+End ConcreteJob.
\ No newline at end of file
diff --git a/implementation/basic/schedule.v b/implementation/basic/schedule.v
index 71ae096b3..8435ae225 100644
--- a/implementation/basic/schedule.v
+++ b/implementation/basic/schedule.v
@@ -4,7 +4,7 @@ Require Import rt.model.basic.job rt.model.basic.arrival_sequence rt.model.basic
rt.model.basic.platform rt.model.basic.priority.
Require Import Program ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
-Module WorkConservingScheduler.
+Module ConcreteScheduler.
Import Job ArrivalSequence Schedule Platform Priority.
@@ -336,4 +336,4 @@ Module WorkConservingScheduler.
End Proofs.
-End WorkConservingScheduler.
\ No newline at end of file
+End ConcreteScheduler.
\ No newline at end of file
diff --git a/implementation/basic/task.v b/implementation/basic/task.v
new file mode 100644
index 000000000..30c7a8965
--- /dev/null
+++ b/implementation/basic/task.v
@@ -0,0 +1,69 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.model.basic.task.
+Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteTask.
+
+ Import SporadicTaskset.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_task :=
+ {
+ task_id: nat; (* for uniqueness *)
+ task_cost: nat;
+ task_period: nat;
+ task_deadline: nat
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete tasks. *)
+ Definition task_eqdef (t1 t2: concrete_task) :=
+ (task_id t1 == task_id t2) &&
+ (task_cost t1 == task_cost t2) &&
+ (task_period t1 == task_period t2) &&
+ (task_deadline t1 == task_deadline t2).
+
+ (* Next, we prove that task_eqdef is indeed an equality, ... *)
+ Lemma eqn_task : Equality.axiom task_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (task_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT.
+ unfold task_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/eqP ID /eqP COST] /eqP PERIOD] /eqP DL].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold task_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP DL]; last by apply DL; inversion BUG.
+ move: EQ => /orP [EQ | /eqP PERIOD].
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID | /eqP COST].
+ by apply ID; inversion BUG.
+ by apply COST; inversion BUG.
+ by apply PERIOD; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_task_eqMixin := EqMixin eqn_task.
+ Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.
+
+ End Defs.
+
+ Section ConcreteTaskset.
+
+ Definition concrete_taskset :=
+ taskset_of concrete_task_eqType.
+
+ End ConcreteTaskset.
+
+End ConcreteTask.
\ No newline at end of file
diff --git a/implementation/jitter/arrival_sequence.v b/implementation/jitter/arrival_sequence.v
new file mode 100644
index 000000000..e50701dc8
--- /dev/null
+++ b/implementation/jitter/arrival_sequence.v
@@ -0,0 +1,114 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.model.jitter.arrival_sequence rt.model.jitter.job
+ rt.model.jitter.task rt.model.jitter.task_arrival.
+Require Import rt.implementation.jitter.task rt.implementation.jitter.job.
+Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq div.
+
+Module ConcreteArrivalSequence.
+
+ Import JobWithJitter ArrivalSequence ConcreteTask ConcreteJob SporadicTaskset SporadicTaskArrival.
+
+ Section PeriodicArrivals.
+
+ Variable ts: concrete_taskset.
+
+ (* At any time t, we release Some job of tsk if t is a multiple of the period,
+ otherwise we release None. *)
+ Definition add_job (t: time) (tsk: concrete_task) :=
+ if task_period tsk %| t then
+ Some (Build_concrete_job (t %/ task_period tsk) (task_cost tsk) (task_deadline tsk) (task_jitter tsk) tsk)
+ else
+ None.
+
+ (* The arrival sequence at any time t is simply the partial map of add_job. *)
+ Definition periodic_arrival_sequence (t: time) := pmap (add_job t) ts.
+
+ End PeriodicArrivals.
+
+ Section Proofs.
+
+ (* Let ts be any concrete task set with valid parameters. *)
+ Variable ts: concrete_taskset.
+ Hypothesis H_valid_task_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+
+ (* Regarding the periodic arrival sequence built from ts, we prove that...*)
+ 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.
+ Proof.
+ intros j.
+ destruct j as [j arr ARRj]; simpl.
+ unfold arr_seq, arrives_at, periodic_arrival_sequence in *.
+ rewrite mem_pmap in ARRj.
+ move: ARRj => /mapP ARRj; destruct ARRj as [tsk IN SOME].
+ by unfold add_job in *; desf.
+ Qed.
+
+ (* ..., jobs have valid parameters, ... *)
+ Theorem periodic_arrivals_valid_job_parameters:
+ forall (j: JobIn arr_seq),
+ valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
+ Proof.
+ rename H_valid_task_parameters into PARAMS.
+ unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
+ intros j; destruct j as [j arr ARRj]; simpl.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in ARRj.
+ rewrite mem_pmap in ARRj; move: ARRj => /mapP [tsk IN SOME].
+ unfold add_job in SOME; desf.
+ specialize (PARAMS tsk IN); des.
+ unfold valid_sporadic_job, valid_realtime_job, job_cost_positive.
+ by repeat split; try (by done); apply leqnn.
+ Qed.
+
+ (* ... job arrivals satisfy the sporadic task model, ... *)
+ Theorem periodic_arrivals_are_sporadic:
+ sporadic_task_model task_period arr_seq job_task.
+ Proof.
+ unfold sporadic_task_model; move => j j' /eqP DIFF SAMEtsk LE.
+ destruct j as [j arr ARR], j' as [j' arr' ARR']; simpl in *.
+ rewrite eqE /= /jobin_eqdef negb_and /= in DIFF.
+ unfold arrives_at, arr_seq, periodic_arrival_sequence in *.
+ rewrite 2!mem_pmap in ARR ARR'.
+ move: ARR ARR' => /mapP [tsk_j INj SOMEj] /mapP [tsk_j' INj' SOMEj'].
+ unfold add_job in *; desf; simpl in *; subst.
+ clear INj'.
+ move: Heq Heq0 => /dvdnP DIV' /dvdnP DIV; des.
+ rewrite DIV DIV' -mulSnr.
+ rewrite leq_eqVlt in LE; move: LE => /orP [/eqP EQ | LESS].
+ {
+ move: DIFF => /orP [/eqP CASE1 | /eqP CASE2].
+ - by exfalso; apply CASE1; repeat f_equal.
+ - by rewrite EQ in CASE2.
+ }
+ rewrite leq_mul2r; apply/orP; right.
+ rewrite ltn_neqAle; apply/andP; split.
+ {
+ apply/eqP; red; intro EQ; subst.
+ by rewrite ltnn in LESS.
+ }
+ rewrite leqNgt; apply/negP; red; intro LT.
+ rewrite ltnNge in LESS; move: LESS => /negP LESS; apply LESS.
+ by subst; rewrite leq_mul2r; apply/orP; right; apply ltnW.
+ Qed.
+
+ (* ... and if the task set has no duplicates, the same applies to
+ the arrival sequence. *)
+ Theorem periodic_arrivals_is_a_set:
+ uniq ts -> arrival_sequence_is_a_set arr_seq.
+ Proof.
+ intros UNIQ t.
+ unfold arr_seq, periodic_arrival_sequence.
+ apply (pmap_uniq) with (g := job_task); last by done.
+ by unfold add_job, ocancel; intro tsk; desf.
+ Qed.
+
+ End Proofs.
+
+End ConcreteArrivalSequence.
\ No newline at end of file
diff --git a/implementation/jitter/bertogna_edf_example.v b/implementation/jitter/bertogna_edf_example.v
new file mode 100644
index 000000000..0a4b32174
--- /dev/null
+++ b/implementation/jitter/bertogna_edf_example.v
@@ -0,0 +1,138 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase rt.util.divround.
+Require Import rt.model.jitter.job rt.model.jitter.task
+ rt.model.jitter.schedule rt.model.jitter.schedulability
+ rt.model.jitter.workload_bound
+ rt.model.jitter.interference_bound_edf
+ rt.model.jitter.priority rt.model.jitter.platform
+ rt.analysis.jitter.bertogna_edf_comp.
+Require Import rt.implementation.jitter.job
+ rt.implementation.jitter.task
+ rt.implementation.jitter.schedule
+ rt.implementation.jitter.arrival_sequence.
+Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.
+
+Module ResponseTimeAnalysisEDF.
+
+ Import JobWithJitter ScheduleWithJitter SporadicTaskset Priority Schedulability Platform InterferenceBoundEDFJitter WorkloadBoundJitter ResponseTimeIterationEDF.
+ Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.
+
+ Section ExampleRTA.
+
+ Let tsk1 := {| task_id := 1; task_cost := 2; task_period := 5; task_deadline := 3; task_jitter := 1|}.
+ Let tsk2 := {| task_id := 2; task_cost := 4; task_period := 6; task_deadline := 5; task_jitter := 0|}.
+ Let tsk3 := {| task_id := 3; task_cost := 2; task_period := 12; task_deadline := 11; task_jitter := 2|}.
+
+ (* Let ts be a task set containing these three tasks. *)
+ Let ts := [:: tsk1; tsk2; tsk3].
+
+ Section FactsAboutTaskset.
+
+ Fact ts_is_a_set: uniq ts.
+ Proof.
+ by compute.
+ Qed.
+
+ Fact ts_has_valid_parameters:
+ valid_sporadic_taskset task_cost task_period task_deadline ts.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
+ Qed.
+
+ Fact ts_has_constrained_deadlines:
+ forall tsk,
+ tsk \in ts ->
+ task_deadline tsk <= task_period tsk.
+ Proof.
+ intros tsk IN.
+ repeat (move: IN => /orP [/eqP EQ | IN]; subst; compute); by done.
+ Qed.
+
+ End FactsAboutTaskset.
+
+ (* Assume there are two processors. *)
+ Let num_cpus := 2.
+
+ (* Recall the EDF RTA schedulability test. *)
+ Let schedulability_test :=
+ edf_schedulable task_cost task_period task_deadline task_jitter num_cpus.
+
+ Fact schedulability_test_succeeds :
+ schedulability_test ts = true.
+ Proof.
+ unfold schedulability_test, edf_schedulable, edf_claimed_bounds; desf.
+ apply negbT in Heq; move: Heq => /negP ALL.
+ exfalso; apply ALL; clear ALL.
+ assert (STEPS: \sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1 = 12).
+ {
+ by rewrite unlock; compute.
+ } rewrite STEPS; clear STEPS.
+
+ Ltac f :=
+ unfold edf_rta_iteration; simpl;
+ unfold edf_response_time_bound, div_floor, total_interference_bound_edf, interference_bound_edf, interference_bound_generic, W_jitter; simpl;
+ repeat rewrite addnE;
+ repeat rewrite big_cons; repeat rewrite big_nil;
+ repeat rewrite addnE; simpl;
+ unfold num_cpus, divn; simpl.
+
+ rewrite [edf_rta_iteration]lock; simpl.
+
+ unfold locked at 12; destruct master_key; f.
+ unfold locked at 11; destruct master_key; f.
+ unfold locked at 10; destruct master_key; f.
+ unfold locked at 9; destruct master_key; f.
+ unfold locked at 8; destruct master_key; f.
+ unfold locked at 7; destruct master_key; f.
+ unfold locked at 6; destruct master_key; f.
+ unfold locked at 5; destruct master_key; f.
+ unfold locked at 4; destruct master_key; f.
+ unfold locked at 3; destruct master_key; f.
+ unfold locked at 2; destruct master_key; f.
+ by unfold locked at 1; destruct master_key; f.
+ Qed.
+
+ (* Let arr_seq be the periodic arrival sequence from ts. *)
+ Let arr_seq := periodic_arrival_sequence ts.
+
+ (* Let sched be the work-conserving EDF scheduler. *)
+ Let sched := scheduler job_cost job_jitter num_cpus arr_seq (EDF job_deadline).
+
+ (* Recall the definition of deadline miss. *)
+ Let no_deadline_missed_by :=
+ task_misses_no_deadline job_cost job_deadline job_task sched.
+
+ (* Next, we prove that ts is schedulable with the result of the test. *)
+ Corollary ts_is_schedulable:
+ forall tsk,
+ tsk \in ts ->
+ no_deadline_missed_by tsk.
+ Proof.
+ intros tsk IN.
+ have VALID := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
+ have EDFVALID := @edf_valid_policy _ arr_seq job_deadline.
+ unfold valid_JLDP_policy, valid_sporadic_job_with_jitter,
+ valid_sporadic_job, valid_realtime_job in *; des.
+ apply taskset_schedulable_by_edf_rta with (task_cost := task_cost) (task_period := task_period) (task_deadline := task_deadline) (ts0 := ts) (task_jitter := task_jitter) (job_jitter := job_jitter).
+ - by apply ts_is_a_set.
+ - by apply ts_has_valid_parameters.
+ - by apply ts_has_constrained_deadlines.
+ - by apply periodic_arrivals_all_jobs_from_taskset.
+ - by apply periodic_arrivals_valid_job_parameters, ts_has_valid_parameters.
+ - by apply periodic_arrivals_are_sporadic.
+ - by compute.
+ - by apply scheduler_jobs_execute_after_jitter.
+ - apply scheduler_completed_jobs_dont_execute; intro j'.
+ -- by specialize (VALID j'); des.
+ -- by apply periodic_arrivals_is_a_set.
+ - by apply scheduler_no_parallelism, periodic_arrivals_is_a_set.
+ - by apply scheduler_work_conserving.
+ - by apply scheduler_enforces_policy; ins.
+ - by apply schedulability_test_succeeds.
+ - by apply IN.
+ Qed.
+
+ End ExampleRTA.
+
+End ResponseTimeAnalysisEDF.
\ No newline at end of file
diff --git a/implementation/jitter/job.v b/implementation/jitter/job.v
new file mode 100644
index 000000000..441a6fb0e
--- /dev/null
+++ b/implementation/jitter/job.v
@@ -0,0 +1,63 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.implementation.jitter.task.
+Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteJob.
+
+ Import ConcreteTask.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_job :=
+ {
+ job_id: nat;
+ job_cost: nat;
+ job_deadline: nat;
+ job_jitter: nat;
+ job_task: concrete_task_eqType
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete jobs. *)
+ Definition job_eqdef (j1 j2: concrete_job) :=
+ (job_id j1 == job_id j2) &&
+ (job_cost j1 == job_cost j2) &&
+ (job_deadline j1 == job_deadline j2) &&
+ (job_jitter j1 == job_jitter j2) &&
+ (job_task j1 == job_task j2).
+
+ (* Next, we prove that job_eqdef is indeed an equality, ... *)
+ Lemma eqn_job : Equality.axiom job_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (job_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT; unfold job_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP DL] /eqP JITTER] /eqP TASK].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold job_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP TASK]; last by apply TASK; inversion BUG.
+ move: EQ => /orP [EQ | /eqP JITTER]; last by apply JITTER; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP DL]; last by apply DL; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID | /eqP COST]; last by apply COST; inversion BUG.
+ by apply ID; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_job_eqMixin := EqMixin eqn_job.
+ Canonical concrete_job_eqType := Eval hnf in EqType concrete_job concrete_job_eqMixin.
+
+ End Defs.
+
+End ConcreteJob.
\ No newline at end of file
diff --git a/implementation/jitter/schedule.v b/implementation/jitter/schedule.v
index c242c70f6..21d18bb3a 100644
--- a/implementation/jitter/schedule.v
+++ b/implementation/jitter/schedule.v
@@ -4,7 +4,7 @@ Require Import rt.model.jitter.job rt.model.jitter.arrival_sequence rt.model.jit
rt.model.jitter.platform rt.model.jitter.priority.
Require Import Program ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.
-Module WorkConservingScheduler.
+Module ConcreteScheduler.
Import Job ArrivalSequence ScheduleWithJitter Platform Priority.
@@ -217,9 +217,9 @@ Module WorkConservingScheduler.
(* Now, we prove the important properties about the implementation. *)
- (* Jobs do not execute before they arrive, ...*)
- Theorem scheduler_jobs_must_arrive_to_execute:
- jobs_must_arrive_to_execute sched.
+ (* Jobs do not execute before the jitter, ...*)
+ Theorem scheduler_jobs_execute_after_jitter:
+ jobs_execute_after_jitter job_jitter sched.
Proof.
unfold jobs_must_arrive_to_execute.
intros j t SCHED.
@@ -230,15 +230,13 @@ Module WorkConservingScheduler.
rewrite /update_schedule eq_refl in SCHED.
apply (nth_or_none_mem _ cpu j) in SCHED.
rewrite mem_sort mem_filter in SCHED.
- move: SCHED => /andP [_ ARR].
- by apply JobIn_has_arrived in ARR.
+ by move: SCHED => /andP [/andP [PENDING _] _].
}
{
unfold update_schedule at 1 in SCHED; rewrite eq_refl /= in SCHED.
apply (nth_or_none_mem _ cpu j) in SCHED.
rewrite mem_sort mem_filter in SCHED.
- move: SCHED => /andP [_ ARR].
- by apply JobIn_has_arrived in ARR.
+ by move: SCHED => /andP [/andP [PENDING _] _].
}
Qed.
@@ -340,4 +338,4 @@ Module WorkConservingScheduler.
End Proofs.
-End WorkConservingScheduler.
\ No newline at end of file
+End ConcreteScheduler.
\ No newline at end of file
diff --git a/implementation/jitter/task.v b/implementation/jitter/task.v
new file mode 100644
index 000000000..ac1e51da3
--- /dev/null
+++ b/implementation/jitter/task.v
@@ -0,0 +1,71 @@
+Add LoadPath "../../" as rt.
+Require Import rt.util.Vbase.
+Require Import rt.model.jitter.task.
+Require Import ssreflect ssrbool ssrnat eqtype seq.
+
+Module ConcreteTask.
+
+ Import SporadicTaskset.
+
+ Section Defs.
+
+ (* Definition of a concrete task. *)
+ Record concrete_task :=
+ {
+ task_id: nat; (* for uniqueness *)
+ task_cost: nat;
+ task_period: nat;
+ task_deadline: nat;
+ task_jitter: nat
+ }.
+
+ (* To make it compatible with ssreflect, we define a decidable
+ equality for concrete tasks. *)
+ Definition task_eqdef (t1 t2: concrete_task) :=
+ (task_id t1 == task_id t2) &&
+ (task_cost t1 == task_cost t2) &&
+ (task_period t1 == task_period t2) &&
+ (task_deadline t1 == task_deadline t2) &&
+ (task_jitter t1 == task_jitter t2).
+
+ (* Next, we prove that task_eqdef is indeed an equality, ... *)
+ Lemma eqn_task : Equality.axiom task_eqdef.
+ Proof.
+ unfold Equality.axiom; intros x y.
+ destruct (task_eqdef x y) eqn:EQ.
+ {
+ apply ReflectT.
+ unfold task_eqdef in *.
+ move: EQ => /andP [/andP [/andP [/andP [/eqP ID /eqP COST] /eqP PERIOD] /eqP DL] /eqP JITTER].
+ by destruct x, y; simpl in *; subst.
+ }
+ {
+ apply ReflectF.
+ unfold task_eqdef, not in *; intro BUG.
+ apply negbT in EQ; rewrite negb_and in EQ.
+ destruct x, y.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/orP [EQ | /eqP DL] | /eqP JITTER]; last by apply JITTER; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [EQ | /eqP DL]; last by apply DL; inversion BUG.
+ rewrite negb_and in EQ.
+ move: EQ => /orP [/eqP ID | /eqP PERIOD]; last by apply PERIOD; inversion BUG.
+ by apply ID; inversion BUG.
+ by apply DL; inversion BUG.
+ }
+ Qed.
+
+ (* ..., which allows instantiating the canonical structure. *)
+ Canonical concrete_task_eqMixin := EqMixin eqn_task.
+ Canonical concrete_task_eqType := Eval hnf in EqType concrete_task concrete_task_eqMixin.
+
+ End Defs.
+
+ Section ConcreteTaskset.
+
+ Definition concrete_taskset :=
+ taskset_of concrete_task_eqType.
+
+ End ConcreteTaskset.
+
+End ConcreteTask.
\ No newline at end of file
--
GitLab