Library prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.limited.schedule
prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions
prosa.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.limited.schedule
prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions
prosa.classic.model.schedule.uni.limited.abstract_RTA.sufficient_condition_for_lock_in_service
prosa.classic.model.schedule.uni.limited.abstract_RTA.reduction_of_search_space.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Abstract Response-Time Analysis
In this module, we propose the general framework for response-time analysis (RTA) of uniprocessor scheduling of real-time tasks with arbitrary arrival models.
Module AbstractRTA.
Import Job UniprocessorSchedule Service ResponseTime AbstractRTADefinitions
AbstractRTALockInService AbstractRTAReduction.
Section Abstract_RTA.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
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_job_cost_le_task_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost
task_cost job_cost job_task arr_seq.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable job_lock_in_service: Job → time.
Variable task_lock_in_service: Task → time.
Hypothesis H_proper_job_lock_in_service:
proper_job_lock_in_service job_cost arr_seq sched job_lock_in_service.
Hypothesis H_proper_task_lock_in_service:
proper_task_lock_in_service
task_cost job_task arr_seq job_lock_in_service task_lock_in_service tsk.
Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
Let busy_intervals_are_bounded_by := busy_intervals_are_bounded_by job_arrival job_cost job_task arr_seq sched tsk.
Let job_interference_is_bounded_by := job_interference_is_bounded_by job_arrival job_cost job_task arr_seq sched tsk.
Variable interference: Job → time → bool.
Variable interfering_workload: Job → time → time.
Hypothesis H_work_conserving: work_conserving interference interfering_workload.
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Variable L: time.
Hypothesis H_busy_interval_exists: busy_intervals_are_bounded_by interference interfering_workload L.
Variable interference_bound_function: Task → time → time → time.
Hypothesis H_job_interference_is_bounded:
job_interference_is_bounded_by interference interfering_workload interference_bound_function.
Let is_in_search_space A := is_in_search_space tsk L interference_bound_function A.
Variable R: nat.
Hypothesis H_R_is_maximum:
∀ A,
is_in_search_space A →
∃ F,
A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section ProofOfTheorem.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval j t1 t2.
Let A := job_arrival j - t1.
Variable A_sp F_sp: time.
Hypothesis H_A_gt_Asp: A_sp ≤ A.
Hypothesis H_equivalent:
are_equivalent_at_values_less_than (interference_bound_function tsk A) (interference_bound_function tsk A_sp) L.
Hypothesis H_Asp_is_in_search_space: is_in_search_space A_sp.
Hypothesis H_fixpoint:
A_sp + F_sp = task_lock_in_service tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
Hypothesis H_R_gt_Fsp: F_sp + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section FixpointOutsideBusyInterval.
Hypothesis H_big_fixpoint_solution: t2 ≤ t1 + (A_sp + F_sp).
Lemma t2_le_arrival_plus_R:
t2 ≤ job_arrival j + R.
Lemma job_completed_by_arrival_plus_R_1:
completed_by job_cost sched j (job_arrival j + R).
End FixpointOutsideBusyInterval.
Section FixpointInsideBusyInterval.
Hypothesis H_small_fixpoint_solution: t1 + (A_sp + F_sp) < t2.
Section FixpointIsNoLessThanArrival.
Hypothesis H_fixpoint_is_no_less_than_relative_arrival_of_j: A ≤ A_sp + F_sp.
Lemma solution_for_A_exists':
∃ F,
A_sp + F_sp = A + F ∧
F ≤ F_sp ∧
A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F).
Lemma job_completed_by_arrival_plus_R_2:
completed_by job_cost sched j (job_arrival j + R).
End FixpointIsNoLessThanArrival.
Section FixpointCannotBeSmallerThanArrival.
Hypothesis H_fixpoint_is_less_that_relative_arrival_of_j: A_sp + F_sp < A.
Lemma relative_arrival_is_bounded: A < L.
Lemma service_of_job_ge_lock_in_service:
service sched j (t1 + (A_sp + F_sp)) ≥ job_lock_in_service j.
Lemma relative_arrival_time_is_no_less_than_fixpoint:
False.
End FixpointCannotBeSmallerThanArrival.
End FixpointInsideBusyInterval.
End ProofOfTheorem.
Theorem uniprocessor_response_time_bound:
response_time_bounded_by tsk R.
End Abstract_RTA.
End AbstractRTA.
Import Job UniprocessorSchedule Service ResponseTime AbstractRTADefinitions
AbstractRTALockInService AbstractRTAReduction.
Section Abstract_RTA.
Context {Task: eqType}.
Variable task_cost: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
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_job_cost_le_task_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost
task_cost job_cost job_task arr_seq.
Variable ts: list Task.
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
Variable job_lock_in_service: Job → time.
Variable task_lock_in_service: Task → time.
Hypothesis H_proper_job_lock_in_service:
proper_job_lock_in_service job_cost arr_seq sched job_lock_in_service.
Hypothesis H_proper_task_lock_in_service:
proper_task_lock_in_service
task_cost job_task arr_seq job_lock_in_service task_lock_in_service tsk.
Let work_conserving := work_conserving job_arrival job_cost job_task arr_seq sched tsk.
Let busy_intervals_are_bounded_by := busy_intervals_are_bounded_by job_arrival job_cost job_task arr_seq sched tsk.
Let job_interference_is_bounded_by := job_interference_is_bounded_by job_arrival job_cost job_task arr_seq sched tsk.
Variable interference: Job → time → bool.
Variable interfering_workload: Job → time → time.
Hypothesis H_work_conserving: work_conserving interference interfering_workload.
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Variable L: time.
Hypothesis H_busy_interval_exists: busy_intervals_are_bounded_by interference interfering_workload L.
Variable interference_bound_function: Task → time → time → time.
Hypothesis H_job_interference_is_bounded:
job_interference_is_bounded_by interference interfering_workload interference_bound_function.
Let is_in_search_space A := is_in_search_space tsk L interference_bound_function A.
Variable R: nat.
Hypothesis H_R_is_maximum:
∀ A,
is_in_search_space A →
∃ F,
A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section ProofOfTheorem.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval j t1 t2.
Let A := job_arrival j - t1.
Variable A_sp F_sp: time.
Hypothesis H_A_gt_Asp: A_sp ≤ A.
Hypothesis H_equivalent:
are_equivalent_at_values_less_than (interference_bound_function tsk A) (interference_bound_function tsk A_sp) L.
Hypothesis H_Asp_is_in_search_space: is_in_search_space A_sp.
Hypothesis H_fixpoint:
A_sp + F_sp = task_lock_in_service tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
Hypothesis H_R_gt_Fsp: F_sp + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section FixpointOutsideBusyInterval.
Hypothesis H_big_fixpoint_solution: t2 ≤ t1 + (A_sp + F_sp).
Lemma t2_le_arrival_plus_R:
t2 ≤ job_arrival j + R.
Lemma job_completed_by_arrival_plus_R_1:
completed_by job_cost sched j (job_arrival j + R).
End FixpointOutsideBusyInterval.
Section FixpointInsideBusyInterval.
Hypothesis H_small_fixpoint_solution: t1 + (A_sp + F_sp) < t2.
Section FixpointIsNoLessThanArrival.
Hypothesis H_fixpoint_is_no_less_than_relative_arrival_of_j: A ≤ A_sp + F_sp.
Lemma solution_for_A_exists':
∃ F,
A_sp + F_sp = A + F ∧
F ≤ F_sp ∧
A + F = task_lock_in_service tsk + interference_bound_function tsk A (A + F).
Lemma job_completed_by_arrival_plus_R_2:
completed_by job_cost sched j (job_arrival j + R).
End FixpointIsNoLessThanArrival.
Section FixpointCannotBeSmallerThanArrival.
Hypothesis H_fixpoint_is_less_that_relative_arrival_of_j: A_sp + F_sp < A.
Lemma relative_arrival_is_bounded: A < L.
Lemma service_of_job_ge_lock_in_service:
service sched j (t1 + (A_sp + F_sp)) ≥ job_lock_in_service j.
Lemma relative_arrival_time_is_no_less_than_fixpoint:
False.
End FixpointCannotBeSmallerThanArrival.
End FixpointInsideBusyInterval.
End ProofOfTheorem.
Theorem uniprocessor_response_time_bound:
response_time_bounded_by tsk R.
End Abstract_RTA.
End AbstractRTA.