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.
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable next_suspension: job_suspension Job.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section JobSuspension.
Variable j: Job.
Section DefiningSuspension.
Variable t: time.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let current_service := service sched j suspension_start.
Definition suspension_duration := next_suspension j current_service.
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
Section SuspensionAwareSchedule.
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
Section Lemmas.
Section InsideSuspensionInterval.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
Section SameService.
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
End SameService.
Section JobSuspendedAtAllTimes.
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
Section StateOfSuspendedJob.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
End StateOfSuspendedJob.
Section BoundOnCumulativeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
End BoundOnCumulativeSuspension.
Section SuspendsForTotalSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
End SuspendsForTotalSuspension.
Section ExecutionBeforeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
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.
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable next_suspension: job_suspension Job.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section JobSuspension.
Variable j: Job.
Section DefiningSuspension.
Variable t: time.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let current_service := service sched j suspension_start.
Definition suspension_duration := next_suspension j current_service.
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
Section SuspensionAwareSchedule.
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
Section Lemmas.
Section InsideSuspensionInterval.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
Section SameService.
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
End SameService.
Section JobSuspendedAtAllTimes.
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
Section StateOfSuspendedJob.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
End StateOfSuspendedJob.
Section BoundOnCumulativeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
End BoundOnCumulativeSuspension.
Section SuspendsForTotalSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
End SuspendsForTotalSuspension.
Section ExecutionBeforeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
Lemma executes_before_suspension:
scheduled_at sched j t.
End ExecutionBeforeSuspension.
End Lemmas.
End DefiningSuspensionIntervals.
End SuspensionIntervals.