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

From changelog of Coq version 8.15:
Changed: [apply with] does not rename arguments unless using
compatibility flag Apply With Renaming (#13837, fixes #13759, by Gaëtan
Gilbert).

So, this commit replaces all occurrences of [apply L with (NAME0 := V)]
to [apply L with (NAME := V)]

The default works just fine (nowadays), so let's use that.

Martin Constantino–Bodin authored 4 years ago and Björn Brandenburg committed 3 years ago

... instead of `service_in`, to mirror the way
the primitive `scheduled_on` is used to realize
`scheduled_in`.

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

There are quite a few places where hypotheses about the task of a job are simply stated as equality (even though a proper predicate exists). This patch replaces the equalities with the predicate.

As Pierre pointed out in [MR187](!187),
we don't want updates in any of our dependencies to accidentally
shadow Prosa symbols. Hence, always import Prosa modules last to make
sure Prosa symbols "win" any name clashes.

This way, an addition in external libraries
cannot shadow a definition in Prosa.

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

Provide an RTA for FIFO scheduling on ideal uniprocessors based on an
instantiation of abstract RTA. The provided RTA is works for tasks
described by arbitrary arrival curves and is independent of the
workload's preemption model (since FIFO schedules are necessarily
non-preemptive). 

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

* Added a lemma for proving `rbf` at `\varepsilon` is more than 0. This is a general fact which can be used in the FIFO RTA to simplify a proof. 
* Changed `1` to `\varepsilon` in one of the existing RBF lemmas for uniformity.

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

Add an implementation of arrival curves via fast
extrapolation of a finite arrival-curve prefix. 

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

* rename [step_function] to [unit_growth]
* restructure file

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

- there is no priority inversion in FIFO schedules
- all jobs of a tasks necessarily execute in arrival order
- the FIFO policy never requires a job to be preempted

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

The existing notion of priority policy compliance is silent on preemptions
that exchange jobs of equal priority. A real scheduler would not engage
in such superfluous preemptions. For some intuitively true properties, it
is natural and necessary to assume the absence of superfluous preemptions.
This patch introduces a definition for this purpose.

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

...and relate it to `nonpreemptive_schedule`, the existing notion of
non-preemptive schedules.

... out of the priority-inversion file, where they are used, but
topically don't belong.

The lemma does not inherently rely on a task abstraction. This patch
removes the accidental dependency so that the lemma can be used in
job-only contexts.

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

I think that this experiment was not successful. These lemmas can be
easily replaced by ssreflect tactics. Also, they encourage to write
proofs that are harder to maintain.

Martin Constantino–Bodin authored 3 years ago and Björn Brandenburg committed 3 years ago

`esy` is an `npm`-like package manager and build tool designed for
reproducibility, by preventing the use of unlisted dependencies and
pinning the exact version of each of these (a bit like `opam`, but
with more guarantees).

A nice feature of `esy` is ease of installation:

1. Install `esy` through `npm`. (However, note that `esy` is not a
   JavaScript program; the `esy` project just uses `npm` as a code
   hoster.

2. Run `esy` in the Prosa repository. 

This will download and compile all dependencies and compile the
repository. (On the flip side, this also means that Coq will be
compiled, so the first time, compilation will be slow.)

See the README.md file for usage instructions. 

See also the discussion: #80

For more information about `esy`, see: https://esy.sh/

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

`Task` should obviously be of type `TaskType`.

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

...to match the description in the aRTA paper.

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

The lemma [instantiated_busy_interval_equivalent_edf_busy_interval] actually does not depend on EDF.