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

Require Export prosa.analysis.facts.model.rbf.

Require Export prosa.analysis.abstract.search_space.

Require Import prosa.analysis.facts.priority.fifo.

Require Import prosa.analysis.definitions.sbf.pred.

Require Export prosa.analysis.abstract.search_space.

Require Import prosa.analysis.facts.priority.fifo.

Require Import prosa.analysis.definitions.sbf.pred.

# The Abstract Search Space is a Subset of the FIFO Search Space

Consider a restricted-supply uniprocessor model where the
minimum amount of supply is defined via a monotone
unit-supply-bound function SBF.

Consider any type of tasks.

Consider an arbitrary task set ts.

Let max_arrivals be a family of valid arrival curves, i.e.,
for any task tsk in ts max_arrival tsk is (1) an arrival
bound of tsk, and (2) it is a monotonic function that equals
0 for the empty interval delta = 0.

Context `{MaxArrivals Task}.

Hypothesis H_valid_arrival_curve :

valid_taskset_arrival_curve ts max_arrivals.

Hypothesis H_valid_arrival_curve :

valid_taskset_arrival_curve ts max_arrivals.

For brevity, let's denote the request-bound function of a task
as rbf.

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.

In the case of FIFO, the concrete search space is the set of
offsets less than L such that there exists a task tsk in
ts such that rbf tsk (A) ≠ rbf tsk (A + ε).

Definition is_in_search_space (A : duration) :=

let rbf_makes_a_step tsk := rbf tsk A != rbf tsk (A + ε) in

(A < L) && has rbf_makes_a_step ts.

let rbf_makes_a_step tsk := rbf tsk A != rbf tsk (A + ε) in

(A < L) && has rbf_makes_a_step ts.

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, let us introduce a shorthand for an IBF (used by
aRTA). The abstract search space is derived via IBF.

Local Definition IBF (A F : duration) :=

(F - SBF F) + (total_request_bound_function ts (A + ε) - task_cost tsk).

(F - SBF F) + (total_request_bound_function ts (A + ε) - task_cost tsk).

Then, abstract RTA's standard search space is a subset of the
computation-oriented version defined above.

Lemma search_space_sub :

∀ A,

abstract.search_space.is_in_search_space L IBF A →

is_in_search_space A.

Proof.

move ⇒ A [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].

{ subst A.

apply/andP; split⇒ [//|].

apply /hasP; ∃ tsk ⇒ [//|].

rewrite neq_ltn; apply/orP; left.

rewrite /rbf task_rbf_0_zero // add0n.

by apply task_rbf_epsilon_gt_0 ⇒ //.

}

{ apply /andP; split⇒ [//|].

apply /hasPn ⇒ EQ2.

rewrite /IBF in INSP2; rewrite /total_request_bound_function.

rewrite subnK in INSP2 ⇒ //.

apply INSP2; clear INSP2.

have ->// : total_request_bound_function ts A = total_request_bound_function ts (A + ε).

apply eq_big_seq ⇒ //= task IN.

by move: (EQ2 task IN) ⇒ /negPn /eqP. }

Qed.

End SearchSpaceSubset.

∀ A,

abstract.search_space.is_in_search_space L IBF A →

is_in_search_space A.

Proof.

move ⇒ A [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].

{ subst A.

apply/andP; split⇒ [//|].

apply /hasP; ∃ tsk ⇒ [//|].

rewrite neq_ltn; apply/orP; left.

rewrite /rbf task_rbf_0_zero // add0n.

by apply task_rbf_epsilon_gt_0 ⇒ //.

}

{ apply /andP; split⇒ [//|].

apply /hasPn ⇒ EQ2.

rewrite /IBF in INSP2; rewrite /total_request_bound_function.

rewrite subnK in INSP2 ⇒ //.

apply INSP2; clear INSP2.

have ->// : total_request_bound_function ts A = total_request_bound_function ts (A + ε).

apply eq_big_seq ⇒ //= task IN.

by move: (EQ2 task IN) ⇒ /negPn /eqP. }

Qed.

End SearchSpaceSubset.