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.task.concept.[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.task_schedule.
Require Export prosa.analysis.facts.behavior.service.
Require Export prosa.analysis.facts.model.scheduled.
(** In this file we provide basic properties related to schedule of a task. *)
Section TaskSchedule .
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any valid arrival sequence of such jobs ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
(** ... and let [sched] be any corresponding uni-processor schedule. *)
Context {PState : ProcessorState Job}.
Hypothesis H_uniproc : uniprocessor_model PState.
Variable sched : schedule PState.
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.
(** Let [tsk] be any task. *)
Variable tsk : Task.
(** First, we show that a task is served at time [t], then the task
is scheduled at time [t]. *)
Lemma task_served_task_scheduled :
forall t ,
task_served_at arr_seq sched tsk t ->
task_scheduled_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
task_served_at arr_seq sched tsk t ->
task_scheduled_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
task_served_at arr_seq sched tsk t ->
task_scheduled_at arr_seq sched tsk t
move => t; apply contra => /eqP SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant SCHED : scheduled_jobs_of_task_at arr_seq sched tsk t =
[::]
served_jobs_of_task_at arr_seq sched tsk t == [::]
by rewrite /served_jobs_of_task_at SCHED.
Qed .
(** Next, we show that, under ideal-progress assumption, the notion
of task served coincides with the notion of task scheduled. *)
Lemma task_served_eq_task_scheduled :
ideal_progress_proc_model PState ->
forall t ,
task_served_at arr_seq sched tsk t = task_scheduled_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
ideal_progress_proc_model PState ->
forall t : instant,
task_served_at arr_seq sched tsk t =
task_scheduled_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
ideal_progress_proc_model PState ->
forall t : instant,
task_served_at arr_seq sched tsk t =
task_scheduled_at arr_seq sched tsk t
move => IDEAL t; apply /idP/idP; first by move => SERV; apply task_served_task_scheduled.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task IDEAL : ideal_progress_proc_model PState t : instant
task_scheduled_at arr_seq sched tsk t ->
task_served_at arr_seq sched tsk t
rewrite /task_scheduled_at -has_filter => /hasP [j SCHED TSK].Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task IDEAL : ideal_progress_proc_model PState t : instant j : Job SCHED : j \in scheduled_jobs_at arr_seq sched t TSK : job_of_task tsk j
task_served_at arr_seq sched tsk t
rewrite -[task_served_at _ _ _ _]has_filter; apply /hasP; exists j .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task IDEAL : ideal_progress_proc_model PState t : instant j : Job SCHED : j \in scheduled_jobs_at arr_seq sched t TSK : job_of_task tsk j
j \in scheduled_jobs_of_task_at arr_seq sched tsk t
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task IDEAL : ideal_progress_proc_model PState t : instant j : Job SCHED : j \in scheduled_jobs_at arr_seq sched t TSK : job_of_task tsk j
j \in scheduled_jobs_of_task_at arr_seq sched tsk t
by rewrite mem_filter; apply /andP; split .
- Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task IDEAL : ideal_progress_proc_model PState t : instant j : Job SCHED : j \in scheduled_jobs_at arr_seq sched t TSK : job_of_task tsk j
receives_service_at sched j t
by apply IDEAL; rewrite scheduled_jobs_at_iff in SCHED.
Qed .
(** We note that if the processor is idle at time [t], then no task
is scheduled. *)
Lemma no_task_scheduled_when_idle :
forall t ,
is_idle arr_seq sched t ->
~~ task_scheduled_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
is_idle arr_seq sched t ->
~~ task_scheduled_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
is_idle arr_seq sched t ->
~~ task_scheduled_at arr_seq sched tsk t
move => t IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t
~~ task_scheduled_at arr_seq sched tsk t
rewrite -[task_scheduled_at _ _ _ _]has_filter.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t
~~
has [eta job_of_task tsk]
(scheduled_jobs_at arr_seq sched t)
rewrite -all_predC.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t
all (predC [eta job_of_task tsk])
(scheduled_jobs_at arr_seq sched t)
apply /allP => j SCHED; exfalso .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t j : Job SCHED : j \in scheduled_jobs_at arr_seq sched t
False
rewrite scheduled_jobs_at_iff in SCHED => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t j : Job SCHED : scheduled_at sched j t
False
eapply not_scheduled_when_idle in IDLE => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant j : Job SCHED : scheduled_at sched j t IDLE : ~~ scheduled_at sched ?j t
False
exact : (negP IDLE).
Qed .
(** Similarly, if the processor is idle at time [t], then no task is
served. *)
Lemma no_task_served_when_idle :
forall t ,
is_idle arr_seq sched t ->
~~ task_served_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
is_idle arr_seq sched t ->
~~ task_served_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall t : instant,
is_idle arr_seq sched t ->
~~ task_served_at arr_seq sched tsk t
move => t IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : is_idle arr_seq sched t
~~ task_served_at arr_seq sched tsk t
apply no_task_scheduled_when_idle in IDLE.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task t : instant IDLE : ~~ task_scheduled_at arr_seq sched tsk t
~~ task_served_at arr_seq sched tsk t
by move : IDLE; apply contra, task_served_task_scheduled.
Qed .
(** We show that if a job is scheduled at time [t], then
[task_scheduled_at tsk t] is equal to [job_of_task tsk j]. In
other words, any occurrence of [task_scheduled_at] can be
replaced with [job_of_task]. *)
Lemma job_of_scheduled_task :
forall j t ,
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t = job_of_task tsk j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t =
job_of_task tsk j
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t =
job_of_task tsk j
move => j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t =
job_of_task tsk j
rewrite -(scheduled_jobs_at_scheduled_at arr_seq) //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
scheduled_jobs_at arr_seq sched t == [:: j] ->
task_scheduled_at arr_seq sched tsk t =
job_of_task tsk j
rewrite /task_scheduled_at /scheduled_jobs_of_task_at => /eqP -> //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
((if job_of_task tsk j then [:: j] else [::]) != [::]) =
job_of_task tsk j
by case : (job_of_task _ _).
Qed .
(** As a corollary, we show that if a job of task [tsk] is scheduled
at time [t], then task [tsk] is scheduled at time [t]. *)
Corollary job_of_task_scheduled :
forall j t ,
job_of_task tsk j ->
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
job_of_task tsk j ->
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
job_of_task tsk j ->
scheduled_at sched j t ->
task_scheduled_at arr_seq sched tsk t
by move => j t TSK SCHED; rewrite (job_of_scheduled_task j) => //.
Qed .
(** And vice versa, if no job of task [tsk] is scheduled at time
[t], then task [tsk] is not scheduled at time [t]. *)
Corollary job_of_other_task_scheduled :
forall j t ,
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_scheduled_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_scheduled_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_scheduled_at arr_seq sched tsk t
by move => j t TSK SCHED; rewrite (job_of_scheduled_task j) => //.
Qed .
(** Similarly, we show that if no job of task [tsk] is scheduled at
time [t], then task [tsk] is not served at time [t]. *)
Corollary job_of_other_task_scheduled' :
forall j t ,
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_served_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_served_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
~~ job_of_task tsk j ->
scheduled_at sched j t ->
~~ task_served_at arr_seq sched tsk t
move => j t TSK SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant TSK : ~~ job_of_task tsk j SCHED : scheduled_at sched j t
~~ task_served_at arr_seq sched tsk t
apply : (contra (task_served_task_scheduled _)).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant TSK : ~~ job_of_task tsk j SCHED : scheduled_at sched j t
~~ task_scheduled_at arr_seq sched tsk t
exact : job_of_other_task_scheduled.
Qed .
(** Lastly, if a job of task [tsk] is scheduled at time [t] but
receives no service, then task [tsk] is not served at time
[t]. *)
Corollary job_of_task_not_served :
forall j t ,
scheduled_at sched j t ->
job_of_task tsk j ->
service_at sched j t = 0 ->
~~ task_served_at arr_seq sched tsk t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
scheduled_at sched j t ->
job_of_task tsk j ->
service_at sched j t = 0 ->
~~ task_served_at arr_seq sched tsk t
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task
forall (j : Job) (t : instant),
scheduled_at sched j t ->
job_of_task tsk j ->
service_at sched j t = 0 ->
~~ task_served_at arr_seq sched tsk t
move => j t.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
scheduled_at sched j t ->
job_of_task tsk j ->
service_at sched j t = 0 ->
~~ task_served_at arr_seq sched tsk t
rewrite -(scheduled_jobs_at_scheduled_at arr_seq) //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
scheduled_jobs_at arr_seq sched t == [:: j] ->
job_of_task tsk j ->
service_at sched j t = 0 ->
~~ task_served_at arr_seq sched tsk t
rewrite /task_scheduled_at /task_served_at /served_jobs_of_task_at /scheduled_jobs_of_task_at => /eqP -> //= -> //=.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task j : Job t : instant
service_at sched j t = 0 ->
~~
((if receives_service_at sched j t
then [:: j]
else [::]) != [::])
by rewrite /receives_service_at => ->.
Qed .
(** In the following section, we prove a rewriting rule between the
predicate [task_served_at] and [job_of_task]. *)
Section SomeJobIsScheduled .
(** Assume that the processor is fully supply-consuming. *)
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
(** Consider a time instant [t] ... *)
Variable t : instant.
(** ... and assume that there is supply at [t]. *)
Hypothesis H_supply : has_supply sched t.
(** Consider jobs [j] and [j'] ([j'] is not necessarily distinct
from job [j]). Assume that [j] is scheduled at time [t]. *)
Variable j : Job.
Hypothesis H_sched : scheduled_at sched j t.
(** Then the predicate [task_served_at] is equal to the predicate
[job_of_task]. *)
Lemma task_served_at_eq_job_of_task :
task_served_at arr_seq sched tsk t = job_of_task tsk j.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t
task_served_at arr_seq sched tsk t = job_of_task tsk j
Proof .Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t
task_served_at arr_seq sched tsk t = job_of_task tsk j
have SERV : receives_service_at sched j t by apply ideal_progress_inside_supplies.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t
task_served_at arr_seq sched tsk t = job_of_task tsk j
rewrite /task_served_at /served_jobs_of_task_at /scheduled_jobs_of_task_at.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t
([seq j <- [seq j <- scheduled_jobs_at arr_seq sched t
| job_of_task tsk j]
| receives_service_at sched j t] != [::]) =
job_of_task tsk j
move : (H_sched) => SCHED.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t SCHED : scheduled_at sched j t
([seq j <- [seq j <- scheduled_jobs_at arr_seq sched t
| job_of_task tsk j]
| receives_service_at sched j t] != [::]) =
job_of_task tsk j
erewrite <-scheduled_jobs_at_scheduled_at in SCHED => //.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t SCHED : scheduled_jobs_at arr_seq sched t == [:: j]
([seq j <- [seq j <- scheduled_jobs_at arr_seq sched t
| job_of_task tsk j]
| receives_service_at sched j t] != [::]) =
job_of_task tsk j
move : SCHED => /eqP ->.Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t
([seq j <- [seq j <- [:: j] | job_of_task tsk j]
| receives_service_at sched j t] != [::]) =
job_of_task tsk j
have [TSK|/negPf NTSK] := boolP (job_of_task tsk j).Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t TSK : job_of_task tsk j
([seq j <- [seq j <- [:: j] | job_of_task tsk j]
| receives_service_at sched j t] != [::]) = true
{ Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t TSK : job_of_task tsk j
([seq j <- [seq j <- [:: j] | job_of_task tsk j]
| receives_service_at sched j t] != [::]) = true
by rewrite //= TSK //= SERV. } Task : TaskType H : TaskCost Task Job : JobType H0 : JobTask Job Task H1 : JobArrival Job H2 : JobCost Job arr_seq : arrival_sequence Job H_valid_arrivals : valid_arrival_sequence arr_seq PState : ProcessorState Job H_uniproc : uniprocessor_model PState 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 tsk : Task H_consumed_supply_proc_model : fully_consuming_proc_model
PState t : instant H_supply : has_supply sched t j : Job H_sched : scheduled_at sched j t SERV : receives_service_at sched j t NTSK : job_of_task tsk j = false
([seq j <- [seq j <- [:: j] | job_of_task tsk j]
| receives_service_at sched j t] != [::]) = false
by rewrite //= NTSK //=.
Qed .
End SomeJobIsScheduled .
End TaskSchedule .