Marco Maida authored 2 years ago and Björn Brandenburg committed 2 years ago

This patch adds the definitions and lemmas of a concrete job-generation
function in pair with the concrete arrival sequence. These building
blocks sit at the basis of POET's assumption-less examples, used to
prove the absence of contradicting hypotheses in abstract RTA and the
certificates.

Additionally, it adds some helper functions and a class instance that
were missing in the concrete task files (`MaxArrivals`).

We've had problems with spurious CI failures and unexpected recompilation of .vo files. Somehow the collection of .vo files in the build stage for reuse in the processing stage is not working properly. This MR simplifies the CI setup to compile, build the documentation, and validate all in one job.

It also disables builds with development versions of Coq and mathcomp (nobody was looking at this output anyway). 

Busy intervals by definition always include the job arrival time, so
stating `t1 <= job_arrival j < t2` explicitly is not required.

Closes: #93

- remove some needless `Let` bindings
- use coqdoc sectioning to expose structure in outline

Mariam Vardishvili authored 2 years ago and Björn Brandenburg committed 2 years ago

Modify the EDF blocking bound so that the arrival offset of the
job under analysis is taken into account when considering from
which task a lower-priority job that is causing arrival-blocking
may stem.

With contributions by Kimaya Bedarkar, Sergey Bozhko,
and Björn Brandenburg.

Kimaya Bedarkar authored 2 years ago and Björn Brandenburg committed 2 years ago

Currently, we have lemmas stating that `task_rbf` at `\vareosilon` is greater than equal to task cost, and `task_rbf` is monotone. I combined these two lemmas to state that `tsk_rbf` at any point greater than `0` is greater than task cost. I find that this fact is regularly required in proofs and, therefore, would be good to have in the facts folder.

Marco Maida authored 2 years ago and Björn Brandenburg committed 2 years ago

This commit defines and adds facts about a concrete arrival sequence in
which tasks release jobs "as quickly as possible" as allowed by their
respective arrival-curve constraints. This maximal arrival sequence is
used in POET to generate assumption-less certificates.

Kimaya Bedarkar authored 2 years ago and Björn Brandenburg committed 2 years ago

The current definitions of `respects_JLFP_policy_at_preemption_time`
and `respects_FP_policy_at_preemption_time` use the predicate
`hep_job_at`. This predicate does not make sense for `JLFP`
and `FP` policies. To avoid this, these definitions should
instead use the definition `respects_JLDP_policy_at_preemption_point`.
Doing this requires coercions from `JLFP` to `JLDP` and from
`FP` to `JLFP`. This patch also introduces these coercions.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

It is exactly big1_eq

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

It was subsumed by sum_nat_gt0

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

Too specific and one liner with existing MathComp lemmas.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

Subsumed by existing MathComp lemmas on division.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

leq_trans and leq_addr seem to be enough.

Pierre Roux authored 3 years ago and Björn Brandenburg committed 2 years ago

Too specific.