# Library prosa.implementation.refinements.FP.preemptive_sched

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

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

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.analysis.facts.preemption.rtc_threshold.preemptive.

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.

## Fully-Preemptive Fixed-Priority Schedules

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

Consider any valid arrival sequence, ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.

... assume sequential readiness, ...

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

sequential_ready_instance arr_seq.

sequential_ready_instance arr_seq.

... and consider any fully-preemptive, fixed-priority schedule.

#[local] Existing Instance fully_preemptive_job_model.

#[local] Existing Instance NumericFPAscending.

Definition sched := uni_schedule arr_seq.

#[local] Existing Instance NumericFPAscending.

Definition sched := uni_schedule arr_seq.

First, we remark that such a schedule is valid.

Remark sched_valid :

valid_schedule sched arr_seq.

Proof.

apply uni_schedule_valid ⇒ //.

by apply sequential_readiness_nonclairvoyance.

Qed.

valid_schedule sched arr_seq.

Proof.

apply uni_schedule_valid ⇒ //.

by apply sequential_readiness_nonclairvoyance.

Qed.

Finally, we show that the fixed-priority policy is respected at each preemption point.

Lemma respects_policy_at_preemption_point :

respects_FP_policy_at_preemption_point arr_seq sched (NumericFPAscending Task).

Proof.

apply schedule_respects_policy ⇒ //.

by apply sequential_readiness_nonclairvoyance.

Qed.

End Schedule.

respects_FP_policy_at_preemption_point arr_seq sched (NumericFPAscending Task).

Proof.

apply schedule_respects_policy ⇒ //.

by apply sequential_readiness_nonclairvoyance.

Qed.

End Schedule.