Commit 4e450bb1 authored by Sergey Bozhko's avatar Sergey Bozhko

Delete redundant busy_interval file

parent e7d7823f
......@@ -4,7 +4,7 @@ Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.p
Require Import rt.model.schedule.uni.schedule_of_task rt.model.schedule.uni.workload
rt.model.schedule.uni.schedulability rt.model.schedule.uni.response_time
rt.model.schedule.uni.service.
Require Import rt.model.schedule.uni.basic.busy_interval rt.model.schedule.uni.basic.platform.
Require Import rt.model.schedule.uni.limited.busy_interval rt.model.schedule.uni.basic.platform.
Require Import rt.analysis.uni.basic.workload_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......@@ -12,7 +12,7 @@ Module ResponseTimeAnalysisFP.
Import Job ScheduleOfTask SporadicTaskset Priority ResponseTime
TaskArrival ArrivalBounds WorkloadBoundFP Platform Schedulability
BusyInterval Workload Service.
BusyIntervalJLFP Workload Service.
(* In this section, we prove that any fixed point in the RTA for uniprocessor
FP scheduling is a response-time bound. *)
......@@ -98,15 +98,45 @@ Module ResponseTimeAnalysisFP.
Proof.
rename H_response_time_is_fixed_point into FIX.
intros j ARRj JOBtsk.
move: (posnP (job_cost j)) => [Z|POS].
{ rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
- by apply H_completed_jobs_dont_execute.
- by rewrite Z.
}
set prio := FP_to_JLFP job_task higher_eq_priority.
apply busy_interval_bounds_response_time with (arr_seq0 := arr_seq)
(higher_eq_priority0 := prio); try (by done).
- by intros x; apply H_priority_is_reflexive.
- by intros x z y; apply H_priority_is_transitive.
apply fp_workload_bound_holds with (job_arrival0 := job_arrival) (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(job_deadline0 := job_deadline) (ts0 := ts); try (by done).
by rewrite JOBtsk.
apply busy_interval_bounds_response_time with
(arr_seq0 := arr_seq)
(higher_eq_priority0 := prio)
(priority_inversion_bound := 0); try by done.
- by intros x; apply H_priority_is_reflexive.
{ intros t1 t2 BUSY.
rewrite /cumulative_priority_inversion /is_priority_inversion leqn0.
rewrite big_nat big1 //; move => t NEQ.
destruct (sched t) eqn:SCHED; last by done.
have HP := pending_hp_job_exists
job_arrival job_cost arr_seq _ sched
prio _ ARRj _ _ _ _ _ _ BUSY _ NEQ.
feed_n 5 HP; try done.
{ by intros x; apply H_priority_is_reflexive. }
move: HP => [jhp [ARRjhp [PEND PRIO]]].
apply/eqP; rewrite eqb0 Bool.negb_involutive.
rewrite /prio /FP_to_JLFP.
eapply H_priority_is_transitive with (job_task jhp); last by done.
destruct (s == jhp) eqn:EQ; first by move: EQ => /eqP EQ; subst s.
apply H_respects_fp_policy with t; try done.
{ apply/andP; split; first by done.
rewrite /scheduled_at SCHED.
apply/negP. intros SNEQ; move: SNEQ => /eqP SNEQ.
move: EQ => /negP EQ; apply EQ.
by inversion SNEQ.
}
{ by rewrite /scheduled_at SCHED. }
}
apply fp_workload_bound_holds with
(job_arrival0 := job_arrival) (task_cost0 := task_cost)
(task_period0 := task_period) (task_deadline0 := task_deadline)
(job_deadline0 := job_deadline) (ts0 := ts); try (by done).
by rewrite JOBtsk.
Qed.
End ResponseTimeBound.
......
Require Import rt.util.all.
Require Import rt.model.arrival.basic.arrival_sequence rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.task_arrival
rt.model.priority.
Require Import rt.model.schedule.uni.basic.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path div.
(* Properties of job arrival. *)
Module ArrivalBounds.
Import ArrivalSequence SporadicTaskset TaskArrival Priority BusyInterval.
Import ArrivalSequence SporadicTaskset TaskArrival Priority.
Section Lemmas.
......
This diff is collapsed.
......@@ -970,6 +970,44 @@ Module BusyIntervalJLFP.
Qed.
End BusyIntervalFromWorkloadBound.
(* If we know that the workload is bounded, we can also use the
busy interval to infer a response-time bound. *)
Section ResponseTimeBoundFromBusyInterval.
(* Let priority_inversion_bound be a constant that bounds the length of a priority inversion. *)
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
(* Assume that for some positive delta, the sum of requested workload at
time (t1 + delta) and priority inversion is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
forall t, priority_inversion_bound + hp_workload t (t + delta) <= delta.
(* Then, job j must complete by (job_arrival j + delta). *)
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
Proof.
have BUSY := exists_busy_interval priority_inversion_bound _ delta.
destruct (job_cost j == 0) eqn:COST.
{ move: COST => /eqP COST.
rewrite /job_completed_by /completed_by eqn_leq.
apply/andP; split;
first by apply cumulative_service_le_job_cost.
by rewrite COST.
}
apply negbT in COST; rewrite -lt0n in COST.
feed_n 4 BUSY; try by done.
move: BUSY => [t1 [t2 [/andP [GE1 LT2] [GE2 BUSY]]]].
apply completion_monotonic with (t := t2); try (by done);
first by apply leq_trans with (n := t1 + delta); [| by rewrite leq_add2r].
apply job_completes_within_busy_interval with (t1 := t1); try by done.
Qed.
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment