diff --git a/results/rs/edf/floating_nonpreemptive.v b/results/rs/edf/floating_nonpreemptive.v
new file mode 100644
index 0000000000000000000000000000000000000000..997bd1cdeb9591b9feca9a36200639508807a21f
--- /dev/null
+++ b/results/rs/edf/floating_nonpreemptive.v
@@ -0,0 +1,225 @@
+Require Import prosa.analysis.facts.readiness.basic.
+Require Export prosa.analysis.facts.model.restricted_supply.schedule.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
+Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.edf.
+Require Export prosa.analysis.abstract.restricted_supply.search_space.edf.
+Require Export prosa.analysis.facts.model.task_cost.
+Require Export prosa.analysis.facts.priority.edf.
+Require Export prosa.analysis.facts.blocking_bound.edf.
+Require Export prosa.analysis.facts.workload.edf_athep_bound.
+Require Export prosa.analysis.definitions.sbf.busy.
+
+(** * RTA for EDF Scheduling with Floating Non-Preemptive Regions on Restricted-Supply Uniprocessors *)
+
+(** In the following, we derive a response-time analysis for EDF
+ 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 sequential variant of _abstract Restricted-Supply
+ Response-Time Analysis_ (aRSA) as provided in the
+ [prosa.analysis.abstract.restricted_supply] module. *)
+Section RTAforFloatingEDFModelwithArrivalCurves.
+
+ (** ** Defining the System Model *)
+
+ (** Before any formal claims can be stated, an initial setup is
+ needed to define the system model under consideration. To this
+ end, we next introduce and define the following notions using
+ Prosa's standard definitions and behavioral semantics:
+
+ - processor model,
+ - 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,
+ - an arbitrary schedule of the task set, and finally,
+ - a supply-bound function. *)
+
+ (** *** Processor Model *)
+
+ (** Consider a restricted-supply uniprocessor model. *)
+ #[local] Existing Instance rs_processor_state.
+
+ (** *** Tasks and Jobs *)
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost], relative deadline [task_deadline], an arrival curve
+ [max_arrivals], and a bound on the the task's longest
+ non-preemptive segment [task_max_nonpreemptive_segment], ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+ Context `{MaxArrivals Task}.
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** ... and any type of jobs associated with these tasks, where each
+ job has a task [job_task], a cost [job_cost], and an arrival
+ time [job_arrival], and a predicate indicating job's preemption
+ points [job_preemptive_points]. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+ Context `{JobArrival Job}.
+ Context `{JobPreemptionPoints Job}.
+
+ (** We assume that jobs are limited-preemptive. *)
+ #[local] Existing Instance limited_preemptive_job_model.
+
+ (** *** The Job Arrival Sequence *)
+
+ (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** *** Absence of Self-Suspensions and WCET Compliance *)
+
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
+ (** We further require that a job's cost cannot exceed its task's stated WCET. *)
+ Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+ (** *** The Task Set *)
+
+ (** We consider an arbitrary task set [ts] ... *)
+ Variable ts : seq Task.
+
+ (** ... and assume that all jobs stem from tasks in this task set. *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** Assume a model with floating non-preemptive regions. I.e., for
+ each task only the length of the maximal non-preemptive segment
+ is known and each job level is divided into a number of
+ non-preemptive segments by inserting preemption points. *)
+ Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions :
+ valid_model_with_floating_nonpreemptive_regions arr_seq.
+
+ (** We assume that [max_arrivals] is a family of valid arrival
+ curves that constrains the arrival sequence [arr_seq], i.e., for
+ any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+ bound of [tsk], and ... *)
+ Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+ (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
+ Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+ (** *** The Task Under Analysis *)
+
+ (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** *** The Schedule *)
+
+ (** Consider any arbitrary, work-conserving, valid restricted-supply
+ uni-processor schedule with limited preemptions of the given
+ arrival sequence [arr_seq] (and hence the given task set [ts]). *)
+ Variable sched : schedule (rs_processor_state Job).
+ Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
+ Hypothesis H_work_conserving : work_conserving arr_seq sched.
+ Hypothesis H_schedule_with_limited_preemptions :
+ schedule_respects_preemption_model arr_seq sched.
+
+ (** Assume that the schedule respects the EDF policy. *)
+ Hypothesis H_respects_policy :
+ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
+
+ (** *** 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
+ (w.r.t. task [tsk]) 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 tsk SBF.
+
+ (** ** Workload Abbreviation *)
+
+ (** Let's denote the relative deadline of a task as [D]. *)
+ Let D tsk := task_deadline tsk.
+
+ (** We introduce [task_rbf] as an abbreviation
+ for the task request bound function of task [tsk]. *)
+ Let task_rbf := task_request_bound_function tsk.
+
+ (** ** Length of Busy Interval *)
+
+ (** The next step is to establish a bound on the maximum busy-window
+ length, which aRSA requires to be given. *)
+
+ (** To this end, let [L] be any positive constant such that ... *)
+ Variable L : duration.
+ Hypothesis H_L_positive : 0 < L.
+
+ (** ... [L] satisfies a fixed-point recurrence for the
+ busy-interval-length bound (i.e., [total_RBF ts L <= SBF L] ... *)
+ Hypothesis H_fixed_point : total_request_bound_function ts L <= SBF L.
+
+ (** ... and [SBF L] bounds [longest_busy_interval_with_pi ts tsk]. *)
+ Hypothesis H_L_bounds_bi_with_pi :
+ longest_busy_interval_with_pi ts tsk <= SBF L.
+
+ (** ** Response-Time Bound *)
+
+ (** Having established all necessary preliminaries, it is finally
+ time to state the claimed response-time bound [R].
+
+ 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]. *)
+ Definition rta_recurrence_solution R :=
+ forall (A : duration),
+ is_in_search_space ts tsk L A ->
+ exists (F : duration),
+ A <= F <= A + R
+ /\ blocking_bound ts tsk A + task_rbf (A + ε) + bound_on_athep_workload ts tsk A F <= SBF F.
+
+ (** Finally, using the sequential variant of abstract
+ restricted-supply analysis, we establish that any such [R] is a
+ sound response-time bound for the concrete model of EDF
+ scheduling with floating non-preemptive regions with arbitrary
+ supply restrictions. *)
+ Theorem uniprocessor_response_time_bound_floating_edf :
+ forall (R : duration),
+ rta_recurrence_solution R ->
+ task_response_time_bound arr_seq sched tsk R.
+ Proof.
+ move=> R SOL js ARRs TSKs.
+ have VAL1 : valid_preemption_model arr_seq sched.
+ { apply valid_fixed_preemption_points_model_lemma => //.
+ by apply H_valid_task_model_with_floating_nonpreemptive_regions. }
+ 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.
+ eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) => //.
+ - exact: instantiated_i_and_w_are_coherent_with_schedule.
+ - exact: EDF_implies_sequential_tasks.
+ - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
+ - apply: busy_intervals_are_bounded_rs_edf => //.
+ - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
+ move => ? ? ? ? [? ?]; split => //.
+ by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+ - apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
+ + by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
+ + apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
+ by apply: nonpreemptive_segments_bounded_by_blocking => //.
+ - move=> A SP.
+ move: (SOL A) => [].
+ { by apply: search_space_sub => //; apply: search_space_switch_IBF. }
+ move=> FF [EQ1 EQ2].
+ exists FF; split; last split.
+ + lia.
+ + by move: EQ2; rewrite /task_intra_IBF -/task_rbf; lia.
+ + by rewrite subnn addn0; apply H_SBF_monotone; lia.
+ Qed.
+
+End RTAforFloatingEDFModelwithArrivalCurves.
diff --git a/results/rs/edf/fully_nonpreemptive.v b/results/rs/edf/fully_nonpreemptive.v
index 5aed50b6a9639cec140ed242f19b533da4762744..15560d9a79d5f8b6a7217b7dfe84eed9e77e6e9f 100644
--- a/results/rs/edf/fully_nonpreemptive.v
+++ b/results/rs/edf/fully_nonpreemptive.v
@@ -17,7 +17,7 @@ Require Export prosa.analysis.definitions.sbf.busy.
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 RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
@@ -34,20 +34,15 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
- 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 lower-bounded 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
@@ -112,28 +107,35 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
(** *** The Schedule *)
- (** Finally, consider any non-preemptive, work-conserving, valid
+ (** Consider any non-preemptive, work-conserving, valid
restricted-supply uni-processor schedule of the given arrival
- sequence [arr_seq] (and hence the given task set [ts]) ... *)
+ sequence [arr_seq] (and hence the given task set [ts]). *)
Variable sched : schedule (rs_processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
- (** ... and assume that the schedule respects the EDF policy. *)
+ (** Assume that the schedule respects the EDF policy. *)
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
- (** Last but not least, we assume that [SBF] properly characterizes
- all busy intervals (w.r.t. task [tsk]) 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
+ (w.r.t. task [tsk]) 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 tsk SBF.
(** ** Workload Abbreviation *)
- (** For brevity, let's denote the relative deadline of a task as [D]. *)
+ (** Let's denote the relative deadline of a task as [D]. *)
Let D tsk := task_deadline tsk.
(** We introduce [task_rbf] as an abbreviation
@@ -157,7 +159,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Hypothesis H_L_bounds_bi_with_pi :
longest_busy_interval_with_pi ts tsk <= SBF L.
-
(** ** Response-Time Bound *)
(** Having established all necessary preliminaries, it is finally
@@ -166,8 +167,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
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 ts tsk L A ->
exists (F : duration),
@@ -184,9 +184,11 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
fully-nonpreemptive EDF scheduling with arbitrary supply
restrictions. *)
Theorem uniprocessor_response_time_bound_fully_nonpreemptive_edf :
- 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 [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 VPR : valid_preemption_model arr_seq sched by exact: valid_fully_nonpreemptive_model => //.
@@ -202,7 +204,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
+ by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
+ apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
by apply: nonpreemptive_segments_bounded_by_blocking => //.
- - move => A SP; move: (H_R_is_maximum A) => [].
+ - move => A SP; move: (SOL A) => [].
+ by apply: search_space_sub => //.
+ move => F [/andP [_ LE] [FIX1 FIX2]]; exists F; split => //.
rewrite /task_intra_IBF /task_rtct /fully_nonpreemptive_rtc_threshold /constant.
diff --git a/results/rs/edf/fully_preemptive.v b/results/rs/edf/fully_preemptive.v
index 7a865caf37f023d33ce2d40b610246dc0d2c41c2..e6ee0ffedd298561141d787f768ee5a974a5aadc 100644
--- a/results/rs/edf/fully_preemptive.v
+++ b/results/rs/edf/fully_preemptive.v
@@ -17,7 +17,7 @@ Require Export prosa.analysis.facts.workload.edf_athep_bound.
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 RTAforFullyPreemptiveEDFModelwithArrivalCurves.
@@ -34,20 +34,15 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
- 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 lower-bounded 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
@@ -112,27 +107,34 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
(** *** The Schedule *)
- (** Finally, 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]) ... *)
+ (** 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).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
- (** ... and assume that the schedule respects the EDF policy. *)
+ (** Assume that the schedule respects the EDF policy. *)
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
- (** Last but not least, we assume that [SBF] properly characterizes
- all busy intervals (w.r.t. task [tsk]) 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
+ (w.r.t. task [tsk]) 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 tsk SBF.
(** ** Workload Abbreviation *)
- (** For brevity, let's denote the relative deadline of a task as [D]. *)
+ (** Let's denote the relative deadline of a task as [D]. *)
Let D tsk := task_deadline tsk.
(** ** Length of Busy Interval *)
@@ -157,8 +159,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
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 ts tsk L A ->
exists (F : duration),
@@ -171,9 +172,11 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
fully-preemptive EDF scheduling with arbitrary supply
restrictions. *)
Theorem uniprocessor_response_time_bound_fully_preemptive_edf :
- 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 [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.
@@ -196,7 +199,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
+ apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
by apply: nonpreemptive_segments_bounded_by_blocking => //.
- move => A SP.
- move: (H_R_is_maximum A) => [].
+ move: (SOL A) => [].
+ by apply: search_space_sub => //.
+ move => F [/andP [_ LE] FIX]; exists F; split => //.
rewrite /task_intra_IBF /task_rtct /fully_preemptive_rtc_threshold.
diff --git a/results/rs/edf/limited_preemptive.v b/results/rs/edf/limited_preemptive.v
new file mode 100644
index 0000000000000000000000000000000000000000..2d5bbbf9a46a417fa106fd1ac75bccca9b803edb
--- /dev/null
+++ b/results/rs/edf/limited_preemptive.v
@@ -0,0 +1,228 @@
+Require Import prosa.analysis.facts.readiness.basic.
+Require Export prosa.analysis.facts.model.restricted_supply.schedule.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
+Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
+Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.edf.
+Require Export prosa.analysis.abstract.restricted_supply.search_space.edf.
+Require Export prosa.analysis.facts.model.task_cost.
+Require Export prosa.analysis.facts.priority.edf.
+Require Export prosa.analysis.facts.blocking_bound.edf.
+Require Export prosa.analysis.facts.workload.edf_athep_bound.
+Require Export prosa.analysis.definitions.sbf.busy.
+
+(** * RTA for EDF Scheduling with Fixed Preemption Points on Restricted-Supply Uniprocessors *)
+
+(** In the following, we derive a response-time analysis for EDF
+ 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 sequential variant of _abstract Restricted-Supply
+ Response-Time Analysis_ (aRSA) as provided in the
+ [prosa.analysis.abstract.restricted_supply] module. *)
+Section RTAforLimitedPreemptiveEDFModelwithArrivalCurves.
+
+ (** ** Defining the System Model *)
+
+ (** Before any formal claims can be stated, an initial setup is
+ needed to define the system model under consideration. To this
+ end, we next introduce and define the following notions using
+ Prosa's standard definitions and behavioral semantics:
+
+ - processor model,
+ - 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,
+ - an arbitrary schedule of the task set, and finally,
+ - a supply-bound function. *)
+
+ (** *** Processor Model *)
+
+ (** Consider a restricted-supply uniprocessor model. *)
+ #[local] Existing Instance rs_processor_state.
+
+ (** *** Tasks and Jobs *)
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost], relative deadline [task_deadline], an arrival curve
+ [max_arrivals], and a predicate indicating task's preemption
+ points [task_preemption_points], ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+ Context `{MaxArrivals Task}.
+ Context `{TaskPreemptionPoints Task}.
+
+ (** ... and any type of jobs associated with these tasks, where each
+ job has a task [job_task], a cost [job_cost], an arrival time
+ [job_arrival], and a predicate indicating job's preemption
+ points [job_preemptive_points]. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+ Context `{JobArrival Job}.
+ Context `{JobPreemptionPoints Job}.
+
+ (** We assume that jobs are limited-preemptive. *)
+ #[local] Existing Instance limited_preemptive_job_model.
+
+ (** *** The Job Arrival Sequence *)
+
+ (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** *** Absence of Self-Suspensions and WCET Compliance *)
+
+ (** We assume the classic (i.e., Liu & Layland) model of readiness
+ without jitter or self-suspensions, wherein pending jobs are
+ always ready. *)
+ #[local] Existing Instance basic_ready_instance.
+
+ (** We further require that a job's cost cannot exceed its task's stated WCET. *)
+ Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+ (** *** The Task Set *)
+
+ (** We consider an arbitrary task set [ts] ... *)
+ Variable ts : seq Task.
+
+ (** ... and assume that all jobs stem from tasks in this task set. *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** We assume a model with fixed preemption points. I.e., each task
+ is divided into a number of non-preemptive segments by inserting
+ statically predefined preemption points. *)
+ Hypothesis H_valid_model_with_fixed_preemption_points :
+ valid_fixed_preemption_points_model arr_seq ts.
+
+ (** We assume that [max_arrivals] is a family of valid arrival
+ curves that constrains the arrival sequence [arr_seq], i.e., for
+ any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+ bound of [tsk], and ... *)
+ Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+ (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
+ Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+ (** *** The Task Under Analysis *)
+
+ (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** *** The Schedule *)
+
+ (** Consider any arbitrary, work-conserving, valid restricted-supply
+ uni-processor schedule with limited preemptions of the given
+ arrival sequence [arr_seq] (and hence the given task set [ts]). *)
+ Variable sched : schedule (rs_processor_state Job).
+ Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
+ Hypothesis H_work_conserving : work_conserving arr_seq sched.
+ Hypothesis H_schedule_with_limited_preemptions:
+ schedule_respects_preemption_model arr_seq sched.
+
+ (** Assume that the schedule respects the EDF policy. *)
+ Hypothesis H_respects_policy :
+ respects_JLFP_policy_at_preemption_point arr_seq sched (EDF Job).
+
+ (** *** 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
+ (w.r.t. task [tsk]) 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 tsk SBF.
+
+ (** ** Workload Abbreviation *)
+
+ (** Let's denote the relative deadline of a task as [D]. *)
+ Let D tsk := task_deadline tsk.
+
+ (** We introduce [task_rbf] as an abbreviation
+ for the task request bound function of task [tsk]. *)
+ Let task_rbf := task_request_bound_function tsk.
+
+ (** ** Length of Busy Interval *)
+
+ (** The next step is to establish a bound on the maximum busy-window
+ length, which aRSA requires to be given. *)
+
+ (** To this end, let [L] be any positive constant such that ... *)
+ Variable L : duration.
+ Hypothesis H_L_positive : 0 < L.
+
+ (** ... [L] satisfies a fixed-point recurrence for the
+ busy-interval-length bound (i.e., [total_RBF ts L <= SBF L] ... *)
+ Hypothesis H_fixed_point : total_request_bound_function ts L <= SBF L.
+
+ (** ... and [SBF L] bounds [longest_busy_interval_with_pi ts tsk]. *)
+ Hypothesis H_L_bounds_bi_with_pi :
+ longest_busy_interval_with_pi ts tsk <= SBF L.
+
+ (** ** Response-Time Bound *)
+
+ (** Having established all necessary preliminaries, it is finally
+ time to state the claimed response-time bound [R].
+
+ 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]. *)
+ Definition rta_recurrence_solution R :=
+ forall (A : duration),
+ is_in_search_space ts tsk L A ->
+ exists (F : duration),
+ A <= F <= A + R
+ /\ blocking_bound ts tsk A
+ + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε))
+ + bound_on_athep_workload ts tsk A F
+ <= SBF F
+ /\ SBF F + (task_last_nonpr_segment tsk - ε) <= SBF (A + R).
+
+ (** Finally, using the sequential variant of abstract
+ restricted-supply analysis, we establish that any such [R] is a
+ sound response-time bound for the concrete model of EDF
+ scheduling with limited preemptions with arbitrary supply
+ restrictions. *)
+ Theorem uniprocessor_response_time_bound_limited_edf :
+ forall (R : duration),
+ rta_recurrence_solution R ->
+ task_response_time_bound arr_seq sched tsk R.
+ Proof.
+ move=> R SOL js ARRs TSKs.
+ have [ZERO|POS] := posnP (job_cost js); first by rewrite /job_response_time_bound /completed_by ZERO.
+ have VAL1 : valid_preemption_model arr_seq sched.
+ { apply valid_fixed_preemption_points_model_lemma => //.
+ by apply H_valid_model_with_fixed_preemption_points. }
+ have READ : work_bearing_readiness arr_seq sched by done.
+ eapply uniprocessor_response_time_bound_restricted_supply_seq with (L := L) => //.
+ - exact: instantiated_i_and_w_are_coherent_with_schedule.
+ - exact: EDF_implies_sequential_tasks.
+ - exact: instantiated_interference_and_workload_consistent_with_sequential_tasks.
+ - apply: busy_intervals_are_bounded_rs_edf => //.
+ - apply: valid_pred_sbf_switch_predicate; last by exact: H_valid_SBF.
+ move => ? ? ? ? [? ?]; split => //.
+ by apply instantiated_busy_interval_prefix_equivalent_busy_interval_prefix.
+ - apply: instantiated_task_intra_interference_is_bounded; eauto 1 => //; first last.
+ + by (apply: bound_on_athep_workload_is_valid; try apply H_fixed_point) => //.
+ + apply: service_inversion_is_bounded => // => jo t1 t2 ARRo TSKo BUSYo.
+ by apply: nonpreemptive_segments_bounded_by_blocking => //.
+ - move=> A SP.
+ move: (SOL A) => [].
+ { by apply: search_space_sub => //; apply: search_space_switch_IBF. }
+ move=> FF [EQ1 [EQ2 EQ3]].
+ exists FF; split; last split.
+ + lia.
+ + move: EQ2; rewrite /task_intra_IBF -/task_rbf.
+ by erewrite last_segment_eq_cost_minus_rtct => //; lia.
+ + by erewrite last_segment_eq_cost_minus_rtct.
+ Qed.
+
+End RTAforLimitedPreemptiveEDFModelwithArrivalCurves.