Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
(** * Arrival Curve Propagation *)SectionArrivalCurvePropagation.(** 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. *)Context {Task1Task2 : TaskType}.(** Consider the corresponding jobs and their arrival times. *)Context {Job1Job2 : JobType}
`{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. *)Variablejob1_of : Job2 -> Job1.Variabletask1_of : Task2 -> Task1.(** 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. *)Variabledelay_bound : Task2 -> duration.(** ** Propagation Validity *)(** Before we continue, let us note under which assumptions delay propagation works. *)(** First, the task- and job-level mappings of course need to agree. *)Letconsistent_task_job_mapping :=
forallj2 : Job2,
job_task (job1_of j2) = task1_of (job_task j2).(** Second, the delay bound must indeed bound the separation between any two jobs (for a given task set). *)Letbounded_arrival_delay (ts : seq Task2) :=
forall (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]). *)Definitionvalid_delay_propagation_mapping (ts : seq Task2) :=
consistent_task_job_mapping /\ bounded_arrival_delay ts.(** ** Derived Arrival Curve *)(** Under the above assumptions, given an arrival curve for the first kind of tasks ... *)Context `{MaxArrivals Task1}.(** ... we define an arrival curve for the second kind of tasks by "enlarging" the analysis window by [delay_bound] ... *)Letpropagated_max_arrivals (tsk2 : Task2) (delta : duration) :=
if delta is0then0else max_arrivals (task1_of tsk2) (delta + delay_bound tsk2).(** .. and register this definition with Coq as a type class instance. *)#[local]
Instancepropagated_arrival_curve : MaxArrivals Task2 := propagated_max_arrivals.(** ** Derived Arrival Sequence *)(** In a similar fashion, we next derive an arrival sequence of jobs of the second kind. *)(** To this end, suppose we are given an arrival sequence for jobs of the first kind. *)Variablearr_seq1 : arrival_sequence Job1.(** 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, ... *)Variablejob2_of : Job1 -> seq Job2.(** ... 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). *)Variablearrival_delay : Job2 -> duration.(** Based on this information, we define the resulting arrival sequence of jobs of the second kind. *)Definitionpropagated_arrival_sequencet :=
letall := [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. *)Letconsistent_job_mapping :=
forallj1j2,
j2 \in job2_of j1 <-> job1_of j2 = j1.(** Second, the inverse mapping must be a proper set for each job in [arr_seq1]. *)Definitionjob_mapping_uniq :=
forallj1,
arrives_in arr_seq1 j1 -> uniq (job2_of j1).(** Third, the claimed bound on arrival delay must indeed bound all delays encountered. *)Letvalid_arrival_delay (ts : seq Task2) :=
forallj2,
(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. *)Letvalid_job_arrival_def :=
forallj2,
job_arrival j2 = job_arrival (job1_of j2) + arrival_delay j2.(** In summary, the derived arrival sequence is valid for a given task set [ts] if all four above conditions are met. *)Definitionvalid_arr_seq_propagation_mapping (ts : seq Task2) :=
[/\ consistent_job_mapping,job_mapping_uniq, valid_arrival_delay ts
& valid_job_arrival_def].EndArrivalCurvePropagation.(** * Release Jitter Propagation *)(** Under some scheduling policies, notably fixed-priority scheduling, it can be useful to "fold" release jitter into the arrival curve. This can be achieved in terms of the above-defined propagation operation. *)(** To this end, recall the definition of release jitter. *)Require Export prosa.model.task.jitter.(** In the following, we instantiate the above-defined delay propagation for release jitter. *)SectionReleaseJitterPropagation.(** Consider any type of tasks described by arrival curves ... *)Context {Task : TaskType} `{MaxArrivals Task}.(** ... and the corresponding jobs. *)Context {Job : JobType} `{JobTask Job Task}.(** Let [original_arrival] denote each job's _actual_ arrival time. *)Context {original_arrival : JobArrival Job}.(** Suppose the jobs are affected by bounded release jitter. *)Context `{TaskJitter Task} `{JobJitter Job}.(** Recall that a job's _release time_ is the first time after its arrival when it becomes ready for execution. *)Letjob_releasej := job_arrival j + job_jitter j.(** If we _reinterpret_ release times as the _effective_ arrival times ... *)#[local]
Instancerelease_as_arrival : JobArrival Job := job_release.(** ... then we obtain a valid "arrival" (= release) curve for this reinterpretation by propagating the original arrival curve while accounting for the jitter bounds. *)#[local]
Instancerelease_curve : MaxArrivals Task :=
propagated_arrival_curve id task_jitter.(** By construction, this meets the delay-propagation validity requirement. *)