This web page provides the Coq proof and supplemental materials for the following paper:
The interested reader is invited to follow the discussion in Section IV of the paper in parallel with the formal Coq development that is being described. For ease of viewing and inspection, two variants of the discussed Coq development are provided:
A static, hyper-linked rendering of the Coq development — start with this one.
As discussed in the paper, the proof builds on Prosa and its abstract RTA framework. (In fact, it has been integrated into Prosa.) It thus leverages a lot of definitions found in Prosa. This rendering of the Coq development is cross-referenced using hyperlinks, which makes it easy to click through to the underlying definitions.
The Ltac proof scripts are contained in static form, but initially hidden. To see a proof script, click on the string Proof that appears after each fact, lemma, and theorem to display their respective proofs.
Note however that Ltac proof scripts are not primarily intended for human consumption. In particular, Ltac proof scripts are not expected to “make sense” when read in static form. Rather, Ltac proof scripts should be “stepped through” interactively to see how each tactic application changes the proof state (i.e., the sets of established facts, assumptions, and remaining proof obligations). To see an example of this, try out the second HTML rendering discussed next.
An interactive, steppable rendering of the Coq proof — most suitable for readers with prior Coq experience.
This variant use Alectyron to provide an interactive view of the Coq development that allows stepping through the proof. Its main benefit is that it allows readers to explore the proof state, i.e., the effect of individual Ltac tactic invocations, without having to install and run Coq locally.
Suggested use: click on “windowed” in the top bar and move the mouse pointer over proof steps to see the proof state change. If the right-hand pane does not fit the screen, decrease your web browser’s font size until it fits.
A Rust implementation of the proposed response-time analysis may be found in the response-time-analysis crate.
More specifically, the function fifo::dedicated_uniproc_rta implements the proposed analysis.
Our artifact evaluation package provides:
The package may be downloaded here: rtss22-artifact.tgz (1.7 MiB)
Please refer to the README files enclosed in the package for further details.