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]
New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
Notation"_ - _" was already used in scope
distn_scope. [notation-overridden,parsing,default]
[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]
Require Export prosa.model.priority.elf.Require Export prosa.analysis.facts.priority.gel.Require Export prosa.analysis.facts.priority.elf.Require Export prosa.analysis.facts.priority.classes.Require Export prosa.analysis.facts.model.sequential.(** * Generality of ELF *)(** In the following, we make some formal remarks on the obvious generality of ELF w.r.t. Fixed Priority and GEL. *)(** We begin with the general setup. *)SectionGeneralityOfELF.(** Consider any type of tasks with relative priority points,...*)Context {Task : TaskType} `{PriorityPoint Task}.(** ...jobs of these tasks, and ... *)Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.(** ... any processor model. *)Context {PState : ProcessorState Job}.(** Suppose the jobs have arrival times and costs, and allow for any preemption and readiness models. *)Context {Arrival : JobArrival Job} {Cost : JobCost Job}
`{JobPreemptable Job} {JR: @JobReady Job PState Cost Arrival}.(** Suppose [fp] is the fixed-priority policy that parameterizes the ELF policy. *)Variablefp: FP_policy Task.(** ** ELF Generalizes GEL *)(** First, let us consider GEL scheduling, which by design ELF trivially generalizes. *)SectionELFGeneralizesGEL.(** If the [fp] fixed-priority policy assigns equal priority to all tasks... *)HypothesisH_FP_policy_is_same:
foralltsk1tsk2, ep_task tsk1 tsk2.(** ... then the ELF policy reduces to GEL. *)
bymove=> sched arr_seq
; split=> RESPECTED j j' t ARR PT BL SCHED
; move: (RESPECTED j j' t ARR PT BL SCHED)
; rewrite !hep_job_at_jlfp hep_job_elf_gel.Qed.(** ** ELF Generalizes Fixed-Priority Scheduling *)(** Next, let us turn to fixed-priority scheduling, which by design ELF also generalizes under certain assumptions. *)SectionELFGeneralizesFixedPriority.(** Since (1) ELF uses GEL only to break ties in fixed task priority, and since (2) a fixed-priority policy says nothing about how jobs of equal-priority tasks should be ordered (i.e., "ties in priority are broken arbitrarily"), an [ELF fp] schedule always is also a valid [fp] schedule. *)
bymove: (RESPECTED j j' t ARR PT BL SCHED)
; rewrite hep_job_at_jlfp /hep_job
=> /orP[/andP[HEP NOTHEP] //| /andP[HEP GEL] //].Qed.(** Additionally, if each task has a distinct priority, or equivalently, no two tasks have equal priority according to the [fp] fixed-priority policy, then the reverse also holds: the ELF policy reduces to the underlying FP policy. To show this, we require some additional setup and assumptions. *)(** First, assume that task priorities are indeed distinct. *)HypothesisH_distinct_fixed_priorities:
foralltsk1tsk2, tsk1 != tsk2 -> ~~ ep_task tsk1 tsk2.(** Second, consider any given valid arrival sequence.*)Variablearr_seq : arrival_sequence Job.HypothesisH_valid_arrival_sequence : valid_arrival_sequence arr_seq.(** Then in any given valid schedule ... *)Variablesched : schedule PState.HypothesisH_sched_valid : valid_schedule sched arr_seq.(** ... in which tasks execute sequentially ... *)HypothesisH_sequential : sequential_tasks arr_seq sched.(** ... the ELF policy and the underlying FP policy are equivalent. *)