Built with
Alectryon , running Coq+SerAPI v8.19.0+0.19.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
Require Export prosa.model.schedule.scheduled.[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ] [Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ] [Loading ML file ring_plugin.cmxs (using legacy method) ... done ] [Loading ML file coq-elpi.elpi ... done ] [Loading ML file zify_plugin.cmxs (using legacy method) ... done ] [Loading ML file micromega_plugin.cmxs (using legacy method) ... done ] [Loading ML file btauto_plugin.cmxs (using legacy method) ... done ] Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.analysis.definitions.service.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.arrivals.
Require Export prosa.util.tactics.
(** * Correctness of the Scheduled Job(s) *)
(** In this file, we establish the correctness of the computable definition of
the (set of) scheduled job(s) and a useful case-analysis lemma. *)
Section ScheduledJobs .
(** Consider any type of jobs with arrival times. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
(** Next, consider _any_ kind of processor state model, ... *)
Context {PState : ProcessorState Job}.
(** ... any valid arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... and any schedule. *)
Variable sched : schedule PState.
(** Now we establish the validity conditions under which these definitions
yield the expected results: all jobs must come from the arrival sequence
and do not execute before their arrival.
NB: We do not use [valid_schedule] here to avoid introducing a dependency
on a readiness mode. *)
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
(** ** The Set of Jobs Scheduled at a Given Time *)
(** Under these assumptions, [scheduled_jobs_at] is correct: a job is included
in the sequence if and only if it scheduled. *)
Lemma scheduled_jobs_at_iff :
forall j t ,
j \in scheduled_jobs_at arr_seq sched t = scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall (j : Job) (t : instant),
(j \in scheduled_jobs_at arr_seq sched t) =
scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall (j : Job) (t : instant),
(j \in scheduled_jobs_at arr_seq sched t) =
scheduled_at sched j t
move => j t; rewrite mem_filter; apply : andb_idr => SCHED.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant SCHED : scheduled_at sched j t
j \in arrivals_up_to arr_seq t
exact : arrivals_before_scheduled_at.
Qed .
(** Conversely, if no jobs are in the sequence, then no job is scheduled. *)
Lemma scheduled_jobs_at_nil :
forall t ,
nilp (scheduled_jobs_at arr_seq sched t)
<-> (forall j , ~~ scheduled_at sched j t).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
nilp (scheduled_jobs_at arr_seq sched t) <->
(forall j : Job, ~~ scheduled_at sched j t)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
nilp (scheduled_jobs_at arr_seq sched t) <->
(forall j : Job, ~~ scheduled_at sched j t)
move => t; split => [/nilP NIL j|NS]
; first by apply : contraT => /negbNE
; rewrite -scheduled_jobs_at_iff NIL in_nil.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j t
nilp (scheduled_jobs_at arr_seq sched t)
apply /nilP.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j t
scheduled_jobs_at arr_seq sched t = [::]
case NN: (scheduled_jobs_at _) => [//|j js].Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j tj : Job js : seq Job NN : scheduled_jobs_at arr_seq sched t = j :: js
j :: js = [::]
exfalso .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j tj : Job js : seq Job NN : scheduled_jobs_at arr_seq sched t = j :: js
False
have : scheduled_at sched j t; last by move : (NS j) => /negP.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j tj : Job js : seq Job NN : scheduled_jobs_at arr_seq sched t = j :: js
scheduled_at sched j t
rewrite -scheduled_jobs_at_iff NN.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant NS : forall j : Job, ~~ scheduled_at sched j tj : Job js : seq Job NN : scheduled_jobs_at arr_seq sched t = j :: js
j \in j :: js
exact : mem_head.
Qed .
(** We restate the previous claim for convenience. *)
Corollary not_scheduled_when_idle :
forall j t ,
is_idle arr_seq sched t -> ~~ scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall (j : Job) (t : instant),
is_idle arr_seq sched t -> ~~ scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall (j : Job) (t : instant),
is_idle arr_seq sched t -> ~~ scheduled_at sched j t
move => j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant
is_idle arr_seq sched t -> ~~ scheduled_at sched j t
rewrite /is_idle => /eqP/nilP.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched j : Job t : instant
nilp (scheduled_jobs_at arr_seq sched t) ->
~~ scheduled_at sched j t
by rewrite scheduled_jobs_at_nil.
Qed .
(** ** The Job Scheduled on an Ideal Progress Processor *)
(** In this section, we prove a simple fact about the relation
between [scheduled_at] and [served_at]. *)
Section IdealProgress .
(** Assume a scheduled job always receives some positive service. *)
Hypothesis H_ideal_progress_model : ideal_progress_proc_model PState.
(** We prove that if a job [j] is scheduled at time [t], then [j]
is in the set of jobs that are served at time [t]. *)
Lemma scheduled_at_implies_in_served_at :
forall j t ,
scheduled_at sched j t ->
j \in served_jobs_at arr_seq sched t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState
forall (j : Job) (t : instant),
scheduled_at sched j t ->
j \in served_jobs_at arr_seq sched t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState
forall (j : Job) (t : instant),
scheduled_at sched j t ->
j \in served_jobs_at arr_seq sched t
move => j t SCHED.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState j : Job t : instant SCHED : scheduled_at sched j t
j \in served_jobs_at arr_seq sched t
rewrite mem_filter; apply /andP; split .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState j : Job t : instant SCHED : scheduled_at sched j t
receives_service_at sched j t
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState j : Job t : instant SCHED : scheduled_at sched j t
receives_service_at sched j t
by apply H_ideal_progress_model.
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_ideal_progress_model : ideal_progress_proc_model
PState j : Job t : instant SCHED : scheduled_at sched j t
j \in arrivals_up_to arr_seq t
by eapply arrivals_before_scheduled_at => //.
Qed .
End IdealProgress .
(** ** The Job Scheduled on a Uniprocessor *)
(** For convenience, we note similar rewriting rules for uniprocessors. *)
Section Uniprocessors .
(** Suppose we are looking at a uniprocessor. *)
Hypothesis H_uni : uniprocessor_model PState.
(** Then clearly there is at most one job scheduled at any time [t]. *)
Corollary scheduled_jobs_at_seq1 :
forall t ,
size (scheduled_jobs_at arr_seq sched t) <= 1 .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
size (scheduled_jobs_at arr_seq sched t) <= 1
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
size (scheduled_jobs_at arr_seq sched t) <= 1
move => t; set sja := scheduled_jobs_at _ _ _; rewrite leqNgt.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant sja := scheduled_jobs_at arr_seq sched t : seq Job
~~ (1 < size sja)
have uniq_sja : uniq sja by apply /filter_uniq/arrivals_uniq.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant sja := scheduled_jobs_at arr_seq sched t : seq Job uniq_sja : uniq sja
~~ (1 < size sja)
apply /negP => /exists_two/(_ uniq_sja)[j1 [j2 [j1j2 [j1sja j2sja]]]].Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant sja := scheduled_jobs_at arr_seq sched t : seq Job uniq_sja : uniq sja j1, j2 : Job j1j2 : j1 <> j2 j1sja : j1 \in sja j2sja : j2 \in sja
False
by apply /j1j2/(H_uni j1 j2 sched t); rewrite -scheduled_jobs_at_iff.
Qed .
(** For convenience, we restate the fact that there is at most one job as a
case analysis. *)
Corollary scheduled_jobs_at_uni_cases :
forall t ,
scheduled_jobs_at arr_seq sched t == [::]
\/ exists j , scheduled_jobs_at arr_seq sched t == [:: j].Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
scheduled_jobs_at arr_seq sched t == [::] \/
(exists j : Job,
scheduled_jobs_at arr_seq sched t == [:: j])
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
scheduled_jobs_at arr_seq sched t == [::] \/
(exists j : Job,
scheduled_jobs_at arr_seq sched t == [:: j])
move => t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
scheduled_jobs_at arr_seq sched t == [::] \/
(exists j : Job,
scheduled_jobs_at arr_seq sched t == [:: j])
rewrite /scheduled_job_at; move : (scheduled_jobs_at_seq1 t).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
size (scheduled_jobs_at arr_seq sched t) <= 1 ->
scheduled_jobs_at arr_seq sched t == [::] \/
(exists j : Job,
scheduled_jobs_at arr_seq sched t == [:: j])
case : scheduled_jobs_at => [//|j [|//]] _ /=.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant j : Job
[:: j] == [::] \/ (exists j0 : Job, [:: j] == [:: j0])
by right .
Qed .
(** We note the obvious relationship between [scheduled_jobs_at] and
[scheduled_job_at] ... *)
Lemma scheduled_jobs_at_uni :
forall j t ,
(scheduled_jobs_at arr_seq sched t == [::j])
= (scheduled_job_at arr_seq sched t == Some j).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_jobs_at arr_seq sched t == [:: j]) =
(scheduled_job_at arr_seq sched t == Some j)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_jobs_at arr_seq sched t == [:: j]) =
(scheduled_job_at arr_seq sched t == Some j)
move => j t; rewrite /scheduled_job_at.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState j : Job t : instant
(scheduled_jobs_at arr_seq sched t == [:: j]) =
(ohead (scheduled_jobs_at arr_seq sched t) == Some j)
have [/eqP -> //|[j' /eqP -> //=]] := scheduled_jobs_at_uni_cases t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState j : Job t : instant j' : Job
([:: j'] == [:: j]) = (Some j' == Some j)
exact : seq1_some.
Qed .
(** ... and observe that [scheduled_job_at t] behaves as expected: it yields
some job [j] if and only if [j] is scheduled at time [t]. *)
Corollary scheduled_job_at_scheduled_at :
forall j t ,
(scheduled_job_at arr_seq sched t == Some j) = scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_job_at arr_seq sched t == Some j) =
scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_job_at arr_seq sched t == Some j) =
scheduled_at sched j t
move => j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState j : Job t : instant
(scheduled_job_at arr_seq sched t == Some j) =
scheduled_at sched j t
rewrite -scheduled_jobs_at_uni -scheduled_jobs_at_iff.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState j : Job t : instant
(scheduled_jobs_at arr_seq sched t == [:: j]) =
(j \in scheduled_jobs_at arr_seq sched t)
by have [/eqP -> //|[j' /eqP -> //=]] := scheduled_jobs_at_uni_cases t.
Qed .
(** Similarly to [scheduled_job_at_scheduled_at], we relate
[scheduled_jobs_at] to [scheduled_at]. *)
Corollary scheduled_jobs_at_scheduled_at :
forall j t ,
(scheduled_jobs_at arr_seq sched t == [:: j])
= scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_jobs_at arr_seq sched t == [:: j]) =
scheduled_at sched j t
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall (j : Job) (t : instant),
(scheduled_jobs_at arr_seq sched t == [:: j]) =
scheduled_at sched j t
move => j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState j : Job t : instant
(scheduled_jobs_at arr_seq sched t == [:: j]) =
scheduled_at sched j t
by rewrite scheduled_jobs_at_uni scheduled_job_at_scheduled_at.
Qed .
(** Conversely, if [scheduled_job_at t] returns [None], then no job is
scheduled at time [t]. *)
Corollary scheduled_job_at_none :
forall t ,
scheduled_job_at arr_seq sched t = None
<-> (forall j , ~~ scheduled_at sched j t).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
scheduled_job_at arr_seq sched t = None <->
(forall j : Job, ~~ scheduled_at sched j t)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
scheduled_job_at arr_seq sched t = None <->
(forall j : Job, ~~ scheduled_at sched j t)
move => t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
scheduled_job_at arr_seq sched t = None <->
(forall j : Job, ~~ scheduled_at sched j t)
rewrite /scheduled_job_at -scheduled_jobs_at_nil.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
ohead (scheduled_jobs_at arr_seq sched t) = None <->
nilp (scheduled_jobs_at arr_seq sched t)
by case : (scheduled_jobs_at arr_seq sched t).
Qed .
(** For convenience, we state a similar observation also for the [is_idle]
wrapper, both for the idle case ... *)
Corollary is_idle_iff :
forall t ,
is_idle arr_seq sched t = (scheduled_job_at arr_seq sched t == None).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
is_idle arr_seq sched t =
(scheduled_job_at arr_seq sched t == None)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
is_idle arr_seq sched t =
(scheduled_job_at arr_seq sched t == None)
move => t; rewrite /is_idle/scheduled_job_at.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
(scheduled_jobs_at arr_seq sched t == [::]) =
(ohead (scheduled_jobs_at arr_seq sched t) == None)
by case : (scheduled_jobs_at _ _ _).
Qed .
(** ... and the non-idle case. *)
Corollary is_nonidle_iff :
forall t ,
~~ is_idle arr_seq sched t <-> exists j , scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
~~ is_idle arr_seq sched t <->
(exists j : Job, scheduled_at sched j t)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState
forall t : instant,
~~ is_idle arr_seq sched t <->
(exists j : Job, scheduled_at sched j t)
move => t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
~~ is_idle arr_seq sched t <->
(exists j : Job, scheduled_at sched j t)
rewrite is_idle_iff.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
scheduled_job_at arr_seq sched t != None <->
(exists j : Job, scheduled_at sched j t)
split => [|[j]]; last by rewrite -scheduled_job_at_scheduled_at => /eqP ->.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant
scheduled_job_at arr_seq sched t != None ->
exists j : Job, scheduled_at sched j t
case SJA: (scheduled_job_at _ _ _) => [j|//] _.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched H_uni : uniprocessor_model PState t : instant j : Job SJA : scheduled_job_at arr_seq sched t = Some j
exists j : Job, scheduled_at sched j t
by exists j ; rewrite -scheduled_job_at_scheduled_at; apply /eqP.
Qed .
End Uniprocessors .
(** ** Case Analysis: a Scheduled Job Exists or no Job is Scheduled*)
(** Last but not least, we note a case analysis that results from the above
considerations: at any point in time, either some job is scheduled, or it
holds that all jobs are not scheduled. *)
Lemma scheduled_at_dec :
forall t ,
{exists j , scheduled_at sched j t} + {forall j , ~~ scheduled_at sched j t}.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
move => t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
case SJA: (scheduled_jobs_at arr_seq sched t) => [|j js].Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant SJA : scheduled_jobs_at arr_seq sched t = [::]
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant SJA : scheduled_jobs_at arr_seq sched t = [::]
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
by right ; rewrite -scheduled_jobs_at_nil SJA.
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant j : Job js : seq Job SJA : scheduled_jobs_at arr_seq sched t = j :: js
{exists j : Job, scheduled_at sched j t} +
{forall j : Job, ~~ scheduled_at sched j t}
left ; exists j .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant j : Job js : seq Job SJA : scheduled_jobs_at arr_seq sched t = j :: js
scheduled_at sched j t
rewrite -scheduled_jobs_at_iff SJA.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant j : Job js : seq Job SJA : scheduled_jobs_at arr_seq sched t = j :: js
j \in j :: js
exact : mem_head.
Qed .
(** For ease of porting, we restate the above case analysis in a form closer
to what was used in earlier versions of Prosa. *)
Corollary scheduled_at_cases :
forall t ,
is_idle arr_seq sched t \/ exists j , scheduled_at sched j t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
Proof .Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched
forall t : instant,
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
move => t.Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
have [SCHED|IDLE] := (scheduled_at_dec t).Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant SCHED : exists j : Job, scheduled_at sched j t
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant SCHED : exists j : Job, scheduled_at sched j t
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
by right .
- Job : JobType H : JobArrival Job PState : ProcessorState Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq sched : schedule PState H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence
sched arr_seq H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute
sched t : instant IDLE : forall j : Job, ~~ scheduled_at sched j t
is_idle arr_seq sched t \/
(exists j : Job, scheduled_at sched j t)
by left ; apply /eqP/nilP; rewrite scheduled_jobs_at_nil.
Qed .
End ScheduledJobs .