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. *) Section CompletionFacts. (** 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. *) Variable sched: schedule PState. (** Let [j] be any job that is to be scheduled. *) Variable j: Job. (** We prove that after job [j] completes, it remains completed. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t t' : nat, t <= t' -> completed_by sched j t -> completed_by sched j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t t' : 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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t t' : nat, t <= t' -> ~~ completed_by sched j t' -> ~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t t' : 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... *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, service sched j t < job_cost j <-> ~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, service sched j t < job_cost j <-> ~~ completed_by sched j t
by move=> ?; rewrite -ltnNge. Qed. (** ...which is also the same as having positive remaining cost. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, ~~ completed_by sched j t <-> 0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, ~~ completed_by sched j t <-> 0 < remaining_cost sched j t
by move=> ?; rewrite -less_service_than_cost_is_incomplete subn_gt0. Qed. (** Trivially, it follows that an incomplete job has a positive cost. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, ~~ completed_by sched j t -> job_cost_positive j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job

forall t : instant, ~~ completed_by sched j t -> job_cost_positive j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
t: instant
INCOMP: ~~ completed_by sched j t

0 < job_cost j - service sched j t
by rewrite -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. *) Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched. Hypothesis H_completed_jobs : completed_jobs_dont_execute sched. (** To simplify subsequent proofs, we restate the assumption [H_completed_jobs] as a trivial corollary. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

forall t : instant, scheduled_at sched j t -> service sched j t < job_cost j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

forall t : instant, scheduled_at sched j t -> service sched j t < job_cost j
exact: H_completed_jobs. Qed. (** We observe that a job that is completed at the instant of its arrival has a cost of zero. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

completed_by sched j (job_arrival j) -> job_cost j = 0
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

completed_by sched j (job_arrival j) -> job_cost j = 0
by rewrite /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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

forall t : instant, 0 < service_at sched j t -> 0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched

forall t : instant, 0 < service_at sched j t -> 0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
t: instant
SERVICE: 0 < service_at sched j t

0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
t: instant
SERVICE: 0 < service_at sched j t

~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
t: instant
SERVICE: 0 < service_at sched j t

service sched j t < job_cost j
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. *) Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState. (** To simplify subsequent proofs, we restate the assumption [H_scheduled_implies_serviced] as a trivial corollary. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall s : PState, scheduled_in j s -> 0 < service_in j s
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall s : PState, scheduled_in j s -> 0 < service_in j s
exact: H_scheduled_implies_serviced. Qed. (** Then a scheduled job has positive remaining cost. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, scheduled_at sched j t -> 0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, scheduled_at sched j t -> 0 < remaining_cost sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState
t: instant
sch: scheduled_at sched j t

0 < remaining_cost sched j t
exact/serviced_implies_positive_remaining_cost/scheduled_implies_serviced. Qed. (** We also prove that a scheduled job cannot be completed... *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, scheduled_at sched j t -> ~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, scheduled_at sched j t -> ~~ completed_by sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState
t: instant
sch: scheduled_at sched j t

~~ completed_by sched j t
by rewrite -less_service_than_cost_is_incomplete service_lt_cost. Qed. (** ... and that a completed job cannot be scheduled. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, completed_by sched j t -> ~~ scheduled_at sched j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched
H_completed_jobs: completed_jobs_dont_execute sched
H_scheduled_implies_serviced: ideal_progress_proc_model PState

forall t : instant, completed_by sched j t -> ~~ scheduled_at sched j t
move=> ? /negPn; exact/contra/scheduled_implies_not_completed. Qed. End CompletionFacts. (** 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. *) Section ServiceAndCompletionFacts. (** Consider any job type,...*) Context {Job: JobType}. Context `{JobCost Job}. (** ...any kind of processor model,... *) Context {PState: ProcessorState Job}. (** ...and a given schedule. *) Variable sched: schedule PState. (** Assume that completed jobs do not execute. *) Hypothesis H_completed_jobs: completed_jobs_dont_execute sched. (** Let [j] be any job that is to be scheduled. *) Variable j: Job. (** Assume that a scheduled job receives exactly one time unit of service. *) Hypothesis H_unit_service: unit_service_proc_model PState. (** To simplify subsequent proofs, we restate the assumption [H_unit_service] as a trivial corollary. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall s : PState, service_in j s <= 1
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall s : PState, service_in j s <= 1
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. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, service sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, service sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat

service sched j t <= job_cost j -> service sched j t.+1 <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat

service sched j t <= job_cost j -> service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
EQ: service sched j t = job_cost j

service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
EQ: service sched j t = job_cost j

service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
EQ: service sched j t = job_cost j

~~ scheduled_at sched j t
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
EQ: service sched j t = job_cost j

completed_by sched j t
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j
service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j

service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j

service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j

service_at sched j t <= 1 -> service sched j t + service_at sched j t <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: nat
LT: service sched j t < job_cost j

service sched j t + 1 <= job_cost j
by rewrite addn1. Qed. (** This lets us conclude that [service] and [remaining_cost] are complements of one another. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, service sched j t + remaining_cost sched j t = job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, service sched j t + remaining_cost sched j t = job_cost j
by move=> ?; rewrite subnKC// service_at_most_cost. Qed. (** We show that the service received by job [j] in any interval is no larger than its cost. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t t' : instant, service_during sched j t t' <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t t' : instant, service_during sched j t t' <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t, t': instant

service_during sched j t t' <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t, t': instant
t_lt_t': t < t'

service_during sched j t t' <= job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t, t': instant
t_lt_t': t < t'

service_during sched j t t' <= service sched j t'
by rewrite -(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]. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, ~~ completed_by sched j t -> ~~ completed_by sched j (t + remaining_cost sched j t - 1)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState

forall t : instant, ~~ completed_by sched j t -> ~~ completed_by sched j (t + remaining_cost sched j t - 1)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

~~ completed_by sched j (t + remaining_cost sched j t - 1)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

service sched j t + service_during sched j t (t + remaining_cost sched j t - 1) < job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

service sched j t + remaining_cost sched j t - 1 < job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t
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
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

service sched j t + remaining_cost sched j t - 1 < job_cost j
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

0 < job_cost j
exact/(leq_trans rem_cost)/leq_subr.
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

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
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
t: instant
rem_cost: 0 < remaining_cost sched j t

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
by rewrite -!addnBA// leq_add2l cumulative_service_le_delta. Qed. Section GuaranteedService. (** Assume a scheduled job always receives some positive service. *) Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState. (** Assume that jobs are not released early. *) Context `{JobArrival Job}. Hypothesis H_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. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
H_scheduled_implies_serviced: ideal_progress_proc_model PState
H0: JobArrival Job
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, scheduled_at sched j t -> has_arrived j t
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
H_scheduled_implies_serviced: ideal_progress_proc_model PState
H0: JobArrival Job
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, scheduled_at sched j t -> has_arrived j t
exact: H_jobs_must_arrive. Qed. (** We show that if job j is scheduled, then it must be pending. *)
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
H_scheduled_implies_serviced: ideal_progress_proc_model PState
H0: JobArrival Job
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, scheduled_at sched j t -> pending sched j t
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
H_scheduled_implies_serviced: ideal_progress_proc_model PState
H0: JobArrival Job
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, scheduled_at sched j t -> pending sched j t
Job: JobType
H: JobCost Job
PState: ProcessorState Job
sched: schedule PState
H_completed_jobs: completed_jobs_dont_execute sched
j: Job
H_unit_service: unit_service_proc_model PState
H_scheduled_implies_serviced: ideal_progress_proc_model PState
H0: JobArrival Job
H_jobs_must_arrive: jobs_must_arrive_to_execute sched
t: instant
sch: scheduled_at sched j t

~~ completed_by sched j t
exact: scheduled_implies_not_completed. Qed. End GuaranteedService. End ServiceAndCompletionFacts. (** In this section, we establish facts that on jobs with non-zero costs that must arrive to execute. *) Section PositiveCost. (** 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. *) Variable sched: schedule PState. (** Let [j] be any job that is to be scheduled. *) Variable j: 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, ... *) Hypothesis H_positive_cost: job_cost j > 0. (** ...and that jobs must arrive to execute. *) Hypothesis H_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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, completed_by sched j t -> exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

forall t : instant, completed_by sched j t -> exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched
t: instant
comp: completed_by sched j t

exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched
t: instant
comp: completed_by sched j t

0 < service sched j t -> exists t' : nat, job_arrival j <= t' < t /\ scheduled_at sched j t'
exact: positive_service_implies_scheduled_since_arrival. Qed. (** We also prove that the job is pending at the moment of its arrival. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

pending sched j (job_arrival j)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

pending sched j (job_arrival j)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState: ProcessorState Job
sched: schedule PState
j: Job
H_positive_cost: 0 < job_cost j
H_jobs_must_arrive: jobs_must_arrive_to_execute sched

~~ completed_by sched j (job_arrival j)
by rewrite /completed_by no_service_before_arrival// -ltnNge. Qed. End PositiveCost. Section CompletedJobs. (** Consider any kinds of jobs and any kind of processor state. *) Context {Job : JobType} {PState : ProcessorState Job}. (** Consider any schedule... *) Variable sched : 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... *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> ~~ completed_by sched j t
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall (j : Job) (t : instant), job_ready sched j t -> ~~ completed_by sched j t
by move=> ? ? /any_ready_job_is_pending /andP[]. Qed. (** ...and lift this observation also to the level of whole schedules. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> completed_jobs_dont_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

jobs_must_be_ready_to_execute sched -> completed_jobs_dont_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
j: Job
t: instant
sch: scheduled_at sched j t
ready: job_ready sched j t

service sched j t < job_cost j
by rewrite less_service_than_cost_is_incomplete ready_implies_incomplete. Qed. (** Furthermore, in a valid schedule, completed jobs don't execute. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> completed_jobs_dont_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

forall arr_seq : arrival_sequence Job, valid_schedule sched arr_seq -> completed_jobs_dont_execute sched
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. *)
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

ideal_progress_proc_model PState -> (forall (j : Job) (t : instant), service sched j t <= job_cost j) -> completed_jobs_dont_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState

ideal_progress_proc_model PState -> (forall (j : Job) (t : instant), service sched j t <= job_cost j) -> completed_jobs_dont_execute sched
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
IDEAL: ideal_progress_proc_model PState
SERVICE_BOUND: forall (j : Job) (t : instant), service sched j t <= job_cost j
j: Job
t: instant
SCHED: scheduled_at sched j t

service sched j t < job_cost j
Job: JobType
PState: ProcessorState Job
sched: schedule PState
H: JobCost Job
H0: JobArrival Job
jr: JobReady Job PState
IDEAL: ideal_progress_proc_model PState
SERVICE_BOUND: forall (j : Job) (t : instant), service sched j t <= job_cost j
j: Job
t: instant
SCHED: scheduled_at sched j t

service sched j t < service sched j t.+1
by rewrite -service_last_plus_before -addn1 leq_add2l IDEAL. Qed. End CompletedJobs. (** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically. *) Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_rt_facts. (** Next, we relate the completion of jobs in schedules with identical prefixes. *) Section CompletionInTwoSchedules. (** 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. *)
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState

forall (sched1 sched2 : schedule PState) (h : instant), identical_prefix sched1 sched2 h -> forall (j : Job) (t : nat), t <= h -> completed_by sched1 j t = completed_by sched2 j t
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState

forall (sched1 sched2 : schedule PState) (h : instant), identical_prefix sched1 sched2 h -> forall (j : Job) (t : nat), t <= h -> completed_by sched1 j t = completed_by sched2 j t
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState
sched1, sched2: schedule PState
h: instant
PREFIX: identical_prefix sched1 sched2 h
j: Job
t: nat
LE_h: t <= h

completed_by sched1 j t = completed_by sched2 j t
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState
sched1, sched2: schedule PState
h: instant
PREFIX: identical_prefix sched1 sched2 h
j: Job
t: nat
LE_h: t <= h

identical_prefix sched1 sched2 t
exact: identical_prefix_inclusion PREFIX. Qed. (** For convenience, we restate the previous lemma in terms of [pending]. *)
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState

forall (sched1 sched2 : schedule PState) (h : instant), identical_prefix sched1 sched2 h -> forall (j : Job) (t : nat), t <= h -> pending sched1 j t = pending sched2 j t
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState

forall (sched1 sched2 : schedule PState) (h : instant), identical_prefix sched1 sched2 h -> forall (j : Job) (t : nat), t <= h -> pending sched1 j t = pending sched2 j t
Job: JobType
PState: ProcessorState Job
jc: JobCost Job
ja: JobArrival Job
jr: JobReady Job PState
sched1, sched2: schedule PState
h: instant
PREFIX: identical_prefix sched1 sched2 h
j: Job
t: nat
t_le_h: t <= h

pending sched1 j t = pending sched2 j t
by rewrite /pending (identical_prefix_completed_by _ sched2 h). Qed. End CompletionInTwoSchedules.