Library prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time
prosa.classic.model.schedule.uni.schedule_of_task.
Require Import prosa.classic.model.schedule.uni.limited.rbf
prosa.classic.model.schedule.uni.limited.schedule.
Require Import prosa.classic.model.arrival.curves.bounds.
Require Import prosa.classic.analysis.uni.arrival_curves.workload_bound.
Require Import 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
prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Require Import prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule
prosa.classic.model.schedule.uni.response_time
prosa.classic.model.schedule.uni.schedule_of_task.
Require Import prosa.classic.model.schedule.uni.limited.rbf
prosa.classic.model.schedule.uni.limited.schedule.
Require Import prosa.classic.model.arrival.curves.bounds.
Require Import prosa.classic.analysis.uni.arrival_curves.workload_bound.
Require Import 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
prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
Abstract Response-Time Analysis with sequential jobs
In this module we propose the general framework for response-time analysis (RTA) of uniprocessor scheduling of real-time tasks with arbitrary arrival models and sequential jobs.
Module AbstractSeqRTA.
Import Job ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
Service ResponseTime MaxArrivalsWorkloadBound
AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction AbstractRTA.
Section Sequential_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.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Let arrivals_between := jobs_arrived_between arr_seq.
Let task_scheduled_at := task_scheduled_at job_task sched.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Variable ts: list Task.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable max_arrivals: Task → time → nat.
Hypothesis H_family_of_proper_arrival_curves:
family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
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.
Variable interference: Job → time → bool.
Variable interfering_workload: Job → time → time.
Let task_rbf := task_request_bound_function task_cost max_arrivals 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.
Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
Let task_workload_between := task_workload_between job_cost job_task arr_seq tsk.
Let arrivals_of_task_before := arrivals_of_task_before job_task arr_seq.
Let task_service_between := task_service_between job_task arr_seq sched tsk.
Section Definitions.
Definition interference_and_workload_consistent_with_sequential_jobs :=
∀ j t1 t2,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
busy_interval j t1 t2 →
task_workload_between 0 t1 = task_service_between 0 t1.
Definition task_interference_received_before (tsk: Task) (upper_bound: time) (t: time) :=
(~~ task_scheduled_at tsk t)
&& has (fun j ⇒ interference j t) (arrivals_of_task_before tsk upper_bound).
Definition cumul_task_interference tsk upper_bound t1 t2 :=
\sum_(t1 ≤ t < t2) task_interference_received_before tsk upper_bound t.
Definition task_interference_is_bounded_by (task_interference_bound_function: Task → time → time → time) :=
∀ j R t1 t2,
arrives_in arr_seq j →
job_task j = tsk →
t1 + R < t2 →
~~ job_completed_by j (t1 + R) →
busy_interval j t1 t2 →
let offset := job_arrival j - t1 in
cumul_task_interference tsk t2 t1 (t1 + R) ≤ task_interference_bound_function tsk offset R.
End Definitions.
Section ResponseTimeBound.
Let cumul_interference := cumul_interference interference.
Let cumul_workload := cumul_interfering_workload interfering_workload.
Let cumul_task_interference := cumul_task_interference tsk.
Hypothesis H_work_conserving: work_conserving interference interfering_workload.
Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
Hypothesis H_interference_and_workload_consistent_with_sequential_jobs:
interference_and_workload_consistent_with_sequential_jobs.
Variable L: time.
Hypothesis H_busy_interval_exists: busy_intervals_are_bounded_by interference interfering_workload L.
Variable task_interference_bound_function: Task → time → time → time.
Hypothesis H_task_interference_is_bounded: task_interference_is_bounded_by task_interference_bound_function.
Let total_interference_bound tsk A Δ :=
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A Δ.
Let is_in_search_space_seq := is_in_search_space tsk L total_interference_bound.
Variable R: nat.
Hypothesis H_R_is_maximum_seq:
∀ A,
is_in_search_space_seq A →
∃ F,
A + F = (task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk))
+ task_interference_bound_function tsk A (A + F) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section CompletionOfJobsFromSameTask.
Variable j1 j2: Job.
Hypothesis H_j1_arrives: arrives_in arr_seq j1.
Hypothesis H_j2_arrives: arrives_in arr_seq j2.
Hypothesis H_j1_from_tsk: job_task j1 = tsk.
Hypothesis H_j2_from_tsk: job_task j2 = tsk.
Hypothesis H_j1_cost_positive: job_cost_positive job_cost j1.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval j1 t1 t2.
Lemma completed_before_beginning_of_busy_interval:
job_arrival j2 < t1 →
completed_by job_cost sched j2 t1.
Lemma arrives_after_beginning_of_busy_interval:
∀ t,
t1 ≤ t →
job_pending_at j2 t →
arrived_between job_arrival j2 t1 t.+1.
End CompletionOfJobsFromSameTask.
Section BoundOfCumulativeJobInterference.
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 x: time.
Hypothesis H_inside_busy_interval: t1 + x < t2.
Hypothesis H_job_j_is_not_completed: ~~ job_completed_by j (t1 + x).
Lemma bound_for_cumulative_job_interference_actual:
cumul_interference j t1 (t1 + x) ≤
(task_workload_between t1 (t1 + A + ε) - job_cost j) + cumul_task_interference t2 t1 (t1 + x).
Lemma task_rbf_excl_tsk_bounds_task_workload_excl_j:
task_workload_between t1 (t1 + A + ε) - job_cost j ≤ task_rbf (A + ε) - task_cost tsk.
Lemma bound_for_cumulative_job_interference:
cumul_interference j t1 (t1 + x)
≤ (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference t2 t1 (t1 + x).
End BoundOfCumulativeJobInterference.
Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Let is_in_search_space A :=
is_in_search_space tsk L total_interference_bound A.
Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
∀ A,
is_in_search_space A →
∃ F,
A + F = task_lock_in_service tsk +
(task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A (A + F)) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
Theorem uniprocessor_response_time_bound_seq:
response_time_bounded_by tsk R.
End ResponseTimeBound.
End Sequential_Abstract_RTA.
End AbstractSeqRTA.
Import Job ArrivalCurves TaskArrival ScheduleOfTask UniprocessorSchedule Workload
Service ResponseTime MaxArrivalsWorkloadBound
AbstractRTADefinitions AbstractRTALockInService AbstractRTAReduction AbstractRTA.
Section Sequential_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.
Let job_pending_at := pending job_arrival job_cost sched.
Let job_completed_by := completed_by job_cost sched.
Let arrivals_between := jobs_arrived_between arr_seq.
Let task_scheduled_at := task_scheduled_at job_task sched.
Let response_time_bounded_by :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
Variable ts: list Task.
Hypothesis H_all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Variable max_arrivals: Task → time → nat.
Hypothesis H_family_of_proper_arrival_curves:
family_of_proper_arrival_curves job_task arr_seq max_arrivals ts.
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.
Variable interference: Job → time → bool.
Variable interfering_workload: Job → time → time.
Let task_rbf := task_request_bound_function task_cost max_arrivals 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.
Let busy_interval := busy_interval job_arrival job_cost sched interference interfering_workload.
Let task_workload_between := task_workload_between job_cost job_task arr_seq tsk.
Let arrivals_of_task_before := arrivals_of_task_before job_task arr_seq.
Let task_service_between := task_service_between job_task arr_seq sched tsk.
Section Definitions.
Definition interference_and_workload_consistent_with_sequential_jobs :=
∀ j t1 t2,
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
busy_interval j t1 t2 →
task_workload_between 0 t1 = task_service_between 0 t1.
Definition task_interference_received_before (tsk: Task) (upper_bound: time) (t: time) :=
(~~ task_scheduled_at tsk t)
&& has (fun j ⇒ interference j t) (arrivals_of_task_before tsk upper_bound).
Definition cumul_task_interference tsk upper_bound t1 t2 :=
\sum_(t1 ≤ t < t2) task_interference_received_before tsk upper_bound t.
Definition task_interference_is_bounded_by (task_interference_bound_function: Task → time → time → time) :=
∀ j R t1 t2,
arrives_in arr_seq j →
job_task j = tsk →
t1 + R < t2 →
~~ job_completed_by j (t1 + R) →
busy_interval j t1 t2 →
let offset := job_arrival j - t1 in
cumul_task_interference tsk t2 t1 (t1 + R) ≤ task_interference_bound_function tsk offset R.
End Definitions.
Section ResponseTimeBound.
Let cumul_interference := cumul_interference interference.
Let cumul_workload := cumul_interfering_workload interfering_workload.
Let cumul_task_interference := cumul_task_interference tsk.
Hypothesis H_work_conserving: work_conserving interference interfering_workload.
Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.
Hypothesis H_interference_and_workload_consistent_with_sequential_jobs:
interference_and_workload_consistent_with_sequential_jobs.
Variable L: time.
Hypothesis H_busy_interval_exists: busy_intervals_are_bounded_by interference interfering_workload L.
Variable task_interference_bound_function: Task → time → time → time.
Hypothesis H_task_interference_is_bounded: task_interference_is_bounded_by task_interference_bound_function.
Let total_interference_bound tsk A Δ :=
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A Δ.
Let is_in_search_space_seq := is_in_search_space tsk L total_interference_bound.
Variable R: nat.
Hypothesis H_R_is_maximum_seq:
∀ A,
is_in_search_space_seq A →
∃ F,
A + F = (task_rbf (A + ε) - (task_cost tsk - task_lock_in_service tsk))
+ task_interference_bound_function tsk A (A + F) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
Section CompletionOfJobsFromSameTask.
Variable j1 j2: Job.
Hypothesis H_j1_arrives: arrives_in arr_seq j1.
Hypothesis H_j2_arrives: arrives_in arr_seq j2.
Hypothesis H_j1_from_tsk: job_task j1 = tsk.
Hypothesis H_j2_from_tsk: job_task j2 = tsk.
Hypothesis H_j1_cost_positive: job_cost_positive job_cost j1.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval j1 t1 t2.
Lemma completed_before_beginning_of_busy_interval:
job_arrival j2 < t1 →
completed_by job_cost sched j2 t1.
Lemma arrives_after_beginning_of_busy_interval:
∀ t,
t1 ≤ t →
job_pending_at j2 t →
arrived_between job_arrival j2 t1 t.+1.
End CompletionOfJobsFromSameTask.
Section BoundOfCumulativeJobInterference.
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 x: time.
Hypothesis H_inside_busy_interval: t1 + x < t2.
Hypothesis H_job_j_is_not_completed: ~~ job_completed_by j (t1 + x).
Lemma bound_for_cumulative_job_interference_actual:
cumul_interference j t1 (t1 + x) ≤
(task_workload_between t1 (t1 + A + ε) - job_cost j) + cumul_task_interference t2 t1 (t1 + x).
Lemma task_rbf_excl_tsk_bounds_task_workload_excl_j:
task_workload_between t1 (t1 + A + ε) - job_cost j ≤ task_rbf (A + ε) - task_cost tsk.
Lemma bound_for_cumulative_job_interference:
cumul_interference j t1 (t1 + x)
≤ (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference t2 t1 (t1 + x).
End BoundOfCumulativeJobInterference.
Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
Let is_in_search_space A :=
is_in_search_space tsk L total_interference_bound A.
Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
∀ A,
is_in_search_space A →
∃ F,
A + F = task_lock_in_service tsk +
(task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A (A + F)) ∧
F + (task_cost tsk - task_lock_in_service tsk) ≤ R.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
Theorem uniprocessor_response_time_bound_seq:
response_time_bounded_by tsk R.
End ResponseTimeBound.
End Sequential_Abstract_RTA.
End AbstractSeqRTA.