Commit f7a79913 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Major Commit - Prosa v0.2

- Add definitions related to APA scheduling
- Prove correctness of reduction-based RTA for APA scheduling (FP and EDF)
- Add implementation of a weak APA scheduler
- Update definition of taskset to assume uniqueness
- Modify names and comments to improve readability
- Remove strong assumptions about priority order in FP scheduling
- Add tests with FP RTA for every model
- Add tests for RTA with parallel jobs
parent 5534c06d
......@@ -14,7 +14,7 @@
#
# This Makefile was generated by the command line :
# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/exists.v ./util/induction.v ./util/sum.v ./util/divround.v ./util/counting.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
# coq_makefile -f _CoqProject ./util/fixedpoint.v ./util/ssromega.v ./util/bigcat.v ./util/nat.v ./util/seqset.v ./util/notation.v ./util/list.v ./util/powerset.v ./util/all.v ./util/sorting.v ./util/tactics.v ./util/bigord.v ./util/exists.v ./util/induction.v ./util/sum.v ./util/divround.v ./util/counting.v ./implementation/basic/bertogna_edf_example.v ./implementation/basic/task.v ./implementation/basic/schedule.v ./implementation/basic/bertogna_fp_example.v ./implementation/basic/job.v ./implementation/basic/arrival_sequence.v ./implementation/parallel/bertogna_edf_example.v ./implementation/parallel/task.v ./implementation/parallel/schedule.v ./implementation/parallel/bertogna_fp_example.v ./implementation/parallel/job.v ./implementation/parallel/arrival_sequence.v ./implementation/jitter/bertogna_edf_example.v ./implementation/jitter/task.v ./implementation/jitter/schedule.v ./implementation/jitter/bertogna_fp_example.v ./implementation/jitter/job.v ./implementation/jitter/arrival_sequence.v ./implementation/apa/bertogna_edf_example.v ./implementation/apa/task.v ./implementation/apa/schedule.v ./implementation/apa/bertogna_fp_example.v ./implementation/apa/job.v ./implementation/apa/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 ./analysis/apa/bertogna_fp_theory.v ./analysis/apa/interference_bound_edf.v ./analysis/apa/interference_bound_fp.v ./analysis/apa/interference_bound.v ./analysis/apa/bertogna_edf_comp.v ./analysis/apa/bertogna_fp_comp.v ./analysis/apa/bertogna_edf_theory.v ./analysis/apa/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/constrained_deadlines.v ./model/basic/workload.v ./model/basic/job.v ./model/basic/arrival_sequence.v ./model/basic/response_time.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/constrained_deadlines.v ./model/jitter/workload.v ./model/jitter/job.v ./model/jitter/arrival_sequence.v ./model/jitter/response_time.v ./model/apa/time.v ./model/apa/schedulability.v ./model/apa/task.v ./model/apa/task_arrival.v ./model/apa/platform.v ./model/apa/schedule.v ./model/apa/priority.v ./model/apa/affinity.v ./model/apa/interference_edf.v ./model/apa/interference.v ./model/apa/constrained_deadlines.v ./model/apa/workload.v ./model/apa/job.v ./model/apa/arrival_sequence.v ./model/apa/response_time.v -o Makefile
#
.DEFAULT_GOAL := all
......@@ -114,13 +114,27 @@ VFILES:=util/fixedpoint.v\
implementation/basic/bertogna_edf_example.v\
implementation/basic/task.v\
implementation/basic/schedule.v\
implementation/basic/bertogna_fp_example.v\
implementation/basic/job.v\
implementation/basic/arrival_sequence.v\
implementation/parallel/bertogna_edf_example.v\
implementation/parallel/task.v\
implementation/parallel/schedule.v\
implementation/parallel/bertogna_fp_example.v\
implementation/parallel/job.v\
implementation/parallel/arrival_sequence.v\
implementation/jitter/bertogna_edf_example.v\
implementation/jitter/task.v\
implementation/jitter/schedule.v\
implementation/jitter/bertogna_fp_example.v\
implementation/jitter/job.v\
implementation/jitter/arrival_sequence.v\
implementation/apa/bertogna_edf_example.v\
implementation/apa/task.v\
implementation/apa/schedule.v\
implementation/apa/bertogna_fp_example.v\
implementation/apa/job.v\
implementation/apa/arrival_sequence.v\
analysis/basic/bertogna_fp_theory.v\
analysis/basic/interference_bound_edf.v\
analysis/basic/interference_bound_fp.v\
......@@ -145,6 +159,14 @@ VFILES:=util/fixedpoint.v\
analysis/jitter/bertogna_fp_comp.v\
analysis/jitter/bertogna_edf_theory.v\
analysis/jitter/workload_bound.v\
analysis/apa/bertogna_fp_theory.v\
analysis/apa/interference_bound_edf.v\
analysis/apa/interference_bound_fp.v\
analysis/apa/interference_bound.v\
analysis/apa/bertogna_edf_comp.v\
analysis/apa/bertogna_fp_comp.v\
analysis/apa/bertogna_edf_theory.v\
analysis/apa/workload_bound.v\
model/basic/time.v\
model/basic/schedulability.v\
model/basic/task.v\
......@@ -154,11 +176,11 @@ VFILES:=util/fixedpoint.v\
model/basic/priority.v\
model/basic/interference_edf.v\
model/basic/interference.v\
model/basic/constrained_deadlines.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\
......@@ -168,11 +190,26 @@ VFILES:=util/fixedpoint.v\
model/jitter/priority.v\
model/jitter/interference_edf.v\
model/jitter/interference.v\
model/jitter/constrained_deadlines.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/apa/time.v\
model/apa/schedulability.v\
model/apa/task.v\
model/apa/task_arrival.v\
model/apa/platform.v\
model/apa/schedule.v\
model/apa/priority.v\
model/apa/affinity.v\
model/apa/interference_edf.v\
model/apa/interference.v\
model/apa/constrained_deadlines.v\
model/apa/workload.v\
model/apa/job.v\
model/apa/arrival_sequence.v\
model/apa/response_time.v
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(VFILES))
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Require Import rt.util.all.
Require Import rt.model.apa.schedule.
Require Import rt.analysis.apa.workload_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundGeneric.
Section Definitions.
Import Schedule WorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
Variable num_cpus: nat.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
Section PerTask.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound_generic :=
minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
End PerTask.
End Definitions.
End InterferenceBoundGeneric.
\ No newline at end of file
This diff is collapsed.
Require Import rt.util.all.
Require Import rt.model.apa.schedule rt.model.apa.priority rt.model.apa.workload
rt.model.apa.interference rt.model.apa.affinity.
Require Import rt.analysis.apa.workload_bound rt.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module InterferenceBoundFP.
Import Schedule WorkloadBound Priority Interference Affinity.
Export InterferenceBoundGeneric.
Section Definitions.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
(* Assume that each task has a processor affinity alpha. *)
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ... under subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* Recall the generic interference bound. *)
Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.
(* Let (hp_task_in alpha') denote the higher-priority tasks that can execute on alpha'. *)
Let hp_task_in alpha' := higher_priority_task_in alpha higher_eq_priority tsk alpha'.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences of tasks in (hp_task_in alpha'). *)
Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev | hp_task_in alpha' tsk_other)
total_interference_bound (tsk_other, R_other).
End Definitions.
End InterferenceBoundFP.
\ No newline at end of file
This diff is collapsed.
......@@ -57,7 +57,7 @@ Module ResponseTimeIterationEDF.
(* To compute the response-time bounds of the entire task set,
We start the iteration with a sequence of tasks and costs:
<(task1, cost1), (task2, cost2), ...>. *)
Let initial_state (ts: taskset_of sporadic_task) :=
Let initial_state (ts: seq sporadic_task) :=
map (fun t => (t, task_cost t)) ts.
(* Then, we successively update the the response-time bounds based
......@@ -68,13 +68,13 @@ Module ResponseTimeIterationEDF.
(* 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) :=
Let max_steps (ts: seq sporadic_task) :=
\sum_(tsk <- ts) (task_deadline tsk - task_cost tsk) + 1.
(* 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) :=
Definition edf_claimed_bounds (ts: seq sporadic_task) :=
let R_values := iter (max_steps ts) edf_rta_iteration (initial_state ts) in
if (all R_le_deadline R_values) then
Some R_values
......@@ -82,7 +82,7 @@ Module ResponseTimeIterationEDF.
(* The schedulability test simply checks if we got a list of
response-time bounds (i.e., if the computation did not fail). *)
Definition edf_schedulable (ts: taskset_of sporadic_task) :=
Definition edf_schedulable (ts: seq sporadic_task) :=
edf_claimed_bounds ts != None.
(* In the following section, we prove several helper lemmas about the
......@@ -205,7 +205,7 @@ Module ResponseTimeIterationEDF.
Section Convergence.
(* Consider any valid task set. *)
Variable ts: taskset_of sporadic_task.
Variable ts: seq sporadic_task.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
......@@ -395,11 +395,11 @@ Module ResponseTimeIterationEDF.
assert (SUBST: forall l delta,
\sum_(j <- l | let '(tsk_other, _) := j in
jldp_can_interfere_with tsk_i tsk_other)
different_task tsk_i tsk_other)
(let '(tsk_other, R_other) := j in
interference_bound_edf task_cost task_period task_deadline tsk_i delta
(tsk_other, R_other)) =
\sum_(j <- l | jldp_can_interfere_with tsk_i (fst j))
\sum_(j <- l | different_task tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta j).
{
intros l x; clear -l.
......@@ -444,13 +444,14 @@ Module ResponseTimeIterationEDF.
}
move: GE_COST => /allP GE_COST.
assert (LESUM: \sum_(j <- x1' | jldp_can_interfere_with tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta j <= \sum_(j <- x2' | jldp_can_interfere_with tsk_i (fst j))
assert (LESUM: \sum_(j <- x1' | different_task tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta j <=
\sum_(j <- x2' | different_task tsk_i (fst j))
interference_bound_edf task_cost task_period task_deadline tsk_i delta' j).
{
set elem := (tsk0, R0); rewrite 2!(big_nth elem).
rewrite -SIZE.
rewrite big_mkcond [\sum_(_ <- _ | jldp_can_interfere_with _ _)_]big_mkcond.
rewrite big_mkcond [\sum_(_ <- _ | different_task _ _)_]big_mkcond.
rewrite big_seq_cond [\sum_(_ <- _ | true) _]big_seq_cond.
apply leq_sum; intros j; rewrite andbT; intros INj.
rewrite mem_iota add0n subn0 in INj; move: INj => /andP [_ INj].
......@@ -459,7 +460,7 @@ Module ResponseTimeIterationEDF.
have MAP := @nth_map _ elem _ tsk0 (fun x => fst x).
by rewrite -2?MAP -?SIZE //; f_equal.
} rewrite -FSTeq.
destruct (jldp_can_interfere_with tsk_i (fst (nth elem x1' j))) eqn:INTERF;
destruct (different_task tsk_i (fst (nth elem x1' j))) eqn:INTERF;
last by done.
{
exploit (LE elem); [by rewrite /= SIZE | | intro LEj].
......@@ -485,7 +486,7 @@ Module ResponseTimeIterationEDF.
by apply interference_bound_edf_monotonic.
}
}
destruct (jldp_can_interfere_with tsk_i tsk0) eqn:INTERFtsk0; last by done.
destruct (different_task tsk_i tsk0) eqn:INTERFtsk0; last by done.
apply leq_add; last by done.
{
exploit (LE (tsk0, R0)); [by rewrite /= SIZE | | intro LEj];
......@@ -820,15 +821,13 @@ Module ResponseTimeIterationEDF.
Qed.
(* Therefore, with regard to the response-time bound recurrence, ...*)
Let rt_recurrence (tsk: sporadic_task) (rt_bounds: seq task_with_response_time) (R: time) :=
task_cost tsk + div_floor (I rt_bounds tsk R) num_cpus.
(* ..., the individual response-time bounds (elements of the list) are also fixed points. *)
Theorem edf_claimed_bounds_finds_fixed_point_for_each_bound :
forall tsk R rt_bounds,
edf_claimed_bounds ts = Some rt_bounds ->
(tsk, R) \in rt_bounds ->
R = rt_recurrence tsk rt_bounds R.
R = edf_response_time_bound rt_bounds tsk R.
Proof.
intros tsk R rt_bounds SOME IN.
have CONV := edf_claimed_bounds_finds_fixed_point_of_list rt_bounds.
......@@ -858,17 +857,14 @@ Module ResponseTimeIterationEDF.
Section MainProof.
(* Consider a task set ts. *)
(* Consider a task set ts where... *)
Variable ts: taskset_of sporadic_task.
(* Assume the task set has no duplicates, ... *)
Hypothesis H_ts_is_a_set: uniq ts.
(* ...all tasks have valid parameters, ... *)
(* ...all tasks have valid parameters ... *)
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
(* ...constrained deadlines, ...*)
(* ...and constrained deadlines. *)
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -34,7 +34,7 @@ Module InterferenceBoundGeneric.
(* Based on the workload bound, Bertogna and Cirinei define the
following interference bound for a task. *)
Definition interference_bound_generic :=
minn (W task_cost task_period tsk_other R_other delta) (delta - (task_cost tsk) + 1).
minn (W task_cost task_period tsk_other R_other delta) (delta - task_cost tsk + 1).
End PerTask.
......
......@@ -64,7 +64,7 @@ Module InterferenceBoundEDF.
(* ... and an interval length delta. *)
Variable delta: time.
Section PerTask.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
......@@ -82,19 +82,21 @@ Module InterferenceBoundEDF.
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End PerTask.
End RecallInterferenceBounds.
Section AllTasks.
(* Next we define the computation of the total interference for APA scheduling. *)
Section TotalInterference.
Let interferes_with_tsk := jldp_can_interfere_with tsk.
(* Let other_task denote tasks different from tsk. *)
Let other_task := different_task tsk.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences. *)
of individual task interferences of the other tasks. *)
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | interferes_with_tsk tsk_other)
\sum_((tsk_other, R_other) <- R_prev | other_task tsk_other)
interference_bound_edf (tsk_other, R_other).
End AllTasks.
End TotalInterference.
End TotalInterferenceBoundEDF.
......
......@@ -21,22 +21,22 @@ Module InterferenceBoundFP.
Let task_with_response_time := (sporadic_task * time)%type.
(* Assume a known response-time bound for each interfering task ... *)
(* Assume a known response-time bound for each higher-priority task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
(* ... in any interval of length delta. *)
Variable delta: time.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.
(* Recall the generic interference bound. *)
Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences. *)
Definition total_interference_bound_fp :=
\sum_((tsk_other, R_other) <- R_prev | can_interfere_with_tsk tsk_other)
\sum_((tsk_other, R_other) <- R_prev)
total_interference_bound (tsk_other, R_other).
End Definitions.
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment