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]
(** Throughout this file, we assume ideal uni-processor schedules. *)Require Import prosa.model.processor.ideal.Require Export prosa.analysis.facts.model.ideal.schedule.(** * Lemmas about Priority Inversion for ideal uni-processors *)(** In this section, we prove a few useful properties about the notion of priority inversion for ideal uni-processors. *)SectionPIIdealProcessorModelLemmas.(** 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 valid arrival sequence. *)Variablearr_seq : arrival_sequence Job.HypothesisH_valid_arrival_sequence : valid_arrival_sequence arr_seq.(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)Variablesched : schedule (ideal.processor_state Job).HypothesisH_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.(** ... where jobs do not execute before their arrival or after completion. *)HypothesisH_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.HypothesisH_completed_jobs_dont_execute : completed_jobs_dont_execute sched.(** Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive. *)Context {JLFP : JLFP_policy Job}.HypothesisH_priority_is_reflexive : reflexive_job_priorities JLFP.(** Let [tsk] be any task to be analyzed. *)Variabletsk : Task.(** Consider a job [j] of task [tsk]. In this subsection, job [j] is deemed to be the main job with respect to which the priority inversion is computed. *)Variablej : Job.HypothesisH_j_tsk : job_of_task tsk j.(** Consider a time instant [t]. *)Variablet : instant.(** We prove that if the processor is idle at time [t], then there is no priority inversion. *)
byrewrite is_idle_def.Qed.(** Next, consider an additional job [j'] and assume it is scheduled at time [t]. *)Variablej' : Job.HypothesisH_j'_sched : scheduled_at sched j' t.(** Then, we prove that from point of view of job [j], priority inversion appears iff [s] has lower priority than job [j]. *)
priority_inversion arr_seq sched j t = ~~ hep_job j' j
exact: priority_inversion_hep_job.Qed.(** Assume that [j'] has higher-or-equal priority than job [j], then we prove that there is no priority inversion for job [j]. *)
byrewrite priority_inversion_equiv_sched_lower_priority => ->.Qed.(** Assume that [j'] has lower priority than job [j], then we prove that [j] incurs priority inversion. *)