Library prosa.classic.model.schedule.uni.nonpreemptive.schedule
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module NonpreemptiveSchedule.
Export UniprocessorSchedule.
Section Definitions.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any uniprocessor schedule. *)
Variable sched: schedule Job.
(* For simplicity, let's define some local names. *)
Let job_completed_by := completed_by job_cost sched.
Let job_remaining_cost j t := remaining_cost job_cost sched j t.
(* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
Definition is_nonpreemptive_schedule :=
∀ j t t',
t ≤ t' →
scheduled_at sched j t →
~~ job_completed_by j t' →
scheduled_at sched j t'.
(* In this section, we prove some basic lemmas about nonpreemptive schedules. *)
Section Lemmas.
(* Assume that we have a nonpreemptive schedule. *)
Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.
Section BasicLemmas.
(* Consider any job j. *)
Variable j: Job.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* First, we show that if j is scheduled at any two time instants,
then it is also scheduled at any time between them. *)
Lemma continuity_of_nonpreemptive_scheduling:
∀ t t1 t2,
t1 ≤ t ≤ t2 →
scheduled_at sched j t1 →
scheduled_at sched j t2 →
scheduled_at sched j t.
(* Next, we show that in any nonpreemptive schedule, once a job is scheduled,
it cannot be preempted until completion. *)
Lemma in_nonpreemption_schedule_preemption_implies_completeness:
∀ t t' ,
t ≤ t' →
scheduled_at sched j t →
~~ scheduled_at sched j t' →
job_completed_by j t'.
End BasicLemmas.
(* In this section, we prove properties related to job completion. *)
Section CompletionUnderNonpreemptive.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
Lemma job_completes_after_remaining_cost:
∀ j t,
scheduled_at sched j t →
job_completed_by j (t + job_remaining_cost j t).
End CompletionUnderNonpreemptive.
(* In this section, we determine bounds on the length of the execution interval. *)
Section ExecutionInterval.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Let j be any job scheduled at time t. *)
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.
(* Is this section we show that there is a bound for how early job j can start. *)
Section LeftBound.
(* We prove that job j is scheduled at time (t - service sched j t)... *)
Lemma j_is_scheduled_at_t_minus_service:
scheduled_at sched j (t - service sched j t).
(* ... and it is not scheduled at time (t - service sched j t - 1). *)
Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
t - service sched j t > 0 →
~~ scheduled_at sched j (t - service sched j t - 1).
(* Using the previous lemma, we show that job j cannot be scheduled
before (t - service sched j t). *)
Lemma j_is_not_scheduled_earlier_t_minus_service:
∀ t',
t' < t - service sched j t →
~~ scheduled_at sched j t'.
End LeftBound.
(* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
Section RightBound.
(* We show that if job j is scheduled at time t,
then it is also scheduled at time (t + remaining_cost j t - 1)... *)
Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
scheduled_at sched j (t + job_remaining_cost j t - 1).
(* ... and it is not scheduled after (t + remaining cost j t - 1). *)
Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
∀ t',
t + job_remaining_cost j t ≤ t' →
~~ scheduled_at sched j t'.
End RightBound.
(* To conclude, we identify the interval where job j is scheduled. *)
Lemma nonpreemptive_executing_interval:
∀ t',
t - service sched j t ≤ t' < t + job_remaining_cost j t →
scheduled_at sched j t'.
End ExecutionInterval.
End Lemmas.
End Definitions.
End NonpreemptiveSchedule.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module NonpreemptiveSchedule.
Export UniprocessorSchedule.
Section Definitions.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any uniprocessor schedule. *)
Variable sched: schedule Job.
(* For simplicity, let's define some local names. *)
Let job_completed_by := completed_by job_cost sched.
Let job_remaining_cost j t := remaining_cost job_cost sched j t.
(* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
Definition is_nonpreemptive_schedule :=
∀ j t t',
t ≤ t' →
scheduled_at sched j t →
~~ job_completed_by j t' →
scheduled_at sched j t'.
(* In this section, we prove some basic lemmas about nonpreemptive schedules. *)
Section Lemmas.
(* Assume that we have a nonpreemptive schedule. *)
Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.
Section BasicLemmas.
(* Consider any job j. *)
Variable j: Job.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* First, we show that if j is scheduled at any two time instants,
then it is also scheduled at any time between them. *)
Lemma continuity_of_nonpreemptive_scheduling:
∀ t t1 t2,
t1 ≤ t ≤ t2 →
scheduled_at sched j t1 →
scheduled_at sched j t2 →
scheduled_at sched j t.
(* Next, we show that in any nonpreemptive schedule, once a job is scheduled,
it cannot be preempted until completion. *)
Lemma in_nonpreemption_schedule_preemption_implies_completeness:
∀ t t' ,
t ≤ t' →
scheduled_at sched j t →
~~ scheduled_at sched j t' →
job_completed_by j t'.
End BasicLemmas.
(* In this section, we prove properties related to job completion. *)
Section CompletionUnderNonpreemptive.
(* Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
Lemma job_completes_after_remaining_cost:
∀ j t,
scheduled_at sched j t →
job_completed_by j (t + job_remaining_cost j t).
End CompletionUnderNonpreemptive.
(* In this section, we determine bounds on the length of the execution interval. *)
Section ExecutionInterval.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Let j be any job scheduled at time t. *)
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.
(* Is this section we show that there is a bound for how early job j can start. *)
Section LeftBound.
(* We prove that job j is scheduled at time (t - service sched j t)... *)
Lemma j_is_scheduled_at_t_minus_service:
scheduled_at sched j (t - service sched j t).
(* ... and it is not scheduled at time (t - service sched j t - 1). *)
Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
t - service sched j t > 0 →
~~ scheduled_at sched j (t - service sched j t - 1).
(* Using the previous lemma, we show that job j cannot be scheduled
before (t - service sched j t). *)
Lemma j_is_not_scheduled_earlier_t_minus_service:
∀ t',
t' < t - service sched j t →
~~ scheduled_at sched j t'.
End LeftBound.
(* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
Section RightBound.
(* We show that if job j is scheduled at time t,
then it is also scheduled at time (t + remaining_cost j t - 1)... *)
Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
scheduled_at sched j (t + job_remaining_cost j t - 1).
(* ... and it is not scheduled after (t + remaining cost j t - 1). *)
Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
∀ t',
t + job_remaining_cost j t ≤ t' →
~~ scheduled_at sched j t'.
End RightBound.
(* To conclude, we identify the interval where job j is scheduled. *)
Lemma nonpreemptive_executing_interval:
∀ t',
t - service sched j t ≤ t' < t + job_remaining_cost j t →
scheduled_at sched j t'.
End ExecutionInterval.
End Lemmas.
End Definitions.
End NonpreemptiveSchedule.