diff --git a/implementation/definitions/generic_scheduler.v b/implementation/definitions/generic_scheduler.v
new file mode 100644
index 0000000000000000000000000000000000000000..7270f996bc4203e97b3814d4ac1d8a55dae3dfa7
--- /dev/null
+++ b/implementation/definitions/generic_scheduler.v
@@ -0,0 +1,55 @@
+Require Export prosa.analysis.transform.swap.
+
+(** * Generic Reference Scheduler *)
+
+(** In this file, we provide a generic procedure that produces a schedule by
+ making a decision on what to schedule at each point in time. *)
+
+(** To begin with, we define the notion of a pointwise scheduling policy that
+ makes a decision at a given time [t] based on given prefix up to time
+ [t.-1]. *)
+Section PointwisePolicy.
+ (** Consider any type of jobs and type of schedule. *)
+ Context {Job : JobType}.
+ Variable PState : Type.
+
+ (** A pointwise scheduling policy is a function that, given a schedule prefix
+ that is valid up to time [t - 1], decides what to schedule at time
+ [t]. *)
+ Definition PointwisePolicy := schedule PState -> instant -> PState.
+End PointwisePolicy.
+
+Section GenericSchedule.
+ (** Consider any type of jobs and type of schedule. *)
+ Context {Job : JobType} {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** Suppose we are given a policy function that, given a schedule prefix that
+ is valid up to time [t - 1], decides what to schedule at time [t]. *)
+ Variable policy : PointwisePolicy PState.
+
+ (** Let [idle_state] denote the processor state that indicates that the
+ entire system is idle. *)
+ Variable idle_state : PState.
+
+ (** We construct the schedule step by step starting from an "empty" schedule
+ that is idle at all times as a base case. *)
+ Definition empty_schedule: schedule PState := fun _ => idle_state.
+
+ (** Next, we define a function that computes a schedule prefix up to a given
+ time horizon [h]. *)
+ Fixpoint schedule_up_to (h : instant) :=
+ let
+ prefix := if h is h'.+1 then schedule_up_to h' else empty_schedule
+ in
+ replace_at prefix h (policy prefix h).
+
+ (** Finally, we define the generic schedule as follows: for a
+ given point in time [t], we compute the finite prefix up to and including
+ [t], namely [schedule_up_to t], and then return the job scheduled at time
+ [t] in that prefix. *)
+ Definition generic_schedule (t : instant) : PState :=
+ schedule_up_to t t.
+
+End GenericSchedule.
+
diff --git a/implementation/definitions/ideal_uni_scheduler.v b/implementation/definitions/ideal_uni_scheduler.v
new file mode 100644
index 0000000000000000000000000000000000000000..d87919807d2a93a4e5853f63915c2a8bd76b530a
--- /dev/null
+++ b/implementation/definitions/ideal_uni_scheduler.v
@@ -0,0 +1,105 @@
+Require Export prosa.implementation.definitions.generic_scheduler.
+
+Require Export prosa.model.preemption.parameter.
+Require Export prosa.model.schedule.priority_driven.
+Require Export prosa.analysis.facts.readiness.backlogged.
+Require Export prosa.analysis.transform.swap.
+
+(** * Ideal Uniprocessor Reference Scheduler *)
+
+(** In this file, we provide a generic priority-aware scheduler that produces
+ an ideal uniprocessor schedule for a given arrival sequence. The scheduler
+ respects nonpreemptive sections and arbitrary readiness models. *)
+
+(** The following definitions assume ideal uniprocessor schedules. *)
+Require prosa.model.processor.ideal.
+
+Section UniprocessorScheduler.
+
+ (** Consider any type of jobs with costs and arrival times, ... *)
+ Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
+
+ (** .. in the context of an ideal uniprocessor model. *)
+ Let PState := ideal.processor_state Job.
+ Let idle_state : PState := None.
+
+ (** Suppose we are given a consistent arrival sequence of such jobs ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
+
+ (** ... and a non-clairvoyant readiness model. *)
+ Context {RM: JobReady Job (ideal.processor_state Job)}.
+ Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
+
+ (** ** Preemption-Aware Scheduler *)
+
+ (** First, we define the notion of a generic uniprocessor scheduler that is
+ cognizant of non-preemptive sections, ... *)
+
+ (** ... so consider any preemption model. *)
+ Context `{JobPreemptable Job}.
+
+ Section NonPreemptiveSectionAware.
+
+ (** Suppose we are given a scheduling policy that applies when jobs are
+ preemptive: given a set of jobs ready at time [t], select which to run
+ (if any) at time [t]. *)
+ Variable choose_job : instant -> seq Job -> option Job.
+
+ (** The next job is then chosen either by [policy] (if the current job is
+ preemptive or the processor is idle) or a non-preemptively executing job
+ continues to execute. *)
+ Section JobAllocation.
+
+ (** Consider a finite schedule prefix ... *)
+ Variable sched_prefix : schedule (ideal.processor_state Job).
+
+ (** ... that is valid up to time [t - 1]. *)
+ Variable t : instant.
+
+ (** We define a predicate that tests whether the job scheduled at the
+ previous instant (if [t > 0]) is nonpreemptive (and hence needs to be
+ continued to be scheduled). *)
+ Definition prev_job_nonpreemptive : bool :=
+ match t with
+ | 0 => false
+ | S t' => if sched_prefix t' is Some j then
+ ~~job_preemptable j (service sched_prefix j t)
+ else
+ false
+ end.
+
+ (** Based on the [prev_job_nonpreemptive] predicate, either the previous
+ job continues to be scheduled or the given policy chooses what to run
+ instead. *)
+ Definition allocation_at : option Job :=
+ if prev_job_nonpreemptive then
+ sched_prefix t.-1
+ else
+ choose_job t (jobs_backlogged_at arr_seq sched_prefix t).
+ End JobAllocation.
+
+ (* A preemption-policy-aware ideal uniprocessor schedule is then produced
+ when using [allocation_at] as the policy for the generic scheduler. *)
+ Definition np_uni_schedule : schedule PState := generic_schedule allocation_at idle_state.
+
+ End NonPreemptiveSectionAware.
+
+ (** ** Priority-Aware Scheduler *)
+
+ (** Building on the preemption-model aware scheduler, we next define a simple priority-aware scheduler. *)
+ Section PriorityAware.
+
+ (** Given any JLDP priority policy... *)
+ Context `{JLDP_policy Job}.
+
+ (** ...always choose the highest-priority job when making a scheduling decision... *)
+ Definition choose_highest_prio_job t jobs := supremum (hep_job_at t) jobs.
+
+ (** ... to obtain a priority- and preemption-model-aware ideal uniprocessor
+ schedule. *)
+ Definition uni_schedule : schedule PState := np_uni_schedule choose_highest_prio_job.
+ End PriorityAware.
+
+End UniprocessorScheduler.
+
diff --git a/implementation/definitions/scheduler.v b/implementation/definitions/scheduler.v
deleted file mode 100644
index 10b33292dbca53a060c0d5483fbb1fd7333ab0b0..0000000000000000000000000000000000000000
--- a/implementation/definitions/scheduler.v
+++ /dev/null
@@ -1,61 +0,0 @@
-Require Export prosa.behavior.all.
-Require Export prosa.model.priority.classes.
-Require Export prosa.util.supremum.
-Require Export prosa.model.preemption.parameter.
-Require Export prosa.model.schedule.work_conserving.
-Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.model.processor.ideal.
-
-Section UniprocessorSchedule.
-
- Context {Job : JobType}.
- Context `{JobCost Job}.
- Context `{JobArrival Job}.
- Context `{JobPreemptable Job}.
- Context `{JLDP_policy Job}.
- Context {Task : eqType}.
- Context `{JobReady Job (ideal.processor_state Job)}.
-
- Variable arr_seq : arrival_sequence Job.
-
- Section JobAllocation.
-
- Variable sched_prefix : schedule (ideal.processor_state Job).
-
- Definition prev_job_nonpreemptive (t : instant) : bool:=
- match t with
- | 0 => false
- | S t' => if sched_prefix t' is Some j then
- ~~job_preemptable j (service sched_prefix j t)
- else
- false
- end.
-
- (** Given an arrival sequence, a prefix schedule [[0, t-1]], computes
- which job has to be scheduled at [t] **)
- Definition allocation_at (t : instant): option Job :=
- if prev_job_nonpreemptive t then
- sched_prefix t.-1
- else
- supremum (hep_job_at t) (jobs_backlogged_at arr_seq sched_prefix t).
-
- End JobAllocation.
-
- Definition empty_schedule: schedule (ideal.processor_state Job) := fun _ => None.
-
- (** Given an arrival sequence, computes a schedule up to time [h] **)
- Fixpoint schedule_up_to (h : instant) : schedule (ideal.processor_state Job) :=
- let
- prefix := if h is S h' then schedule_up_to h' else empty_schedule
- in
- fun t =>
- if t == h then
- allocation_at prefix t
- else
- prefix t.
-
- Definition uni_schedule (t : instant) : ideal.processor_state Job :=
- schedule_up_to t t.
-
-End UniprocessorSchedule.
-
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
new file mode 100644
index 0000000000000000000000000000000000000000..14207570894b28d4f244d72a7b337d79bac95e5c
--- /dev/null
+++ b/implementation/facts/generic_schedule.v
@@ -0,0 +1,87 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+Require Export prosa.implementation.definitions.generic_scheduler.
+Require Export prosa.analysis.facts.transform.replace_at.
+
+(** * Properties of the Generic Reference Scheduler *)
+
+(** This file establishes some facts about the generic reference scheduler that
+ constructs a schedule via pointwise scheduling decisions based on a given
+ policy and the preceding prefix. *)
+
+Section GenericScheduleProperties.
+ (** For any type of jobs and type of schedule, ... *)
+ Context {Job : JobType} {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** ... any scheduling policy, and ... *)
+ Variable policy : PointwisePolicy PState.
+
+ (** ... any notion of idleness. *)
+ Variable idle_state : PState.
+
+ (** For notational convenience, we define [prefix t] to denote the finite
+ prefix considered when scheduling a job at time [t]. *)
+ Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
+
+ (** To begin with, we establish two simple rewriting lemmas for unrolling
+ [schedule_up_to]. First, we observe that the allocation is indeed
+ determined by the policy based on the preceding prefix. *)
+ Lemma schedule_up_to_def:
+ forall t,
+ schedule_up_to policy idle_state t t = policy (prefix t) t.
+ Proof. by elim=> [|n IH]; rewrite [LHS]/schedule_up_to -/(schedule_up_to _) /replace_at; apply ifT. Qed.
+
+ (** Second, we note how to replace [schedule_up_to] in the general case with
+ its definition. *)
+ Lemma schedule_up_to_unfold:
+ forall h t,
+ schedule_up_to policy idle_state h t = replace_at (prefix h) h (policy (prefix h) h) t.
+ Proof. by move=> h t; rewrite [LHS]/schedule_up_to /prefix; elim: h. Qed.
+
+ (** Next, we observe that we can increase a prefix's horizon by one
+ time unit without changing any allocations in the prefix. *)
+ Lemma schedule_up_to_widen:
+ forall h t,
+ t <= h ->
+ schedule_up_to policy idle_state h t = schedule_up_to policy idle_state h.+1 t.
+ Proof.
+ move=> h t RANGE.
+ rewrite [RHS]schedule_up_to_unfold rest_of_schedule_invariant // => EQ.
+ now move: RANGE; rewrite EQ ltnn.
+ Qed.
+
+ (** After the horizon of a prefix, the schedule is still "empty", meaning
+ that all instants are idle. *)
+ Lemma schedule_up_to_empty:
+ forall h t,
+ h < t ->
+ schedule_up_to policy idle_state h t = idle_state.
+ Proof.
+ move=> h t.
+ elim: h => [LT|h IH LT].
+ { rewrite /schedule_up_to rest_of_schedule_invariant // => ZERO.
+ now subst. }
+ { rewrite /schedule_up_to rest_of_schedule_invariant -/(schedule_up_to _ h t);
+ first by apply IH => //; apply ltn_trans with (n := h.+1).
+ move=> EQ. move: LT.
+ now rewrite EQ ltnn. }
+ Qed.
+
+ (** A crucial fact is that a prefix up to horizon [h1] is identical to a
+ prefix up to a later horizon [h2] at times up to [h1]. *)
+ Lemma schedule_up_to_prefix_inclusion:
+ forall h1 h2,
+ h1 <= h2 ->
+ forall t,
+ t <= h1 ->
+ schedule_up_to policy idle_state h1 t = schedule_up_to policy idle_state h2 t.
+ Proof.
+ move=> h1 h2 LEQ t BEFORE.
+ elim: h2 LEQ BEFORE; first by rewrite leqn0 => /eqP ->.
+ move=> t' IH.
+ rewrite leq_eqVlt ltnS => /orP [/eqP <-|LEQ] // t_H1.
+ rewrite IH // schedule_up_to_widen //.
+ now apply (leq_trans t_H1).
+ Qed.
+
+End GenericScheduleProperties.
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
new file mode 100644
index 0000000000000000000000000000000000000000..4a7160f9bf052ed5fc4be4f5ca64dbc4095aa6fe
--- /dev/null
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -0,0 +1,215 @@
+Require Export prosa.implementation.facts.generic_schedule.
+Require Export prosa.implementation.definitions.ideal_uni_scheduler.
+Require Export prosa.analysis.facts.model.ideal_schedule.
+
+(** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
+
+(** This file establishes facts about the reference model of a
+ preemption-model-aware ideal uniprocessor scheduler. *)
+
+(** The following results assume ideal uniprocessor schedules. *)
+Require Import prosa.model.processor.ideal.
+
+Section NPUniprocessorScheduler.
+
+ (** Consider any type of jobs with costs and arrival times, ... *)
+ Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
+
+ (** ... in the context of an ideal uniprocessor model. *)
+ Let PState := ideal.processor_state Job.
+ Let idle_state : PState := None.
+
+ (** Suppose we are given a consistent arrival sequence of such jobs, ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
+
+ (** ... a non-clairvoyant readiness model, ... *)
+ Context {RM: JobReady Job (ideal.processor_state Job)}.
+ Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
+
+ (** ... and a preemption model. *)
+ Context `{JobPreemptable Job}.
+
+ (** For any given job selection policy ... *)
+ Variable choose_job : instant -> seq Job -> option Job.
+
+ (** ... consider the schedule produced by the preemption-aware scheduler for
+ the policy induced by [choose_job]. *)
+ Let schedule := np_uni_schedule arr_seq choose_job.
+ Let policy := allocation_at arr_seq choose_job.
+
+ (** To begin with, we establish that the preemption-aware scheduler does not
+ induce non-work-conserving behavior. *)
+ Section WorkConservation.
+
+ (** If [choose_job] does not voluntarily idle the processor, ... *)
+ Hypothesis H_non_idling:
+ forall t s,
+ choose_job t s = idle_state <-> s = [::].
+
+ (** ... then we can establish work-conservation. *)
+
+ (** First, we observe that [allocation_at] yields [idle_state] only if there are
+ no backlogged jobs. *)
+ Lemma allocation_at_idle:
+ forall sched t,
+ allocation_at arr_seq choose_job sched t = idle_state ->
+ jobs_backlogged_at arr_seq sched t = [::].
+ Proof.
+ move=> sched t.
+ elim: t => [|t _]; first by apply H_non_idling.
+ rewrite /allocation_at /prev_job_nonpreemptive.
+ elim: (sched t) => [j'|]; last by apply H_non_idling.
+ rewrite if_neg.
+ elim: (job_preemptable j' (service sched j' t.+1)); first by apply H_non_idling.
+ now discriminate.
+ Qed.
+
+ (** As a stepping stone, we observe that the generated schedule is idle at
+ a time [t] only if there are no backlogged jobs. *)
+ Lemma idle_schedule_no_backlogged_jobs:
+ forall t,
+ is_idle schedule t ->
+ jobs_backlogged_at arr_seq schedule t = [::].
+ Proof.
+ move=> t.
+ rewrite /is_idle /schedule /np_uni_schedule /generic_schedule => /eqP.
+ move=> NONE. move: (NONE).
+ rewrite schedule_up_to_def => IDLE.
+ apply allocation_at_idle in IDLE.
+ rewrite -IDLE.
+ apply backlogged_jobs_prefix_invariance with (h := t.+1) => //.
+ rewrite /identical_prefix => x.
+ rewrite ltnS leq_eqVlt => /orP [/eqP ->|LT]; last first.
+ { elim: t LT IDLE NONE => // => h IH LT_x IDLE NONE.
+ now apply schedule_up_to_prefix_inclusion. }
+ { elim: t IDLE NONE => [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.
+ rewrite /schedule_up_to replace_at_def.
+ rewrite /allocation_at /prev_job_nonpreemptive IDLE H_non_idling //. }
+ Qed.
+
+ (** From the preceding fact, we conclude that the generated schedule is
+ indeed work-conserving. *)
+ Theorem np_schedule_work_conserving:
+ work_conserving arr_seq schedule.
+ Proof.
+ move=> j t ARRIVES BACKLOGGED.
+ move: (@ideal_proc_model_sched_case_analysis Job schedule t) => [IDLE|SCHED]; last by exact.
+ exfalso.
+ have NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t by apply mem_backlogged_jobs => //.
+ clear BACKLOGGED.
+ move: (idle_schedule_no_backlogged_jobs t IDLE) => EMPTY.
+ now rewrite EMPTY in NON_EMPTY.
+ Qed.
+
+ End WorkConservation.
+
+ (** The next result establishes that the generated preemption-model-aware
+ schedule is structurally valid, meaning all jobs stem from the arrival
+ sequence and only ready jobs are scheduled. *)
+ Section Validity.
+
+ (** Any reasonable job selection policy will not create jobs "out of thin
+ air," i.e., if a job is selected, it was among those given to choose
+ from. *)
+ Hypothesis H_chooses_from_set:
+ forall t s j, choose_job t s = Some j -> j \in s.
+
+ (** For the schedule to be valid, we require the notion of readiness to be
+ consistent with the preemption model: a non-preemptive job remains
+ ready until (at least) the end of its current non-preemptive
+ section. *)
+ Hypothesis H_valid_preemption_behavior:
+ valid_nonpreemptive_readiness RM.
+
+ (** Under this natural assumption, the generated schedule is valid. *)
+ Theorem np_schedule_valid:
+ valid_schedule schedule arr_seq.
+ Proof.
+ rewrite /valid_schedule; split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+ { elim: t => [/eqP | t' IH /eqP].
+ - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
+ move: (H_chooses_from_set _ _ _ IN).
+ now apply backlogged_job_arrives_in.
+ - rewrite schedule_up_to_def /allocation_at.
+ case: (prev_job_nonpreemptive (schedule_up_to _ _ t') t'.+1) => [|IN];
+ first by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
+ move: (H_chooses_from_set _ _ _ IN).
+ now apply backlogged_job_arrives_in. }
+ { elim: t => [/eqP |t' IH /eqP].
+ - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
+ move: (H_chooses_from_set _ _ _ IN).
+ rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
+ now rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
+ - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
+ have JOB: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t') t'.+1)
+ = Some j
+ -> job_ready schedule j t'.+1.
+ { move=> IN.
+ move: (H_chooses_from_set _ _ _ IN).
+ rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
+ rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
+ rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
+ now rewrite (schedule_up_to_prefix_inclusion _ _ t'' t') //. }
+ case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
+ destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
+ apply H_valid_preemption_behavior.
+ injection EQ => <-.
+ move: NP.
+ have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
+ = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
+ rewrite /service.
+ apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
+ now rewrite (schedule_up_to_prefix_inclusion _ _ t t'). }
+ Qed.
+
+ End Validity.
+
+ (** Next, we observe that the resulting schedule is consistent with the
+ definition of "preemption times". *)
+ Section PreemptionTimes.
+
+ (** For notational convenience, recall the definition of a prefix of the
+ schedule based on which the next decision is made. *)
+ Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
+
+ (** First, we observe that non-preemptive jobs remain scheduled as long as
+ they are non-preemptive. *)
+ Lemma np_job_remains_scheduled:
+ forall t,
+ prev_job_nonpreemptive (prefix t) t ->
+ schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1.
+ Proof.
+ elim => [|t _] // NP.
+ rewrite schedule_up_to_def /allocation_at /policy /allocation_at.
+ rewrite ifT // -pred_Sn.
+ now rewrite schedule_up_to_widen.
+ Qed.
+
+ (** From this, we conclude that the predicate used to determine whether the
+ previously scheduled job is nonpreemptive in the computation of
+ [np_uni_schedule] is consistent with the existing notion of a
+ [preemption_time]. *)
+ Lemma np_consistent:
+ forall t,
+ prev_job_nonpreemptive (prefix t) t ->
+ ~~ preemption_time schedule t.
+ Proof.
+ elim => [|t _]; first by rewrite /prev_job_nonpreemptive.
+ rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time schedule_up_to_def /prefix /allocation_at => NP.
+ rewrite ifT //.
+ rewrite -pred_Sn.
+ move: NP. rewrite /prev_job_nonpreemptive.
+ elim: (schedule_up_to policy idle_state t t) => // j.
+ have <-: service (schedule_up_to policy idle_state t) j t.+1
+ = service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 => //.
+ rewrite /service.
+ apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
+ now rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
+ Qed.
+
+ End PreemptionTimes.
+
+End NPUniprocessorScheduler.
+
+
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
new file mode 100644
index 0000000000000000000000000000000000000000..b1df2e0ee708238b5495b490b2a813a71bedbe74
--- /dev/null
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -0,0 +1,122 @@
+Require Export prosa.implementation.facts.ideal_uni.preemption_aware.
+
+(** * Ideal Uniprocessor Scheduler Properties *)
+
+(** This file establishes facts about the reference model of a priority- and
+ preemption-model-aware ideal uniprocessor scheduler. *)
+
+(** The following results assume ideal uniprocessor schedules. *)
+Require Import prosa.model.processor.ideal.
+
+Section PrioAwareUniprocessorScheduler.
+
+ (** Consider any type of jobs with costs and arrival times, ... *)
+ Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
+
+ (** ... in the context of an ideal uniprocessor model. *)
+ Let PState := ideal.processor_state Job.
+ Let idle_state : PState := None.
+
+ (** Suppose we are given a consistent arrival sequence of such jobs, ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
+
+ (** ... a non-clairvoyant readiness model, ... *)
+ Context {RM: JobReady Job (ideal.processor_state Job)}.
+ Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
+
+ (** ... a preemption model that is consistent with the readiness model, ... *)
+ Context `{JobPreemptable Job}.
+ Hypothesis H_valid_preemption_behavior:
+ valid_nonpreemptive_readiness RM.
+
+ (** ... and reflexive, total, and transitive JLDP priority policy. *)
+ Context `{JLDP_policy Job}.
+ Hypothesis H_reflexive_priorities: reflexive_priorities.
+ Hypothesis H_total: total_priorities.
+ Hypothesis H_transitive: transitive_priorities.
+
+ (** Consider the schedule generated by the preemption-policy- and
+ priority-aware ideal uniprocessor scheduler. *)
+ Let schedule := uni_schedule arr_seq.
+
+ (** First, we note that the priority-aware job selection policy obviously
+ maintains work-conservation. *)
+ Corollary uni_schedule_work_conserving:
+ work_conserving arr_seq schedule.
+ Proof.
+ apply np_schedule_work_conserving => //.
+ move=> t jobs.
+ rewrite /choose_highest_prio_job; split.
+ - by apply supremum_none.
+ - by move=> ->.
+ Qed.
+
+ (** Second, we similarly note that schedule validity is also maintained. *)
+ Corollary uni_schedule_valid:
+ valid_schedule schedule arr_seq.
+ Proof.
+ apply np_schedule_valid => //.
+ move=> t jobs j.
+ now apply supremum_in.
+ Qed.
+
+ (** Now we proceed to the main property of the priority-aware scheduler: in
+ the following section we establish that [uni_schedule arr_seq] is
+ compliant with the given priority policy whenever jobs are
+ preemptable. *)
+ Section Priority.
+
+ (** For notational convenience, recall the definitions of the job-selection
+ policy and a prefix of the schedule based on which the next decision is
+ made. *)
+ Let policy := allocation_at arr_seq choose_highest_prio_job.
+ Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
+
+ (** To start, we observe that, at preemption times, the scheduled job is a
+ supremum w.r.t. to the priority order and the set of backlogged
+ jobs. *)
+ Lemma scheduled_job_is_supremum:
+ forall j t,
+ scheduled_at schedule j t ->
+ preemption_time schedule t ->
+ supremum (hep_job_at t) (jobs_backlogged_at arr_seq (prefix t) t) = Some j.
+ Proof.
+ move=> j t SCHED PREEMPT.
+ have NOT_NP: ~~ prev_job_nonpreemptive (prefix t) t.
+ { apply contraL with (b := preemption_time (uni_schedule arr_seq) t) => //.
+ now apply np_consistent. }
+ move: SCHED.
+ rewrite scheduled_at_def => /eqP.
+ rewrite {1}/schedule/uni_schedule/np_uni_schedule/generic_schedule schedule_up_to_def /allocation_at -/(prefix t).
+ rewrite ifF //.
+ now apply negbTE.
+ Qed.
+
+ (** From the preceding facts, we conclude that [uni_schedule arr_seq]
+ respects the priority policy at preemption times. *)
+ Theorem schedule_respects_policy :
+ respects_policy_at_preemption_point arr_seq schedule.
+ Proof.
+ move=> j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
+ case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].
+ { have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).
+ now apply H_reflexive_priorities. }
+ { move: BACK_j1.
+ have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
+ { apply backlogged_prefix_invariance' with (h := t) => //.
+ rewrite /identical_prefix /uni_schedule /prefix => t' LT.
+ induction t => //.
+ rewrite /np_uni_schedule /generic_schedule (schedule_up_to_prefix_inclusion _ _ t' t) //.
+ rewrite /prefix scheduled_at_def.
+ induction t => //.
+ now rewrite schedule_up_to_empty. }
+ move=> BACK_j1.
+ move: (scheduled_job_is_supremum j2 t SCHED_j2 PREEMPT) => SUPREMUM.
+ apply supremum_spec with (s := jobs_backlogged_at arr_seq (prefix t) t) => //.
+ now apply mem_backlogged_jobs. }
+ Qed.
+
+ End Priority.
+
+End PrioAwareUniprocessorScheduler.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index bdf248d267e16ddd49ccc37dd8dc591792dceebc..e74cc4d344fae1f9acf5484e299935b8ed552896 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -50,3 +50,4 @@ TODO
mathcomp
hyperperiod
pointwise
+notational