Library prosa.classic.model.schedule.uni.susp.suspension_intervals
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module SuspensionIntervals.
Export Job UniprocessorSchedule Suspension LastExecution.
(* In this section we define job suspension intervals in a schedule. *)
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any job suspension times... *)
Variable next_suspension: job_suspension Job.
(* ...and any uniprocessor schedule. *)
(*Context {arr_seq: arrival_sequence Job}.*)
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.
(* Based on the time after the last execution of a job, we define next
whether a job is suspended. *)
Section JobSuspension.
(* Let j be any job. *)
Variable j: Job.
Section DefiningSuspension.
(* We are going to define whether job j is suspended at time t. *)
Variable t: time.
(* First, we define the beginning of the latest self suspension as the
time following the last execution of job j in the interval 0, t). (Note that suspension_start can return time t itself.) *)
Let suspension_start := time_after_last_execution job_arrival sched j t.
(* Next, using the service received by j in the interval 0, suspension_start*)
Let),... current_service := service sched j suspension_start.
(* ... we recall the duration of the suspension expected for job j after having
received that amount of service. *)
Definition suspension_duration := next_suspension j current_service.
(* Then, we say that job j is suspended at time t iff j has not completed
by time t and t lies in the latest suspension interval.
(Also note that the suspension interval can have duration 0, in which
case suspended_at will be trivially false.) *)
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
(* Based on the notion of suspension, we also define the cumulative
suspension time of job j in any interval t1, t2)... *)
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
(* ...and the cumulative suspension time in any interval 0, t). *)
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
(* Next, we define whether the schedule respects self-suspensions. *)
Section SuspensionAwareSchedule.
(* We say that the schedule respects self-suspensions iff suspended
jobs are never scheduled. *)
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
(* In this section, we prove several results related to job suspensions. *)
Section Lemmas.
(* First, we prove that at any time within any suspension interval,
a job is always suspended. *)
Section InsideSuspensionInterval.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Consider any time t after the arrival of j... *)
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
(* ...and recall the latest suspension interval of job j relative to time t. *)
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
(* First, we analyze the service received during a suspension interval. *)
Section SameService.
(* Let t_in be any time in the suspension interval relative to time t. *)
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
(* Then, we show that the service received before time t_in
equals the service received before the beginning of the
latest suspension interval (if exists). *)
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
End SameService.
(* Next, we infer that the job is suspended at all times during
the suspension interval. *)
Section JobSuspendedAtAllTimes.
(* Let t_in be any time before the completion of job j. *)
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
(* If t_in lies in the suspension interval relative to time t, ...*)
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
(* ...then job j is suspended at time t_in. More precisely, the suspension
interval relative to time t_in is included in the suspension interval
relative to time t. *)
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
(* Next, we prove lemmas about the state of a suspended job. *)
Section StateOfSuspendedJob.
(* 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.
(* Assume that j is suspended at time t. *)
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
(* First, we show that j must have arrived by time t. *)
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
(* By the definition of suspension, it also follows that j cannot
have completed by time t. *)
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
End StateOfSuspendedJob.
(* Next, we establish a bound on the cumulative suspension time of any job. *)
Section BoundOnCumulativeSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Recall the total suspension of job j as given by the dynamic suspension model. *)
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
(* We prove that the cumulative suspension time of job j in any
interval is upper-bounded by the total suspension time. *)
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
End BoundOnCumulativeSuspension.
(* Next, we show that when a job completes, it must have suspended
as long as the total suspension time. *)
Section SuspendsForTotalSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Assume that j has completed by time t. *)
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
(* Then, we prove that the cumulative suspension time must be
exactly equal to the total suspension time of the job. *)
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
End SuspendsForTotalSuspension.
(* In this section, we prove that a job executes just before it starts suspending. *)
Section ExecutionBeforeSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job... *)
Variable j: Job.
(* ...that has arrived by some time t. *)
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
(* If job j is not suspended at time t, but starts to suspend at time t + 1, ... *)
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
(* ...then j must be scheduled at time t. *)
Lemma executes_before_suspension:
scheduled_at sched j t.
End ExecutionBeforeSuspension.
End Lemmas.
End DefiningSuspensionIntervals.
End SuspensionIntervals.
Require Import prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module SuspensionIntervals.
Export Job UniprocessorSchedule Suspension LastExecution.
(* In this section we define job suspension intervals in a schedule. *)
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
(* Consider any job suspension times... *)
Variable next_suspension: job_suspension Job.
(* ...and any uniprocessor schedule. *)
(*Context {arr_seq: arrival_sequence Job}.*)
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.
(* Based on the time after the last execution of a job, we define next
whether a job is suspended. *)
Section JobSuspension.
(* Let j be any job. *)
Variable j: Job.
Section DefiningSuspension.
(* We are going to define whether job j is suspended at time t. *)
Variable t: time.
(* First, we define the beginning of the latest self suspension as the
time following the last execution of job j in the interval 0, t). (Note that suspension_start can return time t itself.) *)
Let suspension_start := time_after_last_execution job_arrival sched j t.
(* Next, using the service received by j in the interval 0, suspension_start*)
Let),... current_service := service sched j suspension_start.
(* ... we recall the duration of the suspension expected for job j after having
received that amount of service. *)
Definition suspension_duration := next_suspension j current_service.
(* Then, we say that job j is suspended at time t iff j has not completed
by time t and t lies in the latest suspension interval.
(Also note that the suspension interval can have duration 0, in which
case suspended_at will be trivially false.) *)
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
(* Based on the notion of suspension, we also define the cumulative
suspension time of job j in any interval t1, t2)... *)
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
(* ...and the cumulative suspension time in any interval 0, t). *)
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
(* Next, we define whether the schedule respects self-suspensions. *)
Section SuspensionAwareSchedule.
(* We say that the schedule respects self-suspensions iff suspended
jobs are never scheduled. *)
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
(* In this section, we prove several results related to job suspensions. *)
Section Lemmas.
(* First, we prove that at any time within any suspension interval,
a job is always suspended. *)
Section InsideSuspensionInterval.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Consider any time t after the arrival of j... *)
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
(* ...and recall the latest suspension interval of job j relative to time t. *)
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
(* First, we analyze the service received during a suspension interval. *)
Section SameService.
(* Let t_in be any time in the suspension interval relative to time t. *)
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
(* Then, we show that the service received before time t_in
equals the service received before the beginning of the
latest suspension interval (if exists). *)
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
End SameService.
(* Next, we infer that the job is suspended at all times during
the suspension interval. *)
Section JobSuspendedAtAllTimes.
(* Let t_in be any time before the completion of job j. *)
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
(* If t_in lies in the suspension interval relative to time t, ...*)
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
(* ...then job j is suspended at time t_in. More precisely, the suspension
interval relative to time t_in is included in the suspension interval
relative to time t. *)
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
(* Next, we prove lemmas about the state of a suspended job. *)
Section StateOfSuspendedJob.
(* 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.
(* Assume that j is suspended at time t. *)
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
(* First, we show that j must have arrived by time t. *)
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
(* By the definition of suspension, it also follows that j cannot
have completed by time t. *)
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
End StateOfSuspendedJob.
(* Next, we establish a bound on the cumulative suspension time of any job. *)
Section BoundOnCumulativeSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Recall the total suspension of job j as given by the dynamic suspension model. *)
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
(* We prove that the cumulative suspension time of job j in any
interval is upper-bounded by the total suspension time. *)
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
End BoundOnCumulativeSuspension.
(* Next, we show that when a job completes, it must have suspended
as long as the total suspension time. *)
Section SuspendsForTotalSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job. *)
Variable j: Job.
(* Assume that j has completed by time t. *)
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
(* Then, we prove that the cumulative suspension time must be
exactly equal to the total suspension time of the job. *)
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
End SuspendsForTotalSuspension.
(* In this section, we prove that a job executes just before it starts suspending. *)
Section ExecutionBeforeSuspension.
(* Assume that jobs do not execute before they arrive... *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
(* ...and nor after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume that the schedule respects self-suspensions. *)
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
(* Let j be any job... *)
Variable j: Job.
(* ...that has arrived by some time t. *)
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
(* If job j is not suspended at time t, but starts to suspend at time t + 1, ... *)
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
(* ...then j must be scheduled at time t. *)
Lemma executes_before_suspension:
scheduled_at sched j t.
End ExecutionBeforeSuspension.
End Lemmas.
End DefiningSuspensionIntervals.
End SuspensionIntervals.