You should try. But I have some doubts.

Imagine a scenario where your `IBF(A, Δ)`

depends on two parameters and now you have to check the fixpoint for `A = 10`

. If `IBF(10, Δ)`

can take any value for `Δ < 10`

, then (later in the development) your fixpoint (`H_R_is_maximum`

) can converge before your job even arrives.

So, somewhere in the proof you have to make sure that "the fixpoint does not converge too early". In this specific instantiation, you just need `F > 0`

; however, I'm not sure what would happen in the abstract RTA.

This is *probably* doable. You have to try and see if it works.

However, I do not quite see the problem this change solves. You will have to add `F > 0`

or `maxn _ _`

regardless of whether you add this premise or not.

After discussing this with Kimaya, I'll add my five cents. (@bbb)

So, imagine that we remove `maxn`

and use `task_rbf (A + F)`

. Now, there exists a task set `ts`

and a task `tsk \in ts`

for which `search_space = {0}`

and `priority_inversion_bound = 0`

.

Let's find a solution to this equation:

```
exists (F : duration),
A + F >= priority_inversion_bound
+ (task_rbf (A + F) - (task_cost tsk - task_rtct tsk))
+ total_ohep_rbf (A + F)
/\ R >= F + (task_cost tsk - task_rtct tsk).
```

Simplify: `priority_inversion_bound = 0`

and `A = 0`

:

```
exists (F : duration),
F >= (task_rbf F - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf F
/\ R >= F + (task_cost tsk - task_rtct tsk).
```

But note that `F = 0`

works as a solution:

```
F >= (task_rbf F - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf F
==> 0 >= (task_rbf 0 - (task_cost tsk - task_rtct tsk)) + total_ohep_rbf 0
==> 0 >= (0 - (task_cost tsk - task_rtct tsk)) + 0
==> 0 >= 0
```

and for `R = task_cost tsk - task_rtct tsk`

, we satisfy the second part of the equation:

`task_cost tsk - task_rtct tsk >= 0 + (task_cost tsk - task_rtct tsk)`

But `R = task_cost tsk - task_rtct tsk`

cannot be a valid response-time bound since it is smaller than the task cost.

**Sergey Bozhko**
(c1799b50)
*
at
28 Feb 14:37
*

**Sergey Bozhko**
(bffb6f15)
*
at
22 Feb 09:16
*

[to squash]

@bbb,

It seems like our "SBF within busy interval" causes problems for the busy-interval bound.

- The equation for busy-interval bound should look like this
`total_rbf ts L <= SBF L.`

. If we unfold a bit, we will get`(L - SBF L) + total_rbf ts L <= L.`

, which basically translates into a blackout-aware version of "the system is not overloaded". Note that this equation does not have the blocking bound (i.e., a bound on the max segment of a non-preemptive low-priority job). - To prove that this equation implies bounded busy intervals in the ideal case, we used another approach that involves "no-carry-in" time instances.
- The proof worked as follows. Let's start with no-carry-in time, take an interval of length
`L`

, show that there is another no-carry-in time somewhere in the middle. (Since we start with`0`

pending workload, and total workload is bounded by`total_rbf`

) - This does not work if we start with a quiet time, since we can have a potentially unbounded amount of low-priority carry-in.

- The proof worked as follows. Let's start with no-carry-in time, take an interval of length
- So, how can we prove that busy intervals are bounded in the restricted-supply case using
`(L - SBF L) + total_rbf ts L <= L`

?- Let's start with a no-carry-in time
`t1`

(it always exists). - So, next, we pick
`t1 + L`

and show that`total_rbf ts L`

bounds all contribution of all tasks. - Now, we want to use
`L - SBF L`

to bound the contribution of all blackouts. - But this does not work, since we can bound contribution of blackouts only if we start with a
*quiet time*and stay within a busy-interval prefix (recall that we have this fancy SBF). Yes, carry-in implies that we start with a quiet time. But it does not implies that we are still in the same busy-interval prefix.

- Let's start with a no-carry-in time

So, it seems like there are three potential solutions.

- Drop "fancy" from SBF and use the vanilla SBF that lower-bounds supply over any interval (I use this approach in this MR)
- Add blocking bound to the equation so it bounds lower-priority contribution and we don't have to use this "no-carry-in" approach. (This option is probably better for the paper)
- Try to come up with a solution that combines both (I spend roughly one day, and I didn't come up with an idea)

**Sergey Bozhko**
(12a0f509)
*
at
21 Feb 15:56
*

*
... and
4 more commits
*

**Sergey Bozhko**
(6482270c)
*
at
20 Feb 13:46
*

prove some stuff, stuck on busy intervals

*
... and
101 more commits
*

So, then `Hypothesis H_valid_schedule : valid_schedule sched arr_seq.`

is a bad idea? We don't always need *all* assumptions that this hypothesis brings into the context. Your two counter-points apply to this hypothesis.

I don't think that keeping the set of assumptions as small as possible at all times should be our primary goal.

How about moving this hypothesis to the top and simply state

```
// TODO: improve
(** Consider any time interval <<[t1, t1 + Δ)>> such that [j]
arrives inside of this interval. *)
Variables (t1 : instant) (Δ : duration).
Hypothesis H_j_arrives_after_t : t1 <= job_arrival j.
Hypothesis H_job_arrival_lt: job_arrival j < t1 + Δ.
```

If the interval starts "*after* the job's arrival" then the interval does not contain the job's arrival. But it seems like you meant something else.

?

` (** As a first step, we focus our attention on the interval _after_ the`