Built with Alectryon, running Coq+SerAPI v8.19.0+0.19.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing,default]
Require Export prosa.implementation.definitions.ideal_uni_scheduler. Require Export prosa.analysis.facts.model.ideal.schedule. Require Export prosa.model.schedule.limited_preemptive. (** * 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. Require Export prosa.util.tactics. Section NPUniprocessorScheduler. (** Consider any type of jobs with costs and arrival times, ... *) Context {Job : JobType} `{JobCost Job} `{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 valid arrival sequence of such jobs, ... *) Variable arr_seq : arrival_sequence Job. Hypothesis H_valid_arrivals : valid_arrival_sequence 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 := pmc_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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

forall (sched : schedule.schedule (processor_state Job)) (t : instant), allocation_at arr_seq choose_job sched t = idle_state -> jobs_backlogged_at arr_seq sched t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

forall (sched : schedule.schedule (processor_state Job)) (t : instant), allocation_at arr_seq choose_job sched t = idle_state -> jobs_backlogged_at arr_seq sched t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: instant

allocation_at arr_seq choose_job sched t = idle_state -> jobs_backlogged_at arr_seq sched t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: nat

allocation_at arr_seq choose_job sched t.+1 = idle_state -> jobs_backlogged_at arr_seq sched t.+1 = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: nat

(if match sched t with | Some j => job_ready sched j t.+1 && ~~ job_preemptable j (service sched j t.+1) | None => false end then sched t.+1.-1 else choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)) = idle_state -> jobs_backlogged_at arr_seq sched t.+1 = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: nat
j': Job

(if job_ready sched j' t.+1 && ~~ job_preemptable j' (service sched j' t.+1) then Some j' else choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)) = idle_state -> jobs_backlogged_at arr_seq sched t.+1 = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: nat
j': Job
SCHED: (if job_ready sched j' t.+1 && ~~ job_preemptable j' (service sched j' t.+1) then Some j' else choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1)) = idle_state

jobs_backlogged_at arr_seq sched t.+1 = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
sched: schedule.schedule (processor_state Job)
t: nat
j': Job
SCHED: choose_job t.+1 (jobs_backlogged_at arr_seq sched t.+1) = idle_state

jobs_backlogged_at arr_seq sched t.+1 = [::]
by apply (H_non_idling t.+1). Qed. (** As a stepping stone, we observe that the generated schedule is idle at a time [t] only if there are no backlogged jobs. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

forall t : instant, ideal_is_idle schedule t -> jobs_backlogged_at arr_seq schedule t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

forall t : instant, ideal_is_idle schedule t -> jobs_backlogged_at arr_seq schedule t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant

ideal_is_idle schedule t -> jobs_backlogged_at arr_seq schedule t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant

schedule_up_to (allocation_at arr_seq choose_job) None t t = None -> jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None

jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None

schedule_up_to (allocation_at arr_seq choose_job) None t t = None -> jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: allocation_at arr_seq choose_job match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = None

jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]

jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = [::]
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]

jobs_backlogged_at arr_seq (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) t = jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]

identical_prefix (fun t : instant => schedule_up_to (allocation_at arr_seq choose_job) None t t) match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat

x < t.+1 -> schedule_up_to (allocation_at arr_seq choose_job) None x x = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end x
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat
LT: x < t

schedule_up_to (allocation_at arr_seq choose_job) None x x = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end x
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat
schedule_up_to (allocation_at arr_seq choose_job) None t t = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat
LT: x < t

schedule_up_to (allocation_at arr_seq choose_job) None x x = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end x
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
x, h: nat
IH: x < h -> jobs_backlogged_at arr_seq match h with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end h = [::] -> schedule_up_to (allocation_at arr_seq choose_job) None h h = None -> schedule_up_to (allocation_at arr_seq choose_job) None x x = match h with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end x
LT_x: x < h.+1
IDLE: jobs_backlogged_at arr_seq (schedule_up_to (allocation_at arr_seq choose_job) None h) h.+1 = [::]
NONE: schedule_up_to (allocation_at arr_seq choose_job) None h.+1 h.+1 = None

schedule_up_to (allocation_at arr_seq choose_job) None x x = schedule_up_to (allocation_at arr_seq choose_job) None h x
by apply schedule_up_to_prefix_inclusion.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat

schedule_up_to (allocation_at arr_seq choose_job) None t t = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
t: instant
NONE: schedule_up_to (allocation_at arr_seq choose_job) None t t = None
IDLE: jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t = [::]
x: nat

schedule_up_to (allocation_at arr_seq choose_job) None t t = match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
x: nat
IDLE: jobs_backlogged_at arr_seq (empty_schedule None) 0 = [::]

schedule_up_to (allocation_at arr_seq choose_job) None 0 0 = empty_schedule None 0
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
x: nat
IDLE: jobs_backlogged_at arr_seq (empty_schedule None) 0 = [::]

allocation_at arr_seq choose_job (empty_schedule None) 0 = empty_schedule None 0
by 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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

work_conserving arr_seq schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]

work_conserving arr_seq schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged schedule j t

exists j_other : Job, scheduled_at schedule j_other t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged schedule j t
IDLE: ideal_is_idle schedule t

exists j_other : Job, scheduled_at schedule j_other t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged schedule j t
IDLE: ideal_is_idle schedule t

False
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged schedule j t
IDLE: ideal_is_idle schedule t
NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t

False
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_non_idling: forall (t : instant) (s : seq Job), choose_job t s = idle_state <-> s = [::]
j: Job
t: instant
ARRIVES: arrives_in arr_seq j
BACKLOGGED: backlogged schedule j t
IDLE: ideal_is_idle schedule t
NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t
EMPTY: jobs_backlogged_at arr_seq schedule t = [::]

False
by 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. (** First, 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. (** Second, 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 schedule. (** Finally, we assume the readiness model to be non-clairvoyant. *) Hypothesis H_nonclairvoyant_readiness: nonclairvoyant_readiness RM. (** For notational convenience, recall the definition of a prefix of the schedule based on which the next decision is made. *) Let sched_prefix t := if t is t'.+1 then schedule_up_to policy None t' else empty_schedule idle_state. (** We begin by showing that any job in the schedule must come from the arrival sequence used to generate it. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_come_from_arrival_sequence schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_come_from_arrival_sequence schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant

schedule_up_to (allocation_at arr_seq choose_job) None t t == Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job

schedule_up_to (allocation_at arr_seq choose_job) None 0 0 = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j
schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job

schedule_up_to (allocation_at arr_seq choose_job) None 0 0 = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
IN: choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) = Some j

arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
IN: choose_job 0 (jobs_backlogged_at arr_seq (empty_schedule None) 0) = Some j

j \in jobs_backlogged_at arr_seq (empty_schedule None) 0 -> arrives_in arr_seq j
by apply backlogged_job_arrives_in.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j

schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j

(if prev_job_nonpreemptive (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1 then schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' t'.+1.-1 else choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1)) = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j

schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' t'.+1.-1 = Some j -> arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j
IN: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1) = Some j
arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j

schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' t'.+1.-1 = Some j -> arrives_in arr_seq j
by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j
IN: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1) = Some j

arrives_in arr_seq j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t': nat
IH: schedule_up_to (allocation_at arr_seq choose_job) None t' t' == Some j -> arrives_in arr_seq j
IN: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1) = Some j

j \in jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t') t'.+1 -> arrives_in arr_seq j
by apply backlogged_job_arrives_in. Qed. (** Next, we show that any job selected by the job selection policy must be ready. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

forall (j : Job) (t : instant), choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j -> job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

forall (j : Job) (t : instant), choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j -> job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
SCHED: choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) = Some j

job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
SCHED: j \in jobs_backlogged_at arr_seq (sched_prefix t) t

job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
READY: job_ready (sched_prefix t) j t
IN: j \in arrivals_up_to arr_seq t

job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
READY: job_ready (sched_prefix t) j t
IN: j \in arrivals_up_to arr_seq t

identical_prefix schedule (sched_prefix t) t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
READY: job_ready (sched_prefix t) j t
IN: j \in arrivals_up_to arr_seq t
t': nat
LEQt': t' < t

schedule t' = sched_prefix t t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
READY: job_ready (sched_prefix t) j t
IN: j \in arrivals_up_to arr_seq t
t': nat
LEQt': t' < t

allocation_at arr_seq choose_job match t' with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t' = match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: nat
READY: job_ready (sched_prefix t.+1) j t.+1
IN: j \in arrivals_up_to arr_seq t.+1
t': nat
LEQt': t' < t.+1

allocation_at arr_seq choose_job match t' with | 0 => empty_schedule None | t'.+1 => schedule_up_to (allocation_at arr_seq choose_job) None t' end t' = schedule_up_to policy None t t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: nat
READY: job_ready (sched_prefix t.+1) j t.+1
IN: j \in arrivals_up_to arr_seq t.+1
t': nat
LEQt': t' < t.+1

schedule_up_to (allocation_at arr_seq choose_job) None t' t' = schedule_up_to policy None t t'
exact: (schedule_up_to_prefix_inclusion policy). Qed. (** Starting from the previous result we show that, at any instant, only a ready job can be scheduled. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_must_be_ready_to_execute schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_must_be_ready_to_execute schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant

scheduled_at schedule j t -> job_ready schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant

(if prev_job_nonpreemptive match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' end t then match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' end t.-1 else choose_job t (jobs_backlogged_at arr_seq match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' end t)) == Some j -> job_ready (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if prev_job_nonpreemptive sched_prefix t0 then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: instant
PREV: prev_job_nonpreemptive match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' end t = true

match t with | 0 => empty_schedule None | t'.+1 => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' end t.-1 == Some j -> job_ready (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if prev_job_nonpreemptive sched_prefix t0 then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
j: Job
t: nat

prev_job_nonpreemptive (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t) t.+1 = true -> schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t t.+1.-1 == Some j -> job_ready (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if prev_job_nonpreemptive sched_prefix t0 then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
t: nat
j: Job
READY: job_ready (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if match t with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t && ~~ job_preemptable j (service sched_prefix j t) | None => false end end then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t) j t.+1

job_ready (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if match t0 with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t0 && ~~ job_preemptable j (service sched_prefix j t0) | None => false end end then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
t: nat
j: Job
READY: job_ready (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if match t with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t && ~~ job_preemptable j (service sched_prefix j t) | None => false end end then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t) j t.+1
t': nat
LT: t' < t.+1

schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if match t with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t && ~~ job_preemptable j (service sched_prefix j t) | None => false end end then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t' t' = schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if match t with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t && ~~ job_preemptable j (service sched_prefix j t) | None => false end end then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t t'
exact: schedule_up_to_prefix_inclusion. Qed. (** Finally, we show that the generated schedule is valid. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

valid_schedule schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

valid_schedule schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_come_from_arrival_sequence schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState
jobs_must_be_ready_to_execute schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_come_from_arrival_sequence schedule arr_seq
exact: np_schedule_jobs_from_arrival_sequence.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
H_nonclairvoyant_readiness: nonclairvoyant_readiness RM
sched_prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy None t' end: nat -> schedule.schedule PState

jobs_must_be_ready_to_execute schedule
exact: jobs_must_be_ready. Qed. End Validity. (** Next, we observe that the resulting schedule is consistent with the definition of "preemption times". *) Section PreemptionTimes. (** Again, we require that the job-selection policy is reasonable. *) Hypothesis H_chooses_from_set: forall t s j, choose_job t s = Some j -> j \in s. (** 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. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState

forall t : nat, prev_job_nonpreemptive (prefix t) t -> schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState

forall t : nat, prev_job_nonpreemptive (prefix t) t -> schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
NP: prev_job_nonpreemptive (prefix t.+1) t.+1

schedule_up_to policy idle_state t.+1 t.+1 = schedule_up_to policy idle_state t.+1 t.+1.-1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
NP: prev_job_nonpreemptive (prefix t.+1) t.+1

(if prev_job_nonpreemptive (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t) t.+1 then schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t t.+1.-1 else choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t) t.+1)) = schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t.+1 t.+1.-1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
NP: prev_job_nonpreemptive (prefix t.+1) t.+1

schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t t = schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) idle_state t.+1 t
by 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]. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState

forall t : nat, prev_job_nonpreemptive (prefix t) t -> ~~ preemption_time arr_seq schedule t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState

forall t : nat, prev_job_nonpreemptive (prefix t) t -> ~~ preemption_time arr_seq schedule t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

prev_job_nonpreemptive (prefix t) t -> ~~ preemption_time arr_seq schedule t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

prev_job_nonpreemptive (prefix t) t -> ~~ match schedule t with | Some j => job_preemptable j (service schedule j t) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
jobs_come_from_arrival_sequence schedule arr_seq
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

prev_job_nonpreemptive (prefix t) t -> ~~ match schedule t with | Some j => job_preemptable j (service schedule j t) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

prev_job_nonpreemptive (prefix t.+1) t.+1 -> ~~ match schedule t.+1 with | Some j => job_preemptable j (service schedule j t.+1) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
NP: prev_job_nonpreemptive (schedule_up_to policy idle_state t) t.+1

~~ match (if prev_job_nonpreemptive (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t) t.+1 then schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t t.+1.-1 else choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t) t.+1)) with | Some j => job_preemptable j (service (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if prev_job_nonpreemptive sched_prefix t0 then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
NP: prev_job_nonpreemptive (schedule_up_to policy idle_state t) t.+1

~~ match schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if prev_job_nonpreemptive sched_prefix t then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t t with | Some j => job_preemptable j (service (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if prev_job_nonpreemptive sched_prefix t0 then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

match schedule_up_to policy idle_state t t with | Some j => job_ready (schedule_up_to policy idle_state t) j t.+1 && ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1) | None => false end -> ~~ match schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t : instant) => if match t with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t && ~~ job_preemptable j (service sched_prefix j t) | None => false end end then sched_prefix t.-1 else choose_job t (jobs_backlogged_at arr_seq sched_prefix t)) None t t with | Some j => job_preemptable j (service (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if match t0 with | 0 => false | t'.+1 => match sched_prefix t' with | Some j0 => job_ready sched_prefix j0 t0 && ~~ job_preemptable j0 (service sched_prefix j0 t0) | None => false end end then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1) | None => true end
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job

job_ready (schedule_up_to policy idle_state t) j t.+1 && ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1) -> ~~ job_preemptable j (service (fun t : instant => schedule_up_to (fun (sched_prefix : schedule.schedule (processor_state Job)) (t0 : instant) => if match t0 with | 0 => false | t'.+1 => match sched_prefix t' with | Some j => job_ready sched_prefix j t0 && ~~ job_preemptable j (service sched_prefix j t0) | None => false end end then sched_prefix t0.-1 else choose_job t0 (jobs_backlogged_at arr_seq sched_prefix t0)) None t t) j t.+1)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job

service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 = service (schedule_up_to policy idle_state t) j t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job
job_ready (schedule_up_to policy idle_state t) j t.+1 && ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1) -> ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job

service (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j t.+1 = service (schedule_up_to policy idle_state t) j t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job

service_during (fun t0 : instant => schedule_up_to policy idle_state t0 t0) j 0 t.+1 = service_during (schedule_up_to policy idle_state t) j 0 t.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job
t': nat
BOUND: t' < t.+1

schedule_up_to policy idle_state t' t' = schedule_up_to policy idle_state t t'
rewrite (schedule_up_to_prefix_inclusion _ _ t' t) //.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat
j: Job

job_ready (schedule_up_to policy idle_state t) j t.+1 && ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1) -> ~~ job_preemptable j (service (schedule_up_to policy idle_state t) j t.+1)
by move=> /andP [? ?].
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_chooses_from_set: forall (t : instant) (s : seq Job) (j : Job), choose_job t s = Some j -> j \in s
prefix:= fun t : nat => match t with | 0 => empty_schedule idle_state | t'.+1 => schedule_up_to policy idle_state t' end: nat -> schedule.schedule PState
t: nat

jobs_come_from_arrival_sequence schedule arr_seq
exact: np_schedule_jobs_from_arrival_sequence. Qed. End PreemptionTimes. (** Finally, we establish the main feature: the generated schedule respects the preemption-model semantics. *) Section PreemptionCompliance. (** As a minimal validity requirement (which is a part of [valid_preemption_model]), we require that any job in [arr_seq] must start execution to become nonpreemptive. *) Hypothesis H_valid_preemption_function : forall j, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j. (** Second, 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 schedule. (** Given such a valid preemption model, we establish that the generated schedule indeed respects the preemption model semantics. *)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule

schedule_respects_preemption_model arr_seq schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule

schedule_respects_preemption_model arr_seq schedule
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job

forall t : instant, arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t) -> scheduled_at schedule j t
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'

arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t'.+1) -> scheduled_at schedule j t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)

scheduled_at schedule j t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)

scheduled_at schedule j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
scheduled_at schedule j t' -> scheduled_at schedule j t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)

scheduled_at schedule j t'
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
NOT_SCHED: ~~ scheduled_at schedule j t'

false
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
NOT_SCHED: ~~ scheduled_at schedule j t'
NO_SERVICE: service_at schedule j t' = 0

false
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NOT_SCHED: ~~ scheduled_at schedule j t'
NO_SERVICE: service_at schedule j t' = 0
NP: scheduled_at schedule j t'

false
by move /negP in NOT_SCHED.
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)

scheduled_at schedule j t' -> scheduled_at schedule j t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

schedule_up_to (allocation_at arr_seq choose_job) None t'.+1 t'.+1 == Some j
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

prev_job_nonpreemptive (schedule_up_to policy idle_state t') t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

job_ready (schedule_up_to policy idle_state t') j t'.+1 && ~~ job_preemptable j (service (schedule_up_to policy idle_state t') j t'.+1)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

job_ready (schedule_up_to policy idle_state t') j t'.+1 && ~~ job_preemptable j (service schedule j t'.+1)
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

job_ready (schedule_up_to policy idle_state t') j t'.+1
Job: JobType
H: JobCost Job
H0: JobArrival Job
PState:= processor_state Job: ProcessorState Job
idle_state:= None: PState
arr_seq: arrival_sequence Job
H_valid_arrivals: valid_arrival_sequence arr_seq
RM: JobReady Job (processor_state Job)
H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM
H1: JobPreemptable Job
choose_job: instant -> seq Job -> option Job
schedule:= pmc_uni_schedule arr_seq choose_job: schedule.schedule (processor_state Job)
policy:= allocation_at arr_seq choose_job: schedule.schedule (processor_state Job) -> instant -> option Job
H_valid_preemption_function: forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j
H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule
j: Job
t': nat
IH: arrives_in arr_seq j -> ~~ job_preemptable j (service schedule j t') -> scheduled_at schedule j t'
ARR: arrives_in arr_seq j
NP: ~~ job_preemptable j (service schedule j t'.+1)
SCHED: schedule_up_to (allocation_at arr_seq choose_job) None t' t' = Some j

identical_prefix (schedule_up_to policy idle_state t') schedule t'.+1
exact: schedule_up_to_identical_prefix. Qed. End PreemptionCompliance. End NPUniprocessorScheduler.