Project Page Index Table of Contents

# Library prosa.analysis.facts.readiness_interference

Require Export prosa.analysis.definitions.readiness_interference.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.facts.interference.
Require Export prosa.analysis.definitions.service_inversion.readiness_aware.
In this file, we establish facts about readiness interference.
Section ReadinessInterference.
Consider any kind of jobs with arrival times and execution costs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any processor state model.
Context `{PState : ProcessorState Job}.
Consider any notion of job readiness.
Context `{!JobReady Job PState}.
Consider any valid arrival sequence of jobs ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any valid schedule of the given arrival sequence.
Variable sched : schedule PState.
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Allow for any JLFP priority policy.
Context {JLFP : JLFP_policy Job}.
First, note that readiness interference is exclusive of the interference due to other higher-or-equal-priority jobs.
Lemma no_hep_ready_implies_no_another_hep_interference :
∀ j t,
~~ some_hep_job_ready arr_seq sched j t →
~~ another_hep_job_interference arr_seq sched j t.
Proof.
move⇒ j t /hasPn NO_HEP_READY.
apply/negP ⇒ /hasP[jo INjo /andP[HEP NEQ]].
move: INjo; rewrite mem_filter ⇒ /andP[SERVjo INjo].
have SCHEDjo : scheduled_at sched jo t by apply service_at_implies_scheduled_at.
have PENDjo : pending sched jo t by apply scheduled_implies_pending.
have READYjo : job_ready sched jo t by done.
have IN : jo \in [seq j' <- arrivals_up_to arr_seq t | hep_job j' j].
{ rewrite mem_filter.
by do 2! [apply /andP; split; eauto]. }
by move: (NO_HEP_READY jo IN); rewrite READYjo.
Qed.
Next, we observe that readiness interference is exclusive of service inversion.
Lemma no_hep_ready_implies_no_service_inversion :
∀ j t,
~~ some_hep_job_ready arr_seq sched j t →
~~ service_inversion arr_seq sched j t.
Proof.
move⇒ j t NO_HEP_READY.
by rewrite /service_inversion; apply/nandP; left.
Qed.
End ReadinessInterference.