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]
(** In this section, we prove a few properties about EDF policy. *) Section PropertiesOfEDF. (** Consider any type of tasks with relative deadlines ... *) Context {Task : TaskType}. Context `{TaskDeadline Task}. (** ... and any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{JobArrival Job}. Context `{JobCost Job}. (** Consider any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** EDF respects sequential tasks hypothesis. *)
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job

policy_respects_sequential_tasks
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job

policy_respects_sequential_tasks
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2

hep_job j1 j2
Task: TaskType
H: TaskDeadline Task
Job: JobType
H0: JobTask Job Task
H1: JobArrival Job
H2: JobCost Job
arr_seq: arrival_sequence Job
j1, j2: Job
TSK: job_task j1 = job_task j2
ARR: job_arrival j1 <= job_arrival j2

job_arrival j1 + task_deadline (job_task j2) <= job_arrival j2 + task_deadline (job_task j2)
by lia. Qed. End PropertiesOfEDF. (** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically. *) Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.
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]
(** In this section, we prove that EDF priority policy implies that tasks are sequential. *) Section SequentialEDF. (** Consider any type of tasks ... *) Context {Task : TaskType}. Context `{TaskCost Task}. Context `{TaskDeadline Task}. (** ... with a bound on the maximum non-preemptive segment length. The bound is needed to ensure that, at any instant, it always exists a subsequent preemption time in which the scheduler can, if needed, switch to another higher-priority job. *) Context `{TaskMaxNonpreemptiveSegment Task}. (** Further, consider any type of jobs associated with these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. Context `{Arrival : JobArrival Job}. Context `{Cost : JobCost Job}. (** Consider any arrival sequence. *) Variable arr_seq : arrival_sequence Job. (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *) Variable sched : schedule (ideal.processor_state Job). (** ... allow for any work-bearing notion of job readiness, ... *) Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}. Hypothesis H_job_ready : work_bearing_readiness arr_seq sched. (** ... and assume that the schedule is valid. *) Hypothesis H_sched_valid : valid_schedule sched arr_seq. (** In addition, we assume the existence of a function mapping jobs to their preemption points ... *) Context `{JobPreemptable Job}. (** ... and assume that it defines a valid preemption model with bounded non-preemptive segments. *) Hypothesis H_valid_preemption_model: valid_preemption_model arr_seq sched. (** Next, we assume that the schedule respects the scheduling policy at every preemption point. *) Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job). (** To prove sequentiality, we use lemma [early_hep_job_is_scheduled]. Clearly, under the EDF priority policy, jobs satisfy the conditions described by the lemma (i.e., given two jobs [j1] and [j2] from the same task, if [j1] arrives earlier than [j2], then [j1] always has a higher priority than job [j2], and hence completes before [j2]); therefore EDF implies sequential tasks. *)
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job)

sequential_tasks arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job)

sequential_tasks arr_seq sched
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2

scheduled_at sched j2 t -> completed_by sched j1 t
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant

hep_job_at t' j1 j2 && ~~ hep_job_at t' j2 j1
Task: TaskType
H: TaskCost Task
H0: TaskDeadline Task
H1: TaskMaxNonpreemptiveSegment Task
Job: JobType
H2: JobTask Job Task
Arrival: JobArrival Job
Cost: JobCost Job
arr_seq: arrival_sequence Job
sched: schedule (ideal.processor_state Job)
H3: JobReady Job (ideal.processor_state Job)
H_job_ready: work_bearing_readiness arr_seq sched
H_sched_valid: valid_schedule sched arr_seq
H4: JobPreemptable Job
H_valid_preemption_model: valid_preemption_model arr_seq sched
H_respects_policy: respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job)
j1, j2: Job
t: instant
ARR1: arrives_in arr_seq j1
ARR2: arrives_in arr_seq j2
SAME: job_task j1 = job_task j2
LT: job_arrival j1 < job_arrival j2
t': instant

(job_arrival j1 + task_deadline (job_task j2) <= job_arrival j2 + task_deadline (job_task j2)) && ~~ (job_arrival j2 + task_deadline (job_task j2) <= job_arrival j1 + task_deadline (job_task j2))
by lia. Qed. End SequentialEDF.