Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.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.
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation"_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]
Notation"[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * Service *)(** In this file, we establish basic facts about the service received by jobs. *)(** To begin with, we provide some simple but handy rewriting rules for [service] and [service_during]. *)SectionComposition.(** Consider any job type and any processor state. *)Context {Job: JobType}.Context {PState: ProcessorState Job}.(** For any given schedule... *)Variablesched: schedule PState.(** ...and any given job... *)Variablej: Job.(** ...we establish a number of useful rewriting rules that decompose the service received during an interval into smaller intervals. *)(** As a trivial base case, no job receives any service during an empty interval. *)
forallt : instant,
service_during sched j t t.+1 = service_at sched j t
bymove=> ?; rewrite /service_during big_nat_recr// big_geq.Qed.(** Next, we observe that we can look at the service received during an interval <<[t1, t3)>> as the sum of the service during [t1, t2) and [t2, t3) for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of the two intervals.) *)
move=> ? ? ?; exact: service_during_cat.Qed.(** As a special case, we observe that the service during an interval can be decomposed into the first instant and the rest of the interval. *)
forallt : instant,
service sched j t + service_at sched j t =
service sched j t.+1
move=> ?; exact: service_during_last_plus_before.Qed.(** Finally, we deconstruct the service received during an interval <<[t1, t3)>> into the service at a midpoint t2 and the service in the intervals before and after. *)
byrewrite t1t2 ltnW.Qed.EndComposition.(** As a common special case, we establish facts about schedules in which a job receives either 1 or 0 service units at all times. *)SectionUnitService.(** Consider any job type and any processor state. *)Context {Job : JobType}.Context {PState : ProcessorState Job}.(** Let's consider a unit-service model... *)HypothesisH_unit_service: unit_service_proc_model PState.(** ...and a given schedule. *)Variablesched : schedule PState.(** Let [j] be any job that is to be scheduled. *)Variablej : Job.(** First, we prove that the instantaneous service cannot be greater than 1, ... *)
service_at sched j t = 0 \/ service_at sched j t = 1
bycase: service_at (service_at_most_one t) => [|[|//]] _; [left|right].Qed.(** Next we prove that the cumulative service received by job [j] in any interval of length [delta] is at most [delta]. *)
service_during sched j t (t + delta) <=
\sum_(t <= x < t + delta) 1
apply: leq_sum => t' _; exact: service_at_most_one.Qed.(** Conversely, we prove that if the cumulative service received by job [j] in an interval of length [delta] is greater than or equal to [ρ], then [ρ ≤ delta]. *)
move=> ??? /leq_trans; apply; exact: cumulative_service_le_delta.Qed.SectionServiceIsUnitGrowthFunction.(** We show that the service received by any job [j] is a unit growth function. *)
exact: service_at_most_one.Qed.(** Next, consider any time [t]... *)Variablet : instant.(** ...and let [s] be any value less than the service received by job [j] by time [t]. *)Variables : duration.HypothesisH_less_than_s: s < service sched j t.(** Then, we show that there exists an earlier time [t'] where job [j] had [s] units of service. *)
Job: JobType PState: ProcessorState Job H_unit_service: unit_service_proc_model PState sched: schedule PState j: Job t: instant s: duration H_less_than_s: s < service sched j t
existst' : nat, t' < t /\ service sched j t' = s
Job: JobType PState: ProcessorState Job H_unit_service: unit_service_proc_model PState sched: schedule PState j: Job t: instant s: duration H_less_than_s: s < service sched j t
existst' : nat, t' < t /\ service sched j t' = s
Job: JobType PState: ProcessorState Job H_unit_service: unit_service_proc_model PState sched: schedule PState j: Job t: instant s: duration H_less_than_s: s < service sched j t
service sched j 0 <= s < service sched j t
byrewrite service0.Qed.EndServiceIsUnitGrowthFunction.EndUnitService.(** We establish a basic fact about the monotonicity of service. *)SectionMonotonicity.(** Consider any job type and any processor model. *)Context {Job: JobType}.Context {PState: ProcessorState Job}.(** Consider any given schedule... *)Variablesched: schedule PState.(** ...and a given job that is to be scheduled. *)Variablej: Job.(** We observe that the amount of service received is monotonic by definition. *)
forallt1t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
bymove=> t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr.Qed.EndMonotonicity.(** Consider any job type and any processor model. *)SectionRelationToScheduled.Context {Job: JobType}.Context {PState: ProcessorState Job}.(** Consider any given schedule... *)Variablesched: schedule PState.(** ...and a given job that is to be scheduled. *)Variablej: Job.(** We observe that a job that isn't scheduled in a given processor state cannot possibly receive service in that state. *)
0 < service_at sched j t -> scheduled_at sched j t
exact: service_at_implies_scheduled_at.Qed.(** We observe that a job receives cumulative service during some interval iff it receives services at some specific time in the interval. *)
exists2 x : nat_eqType,
x \in [seq _ <- index_iota t1 t2 | true] &
0 < service_at sched j x
byexistst; [rewrite filter_predT mem_index_iota|].Qed.(** Thus, any job that receives some service during an interval must be scheduled at some point during the interval... *)
existst : nat, t1 <= t < t2 /\ scheduled_at sched j t
existst'; split=> //; exact: service_at_implies_scheduled_at.Qed.(** ...which implies that any job with positive cumulative service must have been scheduled at some point. *)
forallt : instant,
0 < service sched j t ->
existst' : nat, t' < t /\ scheduled_at sched j t'
bymove=> t /cumulative_service_implies_scheduled[t' ?]; existst'.Qed.(** If we can assume that a scheduled job always receives service, we can further prove the converse. *)SectionGuaranteedService.(** Assume [j] always receives some positive service. *)HypothesisH_scheduled_implies_serviced: ideal_progress_proc_model PState.(** In other words, not being scheduled is equivalent to receiving zero service. *)
bymove=> + t titv; rewrite no_service_not_scheduled big_nat_eq0; apply.Qed.(** Conversely, if a job is not scheduled during an interval, then it does not receive any service in that interval *)
~~ scheduled_at sched j t -> service_at sched j t = 0
byrewrite no_service_not_scheduled.Qed.(** If a job is scheduled at some point in an interval, it receives positive cumulative service during the interval... *)
(existst' : nat, t' < t /\ scheduled_at sched j t') ->
0 < service sched j t
bymove=> [t' ?]; apply: scheduled_implies_cumulative_service; existst'.Qed.EndGuaranteedService.(** Furthermore, if we know that jobs are not released early, then we can narrow the interval during which they must have been scheduled. *)SectionAfterArrival.Context `{JobArrival Job}.(** Assume that jobs must arrive to execute. *)HypothesisH_jobs_must_arrive:
jobs_must_arrive_to_execute sched.(** We prove that any job with positive cumulative service at time [t] must have been scheduled some time since its arrival and before time [t]. *)
forallt : nat,
t < job_arrival j -> ~~ scheduled_at sched j t
bymove=> t ?; apply: (contra (H_jobs_must_arrive j t)); rewrite -ltnNge.Qed.(** We show that job [j] does not receive service at any time [t] prior to its arrival. *)
apply: service_before_job_arrival_zero; exact: leq_trans early.Qed.(** Hence, one can ignore the service received by a job before its arrival time... *)
forallt : nat,
t <= job_arrival j -> service sched j t = 0
exact: cumulative_service_before_job_arrival_zero.Qed.EndAfterArrival.(** In this section, we prove some lemmas about time instants with same service. *)SectionTimesWithSameService.(** Consider any time instants [t1] and [t2]... *)Variablet1t2: instant.(** ...where [t1] is no later than [t2]... *)HypothesisH_t1_le_t2: t1 <= t2.(** ...and where job [j] has received the same amount of service. *)HypothesisH_same_service: service sched j t1 = service sched j t2.(** First, we observe that this means that the job receives no service during <<[t1, t2)>>... *)
byapply/eqP/constant_service_implies_not_scheduled; rewrite t1_le_t /=.Qed.(** Then, under the assumption that scheduled jobs receives service, we can translate this into a claim about scheduled_at. *)(** Assume [j] always receives some positive service. *)HypothesisH_scheduled_implies_serviced: ideal_progress_proc_model PState.(** We show that job [j] is scheduled at some point [t < t1] iff [j] is scheduled at some point [t' < t2]. *)
byrewrite !CONV same_service_implies_serviced_at_earlier_times.Qed.EndTimesWithSameService.EndRelationToScheduled.SectionServiceInTwoSchedules.(** Consider any job type and any processor model. *)Context {Job: JobType}.Context {PState: ProcessorState Job}.(** Consider any two given schedules... *)Variablesched1sched2: schedule PState.(** Given an interval in which the schedules provide the same service to a job at each instant, we can prove that the cumulative service received during the interval has to be the same. *)SectionServiceDuringEquivalentInterval.(** Consider two time instants... *)Variablet1t2 : instant.(** ...and a given job that is to be scheduled. *)Variablej: Job.(** Assume that, in any instant between [t1] and [t2] the service provided to [j] from the two schedules is the same. *)HypothesisH_sched1_sched2_same_service_at:
forallt, t1 <= t < t2 ->
service_at sched1 j t = service_at sched2 j t.(** It follows that the service provided during [t1] and [t2] is also the same. *)
exact/eq_big_nat/H_sched1_sched2_same_service_at.Qed.EndServiceDuringEquivalentInterval.(** We can leverage the previous lemma to conclude that two schedules that match in a given interval will also have the same cumulative service across the interval. *)