diff --git a/results/rs/edf/fully_nonpreemptive.v b/results/rs/edf/fully_nonpreemptive.v
index ac69e0d1f522deb164a2c92db368522ff325c3fd..165f9b43f99b925134d381a0fb0f053f13669c8b 100644
--- a/results/rs/edf/fully_nonpreemptive.v
+++ b/results/rs/edf/fully_nonpreemptive.v
@@ -188,7 +188,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
move=> js ARRs TSKs.
have [ZERO|POS] := posnP (job_cost js); first by rewrite /job_response_time_bound /completed_by ZERO.
have READ : work_bearing_readiness arr_seq sched by done.
- have UNIT: unit_service_proc_model (rs_processor_state Job) by exact: unit_supply_is_unit_service.
have VPR : valid_preemption_model arr_seq sched by exact: valid_fully_nonpreemptive_model => //.
eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) => //.
- exact: instantiated_i_and_w_are_coherent_with_schedule.
diff --git a/results/rs/fifo/bounded_nps.v b/results/rs/fifo/bounded_nps.v
index ee9b32e3a8b399ceb8e9a2de5f8e6d71b0fdd704..4f3bc630182a7dd558beb782eb5f6172380d8531 100644
--- a/results/rs/fifo/bounded_nps.v
+++ b/results/rs/fifo/bounded_nps.v
@@ -30,9 +30,9 @@ Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
- tasks, jobs, and their parameters,
- the sequence of job arrivals,
- worst-case execution time (WCET) and the absence of self-suspensions,
- - the task under analysis, and, finally,
- - an arbitrary schedule of the task set,
- - and a supply-bound function. *)
+ - the task under analysis,
+ - an arbitrary schedule of the task set, and finally,
+ - a supply-bound function. *)
(** *** Processor Model *)
diff --git a/results/rs/fp/fully_preemptive.v b/results/rs/fp/fully_preemptive.v
index 959a674496ba624f3e0684e16cdb972f9df3b2b0..4fe4e02cde4146e1c8e981c5a763cb69109db8a8 100644
--- a/results/rs/fp/fully_preemptive.v
+++ b/results/rs/fp/fully_preemptive.v
@@ -13,7 +13,7 @@ Require Export prosa.analysis.facts.model.task_cost.
schedulers, assuming a workload of sporadic real-time tasks
characterized by arbitrary arrival curves executing upon a
uniprocessor with arbitrary supply restrictions. To this end, we
- instantiate the _abstract Sequential Restricted-Supply
+ instantiate the sequential variant of _abstract Restricted-Supply
Response-Time Analysis_ (aRSA) as provided in the
[prosa.analysis.abstract.restricted_supply] module. *)
Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
@@ -29,21 +29,15 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
- tasks, jobs, and their parameters,
- the sequence of job arrivals,
- worst-case execution time (WCET) and the absence of self-suspensions,
- - the set of tasks under analysis,
- - the task under analysis, and, finally,
- - an arbitrary schedule of the task set. *)
+ - the task under analysis,
+ - an arbitrary schedule of the task set, and finally,
+ - a supply-bound function. *)
(** *** Processor Model *)
- (** Consider a restricted-supply uniprocessor model, ... *)
+ (** Consider a restricted-supply uniprocessor model. *)
#[local] Existing Instance rs_processor_state.
- (** ... where the minimum amount of supply is defined via a monotone
- unit-supply-bound function [SBF]. *)
- Context {SBF : SupplyBoundFunction}.
- Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
- Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
-
(** *** Tasks and Jobs *)
(** Consider any type of tasks, each characterized by a WCET
@@ -107,7 +101,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** *** The Schedule *)
- (** Finally, consider any arbitrary, work-conserving, valid
+ (** Consider any arbitrary, work-conserving, valid
restricted-supply uni-processor schedule of the given arrival
sequence [arr_seq] (and hence the given task set [ts]). *)
Variable sched : schedule (rs_processor_state Job).
@@ -121,15 +115,22 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
Hypothesis H_priority_is_reflexive : reflexive_task_priorities FP.
Hypothesis H_priority_is_transitive : transitive_task_priorities FP.
- (** We assume that the schedule respects the
- [FP] scheduling policy. *)
+ (** We assume that the schedule respects the [FP] scheduling policy. *)
Hypothesis H_respects_policy_at_preemption_point :
respects_FP_policy_at_preemption_point arr_seq sched FP.
- (** Last but not least, we assume that [SBF] properly characterizes
- all busy intervals in [sched]. That is, (1) [SBF 0 = 0] and (2)
- for any duration [Δ], at least [SBF Δ] supply is available in
- any busy-interval prefix of length [Δ]. *)
+ (** *** Supply-Bound Function *)
+
+ (** Assume the minimum amount of supply that any job of task [tsk]
+ receives is defined by a monotone unit-supply-bound function [SBF]. *)
+ Context {SBF : SupplyBoundFunction}.
+ Hypothesis H_SBF_monotone : sbf_is_monotone SBF.
+ Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+ (** We assume that [SBF] properly characterizes all busy intervals
+ in [sched]. That is, (1) [SBF 0 = 0] and (2) for any duration
+ [Δ], at least [SBF Δ] supply is available in any busy-interval
+ prefix of length [Δ]. *)
Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched SBF.
(** ** Workload Abbreviation *)
@@ -152,13 +153,13 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** ** Length of Busy Interval *)
(** The next step is to establish a bound on the maximum busy-window
- length, which aRTA requires to be given. *)
+ length, which aRSA requires to be given. *)
(** To this end, let [L] be any positive fixed point of the
- busy-interval recurrence. As the
- [busy_intervals_are_bounded_rs_fp] lemma shows, under [FP]
- scheduling, this is sufficient to guarantee that all busy
- intervals are bounded by [L]. *)
+ busy-interval recurrence. As the lemma
+ [busy_intervals_are_bounded_rs_fp] shows, under [FP] scheduling,
+ this is sufficient to guarantee that all busy intervals are
+ bounded by [L]. *)
Variable L : duration.
Hypothesis H_L_positive : 0 < L.
Hypothesis H_fixed_point : total_hep_rbf L <= SBF L.
@@ -166,13 +167,12 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
(** ** Response-Time Bound *)
(** Having established all necessary preliminaries, it is finally
- time to state the claimed response-time bound [R].
+ time to state the claimed response-time bound [R]. *)
- A value [R] is a response-time bound if, for any given offset
+ (** A value [R] is a response-time bound if, for any given offset
[A] in the search space, the response-time bound recurrence has
a solution [F] not exceeding [R]. *)
- Variable R : duration.
- Hypothesis H_R_is_maximum :
+ Definition rta_recurrence_solution R :=
forall (A : duration),
is_in_search_space tsk L A ->
exists (F : duration),
@@ -185,9 +185,11 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
fully-preemptive fixed-priority scheduling with arbitrary supply
restrictions. *)
Theorem uniprocessor_response_time_bound_fully_preemptive_fp :
- task_response_time_bound arr_seq sched tsk R.
+ forall (R : duration),
+ rta_recurrence_solution R ->
+ task_response_time_bound arr_seq sched tsk R.
Proof.
- move=> js ARRs TSKs.
+ move=> R SOL js ARRs TSKs.
have BLOCK: forall tsk , blocking_bound ts tsk = 0.
{ by move=> tsk2; rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
/fully_preemptive_task_model subnn big1_eq. }
@@ -206,7 +208,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
+ by apply athep_workload_le_total_ohep_rbf.
+ apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
by unshelve rewrite (leqRW (nonpreemptive_segments_bounded_by_blocking _ _ _ _ _ _ _ _ _)) => //.
- - move => A SP; move: (H_R_is_maximum A) => [].
+ - move => A SP; move: (SOL A) => [].
+ apply: search_space_sub => //; apply: search_space_switch_IBF; last by exact: SP.
by move=> A1 Δ1; rewrite //= BLOCK.
+ move => F [/andP [_ LE] FIX]; exists F; split => //.