Define fixpoint predicates
The following discussion from !319 (merged) should be addressed:
-
@bbb started a discussion: (+1 comment)
Should we make these predicates proper definitions (
nat -> Prop)?aRSA_fixpoint RaRTA_fixpoint Rbw_fixpoint L
Looks kinda neat, I think.
We keep referring to these, also in discussion (e.g., w/ Matteo), perhaps named definitions would help?
Activity
assigned to @sbozhko
mentioned in merge request !319 (merged)
mentioned in merge request !366 (merged)
Since it came up again, let's discuss a more concrete proposal.
Let's say we have the following bound:
Variable R : duration. Hypothesis H_R_is_maximum : forall (A : duration), is_in_search_space ts L A -> exists (F : duration), A <= F <= A + R /\ total_request_bound_function ts (A + ε) <= SBF F.Is your suggestion that we can simply introduce a definition for
H_R_is_maximum? I.e.,(* File prosa/analysis/definitions/???.v *) Definition FIFO_bounded_nps_fixpoint R := forall (A : duration), is_in_search_space ts L A -> exists (F : duration), A <= F <= A + R /\ total_request_bound_function ts (A + ε) <= SBF F. (* File results/rs/fifo/bounded_nps.v *) Variable R : duration. Hypothesis H_R_is_maximum : FIFO_bounded_nps_fixpoint R.I'm a bit worried that
- We will end up with 20 different bounds for different kinds of results ({preem, non-pree, lim, float} × {FIFO, EDF, FP} × {ideal, rs, overheads, ...} + abstract fixpoints)
- This might reduce readability, since you won't be able to copy-paste/print just the page with the result.
Good points, thanks for starting a discussion.
We will end up with 20 different bounds for different kinds of results
I think the fact that we will end up having so many different bounds is actually a reason to give them names. Otherwise, how do you refer to them precisely? Currently we say things like "the EDF fixpoint", "the FP fixpoint", etc. Once we have RS, plain, whatever next... this will become rather ambiguous. Especially for non-Coq experts, it will be a lot easier to be pointed to one concise definition.
This might reduce readability, since you won't be able to copy-paste/print just the page with the result.
I definitely do not want to split it across multiple files. I would keep each RTA together in one RTA file like we do today. Though we already split stuff out like the search space and the blocking bound (for good reason, to avoid repetition). For the fix points, there is no reuse, so they should stay local.
On further thought, I would also maybe no longer these things "fix points" or "recurrences". We've relaxed them, so they no longer are fix points, strictly speaking. They are just sufficient conditions. And they are becoming more complicated conditions, like your EDF busy-window bound.
Currently, we have always this pattern in each RTA file:
- Introduce a variable
R. - State a condition on
Ras a hypothesis. - A theorem saying that
Ris a response-time bound.
How about something like this instead?
Definition response_time_bound R := forall (A : duration), is_in_search_space ts L A -> exists (F : duration), A <= F <= A + R /\ total_request_bound_function ts (A + ε) <= SBF F. Theorem response_time_bound_correctness : forall R, response_time_bound R -> task_response_time_bound arr_seq sched R.This doesn't take more space than the current pattern, keeps everything in one place, and maybe makes the correctness claim even a bit more readable (at least the "if ... then ..." structure becomes more obvious). What do you think?
The names are not meant as a final proposal. I'm divided on whether we should keep them simple like this (so they are distinguished only by module name, e.g.,
rs.edf.response_time_bound) or continue to mention major policy aspects in them (to prevent accidental mixups, e.g.,uniprocessor_response_time_bound_fully_preemptive_edf).- Introduce a variable
-
In some cases, we might want to use the same fixpoint in multiple files. For example, this one. I guess we can use the
Letconstruction in the supporting files.Overall, I'm not against the idea. But at the same time, I don't see many advantages.
(@kbedarka, what do you think?)
Edited by Sergey Bozhko Ah I had missed this discussion. I am quite in favor of this. I think it makes the final theorem quite a bit more readable. With Bjoerns suggested design it is very clear that the final result establishes the property that proving the response time bound can be reduced to proving R is the solution to some equation. This is quite nice.
I have something similar for my project in my files.
-
In some cases, we might want to use the same fixpoint in multiple files. For example, this one. I guess we can use the
Letconstruction in the supporting files.Yes, in those cases we have a choice: either accept that the "is a valid bound" predicate is defined in a file external to the RTA file, or duplicate the definition in the RTA file and the auxiliary file(s).
I don't see many advantages.
The main advantage I see is ease of reference: it makes it much easier to communicate to people outside of the project what bounds we've actually proven.
Case in point, Matteo currently has a big TODO "how to cite Prosa results?" in his aRTA background section. I'd like him to link to FP, EDF, FIFO... results (the specific formulas, not the RTA file as a whole). Readers should be able to click on it and immediately see something closely resembling the formula in Matteo's table. In the current setup, what should he link to?
-
I imagine something like this might work.
See the NP-FP RTA equation~[1].
(Btw, I just noticed that the pretty-html does not recognise hypotheses as links)
-
That said, I already updated the RS-FIFO file to have a separate definition
-
Maybe
response_time_boundis not the best name, though. Since the final statement looks like "ifRis a response-time bound, thenRis a response-time bound"Theorem uniprocessor_response_time_bound_fifo : forall (R : duration), response_time_bound R -> task_response_time_bound arr_seq sched tsk R.
