Library rt.model.schedule.uni.nonpreemptive.schedule
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job.
Require Import rt.model.schedule.uni.schedule.
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 rt.model.arrival.basic.job.
Require Import rt.model.schedule.uni.schedule.
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.