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]
(** * Completion *)(** In this file, we establish basic facts about job completions. *)SectionCompletionFacts.(** Consider any job type,...*)Context {Job: JobType}.Context `{JobCost Job}.Context `{JobArrival Job}.(** ...any kind of processor model,... *)Context {PState: ProcessorState Job}.(** ...and a given schedule. *)Variablesched: schedule PState.(** Let [j] be any job that is to be scheduled. *)Variablej: Job.(** We prove that after job [j] completes, it remains completed. *)
foralltt' : nat,
t <= t' ->
completed_by sched j t -> completed_by sched j t'
move=> ? ? ? /leq_trans; apply; exact: service_monotonic.Qed.(** We prove that if [j] is not completed by [t'], then it's also not completed by any earlier instant. *)
foralltt' : nat,
t <= t' ->
~~ completed_by sched j t' ->
~~ completed_by sched j t
move=> ? ? ?; exact/contra/completion_monotonic.Qed.(** We observe that being incomplete is the same as not having received sufficient service yet... *)
byrewrite -incomplete_is_positive_remaining_cost.Qed.(** In the remainder of this section, we assume that schedules are "well-formed": jobs are scheduled neither before their arrival nor after their completion. *)HypothesisH_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.HypothesisH_completed_jobs : completed_jobs_dont_execute sched.(** To simplify subsequent proofs, we restate the assumption [H_completed_jobs] as a trivial corollary. *)
byrewrite /completed_by no_service_before_arrival// leqn0 => /eqP.Qed.(** Further, we note that if a job receives service at some time t, then its remaining cost at this time is positive. *)
exact/service_lt_cost/service_at_implies_scheduled_at.Qed.(** Consequently, if we have a have processor model where scheduled jobs necessarily receive service, we can conclude that scheduled jobs have remaining positive cost. *)(** Assume a scheduled job always receives some positive service. *)HypothesisH_scheduled_implies_serviced: ideal_progress_proc_model PState.(** To simplify subsequent proofs, we restate the assumption [H_scheduled_implies_serviced] as a trivial corollary. *)
forallt : instant,
completed_by sched j t -> ~~ scheduled_at sched j t
move=> ? /negPn; exact/contra/scheduled_implies_not_completed.Qed.EndCompletionFacts.(** In this section, we establish some facts that are really about service, but are also related to completion and rely on some of the above lemmas. Hence they are in this file rather than in the service facts file. *)SectionServiceAndCompletionFacts.(** Consider any job type,...*)Context {Job: JobType}.Context `{JobCost Job}.(** ...any kind of processor model,... *)Context {PState: ProcessorState Job}.(** ...and a given schedule. *)Variablesched: schedule PState.(** Assume that completed jobs do not execute. *)HypothesisH_completed_jobs:
completed_jobs_dont_execute sched.(** Let [j] be any job that is to be scheduled. *)Variablej: Job.(** Assume that a scheduled job receives exactly one time unit of service. *)HypothesisH_unit_service: unit_service_proc_model PState.(** To simplify subsequent proofs, we restate the assumption [H_unit_service] as a trivial corollary. *)
exact: H_unit_service.Qed.(** To begin with, we establish that the cumulative service never exceeds a job's total cost if service increases only by one at each step since completed jobs don't execute. *)
byrewrite -(service_cat _ _ _ _ (ltnW t_lt_t')) leq_addl.Qed.(** If a job isn't complete at time [t], it can't be completed at time [t + remaining_cost j t - 1]. *)
service sched j t + remaining_cost sched j t - 1 <
job_cost j ->
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1) <
job_cost j
service sched j t + remaining_cost sched j t - 1 <
job_cost j ->
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1) < job_cost j
service sched j t +
service_during sched j t
(t + remaining_cost sched j t - 1) <=
service sched j t + remaining_cost sched j t - 1
byrewrite -!addnBA// leq_add2l cumulative_service_le_delta.Qed.SectionGuaranteedService.(** Assume a scheduled job always receives some positive service. *)HypothesisH_scheduled_implies_serviced: ideal_progress_proc_model PState.(** Assume that jobs are not released early. *)Context `{JobArrival Job}.HypothesisH_jobs_must_arrive: jobs_must_arrive_to_execute sched.(** To simplify subsequent proofs, we restate the assumption [H_jobs_must_arrive] as a trivial corollary. *)
exact: scheduled_implies_not_completed.Qed.EndGuaranteedService.EndServiceAndCompletionFacts.(** In this section, we establish facts that on jobs with non-zero costs that must arrive to execute. *)SectionPositiveCost.(** Consider any type of jobs with cost and arrival-time attributes,...*)Context {Job: JobType}.Context `{JobCost Job}.Context `{JobArrival Job}.(** ...any kind of processor model,... *)Context {PState: ProcessorState Job}.(** ...and a given schedule. *)Variablesched: schedule PState.(** Let [j] be any job that is to be scheduled. *)Variablej: Job.(** We assume that job [j] has positive cost, from which we can infer that there always is a time in which [j] is pending, ... *)HypothesisH_positive_cost: job_cost j > 0.(** ...and that jobs must arrive to execute. *)HypothesisH_jobs_must_arrive:
jobs_must_arrive_to_execute sched.(** Then, we prove that the job with a positive cost must be scheduled to be completed. *)
byrewrite /completed_by no_service_before_arrival// -ltnNge.Qed.EndPositiveCost.SectionCompletedJobs.(** Consider any kinds of jobs and any kind of processor state. *)Context {Job : JobType} {PState : ProcessorState Job}.(** Consider any schedule... *)Variablesched : schedule PState.(** ...and suppose that jobs have a cost, an arrival time, and a notion of readiness. *)Context `{JobCost Job}.Context `{JobArrival Job}.Context {jr : JobReady Job PState}.(** We observe that a given job is ready only if it is also incomplete... *)
move=> ? [? ?]; exact: completed_jobs_are_not_ready.Qed.(** We further observe that completed jobs don't execute if scheduled jobs always receive non-zero service and cumulative service never exceeds job costs. *)
byrewrite -service_last_plus_before -addn1 leq_add2l IDEAL.Qed.EndCompletedJobs.(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically. *)GlobalHint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_rt_facts.(** Next, we relate the completion of jobs in schedules with identical prefixes. *)SectionCompletionInTwoSchedules.(** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)Context {Job: JobType} {PState: ProcessorState Job}.Context {jc : JobCost Job} {ja : JobArrival Job} {jr : JobReady Job PState}.(** If two schedules share a common prefix, then (in the prefix) jobs complete in one schedule iff they complete in the other. *)