Library prosa.classic.model.schedule.uni.susp.last_execution
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In this file, we show how to compute the time instant after the last
execution of a job and prove several lemmas about that instant. This
notion is crucial for defining suspension intervals. *)
Module LastExecution.
Export Job UniprocessorSchedule.
(* In this section we define the time after the last execution of a job (if exists). *)
Section TimeAfterLastExecution.
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_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section Defs.
(* Let j be any job in the arrival sequence. *)
Variable j: Job.
(* Next, we will show how to find the time after the most recent
execution of a given job j in the interval job_arrival j, t). (Note that this instant can be time t itself.) *)
Variable t: time.
(* Let scheduled_before denote whether job j was scheduled in the interval 0, t). *)
Let scheduled_before :=
[∃ t0: 'I_t, job_scheduled_at j t0].
(* In case j was scheduled before, we define the last time in which j was scheduled. *)
Let last_time_scheduled :=
\max_(t_last < t | job_scheduled_at j t_last) t_last.
(* Then, the time after the last execution of job j in the interval 0, t), if ∃, occurs: (a) immediately after the last time in which job j was scheduled, or, (b) if j was never scheduled, at the arrival time of j. *)
Definition time_after_last_execution :=
if scheduled_before then
last_time_scheduled + 1
else job_arrival j.
End Defs.
(* Next, we prove lemmas about the time after the last execution. *)
Section Lemmas.
(* Assume that jobs do not execute before they arrived. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* Let j be any job. *)
Variable j: Job.
(* In this section, we show that the time after the last execution occurs
no earlier than the arrival of the job. *)
Section JobHasArrived.
(* Then, the time following the last execution of job j in the
interval 0, t) occurs no earlier than the arrival of j. *)
Lemma last_execution_after_arrival:
∀ t,
has_arrived job_arrival j (time_after_last_execution j t).
End JobHasArrived.
(* Next, we establish the monotonicity of the function. *)
Section Monotonicity.
(* Let t1 be any time no earlier than the arrival of job j. *)
Variable t1: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t1.
(* Then, (time_after_last_execution j) grows monotonically
after that point. *)
Lemma last_execution_monotonic:
∀ t2,
t1 ≤ t2 →
time_after_last_execution j t1 ≤ time_after_last_execution j t2.
End Monotonicity.
(* Next, we prove that the function is idempotent. *)
Section Idempotence.
(* The time after the last execution of job j is an idempotent function. *)
Lemma last_execution_idempotent:
∀ t,
time_after_last_execution j (time_after_last_execution j t)
= time_after_last_execution j t.
End Idempotence.
(* Next, we show that time_after_last_execution is bounded by the identity function. *)
Section BoundedByIdentity.
(* Let t be any time no earlier than the arrival of j. *)
Variable t: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t.
(* Then, the time following the last execution of job j in the interval 0, t) occurs no later than time t. *)
Lemma last_execution_bounded_by_identity:
time_after_last_execution j t ≤ t.
End BoundedByIdentity.
(* In this section, we show that if the service received by a job
remains the same, the time after last execution also doesn't change. *)
Section SameLastExecution.
(* Consider any time instants t and t'... *)
Variable t t': time.
(* ...in which job j has received the same amount of service. *)
Hypothesis H_same_service: service sched j t = service sched j t'.
(* Then, we prove that the times after last execution relative to
instants t and t' are exactly the same. *)
Lemma same_service_implies_same_last_execution:
time_after_last_execution j t = time_after_last_execution j t'.
End SameLastExecution.
(* In this section, we show that the service received by a job
does not change since the last execution. *)
Section SameService.
(* We prove that, for any time t, the service received by job j
before (time_after_last_execution j t) is the same as the service
by j before time t. *)
Lemma same_service_since_last_execution:
∀ t,
service sched j (time_after_last_execution j t) = service sched j t.
End SameService.
(* In this section, we show that for any smaller value of service, we can
always find the last execution that corresponds to that service. *)
Section ExistsIntermediateExecution.
(* Assume that job j has completed by time t. *)
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
(* Then, for any value of service less than the cost of j, ...*)
Variable s: time.
Hypothesis H_less_than_cost: s < job_cost j.
(* ...there exists a last execution where the service received
by job j equals s. *)
Lemma exists_last_execution_with_smaller_service:
∃ t0,
service sched j (time_after_last_execution j t0) = s.
End ExistsIntermediateExecution.
(* In this section we prove that before the last execution the job
must have received strictly less service. *)
Section LessServiceBeforeLastExecution.
(* Let t be any time... *)
Variable t: time.
(* ...and consider any earlier time t0 no earlier than the arrival of job j... *)
Variable t0: time.
Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.
(* ...and before the last execution of job j (with respect to time t). *)
Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.
(* Then, we can prove that the service received by j before time t0
is strictly less than the service received by j before time t. *)
Lemma less_service_before_start_of_suspension:
service sched j t0 < service sched j t.
End LessServiceBeforeLastExecution.
End Lemmas.
End TimeAfterLastExecution.
End LastExecution.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(* In this file, we show how to compute the time instant after the last
execution of a job and prove several lemmas about that instant. This
notion is crucial for defining suspension intervals. *)
Module LastExecution.
Export Job UniprocessorSchedule.
(* In this section we define the time after the last execution of a job (if exists). *)
Section TimeAfterLastExecution.
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_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section Defs.
(* Let j be any job in the arrival sequence. *)
Variable j: Job.
(* Next, we will show how to find the time after the most recent
execution of a given job j in the interval job_arrival j, t). (Note that this instant can be time t itself.) *)
Variable t: time.
(* Let scheduled_before denote whether job j was scheduled in the interval 0, t). *)
Let scheduled_before :=
[∃ t0: 'I_t, job_scheduled_at j t0].
(* In case j was scheduled before, we define the last time in which j was scheduled. *)
Let last_time_scheduled :=
\max_(t_last < t | job_scheduled_at j t_last) t_last.
(* Then, the time after the last execution of job j in the interval 0, t), if ∃, occurs: (a) immediately after the last time in which job j was scheduled, or, (b) if j was never scheduled, at the arrival time of j. *)
Definition time_after_last_execution :=
if scheduled_before then
last_time_scheduled + 1
else job_arrival j.
End Defs.
(* Next, we prove lemmas about the time after the last execution. *)
Section Lemmas.
(* Assume that jobs do not execute before they arrived. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* Let j be any job. *)
Variable j: Job.
(* In this section, we show that the time after the last execution occurs
no earlier than the arrival of the job. *)
Section JobHasArrived.
(* Then, the time following the last execution of job j in the
interval 0, t) occurs no earlier than the arrival of j. *)
Lemma last_execution_after_arrival:
∀ t,
has_arrived job_arrival j (time_after_last_execution j t).
End JobHasArrived.
(* Next, we establish the monotonicity of the function. *)
Section Monotonicity.
(* Let t1 be any time no earlier than the arrival of job j. *)
Variable t1: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t1.
(* Then, (time_after_last_execution j) grows monotonically
after that point. *)
Lemma last_execution_monotonic:
∀ t2,
t1 ≤ t2 →
time_after_last_execution j t1 ≤ time_after_last_execution j t2.
End Monotonicity.
(* Next, we prove that the function is idempotent. *)
Section Idempotence.
(* The time after the last execution of job j is an idempotent function. *)
Lemma last_execution_idempotent:
∀ t,
time_after_last_execution j (time_after_last_execution j t)
= time_after_last_execution j t.
End Idempotence.
(* Next, we show that time_after_last_execution is bounded by the identity function. *)
Section BoundedByIdentity.
(* Let t be any time no earlier than the arrival of j. *)
Variable t: time.
Hypothesis H_after_arrival: has_arrived job_arrival j t.
(* Then, the time following the last execution of job j in the interval 0, t) occurs no later than time t. *)
Lemma last_execution_bounded_by_identity:
time_after_last_execution j t ≤ t.
End BoundedByIdentity.
(* In this section, we show that if the service received by a job
remains the same, the time after last execution also doesn't change. *)
Section SameLastExecution.
(* Consider any time instants t and t'... *)
Variable t t': time.
(* ...in which job j has received the same amount of service. *)
Hypothesis H_same_service: service sched j t = service sched j t'.
(* Then, we prove that the times after last execution relative to
instants t and t' are exactly the same. *)
Lemma same_service_implies_same_last_execution:
time_after_last_execution j t = time_after_last_execution j t'.
End SameLastExecution.
(* In this section, we show that the service received by a job
does not change since the last execution. *)
Section SameService.
(* We prove that, for any time t, the service received by job j
before (time_after_last_execution j t) is the same as the service
by j before time t. *)
Lemma same_service_since_last_execution:
∀ t,
service sched j (time_after_last_execution j t) = service sched j t.
End SameService.
(* In this section, we show that for any smaller value of service, we can
always find the last execution that corresponds to that service. *)
Section ExistsIntermediateExecution.
(* Assume that job j has completed by time t. *)
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
(* Then, for any value of service less than the cost of j, ...*)
Variable s: time.
Hypothesis H_less_than_cost: s < job_cost j.
(* ...there exists a last execution where the service received
by job j equals s. *)
Lemma exists_last_execution_with_smaller_service:
∃ t0,
service sched j (time_after_last_execution j t0) = s.
End ExistsIntermediateExecution.
(* In this section we prove that before the last execution the job
must have received strictly less service. *)
Section LessServiceBeforeLastExecution.
(* Let t be any time... *)
Variable t: time.
(* ...and consider any earlier time t0 no earlier than the arrival of job j... *)
Variable t0: time.
Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.
(* ...and before the last execution of job j (with respect to time t). *)
Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.
(* Then, we can prove that the service received by j before time t0
is strictly less than the service received by j before time t. *)
Lemma less_service_before_start_of_suspension:
service sched j t0 < service sched j t.
End LessServiceBeforeLastExecution.
End Lemmas.
End TimeAfterLastExecution.
End LastExecution.