 15 Oct, 2019 2 commits


Sergey Bozhko authored

Pierre Roux authored
We no longer support Coq 8.8.

 11 Oct, 2019 1 commit


Marco Perronet authored
Add the `htmlpretty` target to the Makefile to generate prettier documentation, based on the CoqdocJS project. https://www.ps.unisaarland.de/~ttebbi/coqdocjs/ https://github.com/tebbi/coqdocjs Many thanks to Tobias Tebbi for creating CoqdocJS.

 24 Sep, 2019 1 commit


Sergey Bozhko authored

 23 Sep, 2019 7 commits


Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

 17 Sep, 2019 4 commits


Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

Sergey Bozhko authored

 30 Aug, 2019 3 commits


Björn Brandenburg authored
Rationale: reserve the behavior folder for tracebased 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.

Björn Brandenburg authored

Sergey Bozhko authored
Also removes an unnecessary module in rt.util.epsilon.

 23 Aug, 2019 10 commits


Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored
Make it a statement about scheduled jobs, to match the neighboring definitions.

Björn Brandenburg authored

Björn Brandenburg authored
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 selfsuspensions.

Björn Brandenburg authored

 21 Aug, 2019 1 commit


Björn Brandenburg authored

 20 Aug, 2019 2 commits


Sergey Bozhko authored
When we were writing the paper on Abstract RTA, we noticed that the responsetime recurrence for EDF does not match the known bound. This merge request tightens the analysis in Prosa to match the known bound.

Sergey Bozhko authored

 13 Aug, 2019 9 commits


Björn Brandenburg authored
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.

Björn Brandenburg authored

Björn Brandenburg authored
Given an interval [a, b), a function f: nat > T, a predicate P, and a total, reflexive, transitive relation R, [search_arg f P R a b] will find the x in [a, b) that is an extremum w.r.t. R among all elements x in [a, b) for which (f x) satisfies P. For example, this can be used to search in a schedule for a scheduled job released before some reference time with the earliest deadline.

Björn Brandenburg authored
This patch adds functions for transforming a given schedule either by replacing the allocation at a given point, or by swapping the allocations at two points, together with a bunch of supporting lemmas and service invariants.

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored
Points before or after an interval are not in the interval...

Björn Brandenburg authored
n + a  b + b  a = n if n >= b

Björn Brandenburg authored
...to match leq_ltn_trans in ssrnat
