As part of the artifact evaluation of AbstractRTA, we will demonstrate how to compile the source code and automatically check the proofs of each theorem. In addition, we will provide references to the important results claimed to be proven in the paper, so that readers can confirm that no proofs have been omitted.

*Note: if the specification appears to be missing all comments, try reloading the page with your ad-blocker disabled; there are some false-positive issues with coqdoc and certain blockers.*

This document is organized as follows.

*Note: this step can be omitted if you use Docker.*

In order to compile AbstractRTA, the first step is to install (1) the `Coq`

proof assistant and (2) the `Mathematical Components`

extension library, which contains simplified notations and lemmas used in our formalization.

One can also use this guide for simple step-by-step instructions for setting up a Coq environment that is suitable for working with AbstractRTA.

Clone the repositoty with the source code. Next, move into AbstractRTA's directory and compile the entire source code.

```
$ git clone -b ecrts20 https://gitlab.mpi-sws.org/sbozhko/rt-proofs.git AbstractRTA
$ cd AbstractRTA/specification
$ ./create_makefile.sh
$ make -j 4
```

For Docker users:
```
$ git clone -b ecrts20 https://gitlab.mpi-sws.org/sbozhko/rt-proofs.git AbstractRTA
$ cd AbstractRTA/specification
$ docker run --rm -v $(pwd):/prosa -w /prosa mathcomp/mathcomp:1.9.0-coq-8.10 ./create_makefile.sh
$ docker run --rm -v $(pwd):/prosa -w /prosa mathcomp/mathcomp:1.9.0-coq-8.10 make -j4
```

The compilation should take only a few minutes and return no errors.

To simplify the proof development, Coq allows users to temporarily admit unproven results, which can be done in two ways:

incomplete proofs can be assumed to hold by calling the

`admit`

or`Admitted`

commands, andunproven facts can be blindly assumed to be true if they are declared as an

`Axiom`

.

As part of validating any mechanized proof in Coq, we need to ensure that there are no theorems that are "proven" using `admit`

, `Admitted`

or `Axiom`

.

To facilitate this check, Coq already offers a tool called `coqchk`

, which is a lightweight proof checker that is more reliable than the Coq compiler `coqc`

(which we used during compilation), since it has a small code footprint and does not implement optimizations and optional features. Apart from checking for correctness, `coqchk`

also prints the list of axioms and admitted proofs, as shown next.

In order to run `coqchk`

, please run the following commands on the terminal.

```
$ make validate
```

For Docker users:
```
$ docker run --rm -v $(pwd):/prosa -w /prosa mathcomp/mathcomp:1.9.0-coq-8.10 make validate
```

The verification process is different from the compilation since it does not import pre-compiled binaries but completely checks AbstractRTA and all of its dependencies, including the libraries from `Mathcomp`

and basic theories from `Coq`

. In fact, it checks every proof up to the foundations of the logic.

After a couple minutes, `coqchk`

should produce the following output, which we will analyze next.

```
CONTEXT SUMMARY
===============
* Theory: Set is predicative
* Axioms:
mathcomp.ssreflect.finset.Imset.imsetE
mathcomp.ssreflect.finset.Imset.imset2
Coq.ssr.ssreflect.Under_eq.Under_eq
mathcomp.ssreflect.finfun.FinfunDef.finfunE
mathcomp.ssreflect.fintype.SubsetDef.subsetEdef
Coq.ssr.ssreflect.Under_iff.Under_iff
Coq.ssr.ssreflect.Under_eq.Over_eq
mathcomp.ssreflect.generic_quotient.MPi.f
mathcomp.ssreflect.generic_quotient.MPi.E
Coq.ssr.ssreflect.Under_eq.Under_eq_from_eq
mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef
mathcomp.ssreflect.generic_quotient.Repr.f
mathcomp.ssreflect.generic_quotient.Repr.E
mathcomp.ssreflect.finset.Imset.imset
mathcomp.ssreflect.finset.Imset.imset2E
mathcomp.ssreflect.finset.SetDef.pred_of_set
mathcomp.ssreflect.finset.SetDef.finset
Coq.ssr.ssreflect.Under_eq.under_eq_done
mathcomp.ssreflect.tuple.FinTuple.enumP
Coq.ssr.ssreflect.Under_iff.over_iff_done
mathcomp.ssreflect.tuple.FinTuple.enum
mathcomp.ssreflect.bigop.BigOp.bigopE
mathcomp.ssreflect.tuple.FinTuple.size_enum
mathcomp.ssreflect.finfun.FinfunDef.finfun
Coq.ssr.ssreflect.Under_iff.Over_iff
mathcomp.ssreflect.fintype.CardDef.card
mathcomp.ssreflect.fintype.CardDef.cardEdef
mathcomp.ssreflect.finset.SetDef.pred_of_setE
Coq.ssr.ssreflect.Under_eq.over_eq
mathcomp.ssreflect.bigop.BigOp.bigop
mathcomp.ssreflect.fintype.SubsetDef.subset
Coq.ssr.ssreflect.Under_eq.over_eq_done
mathcomp.ssreflect.generic_quotient.Pi.f
mathcomp.ssreflect.generic_quotient.Pi.E
Coq.ssr.ssreflect.Under_iff.under_iff_done
mathcomp.ssreflect.fintype.Finite.EnumDef.enum
Coq.ssr.ssreflect.Under_iff.over_iff
Coq.ssr.ssreflect.Under_iff.Under_iff_from_iff
mathcomp.ssreflect.finset.SetDef.finsetE
```

In the output above, note that there are no references to `admit`

or `admitted`

proofs, but only to `Axioms`

. With regard to these axioms, we make two observations:

The

`Axioms`

starting with`mathcomp.*`

are part of the Mathematical Components library. They are not axioms in the usual sense but interfaces of Module Types, a Coq facility for generating generic modules (see this tutorial for an introduction). Note, however, that the concrete instantiations of these modules are based on correct,`Axiom`

-free proofs.Most importantly, there are no entries starting with

`prosa.*`

(the logical base directory of AbstractRTA), which implies that**there are no axioms or admitted proofs in our proof**.

The result of `coqchk`

confirms that every proof in AbstractRTA is correct.

The paper introduces the first general and rigorous formalization of the busy-window principle. The essence of the principle is identified as a minimal set of generic, high-level assumptions that allow for a unified and general abstract response-time analysis, which is independent of specific scheduling policies, workload models, and preemption policy details. From this abstract core, the paper shows how to obtain concrete analysis instantiations for specific schedulers via a sequence of refinement steps, and provides formally verified response-time bounds for eight common schedulers and workloads, including the widely used fixed-priority (FP) and earliest-deadline first (EDF) scheduling of fully, limited-, and non-preemptive sporadic tasks.

If you would like to see more of how the AbstractRTA is organized, have a look at the table of contents.

- Busy Intervals Are Bounded By A Constant (Precondition 7)
- Work-Conserving In The Abstract Sense (Precondition 8)
- Interference-Bound Function (Precondition 10)

- Tasks are sequential (Precondition 22)
- Consistent I and W (Precondition 23)
- Sequential Interference-Bound Function (Precondition 24)

- Preemption-model compliant (Precondition 28)
- Respects priority policy at preemption points (Precondition 28)
- Work-conserving in classical sense (Precondition 29)
- Priority Inversion
- Cumulative Priority Inversion