Commit c8db68d0 authored by Felipe Cerqueira's avatar Felipe Cerqueira

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.
parent 85faa1d3
......@@ -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\
......
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
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
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
......@@ -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
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
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
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.