add ideal uniprocessor reference scheduler

implementation/definitions/generic_scheduler.v

+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.
+

implementation/definitions/ideal_uni_scheduler.v

+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.
+

implementation/definitions/scheduler.v

-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.
-

implementation/facts/generic_schedule.v

+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.

implementation/facts/ideal_uni/preemption_aware.v

+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.
+
+

implementation/facts/ideal_uni/prio_aware.v

+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.

scripts/wordlist.pws

@@ -50,3 +50,4 @@ TODO
 mathcomp
 hyperperiod
 pointwise
+notational