Built with
Alectryon , running Coq+SerAPI v8.20.0+0.20.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 .
Require Export prosa.implementation.facts.generic_schedule.[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 ] Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted. [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_core_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. *)
Lemma allocation_at_idle :
forall sched t ,
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 = [::]
Proof .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 = [::]
move => 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 = [::]
elim : t => [|t _]; first by apply H_non_idling.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 = [::]
rewrite /allocation_at /prev_job_nonpreemptive.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 = [::]
elim : (sched t) => [j'|]; last by apply H_non_idling.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 = [::]
move => 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_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 = [::]
destruct (job_ready sched j' t.+1 && ~~ job_preemptable j' (service sched 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_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. *)
Lemma idle_schedule_no_backlogged_jobs :
forall t ,
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 = [::]
Proof .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 = [::]
move => 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 = [::]
rewrite /ideal_is_idle /schedule /pmc_uni_schedule /generic_schedule => /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_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 = [::]
move => NONE.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 = [::]
move : (NONE).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 = [::]
rewrite schedule_up_to_def => IDLE.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 = [::]
apply allocation_at_idle in IDLE.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 = [::]
rewrite -IDLE.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
apply backlogged_jobs_prefix_invariance with (h := 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 = [::]
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
rewrite /identical_prefix => 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
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
rewrite ltnS leq_eqVlt => /orP [/eqP ->|LT]; last first .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 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
elim : t LT IDLE NONE => // => h IH LT_x IDLE NONE.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
elim : t IDLE NONE => [IDLE _| t' _ _ ->]; last by rewrite schedule_up_to_empty.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
rewrite /schedule_up_to replace_at_def.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. *)
Theorem np_schedule_work_conserving :
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
Proof .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
move => j t ARRIVES BACKLOGGED.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
move : (@ideal_proc_model_sched_case_analysis Job schedule t) => [IDLE|SCHED]; last by exact .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
exfalso .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
have NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t by exact : mem_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 = [::]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
move : (idle_schedule_no_backlogged_jobs t IDLE) => EMPTY.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. *)
Lemma np_schedule_jobs_from_arrival_sequence :
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 sH_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
Proof .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 sH_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
move => j t; rewrite scheduled_at_def /schedule /pmc_uni_schedule /generic_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 sH_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
elim : t => [/eqP | t' IH /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 sH_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 sH_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
rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => 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 sH_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
move : (H_chooses_from_set _ _ _ 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 sH_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 sH_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
rewrite schedule_up_to_def /allocation_at.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 sH_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
case : (prev_job_nonpreemptive (schedule_up_to _ _ t') t'.+1 ) => [|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 sH_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 sH_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 sH_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
move : (H_chooses_from_set _ _ _ 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 sH_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. *)
Theorem chosen_job_is_ready :
forall j t ,
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 sH_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
Proof .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 sH_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
move => j t /eqP 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_chooses_from_set : forall (t : instant)
(s : seq Job)
(j : Job),
choose_job t s = Some j ->
j \in sH_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
apply H_chooses_from_set in 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_chooses_from_set : forall (t : instant)
(s : seq Job)
(j : Job),
choose_job t s = Some j ->
j \in sH_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
move : SCHED; rewrite mem_filter => /andP [/andP[READY _] 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 sH_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
rewrite (H_nonclairvoyant_readiness _ (sched_prefix 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 sH_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
move => t' LEQt'.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 sH_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'
rewrite /schedule /pmc_uni_schedule /generic_schedule
schedule_up_to_def /sched_prefix.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 sH_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'
destruct 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 sH_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'
rewrite -schedule_up_to_def.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 sH_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. *)
Theorem jobs_must_be_ready :
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 sH_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
Proof .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 sH_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
move => 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 sH_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
rewrite scheduled_at_def /schedule/pmc_uni_schedule/allocation_at
/generic_schedule schedule_up_to_def.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 sH_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
case PREV: prev_job_nonpreemptive;
last exact : chosen_job_is_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 sH_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
case : t PREV => // 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 sH_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
rewrite /prev_job_nonpreemptive; case : (schedule_up_to) => // {}j /andP [READY _] /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 sH_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
erewrite (H_nonclairvoyant_readiness _ _ _ t.+1 ) => // t' LT.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 sH_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. *)
Theorem np_schedule_valid :
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 sH_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
Proof .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 sH_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
split .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 sH_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 sH_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 sH_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. *)
Lemma np_job_remains_scheduled :
forall t ,
prev_job_nonpreemptive (prefix t) t ->
schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1 .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 sprefix := 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
Proof .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 sprefix := 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
elim => [|t _] // NP.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 sprefix := 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
rewrite schedule_up_to_def /allocation_at /policy /allocation_at.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 sprefix := 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
rewrite ifT // -pred_Sn.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 sprefix := 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]. *)
Lemma np_consistent :
forall t ,
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 sprefix := 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
Proof .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 sprefix := 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
move => 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 sprefix := 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
rewrite /preemption_time scheduled_job_at_def//;
last by exact /jobs_must_arrive_to_be_ready/jobs_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 sprefix := 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 sprefix := 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
elim : t => [|t _]; first by rewrite /prev_job_nonpreemptive.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 sprefix := 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
rewrite /schedule /pmc_uni_schedule /generic_schedule
schedule_up_to_def /prefix /allocation_at => NP.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 sprefix := 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
rewrite ifT // -pred_Sn.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 sprefix := 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
move : NP; rewrite /prev_job_nonpreemptive.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 sprefix := 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
elim : (schedule_up_to policy idle_state t t) => // 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 sprefix := 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 )
have ->: (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 sprefix := 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 sprefix := 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
rewrite /service.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 sprefix := 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
apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].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 sprefix := 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 sprefix := 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 sprefix := 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. *)
Lemma np_respects_preemption_model :
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
jH_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
schedule_respects_preemption_model arr_seq schedule
Proof .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
jH_valid_preemption_behavior : valid_nonpreemptive_readiness
RM schedule
schedule_respects_preemption_model arr_seq schedule
move => 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
jH_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
elim => [| t' IH];[by rewrite service0=>ARR /negP ?;move :(H_valid_preemption_function j ARR)|].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
jH_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
move => ARR NP.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
jH_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
have : 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
jH_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
jH_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'
apply contraT => 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
jH_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
move : (not_scheduled_implies_no_service _ _ _ NOT_SCHED) => NO_SERVICE.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
jH_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
rewrite -(service_last_plus_before) NO_SERVICE addn0 in NP; apply IH in NP => //.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
jH_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
jH_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
rewrite !scheduled_at_def /schedule/pmc_uni_schedule/generic_schedule => /eqP 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
jH_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
rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1 ) // np_job_remains_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_valid_preemption_function : forall j : Job,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution
jH_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
rewrite /prev_job_nonpreemptive 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
jH_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 )
rewrite (identical_prefix_service _ schedule); last by apply schedule_up_to_identical_prefix.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
jH_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 )
apply /andP; split => //.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
jH_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
rewrite (H_nonclairvoyant_job_readiness _ schedule _ 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
jH_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 .