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.

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

With some misc. cleanups and reorganization thrown in.

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

Add a few lemmas that will be useful later.

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

also, removed one assumption in [eq_ind_in_seq]

lemma [count_filter_fun] is equivalent to ssreflect's [size_filter]

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

Note that many files have changed; however, this is due to the fact that some of the lemmas in nat.v have been renamed or removed.

Remove the use of ideal uniprocessor schedules in a couple of places where
it's not actually required.

Also fix some coqdoc styling issues while at it.

Superseded by alectryon, no longer needed.

See: https://github.com/cpitclaudel/alectryon

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

A standard mechanism for enforcing sequentiality of job execution is to use a readiness predicate that ensures that a job is not ready until all prior jobs of the same task are completed.

This patch introduces such predicates.

LailaElbeheiry authored 4 years ago and Björn Brandenburg committed 4 years ago

With help from Marco Maida <mmaida@mpi-sws.org>, Sergey Bozhko <sbozhko@mpi-sws.org>, Björn Brandenburg <bbb@mpi-sws.org>.

LailaElbeheiry authored 4 years ago and Björn Brandenburg committed 4 years ago

This commit connects the two ways with which one can specify that a
schedule is an EDF schedule in PROSA: the `EDF_schedule` predicate
and the `respects_policy_at_preemption_point` with the EDF priority
policy predicate. We connect these two definitions by showing that
they're equivalent. We then restate the optimality proof of EDF
schedules using the proven equivalence.

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

...and some supporting theory. This will be needed to handle arrival curves extrapolated from a finite prefix.

Pierre Roux authored 4 years ago and Björn Brandenburg committed 4 years ago

Completion sequences are defined (as arrival sequences) from an arrival sequence and a schedule.