# Library prosa.analysis.abstract.restricted_supply.search_space.fifo_fixpoint

Require Export prosa.model.priority.fifo.

Require Export prosa.model.task.preemption.parameters.

Require Export prosa.analysis.definitions.sbf.busy.

Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo.

Require Export prosa.model.task.preemption.parameters.

Require Export prosa.analysis.definitions.sbf.busy.

Require Export prosa.analysis.abstract.restricted_supply.search_space.fifo.

# Concrete to Abstract Fixpoint Reduction

Consider any type of tasks, each characterized by a WCET
task_cost, an arrival curve max_arrivals, a
run-to-completion threshold task_rtct, and a bound on the
task's maximum non-preemptive segment
task_max_nonpreemptive_segment ...

Context {Task : TaskType}.

Context `{TaskCost Task}.

Context `{MaxArrivals Task}.

Context `{TaskRunToCompletionThreshold Task}.

Context `{TaskMaxNonpreemptiveSegment Task}.

Context `{TaskCost Task}.

Context `{MaxArrivals Task}.

Context `{TaskRunToCompletionThreshold 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, an arrival time
job_arrival, and a predicate indicating when the job is
preemptable job_preemptable.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobCost Job}.

Context `{JobArrival Job}.

Context `{JobPreemptable Job}.

Context `{JobTask Job Task}.

Context `{JobCost Job}.

Context `{JobArrival Job}.

Context `{JobPreemptable Job}.

Consider any processor model ...

... 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.

Hypothesis H_SBF_monotone : sbf_is_monotone SBF.

Hypothesis H_unit_SBF : unit_supply_bound_function SBF.

We consider an arbitrary task set ts.

Consider any arrival sequence ...

... and assume that max_arrivals defines a valid arrival curve
for each task.

Consider any schedule.

Next, 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 Δ.

We assume that tsk is described by a valid task
run-to-completion threshold

Hypothesis H_valid_run_to_completion_threshold :

valid_task_run_to_completion_threshold arr_seq tsk.

valid_task_run_to_completion_threshold arr_seq tsk.

Let L be an arbitrary positive constant. Typically, L
denotes an upper bound on the length of a busy interval of a job
of tsk. In this file, however, L can be any positive
constant.

To rule out pathological cases with the search space, we assume
that the task cost is positive and the arrival curve is
non-pathological.

Hypothesis H_task_cost_pos : 0 < task_cost tsk.

Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.

Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.

For brevity, we define the intra-supply interference bound
function (intra_IBF). Note that in the case of FIFO,
intra-supply IBF does not depend on the second argument.

Local Definition intra_IBF (A _Δ : duration) :=

total_request_bound_function ts (A + ε) - task_cost tsk.

total_request_bound_function ts (A + ε) - task_cost tsk.

Ultimately, we seek to apply aRSA to prove the correctness of
the following R.

Variable R : duration.

Hypothesis H_R_is_maximum :

∀ (A : duration),

is_in_search_space ts L A →

∃ (F : duration),

A ≤ F ≤ A + R

∧ total_request_bound_function ts (A + ε) ≤ SBF F.

Hypothesis H_R_is_maximum :

∀ (A : duration),

is_in_search_space ts L A →

∃ (F : duration),

A ≤ F ≤ A + R

∧ total_request_bound_function ts (A + ε) ≤ SBF F.

However, in order to connect the definition of R with aRSA, we
must first restate the bound in the shape of the abstract
response-time bound equation that aRSA expects, which we do
next.
We know that:

- if A is in the abstract search space, then it is also in the concrete search space; and
- if A is in the concrete search space, then there exists a solution that satisfies the inequalities stated in H_R_is_maximum. Using these facts, we prove that, if A is in the abstract search space, then there also exists a solution F to the response-time equation as expected by aRSA.

Lemma soln_abstract_response_time_recurrence :

∀ A : duration,

abstract.search_space.is_in_search_space L (fifo.IBF ts tsk) A →

∃ F : duration,

F ≤ A + R

∧ task_rtct tsk + intra_IBF A F ≤ SBF F

∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).

Proof.

move ⇒ A SP; move: (H_R_is_maximum A) ⇒ MAX.

rewrite /intra_IBF.

feed MAX; first by apply: search_space_sub ⇒ //.

move: MAX ⇒ [F' [FE LGL]].

have Leq1 : SBF F' ≤ SBF (A + R) by apply H_SBF_monotone; lia.

have Leq2 : total_request_bound_function ts (A + 1) ≥ task_cost tsk by apply task_cost_le_sum_rbf ⇒ //; lia.

have Leq3 : task_cost tsk ≥ task_rtct tsk by apply H_valid_run_to_completion_threshold.

unfold total_request_bound_function in ×.

have [F'' [LE EX]]:

∃ F'',

0 ≤ F'' ≤ A + R

∧ SBF F'' = SBF (A + R) - (task_cost tsk - task_rtct tsk).

{ apply exists_intermediate_point_leq.

- by move⇒ t; rewrite !addn1; apply H_unit_SBF.

- lia.

- apply/andP; split.

+ rewrite (fst H_valid_SBF); lia.

+ lia.

}

∃ F''; split; last split.

+ by move: LE; clear; lia.

+ by rewrite EX; lia.

+ by rewrite EX; lia.

Qed.

End ConcreteToAbstractFixpointReduction.

∀ A : duration,

abstract.search_space.is_in_search_space L (fifo.IBF ts tsk) A →

∃ F : duration,

F ≤ A + R

∧ task_rtct tsk + intra_IBF A F ≤ SBF F

∧ SBF F + (task_cost tsk - task_rtct tsk) ≤ SBF (A + R).

Proof.

move ⇒ A SP; move: (H_R_is_maximum A) ⇒ MAX.

rewrite /intra_IBF.

feed MAX; first by apply: search_space_sub ⇒ //.

move: MAX ⇒ [F' [FE LGL]].

have Leq1 : SBF F' ≤ SBF (A + R) by apply H_SBF_monotone; lia.

have Leq2 : total_request_bound_function ts (A + 1) ≥ task_cost tsk by apply task_cost_le_sum_rbf ⇒ //; lia.

have Leq3 : task_cost tsk ≥ task_rtct tsk by apply H_valid_run_to_completion_threshold.

unfold total_request_bound_function in ×.

have [F'' [LE EX]]:

∃ F'',

0 ≤ F'' ≤ A + R

∧ SBF F'' = SBF (A + R) - (task_cost tsk - task_rtct tsk).

{ apply exists_intermediate_point_leq.

- by move⇒ t; rewrite !addn1; apply H_unit_SBF.

- lia.

- apply/andP; split.

+ rewrite (fst H_valid_SBF); lia.

+ lia.

}

∃ F''; split; last split.

+ by move: LE; clear; lia.

+ by rewrite EX; lia.

+ by rewrite EX; lia.

Qed.

End ConcreteToAbstractFixpointReduction.