Library prosa.analysis.definitions.delay_propagation
In the following, consider two kinds of tasks, Task1 and Task2. We
seek to relate the arrivals of jobs of the Task1 kind to the arrivals of
jobs of the Task2 kind. In particular, we will derive an arrival curve
for the second kind from an arrival curve for the first kind under the
assumption that job arrivals are related in time within some known delay
bound.
Consider the corresponding jobs and their arrival times.
Context {Job1 Job2 : JobType}
`{JobTask Job1 Task1} `{JobTask Job2 Task2}
`(JobArrival Job1) `(JobArrival Job2).
`{JobTask Job1 Task1} `{JobTask Job2 Task2}
`(JobArrival Job1) `(JobArrival Job2).
Suppose there is a mapping of jobs (respectively, tasks) of the second
kind to jobs (respectively, tasks) of the first kind. For example, this
could be a "predecessor" or "triggered by" relationship.
Furthermore, suppose that the arrival time of any job of the second kind
occurs within a bounded time of the arrival of the corresponding job of the
first kind.
Propagation Validity
Second, the delay bound must indeed bound the separation between any two
jobs (for a given task set).
Let bounded_arrival_delay (ts : seq Task2) :=
∀ (j2 : Job2),
(job_task j2) \in ts →
job_arrival j2 ≤ job_arrival (job1_of j2) + delay_bound (job_task j2).
∀ (j2 : Job2),
(job_task j2) \in ts →
job_arrival j2 ≤ job_arrival (job1_of j2) + delay_bound (job_task j2).
In summary, a delay propagation mapping is valid for a given task set ts
if it both is structurally consistent (consistent_task_job_mapping) and
ensures bounded arrival delay (bounded_arrival_delay).
Definition valid_delay_propagation_mapping (ts : seq Task2) :=
consistent_task_job_mapping ∧ bounded_arrival_delay ts.
consistent_task_job_mapping ∧ bounded_arrival_delay ts.
Derived Arrival Curve
... we define an arrival curve for the second kind of tasks by "enlarging"
the analysis window by delay_bound ...
Let propagated_max_arrivals (tsk2 : Task2) (delta : duration) :=
if delta is 0 then 0
else max_arrivals (task1_of tsk2) (delta + delay_bound tsk2).
if delta is 0 then 0
else max_arrivals (task1_of tsk2) (delta + delay_bound tsk2).
.. and register this definition with Coq as a type class instance.
Derived Arrival Sequence
Furthermore, suppose we are given the inverse mapping of jobs, i.e., a
function that maps each job in the arrival sequence to the corresponding
job(s) of the second kind, ...
... and a function mapping each job of the second kind to the exact
delay that it incurs (relative to the arrival of its corresponding job of
the first kind).
Based on this information, we define the resulting arrival sequence of
jobs of the second kind.
Definition propagated_arrival_sequence t :=
let all := [seq job2_of j | j <- arrivals_up_to arr_seq1 t] in
[seq j2 <- flatten all | job_arrival (job1_of j2) + arrival_delay j2 == t].
let all := [seq job2_of j | j <- arrivals_up_to arr_seq1 t] in
[seq j2 <- flatten all | job_arrival (job1_of j2) + arrival_delay j2 == t].
The derived arrival sequence makes sense under the following assumptions:
First, job1_of and job2_of must agree.
Second, the inverse mapping must be a proper set for each job in arr_seq1.
Third, the claimed bound on arrival delay must indeed bound all delays
encountered.
Let valid_arrival_delay (ts : seq Task2) :=
∀ j2,
(job_task j2) \in ts →
arrives_in arr_seq1 (job1_of j2) →
arrival_delay j2 ≤ delay_bound (job_task j2).
∀ j2,
(job_task j2) \in ts →
arrives_in arr_seq1 (job1_of j2) →
arrival_delay j2 ≤ delay_bound (job_task j2).
Fourth, the arrival delay must indeed be the difference between the arrival
times of related jobs.
In summary, the derived arrival sequence is valid for a given task set
ts if all four above conditions are met.
Definition valid_arr_seq_propagation_mapping (ts : seq Task2) :=
[/\ consistent_job_mapping,job_mapping_uniq, valid_arrival_delay ts
& valid_job_arrival_def].
End ArrivalCurvePropagation.
[/\ consistent_job_mapping,job_mapping_uniq, valid_arrival_delay ts
& valid_job_arrival_def].
End ArrivalCurvePropagation.
Release Jitter Propagation
In the following, we instantiate the above-defined delay propagation for
release jitter.
Consider any type of tasks described by arrival curves ...
... and the corresponding jobs.
Let original_arrival denote each job's actual arrival time.
Suppose the jobs are affected by bounded release jitter.
Recall that a job's release time is the first time after its arrival
when it becomes ready for execution.
If we reinterpret release times as the effective arrival times ...
... then we obtain a valid "arrival" (= release) curve for this
reinterpretation by propagating the original arrival curve while
accounting for the jitter bounds.
By construction, this meets the delay-propagation validity
requirement.
Remark jitter_delay_mapping_valid :
∀ ts,
valid_jitter_bounds ts →
valid_delay_propagation_mapping
original_arrival release_as_arrival
id id task_jitter ts.
∀ ts,
valid_jitter_bounds ts →
valid_delay_propagation_mapping
original_arrival release_as_arrival
id id task_jitter ts.
Similarly, the induced "arrival" (= release) sequence ...
Definition release_sequence (arr_seq : arrival_sequence Job) :=
propagated_arrival_sequence original_arrival id arr_seq (fun j ⇒ [:: j]) job_jitter.
propagated_arrival_sequence original_arrival id arr_seq (fun j ⇒ [:: j]) job_jitter.
... meets all requirements of the generic delay-propagation
construction.