 25 Sep, 2020 1 commit


Sergey Bozhko authored
The definition of busy interval can be generalized to an arbitrary processor state model without affecting other parts of the project.

 23 Sep, 2020 1 commit


Sergey Bozhko authored
Note that the prior definition of [sequential_tasks] did not differentiate between a job coming from the arrival sequence and any other job. However, all computable properties (such as [job_respects_task_rtc, valid_preemption_model, arrivals_have_valid_job_costs, all_deadlines_of_arrivals_met]) are stated exclusively for jobs from the arrival sequence. In order to make the definition of [sequential_tasks] compatible with computable properties, we add preconditions [arrives_in arr_seq j1] and [arrives_in arr_seq j2].

 22 Sep, 2020 7 commits


Marco Maida authored
max arrival curve + WCET ➔ max RBF min arrival curve + BCET ➔ min RBF

Björn Brandenburg authored

Björn Brandenburg authored
The vernacular commands Opaque / Transparent change coqtop's prompt counter without generating a prompt (for whatever reason). The proof state recorder needs to be aware of this to avoid a outofsync assertion false positive.

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored
For debugging purposes, slow down the interaction with coqtop to maybe trigger some potential races more reliably.

Björn Brandenburg authored
If coqtop reports a different number of interactions in its prompt than we provided, we're out of sync.

 09 Sep, 2020 4 commits


Björn Brandenburg authored

Vedant Chavda authored

Björn Brandenburg authored
... to comments and closing braces on lines before bulleted subproofs. For better debugging support, add parseonly and parseonly verbose modes.

LailaElbeheiry authored

 28 Aug, 2020 2 commits


Pierre Roux authored
So that we can link them to arrival curves of Network Calculus in NCCoq.

Pierre Roux authored

 27 Aug, 2020 1 commit


Pierre Roux authored

 10 Aug, 2020 4 commits


Vedant Chavda authored

Björn Brandenburg authored
Don't always "drill to the bottom" and unfold to sums; instead explicitly make use of the fact that the EDF proof reasons about finite identical prefixes, which allows staying at a semantically higher level in the proof. While at it, switch the file to using the preferred `now` tactical when closing out proofs (rather than `by`) to avoid emacs indentation issues.

Björn Brandenburg authored

Björn Brandenburg authored

 06 Aug, 2020 1 commit


Björn Brandenburg authored
Before mathcomp 1.11.0 (which requires Coq 8.12), case analysis doesn't automatically rewrite destructed `minn` premises, so "try" this manually until we drop support for mathcomp 1.11.0.

 05 Aug, 2020 6 commits


Björn Brandenburg authored
Can't rely on arg_maxnP just yet.

Björn Brandenburg authored
This change breaks compatibility with mathcomp < 1.10.

Björn Brandenburg authored
There's now also a `findP` in ssreflect's seq library.

Marco Maida authored

Marco Maida authored

Marco Maida authored

 04 Aug, 2020 4 commits


Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

Björn Brandenburg authored

 30 Jul, 2020 1 commit


Björn Brandenburg authored

 09 Jul, 2020 4 commits


Björn Brandenburg authored

Björn Brandenburg authored
add lemmas on consistency of backlogged jobs set add notion of a nonclairvoyant readiness model

Björn Brandenburg authored

Björn Brandenburg authored

 08 Jul, 2020 4 commits


Björn Brandenburg authored

Björn Brandenburg authored
This is a general definition and not specific to a particular implementation.

Marco Perronet authored

Björn Brandenburg authored
