Built with
Alectryon , running Coq+SerAPI v8.14.0+0.14.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.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Require Export prosa.implementation.definitions.ideal_uni_scheduler.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.analysis.facts.model.ideal_schedule.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Require Export prosa.model.schedule.limited_preemptive.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
(** * 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.Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ | _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ : _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ | _ ]" was already used
in scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ & _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ | _ ]" was already used in
scope fun_scope. [notation-overridden,parsing]Notation "[ rel _ _ in _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Section NPUniprocessorScheduler .
(** Consider any type of jobs with costs and arrival times, ... *)
Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
(** ... in the context of an ideal uniprocessor model. *)
Let PState := ideal.processor_state Job.
Let idle_state : PState := None.
(** Suppose we are given a consistent arrival sequence of such jobs, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
(** ... a non-clairvoyant readiness model, ... *)
Context {RM : JobReady Job (ideal.processor_state Job)}.
Hypothesis H_nonclairvoyant_job_readiness : nonclairvoyant_readiness RM.
(** ... and a preemption model. *)
Context `{JobPreemptable Job}.
(** For any given job selection policy ... *)
Variable choose_job : instant -> seq Job -> option Job.
(** ... consider the schedule produced by the preemption-aware scheduler for
the policy induced by [choose_job]. *)
Let schedule := np_uni_schedule arr_seq choose_job.
Let policy := allocation_at arr_seq choose_job.
(** To begin with, we establish that the preemption-aware scheduler does not
induce non-work-conserving behavior. *)
Section WorkConservation .
(** If [choose_job] does not voluntarily idle the processor, ... *)
Hypothesis H_non_idling :
forall t s ,
choose_job t s = idle_state <-> s = [::].
(** ... then we can establish work-conservation. *)
(** First, we observe that [allocation_at] yields [idle_state] only if there are
no backlogged jobs. *)
Lemma allocation_at_idle :
forall sched t ,
allocation_at arr_seq choose_job sched t = idle_state ->
jobs_backlogged_at arr_seq sched t = [::].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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_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 = [::]
rewrite if_neg.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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_preemptable j' (service sched j' t.+1 )
then
choose_job t.+1
(jobs_backlogged_at arr_seq sched t.+1 )
else Some j') = idle_state ->
jobs_backlogged_at arr_seq sched t.+1 = [::]
elim : (job_preemptable j' (service sched j' t.+1 )); first by apply H_non_idling.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
Some j' = idle_state ->
jobs_backlogged_at arr_seq sched t.+1 = [::]
by discriminate .
Qed .
(** As a stepping stone, we observe that the generated schedule is idle at
a time [t] only if there are no backlogged jobs. *)
Lemma idle_schedule_no_backlogged_jobs :
forall t ,
is_idle schedule t ->
jobs_backlogged_at arr_seq schedule t = [::].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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,
is_idle schedule t ->
jobs_backlogged_at arr_seq schedule t = [::]
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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,
is_idle schedule t ->
jobs_backlogged_at arr_seq schedule t = [::]
move => t.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
is_idle schedule t ->
jobs_backlogged_at arr_seq schedule t = [::]
rewrite /is_idle /schedule /np_uni_schedule /generic_schedule => /eqP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 : is_idle schedule t
exists j_other : Job, scheduled_at schedule j_other t
exfalso .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 : is_idle schedule t
False
have NON_EMPTY: j \in jobs_backlogged_at arr_seq schedule t by apply mem_backlogged_jobs => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 : is_idle schedule t NON_EMPTY : j
\in jobs_backlogged_at arr_seq schedule
t
False
clear BACKLOGGED.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 IDLE : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 IDLE : 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 .
(** Any reasonable job selection policy will not create jobs "out of thin
air," i.e., if a job is selected, it was among those given to choose
from. *)
Hypothesis H_chooses_from_set :
forall t s j , choose_job t s = Some j -> j \in s.
(** For the schedule to be valid, we require the notion of readiness to be
consistent with the preemption model: a non-preemptive job remains
ready until (at least) the end of its current non-preemptive
section. *)
Hypothesis H_valid_preemption_behavior :
valid_nonpreemptive_readiness RM.
(** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
Lemma choose_job_implies_job_ready :
forall t j ,
choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1 ) = Some j
-> job_ready schedule j t.+1 .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
forall (t : nat) (j : Job),
choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j -> job_ready schedule j t.+1
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
forall (t : nat) (j : Job),
choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j -> job_ready schedule j t.+1
move => t j IN.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 t : nat j : Job IN : choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j
job_ready schedule j t.+1
move : (H_chooses_from_set _ _ _ IN).Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 t : nat j : Job IN : choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j
j
\in jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ->
job_ready schedule j t.+1
rewrite mem_filter /backlogged => /andP [/andP [READY _] _].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 t : nat j : Job IN : choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j READY : job_ready (schedule_up_to policy idle_state t)
j t.+1
job_ready schedule j t.+1
rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t) schedule j t.+1 ) //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 t : nat j : Job IN : choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to policy idle_state t) t.+1 ) =
Some j READY : job_ready (schedule_up_to policy idle_state t)
j t.+1
identical_prefix (schedule_up_to policy idle_state t)
schedule t.+1
by apply schedule_up_to_identical_prefix.
Qed .
(** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
Theorem np_schedule_valid :
valid_schedule schedule arr_seq.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
valid_schedule schedule arr_seq
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
valid_schedule schedule arr_seq
split ; move => j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t : instant
schedule_up_to (allocation_at arr_seq choose_job) None
t t == Some j -> arrives_in arr_seq j
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job
schedule_up_to (allocation_at arr_seq choose_job) None
0 0 = Some j -> arrives_in arr_seq j
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j -> arrives_in arr_seq j
schedule_up_to (allocation_at arr_seq choose_job) None
t'.+1 t'.+1 = Some j -> arrives_in arr_seq j
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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];
first by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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. } Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t : instant
schedule_up_to (allocation_at arr_seq choose_job) None
t t == Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j t
{ Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t : instant
schedule_up_to (allocation_at arr_seq choose_job) None
t t == Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j t
elim : t => [/eqP |t' IH /eqP].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job
schedule_up_to (allocation_at arr_seq choose_job) None
0 0 = Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j 0
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job
schedule_up_to (allocation_at arr_seq choose_job) None
0 0 = Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j 0
rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job IN : choose_job 0
(jobs_backlogged_at arr_seq
(empty_schedule None) 0 ) =
Some j
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_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 0
move : (H_chooses_from_set _ _ _ IN).Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 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 ->
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_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 0
rewrite mem_filter /backlogged => /andP [/andP [READY _] _].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job IN : choose_job 0
(jobs_backlogged_at arr_seq
(empty_schedule None) 0 ) =
Some j READY : job_ready (empty_schedule None) j 0
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_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 0
by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0 ).Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t'
schedule_up_to (allocation_at arr_seq choose_job) None
t'.+1 t'.+1 = Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j t'.+1
- Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t'
schedule_up_to (allocation_at arr_seq choose_job) None
t'.+1 t'.+1 = Some j ->
job_ready
(fun t : instant =>
schedule_up_to (allocation_at arr_seq choose_job)
None t t) j t'.+1
rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t'
(if
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_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
(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 j0 =>
~~
job_preemptable j0
(service sched_prefix j0 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 )
| None => false
end
then
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_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'.+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
match t with
| 0 => false
| t'.+1 =>
match sched_prefix t' with
| Some j =>
~~
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'.+1 )) = Some j ->
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_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
case : (schedule_up_to _ _ t' t') => [j' | IN]; last by apply choose_job_implies_job_ready.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job
(if
~~
job_preemptable j'
(service
(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_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 )
then Some j'
else
choose_job t'.+1
(jobs_backlogged_at arr_seq
(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_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'.+1 )) = Some j ->
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_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
destruct (~~ job_preemptable j' _) eqn :NP => [EQ|IN]; last by apply choose_job_implies_job_ready.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job NP : ~~
job_preemptable j'
(service
(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_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 ) =
true EQ : Some j' = Some j
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_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
apply H_valid_preemption_behavior.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job NP : ~~
job_preemptable j'
(service
(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_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 ) =
true EQ : Some j' = 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 j =>
~~
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 )
injection EQ => <-.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job NP : ~~
job_preemptable j'
(service
(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_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 ) =
true EQ : Some j' = 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 j =>
~~
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 )
move : NP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job EQ : Some j' = Some j
~~
job_preemptable j'
(service
(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_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 ) = true ->
~~
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_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 (schedule_up_to policy idle_state t') j' t'.+1
= service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1 ) => //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job EQ : Some j' = Some j
service (schedule_up_to policy idle_state t') j' t'.+1 =
service
(fun t : instant =>
schedule_up_to policy idle_state t t) j' t'.+1
rewrite /service.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job EQ : Some j' = Some j
service_during (schedule_up_to policy idle_state t')
j' 0 t'.+1 =
service_during
(fun t : instant =>
schedule_up_to policy idle_state t t) j' 0 t'.+1
apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 j : Job t' : nat IH : schedule_up_to
(allocation_at arr_seq choose_job) None t' t' ==
Some j ->
job_ready
(fun t : instant =>
schedule_up_to
(allocation_at arr_seq choose_job) None t t)
j t' j' : Job EQ : Some j' = Some j t : nat BOUND : t < t'.+1
schedule_up_to policy idle_state t' t =
schedule_up_to policy idle_state t t
by rewrite (schedule_up_to_prefix_inclusion _ _ t t'). }
Qed .
End Validity .
(** Next, we observe that the resulting schedule is consistent with the
definition of "preemption times". *)
Section PreemptionTimes .
(** For notational convenience, recall the definition of a prefix of the
schedule based on which the next decision is made. *)
Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
(** First, we observe that non-preemptive jobs remain scheduled as long as
they are non-preemptive. *)
Lemma np_job_remains_scheduled :
forall t ,
prev_job_nonpreemptive (prefix t) t ->
schedule_up_to policy idle_state t t = schedule_up_to policy idle_state t t.-1 .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall t : nat,
prev_job_nonpreemptive (prefix t) t ->
schedule_up_to policy idle_state t t =
schedule_up_to policy idle_state t t.-1
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall t : nat,
prev_job_nonpreemptive (prefix t) t ->
schedule_up_to policy idle_state t t =
schedule_up_to policy idle_state t t.-1
elim => [|t _] // NP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat NP : prev_job_nonpreemptive (prefix t.+1 ) t.+1
schedule_up_to policy idle_state t.+1 t.+1 =
schedule_up_to policy idle_state t.+1 t.+1 .-1
rewrite schedule_up_to_def /allocation_at /policy /allocation_at.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat NP : prev_job_nonpreemptive (prefix t.+1 ) t.+1
(if
prev_job_nonpreemptive
(schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
idle_state t) t.+1
then
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
idle_state t t.+1 .-1
else
choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix
t)) idle_state t) t.+1 )) =
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
idle_state t.+1 t.+1 .-1
rewrite ifT // -pred_Sn.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat NP : prev_job_nonpreemptive (prefix t.+1 ) t.+1
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
idle_state t t =
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
idle_state t.+1 t
by rewrite schedule_up_to_widen.
Qed .
(** From this, we conclude that the predicate used to determine whether the
previously scheduled job is nonpreemptive in the computation of
[np_uni_schedule] is consistent with the existing notion of a
[preemption_time]. *)
Lemma np_consistent :
forall t ,
prev_job_nonpreemptive (prefix t) t ->
~~ preemption_time schedule t.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall t : nat,
prev_job_nonpreemptive (prefix t) t ->
~~ preemption_time schedule t
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState
forall t : nat,
prev_job_nonpreemptive (prefix t) t ->
~~ preemption_time schedule t
elim => [|t _]; first by rewrite /prev_job_nonpreemptive.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat
prev_job_nonpreemptive (prefix t.+1 ) t.+1 ->
~~ preemption_time schedule t.+1
rewrite /schedule /np_uni_schedule /generic_schedule /preemption_time
schedule_up_to_def /prefix /allocation_at => NP.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat NP : prev_job_nonpreemptive
(schedule_up_to policy idle_state t) t.+1
~~
match
(if
prev_job_nonpreemptive
(schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix
t)) None t) t.+1
then
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
None t t.+1 .-1
else
choose_job t.+1
(jobs_backlogged_at arr_seq
(schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq
sched_prefix t)) None t) t.+1 ))
with
| Some j =>
job_preemptable j
(service
(fun t : instant =>
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t0 : instant) =>
if prev_job_nonpreemptive sched_prefix t0
then sched_prefix t0.-1
else
choose_job t0
(jobs_backlogged_at arr_seq
sched_prefix t0)) None t t) j t.+1 )
| None => true
end
rewrite ifT // -pred_Sn.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat NP : prev_job_nonpreemptive
(schedule_up_to policy idle_state t) t.+1
~~
match
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t : instant) =>
if prev_job_nonpreemptive sched_prefix t
then sched_prefix t.-1
else
choose_job t
(jobs_backlogged_at arr_seq sched_prefix t))
None t t
with
| Some j =>
job_preemptable j
(service
(fun t : instant =>
schedule_up_to
(fun
(sched_prefix : schedule.schedule
(processor_state Job))
(t0 : instant) =>
if prev_job_nonpreemptive sched_prefix t0
then sched_prefix t0.-1
else
choose_job t0
(jobs_backlogged_at arr_seq
sched_prefix t0)) None t t) j t.+1 )
| None => true
end
move : NP; rewrite /prev_job_nonpreemptive.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat
match schedule_up_to policy idle_state t t with
| Some j =>
~~
job_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_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_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat j : Job
~~
job_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_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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat j : Job
service
(fun t0 : instant =>
schedule_up_to policy idle_state t0 t0) j t.+1 =
service (schedule_up_to policy idle_state t) j t.+1
rewrite /service.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat j : Job
service_during
(fun t0 : instant =>
schedule_up_to policy idle_state t0 t0) j 0 t.+1 =
service_during (schedule_up_to policy idle_state t) j
0 t.+1
apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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 prefix := fun t : nat =>
match t with
| 0 => empty_schedule idle_state
| t'.+1 => schedule_up_to policy idle_state t'
end : nat -> schedule.schedule PState t : nat j : Job t' : nat BOUND : t' < t.+1
schedule_up_to policy idle_state t' t' =
schedule_up_to policy idle_state t t'
by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
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.
(** 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_uni_schedule arr_seq choose_job : schedule.schedule (processor_state Job) policy := allocation_at arr_seq choose_job : schedule.schedule (processor_state Job) ->
instant -> option Job H_valid_preemption_function : forall j : Job,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution
j
schedule_respects_preemption_model arr_seq schedule
Proof .Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_uni_schedule arr_seq choose_job : schedule.schedule (processor_state Job) policy := allocation_at arr_seq choose_job : schedule.schedule (processor_state Job) ->
instant -> option Job H_valid_preemption_function : forall j : Job,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution
j
schedule_respects_preemption_model arr_seq schedule
move => j.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : Job
forall t : instant,
arrives_in arr_seq j ->
~~ job_preemptable j (service schedule j t) ->
scheduled_at schedule j t
elim => [| t' IH]; first by rewrite service0 => ARR /negP NP; move : (H_valid_preemption_function j ARR).Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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/np_uni_schedule/generic_schedule => /eqP SCHED.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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 (identical_prefix_service _ schedule) //.Job : JobType JC : JobCost Job JA : JobArrival Job PState := processor_state Job : Type idle_state := None : PState arr_seq : arrival_sequence Job H_consistent_arrival_times : consistent_arrival_times
arr_seq RM : JobReady Job (processor_state Job) H_nonclairvoyant_job_readiness : nonclairvoyant_readiness
RM H : JobPreemptable Job choose_job : instant -> seq Job -> option Job schedule := np_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
jj : 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
by apply schedule_up_to_identical_prefix.
Qed .
End PreemptionCompliance .
End NPUniprocessorScheduler .