Newer
Older
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.platform prosa.classic.model.schedule.apa.interference
prosa.classic.model.schedule.apa.interference_edf prosa.classic.model.schedule.apa.affinity.
Require Import prosa.classic.analysis.apa.workload_bound prosa.classic.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
(* In this file, we define the reduction-based interference bound for APA
scheduling with EDF, based on Bertogna and Cirinei's interference bound. *)
Module InterferenceBoundEDF.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
WorkloadBound ResponseTime Priority Affinity
TaskArrival Interference InterferenceEDF.
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
Export InterferenceBoundGeneric.
(* First we define Bertogna and Cirinei's EDF-specific interference bound. *)
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
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.
(* 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. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
(* Bertogna and Cirinei define the following bound for task interference
under EDF scheduling. *)
Definition edf_specific_interference_bound :=
let d_tsk := task_deadline tsk in
let e_other := task_cost tsk_other in
let p_other := task_period tsk_other in
let d_other := task_deadline tsk_other in
(div_floor d_tsk p_other) * e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other)).
End SpecificBoundDef.
(* Next, we define the total interference bound for EDF, which combines the generic
and the EDF-specific bounds. *)
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
Context {num_cpus: nat}.
(* Assume that each task has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task num_cpus.
Let task_with_response_time := (sporadic_task * time)%type.
(* Let tsk be the task to be analyzed, ... *)
Variable tsk: sporadic_task.
(* ... and let alpha' be any subaffinity of tsk. *)
Variable alpha': affinity num_cpus.
(* 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.
(* First we recall the interference bounds. *)
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* By combining Bertogna's interference bound for a work-conserving
scheduler ... *)
Let basic_interference_bound := interference_bound_generic task_cost task_period tsk delta tsk_R.
(* ... 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
under EDF scheduling. *)
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
(* Next we define the computation of the total interference for APA scheduling. *)
Section TotalInterference.
(* Let (other_task_in alpha') denote the other tasks that can execute on alpha'. *)
Let other_task_in alpha' := different_task_in alpha tsk alpha'.
(* The total interference incurred by tsk is bounded by the sum of individual
interferences of the other tasks that can be scheduled on alpha'. *)
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task_in alpha' tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
(* In this section, we show that the EDF-specific interference bound is safe. *)
Section ProofSpecificBound.
Import Schedule Interference Platform SporadicTaskset Affinity.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> time.
Variable task_period: sporadic_task -> time.
Variable task_deadline: sporadic_task -> time.
Context {Job: eqType}.
Variable job_arrival: Job -> time.
Variable job_cost: Job -> time.
Variable job_deadline: Job -> time.
Variable job_task: Job -> sporadic_task.
(* Assume any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
forall j,
arrives_in arr_seq j ->
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* ...jobs do not execute before their arrival times nor longer
than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Also assume that jobs are sequential and that
there exists at least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that every job at any time has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task num_cpus.
(* Consider a task set ts where all jobs come from the task set
and tasks have valid parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
forall j, arrives_in arr_seq j -> job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
forall tsk, tsk \in ts -> task_deadline tsk <= task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
(* Assume that the scheduler is a work-conserving EDF scheduler. *)
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
sched alpha (EDF job_arrival job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
(* ... and j_i one of its jobs. *)
Variable j_i: Job.
Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
(* Let tsk_k denote any interfering task, ... *)
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
(* ...and R_k its response-time bound. *)
Variable R_k: time.
Hypothesis H_R_k_le_deadline: R_k <= task_deadline tsk_k.
(* Consider a time window of length delta <= D_i, starting with j_i's arrival time. *)
Loading
Loading full blame...