Also switch how this is patched into the Makefile while we're at it.

...while at it, remove some old cruft in there.

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

We no longer support Coq 8.8.

Marco Perronet authored 5 years ago and Björn Brandenburg committed 5 years ago

Add the `htmlpretty` target to the Makefile to generate prettier documentation,
based on the CoqdocJS project.

     https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/

     https://github.com/tebbi/coqdocjs

Many thanks to Tobias Tebbi for creating CoqdocJS.

Rationale: reserve the behavior folder for trace-based semantics.

These lemmas really constitute an analysis of the basic consequences
arising from the chosen semantics and hence logically belong to the
"analysis" part of Prosa.

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

Also removes an unnecessary module in rt.util.epsilon.

Make it a statement about scheduled jobs, to match the neighboring
definitions.

Add a [job_ready] parameter to the job model, akin to [pending], that
defines whether a job can be scheduled at a given time in a given schedule.

Then use this new general notion of readiness to define [backlogged].

A pending job may not be ready, whereas (under any reasonable
definition) a ready job ought to be pending, so this definition is
more precise and captures effects such as jitter and self-suspensions.

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

When we were writing the paper on Abstract RTA, we noticed that the response-time recurrence for EDF does not match the known bound.

This merge request tightens the analysis in Prosa to match the known bound.

This patch adds the classic EDF optimality argument: by swapping
allocations, any schedule in which no job misses a deadline can be
transformed into an EDF schedule in which also no job misses a deadline.