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.

mathcomp has deprecated `iota_add` in favor of `iotaD`.

However, `iotaD` wasn't added until mathcomp 1.12, so this patch breaks
compatibility with earlier versions.

Added a few lemmas to util/div_mod that are needed for POET

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

Coq 8.11, Coq 8.12, ssreflect 1.10, and ssreflect 1.11
are no longer supported

Due to whatever the CI environment does to cache and restore
intermediate result files, somehow `make validate` triggers some
spurious recompilation. To avoid confusing the checking script,
trigger any possible re-compilation steps before capturing the output
of `make validate`.

Closes #79

* use more concise name
* add cases with [is_true _] in addition to cases with [_ = true]

Currently, aRTA required [F] to be solution of equation
[A + F = task_rtct + IBF A (A + F)], this commit relaxes
this assumption to [A + F >= task_rtct + IBF A (A + F)]

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

Added helper lemmas relating `valid_schedule` to job execution hps with hint.
Removed useless hps in aRTA.