Changes:

* This commit generalises aRTA to "multi-stage" aRTA. The general idea
is explained in file [analysis/abstract/abstract_rta.v]. Short idea is
that the fixpoint equation can be extended to a sequence of fixpoint
equations. Solution to an equation can be used in later fixpoints. This
way one can support move expressive models of execution. The prior
version of aRTA (applicable to ideal uni-processors) is now an
instantiation of the new RTA theorem.

* Interference and Interfering workload are now type-classes. Note that
this changes files in directory [results], since [Variables] were
replaced with [Instance] declarations.

* IBF supports arbitrary parameters (not just relative arrival time).
IBF parametrised by the relative arrival time is not expressive enough
to support restricted-supply analysis. It was generalized to support a
larger class of parameters

* Rename [run to completion] file into [lower bound on service]. The
file was slightly generalized, now  it derives a lower bound on any
pre-defined amount of service.

* Generalize instantiations of interference and interfering workload.
Now, the definitions do not directly destruct the processor state.
Also, definitions for these functions have been made opaque.

Remove the classic module from the source tree, to speed up CI and to
avoid having to maintain it going forward as we adopt newer Coq and
mathcomp versions.

Issue: RT-PROOFS/rt-proofs#98

Sergey Bozhko authored 2 years ago and Björn Brandenburg committed 2 years ago

Clean up the various committer names and email addresses. For example, see
```
git log  --pretty="format:%an <%aE>" | git check-mailmap --stdin | sort -u
```
to get a clean list of all contributors to Prosa. 

Carina Schmitt authored 2 years ago and Björn Brandenburg committed 2 years ago

The generated HTML pages must reference MPI-SWS servers, not third-party CDNs.

This fixes compilation with current Coq master.

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

This is a collection of facts and refinements specific to the aRTA
instantiations used in POET-generated certificates.

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

Currently a lot of files use two hypotheses

```
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
```

instead of the combined `valid_arrival_sequence`.

This patch aims to fix this.

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

... to better match the structure of the paper and
simplify some proofs.

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

In the recent revision of the EDF RTA, a lemma relating the
priority inversion bound and cumulative priority inversion bound
was generalized. Using this, the proof of the bound on cumulative
priority inversion under FIFO scheduling was simplified.

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

* Add GEL basic facts file.
* Add RTA for GEL with bounded priority inversion by instantiating aRTA.

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

This patch adds more refinements for POET, in particular for tasks and for task properties. Further, there are some new definitions and helper lemmas.

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

* Some of the inequalities used in the EDF RTA to prove the soundness of IBF were not specific to EDF. These have been moved to `analysis.facts.busy_interval.inequalities`.
* The lemma `reorder_summation` can be generalized to sums over partitions. Therefore, it has been moved to `util.sum`.

Paul Hermes authored 2 years ago and Björn Brandenburg committed 2 years ago

Using util.fixpoints, we now calculate the response-time bounds
and prove their properties, instead of assuming them.

Paul Hermes authored 2 years ago and Björn Brandenburg committed 2 years ago

The file `util/fixpoints.v` provides tools to find
fixpoints of functions and contains lemma proving
properties about the results.

There also had to be added an additional lemma to
`util/list.v` and a function to unwrap option types,
contained in `util/option.v`.

- monotonicity
- degenerate response-time bounds

Note: the patch also reorders the import order in util.classic.all to resolve
a name clash caused by the transitive inclusion of util.rel.

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

previously the lemma proving the soundness
for the bound on the length of the busy window
was proved separately in the edf and fifo RTAs.
However, this lemma does not depend on the
scheduling policy under consideration, and therefore
has been moved to analysis.abstract.ideal_jlfp_rta