- Feb 22, 2023
-
-
Pierre Roux authored
-
- Feb 21, 2023
-
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
-
Pierre Roux authored
Now advise to just install the Coq platform
-
Pierre Roux authored
-
Pierre Roux authored
-
The tutorial document, based on RST, is too complex for the simple CI spell check. Please use your editor's spell checker when editing the tutorial.
-
-
-
-
- Feb 20, 2023
-
-
-
Pierre Roux authored
-
- Feb 14, 2023
-
-
This should make CI failures faster by compiling most of Prosa (the coq-prosa OPAM package) before compiling the dependencies (CoqEAL) and the remaining (coq-prosa-refinements package).
-
… in the proofs of basic properties of various priority policies.
-
Pierre Roux authored
Those weren't needed before we depend on coqeal but now are.
-
- Jan 28, 2023
-
-
Lasse Blaauwbroek authored
Fixes #104
-
- Jan 20, 2023
-
-
Sergey Bozhko authored
Changes: * This commit generalises aRTA to "multi-stage" aRTA. The general idea is explained in file [analysis/abstract/abstract_rta.v]. Short idea is that the fixpoint equation can be extended to a sequence of fixpoint equations. Solution to an equation can be used in later fixpoints. This way one can support move expressive models of execution. The prior version of aRTA (applicable to ideal uni-processors) is now an instantiation of the new RTA theorem. * Interference and Interfering workload are now type-classes. Note that this changes files in directory [results], since [Variables] were replaced with [Instance] declarations. * IBF supports arbitrary parameters (not just relative arrival time). IBF parametrised by the relative arrival time is not expressive enough to support restricted-supply analysis. It was generalized to support a larger class of parameters * Rename [run to completion] file into [lower bound on service]. The file was slightly generalized, now it derives a lower bound on any pre-defined amount of service. * Generalize instantiations of interference and interfering workload. Now, the definitions do not directly destruct the processor state. Also, definitions for these functions have been made opaque.
-
- Nov 11, 2022
-
-
Sergey Bozhko authored
-
Sergey Bozhko authored
-