# Library prosa.implementation.refinements.FP.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.sequential.
Require Export prosa.analysis.definitions.tardiness.
Require Export prosa.implementation.facts.ideal_uni.prio_aware.
Require Export prosa.implementation.definitions.task.
Require Export prosa.implementation.priority.numeric_fixed_priority.
Require Export prosa.implementation.readiness.sequential.

## Fully-Nonpreemptive Fixed-Priority Schedules

In this section, we prove some facts about the fully-nonpreemptive preemption policy under fixed-priority schedules.
Some lemmas in this file are not novel facts; they are used to uniform POET's certificates and minimize their verbosity.
Section Schedule.
In this file, we adopt the Prosa standard implementation of jobs and tasks.
Definition Task := concrete_task : eqType.
Definition Job := concrete_job : eqType.
Consider any valid arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... assume sequential readiness, ...
Instance sequential_ready_instance : JobReady Job (ideal.processor_state Job) :=
sequential.sequential_ready_instance arr_seq.
... and consider any fully-nonpreemptive, fixed-priority schedule.
#[local] Existing Instance fully_nonpreemptive_job_model.
#[local] Existing Instance numeric_fp_ascending.
Definition sched := uni_schedule arr_seq.
First, we show that only ready jobs execute.
Lemma sched_jobs_must_be_ready_to_execute :
jobs_must_be_ready_to_execute sched.
Next, we remark that such a schedule is valid.
Remark sched_valid :
valid_schedule sched arr_seq.
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.
Using the lemma above, we show that the schedule is nonpreemptive.
Lemma sched_nonpreemptive :
nonpreemptive_schedule (uni_schedule arr_seq).
Finally, we show that the fixed-priority policy is respected at each preemption point.
Lemma respects_policy_at_preemption_point_np :
respects_FP_policy_at_preemption_point arr_seq sched (numeric_fp_ascending Task).
End Schedule.