Built with Alectryon, running Coq+SerAPI v8.20.0+0.20.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]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_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]
Require Export prosa.analysis.facts.behavior.completion.Require Export prosa.analysis.definitions.service.(** * Service Inversion *)(** In this section, we define the notion of service inversion for arbitrary processors. *)SectionServiceInversion.(** Consider any type of tasks ... *)Context {Task : TaskType}.Context `{TaskCost Task}.(** ... and any type of jobs associated with these tasks. *)Context {Job : JobType}.Context `{JobTask Job Task}.Context `{JobArrival Job}.Context `{JobCost Job}.(** Next, consider _any_ kind of processor state model, ... *)Context {PState : ProcessorState Job}.(** ... any arrival sequence, ... *)Variablearr_seq : arrival_sequence Job.(** ... and any schedule of this arrival sequence. *)Variablesched : schedule PState.(** Assume a given JLDP policy. *)Context `{JLDP_policy Job}.(** Consider an arbitrary predicate on time intervals. *)VariableP : Job -> instant -> instant -> Prop.(** Consider a job [j]. *)Variablej : Job.(** We say that the job incurs service inversion if it has higher priority than the job receiving service. Note that this definition is oblivious to whether job [j] is ready. Therefore, it may not apply as intuitively expected in models with jitter or self-suspensions. Further generalization of the concept is likely necessary to efficiently analyze models in which jobs may be pending without being ready. *)Definitionservice_inversion (t : instant) :=
(j \notin served_jobs_at arr_seq sched t)
&& has (funjlp => ~~ hep_job_at t jlp j) (served_jobs_at arr_seq sched t).(** Then we compute the cumulative service inversion incurred by a job within some time interval <<[t1, t2)>>. *)Definitioncumulative_service_inversion (t1t2 : instant) :=
\sum_(t1 <= t < t2) service_inversion t.(** For proof purposes, it is often useful to bound the cumulative service interference in a time interval <<[t1, t2)>> that satisfies a given predicate (e.g., <<[t1, t2)>> is a busy interval prefix). To this end, we say that the cumulative service inversion of job [j] is bounded by a function [B : duration -> duration] w.r.t. to predicate [P] iff, for any interval <<[t1, t2)>> that satisfies [P j], the cumulative priority inversion in <<[t1, t2)>> is bounded by [B (job_arrival j - t1)]. *)Definitionpred_service_inversion_of_job_is_bounded_by (B : duration -> duration) :=
forall (t1t2 : instant),
P j t1 t2 ->
cumulative_service_inversion t1 t2 <= B (job_arrival j - t1).EndServiceInversion.(** In this section, we define a notion of the bounded service inversion for tasks. *)SectionTaskServiceInversionBound.(** Consider any type of tasks ... *)Context {Task : TaskType}.Context `{TaskCost Task}.(** ... and any type of jobs associated with these tasks. *)Context {Job : JobType}.Context `{JobTask Job Task}.Context `{JobArrival Job}.Context `{JobCost Job}.(** Consider _any_ kind of processor state model, ... *)Context {PState : ProcessorState Job}.(** ... any arrival sequence, ... *)Variablearr_seq : arrival_sequence Job.(** ... and any schedule. *)Variablesched : schedule PState.(** Assume a given JLDP policy. *)Context `{JLDP_policy Job}.(** Consider an arbitrary predicate on jobs and time intervals. *)VariableP : Job -> instant -> instant -> Prop.(** Consider an arbitrary task [tsk]. *)Variabletsk : Task.(** We say that task [tsk] has bounded service inversion if all its jobs have cumulative service inversion bounded by function [B : duration -> duration]. *)Definitionpred_service_inversion_is_bounded_by (B : duration -> duration) :=
forall (j : Job),
arrives_in arr_seq j ->
job_of_task tsk j ->
job_cost j > 0 ->
pred_service_inversion_of_job_is_bounded_by arr_seq sched P j B.EndTaskServiceInversionBound.