# Library prosa.implementation.refinements.EDF.nonpreemptive_sched

Require Export prosa.analysis.facts.preemption.task.nonpreemptive.

Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.

Require Export prosa.analysis.facts.readiness.basic.

Require Export prosa.analysis.definitions.tardiness.

Require Export prosa.implementation.facts.ideal_uni.prio_aware.

Require Export prosa.implementation.definitions.task.

Require Export prosa.model.priority.edf.

Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.

Require Export prosa.analysis.facts.readiness.basic.

Require Export prosa.analysis.definitions.tardiness.

Require Export prosa.implementation.facts.ideal_uni.prio_aware.

Require Export prosa.implementation.definitions.task.

Require Export prosa.model.priority.edf.

## Fully-Nonpreemptive Earliest-Deadline-First Schedules

In this file, we adopt the Prosa standard implementation of jobs and tasks.

Consider any arrival sequence with consistent arrivals, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... assume basic readiness, ...

Instance basic_ready_instance : JobReady Job (ideal.processor_state Job) :=

basic.basic_ready_instance.

basic.basic_ready_instance.

... and consider any fully-nonpreemptive, earliest-deadline-first schedule.

#[local] Existing Instance fully_nonpreemptive_job_model.

#[local] Existing Instance EDF.

Definition sched := uni_schedule arr_seq.

#[local] Existing Instance EDF.

Definition sched := uni_schedule arr_seq.

First, we show that only ready jobs execute.

Next, we remark that such a schedule is valid.

Next, we show that an unfinished job scheduled at time t is
always scheduled at time t+1 as well. Note that the validity of
this fact also depends on which readiness model is used.

Lemma sched_nonpreemptive_next :

∀ j t,

scheduled_at sched j t →

~~ completed_by sched j t.+1 →

scheduled_at sched j t.+1.

∀ j t,

scheduled_at sched j t →

~~ completed_by sched j t.+1 →

scheduled_at sched j t.+1.

Using the lemma above, we show that the schedule is nonpreemptive.

Finally, we show that the earliest-deadline-first policy is respected
at each preemption point.