AbstractRTA - ECRTS'20 Artifact Evaluation

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.

  1. Installing the Proof Framework

  2. Compiling AbstractRTA

  3. Verifying the Correctness of the Proofs

  4. Locating the Main Results of the Paper

1. Installing the Proof Framework

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.

2. Compiling 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.

3. Verifying the Correctness of the Proofs

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

  1. incomplete proofs can be assumed to hold by calling the admit or Admitted commands, and

  2. unproven 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:

  1. 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.

  2. 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.

4. Locating the Main Results of the Paper

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.

Abstract Foundation

Abstract Reponse-Time Analysis

Abstract Sequential Reponse-Time Analysis

Preemption model

Instantiations