Prosa - ECRTS’16 Artifact Evaluation

In the Prosa paper, we argue in favor of mechanized proofs, since they can be automatically verified by a computer. Moreover, an important aspect of this verification process is that it can be easily performed by independent parties.

As part of the artifact evaluation of Prosa, 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. Finally, we will take one of the schedulability analyses as an example and show how to identify the assumptions required in the proofs.

This document is organized as follows.

1. Installing the Proof Framework

2. Compiling Prosa

3. Verifying the Correctness of the Proofs

4. Locating the Main Results of the Paper

5. Identifying Hypotheses

Please follow the instructions detailed in each section. In case of problems or further questions, feel free to contact us by email.

1. Installing the Proof Framework

In order to compile Prosa, 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. Although we provide some instructions for manual installation, we recommend using our provided Virtual Machine (VM) image.

Using our VM Image (Recommended)

The easiest way to compile Prosa is by using our Ubuntu 15.10 VM, which already has all necessary packages pre-installed. This VM also includes Proof General, an extension for Emacs for editing Coq proofs in an interactive manner.

The VM image is available here: [Download VM Image].

After decompressing the gzip file, you should obtain a file called prosa.qcow, a disk image that can be imported with VirtualBox. For further instructions on how to boot the image, please check this tutorial.

Before initializing the VM, make sure it has at least 2GB of allocated memory. If you need root privileges, note that the user login and password are both ‘prosa’.

Manual Installation (Skip if you use the VM)

If you skipped the VM installation and prefer to run Prosa in the system of your choice, please compile and install the following versions of Coq and Mathematical Components.

• Coq 8.5pl1
• Mathematical Components 1.6

The instructions we provide have been tested in the latest versions of Ubuntu and should work for other Linux distributions. For installation on Mac OSX and Windows, please refer to the Coq and Mathematical Components webpages.

Installing Coq

Start by decompressing coq-8.5pl1.tar.gz into some directory (e.g., ~/coq-8.5). Then, proceed with the installation using the provided Makefile.

$ cd ~/coq-8.5
$ make
$ sudo make install

The configure step should inform you about any missing packages (e.g., ocaml, camlp5). The package liblablgtk2-ocaml is not required, except if you decide to use Coq IDE.

After installing Coq, the aliases to the Coq utilities (e.g., coqc, coqchk, etc.) should be available in the PATH variable.

Installing Mathematical Components

After decompressing mathcomp-1.6.tar.gz into some directory (e.g., ~/mathcomp-1.6), use the Makefile for the installation. Since we use a small part of Mathematical Components, it suffices to install ssreflect only.

$ cd ~/mathcomp-1.6
$ cd mathcomp/ssreflect
$ make
$ sudo make install

After these steps, ssreflect can be readily imported by Coq source files.

2. Compiling Prosa

If there were no problems with the Coq installation, you should be able to run the Coq compiler coqc.

Start by opening the Terminal Emulator (available in Ubuntu menu). Then, create a directory, download Prosa and decompress the zip file.

$ mkdir ~/dev; cd ~/dev
$ wget http://prosa.mpi-sws.org/releases/v0.1/prosa_v01.zip
$ unzip prosa_v01.zip

Now move into Prosa’s directory and compile the entire source code. (Note that the Coq compiler has a large memory footprint, so we spawn only 4 Make threads. But feel free to add more if your VM has more than 2GB of RAM.)

$ cd ~/dev/prosa
$ make -j4

The compilation should take only a few minutes and return no errors. The purpose of the compilation is two-fold:

1. Coq successfully compiles the code only if every proof is correct, and

2. Coq generates corresponding binary files so that the definitions and proofs can be readily imported by other libraries.

The clean compilation already shows that there are no errors in the proofs. But for safety, we are going to perform additional checks, as discussed next.

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.

Running the Proof Checker

In order to run coqchk, please run the following commands on the terminal.

$ cd ~/dev/prosa
$ make validate

The verification process is different from the compilation since it does not import pre-compiled binaries but completely checks Prosa 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 predicativeTheory: Stratified type hierarchy
  
*Axioms:
    mathcomp.ssreflect.finfun.FunFinfun.finfunE
    mathcomp.ssreflect.finfun.FunFinfun.fun_of_finE
    mathcomp.ssreflect.fintype.SubsetDef.subsetEdef
    mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef
    mathcomp.ssreflect.finfun.FunFinfun.fun_of_fin
    mathcomp.ssreflect.tuple.FinTuple.enumP
    mathcomp.ssreflect.tuple.FinTuple.enum
    mathcomp.ssreflect.bigop.BigOp.bigopE
    mathcomp.ssreflect.finfun.FunFinfun.finfun
    mathcomp.ssreflect.tuple.FinTuple.size_enum
    mathcomp.ssreflect.fintype.CardDef.card
    mathcomp.ssreflect.fintype.CardDef.cardEdef
    mathcomp.ssreflect.bigop.BigOp.bigop
    mathcomp.ssreflect.fintype.SubsetDef.subset
    mathcomp.ssreflect.fintype.Finite.EnumDef.enum

Analyzing the output

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 rt.* (the logical base directory of PROSA), which implies that there are no axioms or admitted proofs in our library.

The result of coqchk confirms that every proof in Prosa is correct. But note that this does not imply that we proved every result claimed in the paper. For that, we will perform manual checks.

4. Locating the Main Results of the Paper

In the paper, we claim to have formally verified some variations of Bertogna and Cirinei’s response-time analysis. Here we provide the complete list of contributions along with hyperlinks to the corresponding definitions and proofs in Prosa. For an easier navigation through the files, please check the code snippets.

If you would like to understand how the Prosa directory is organized, have a look at the table of contents.

Basic Sporadic Task Model (B)

This corresponds to the sporadic task model from the literature.

Interference Bounds

  B1) Definition of the interference bound for work-conserving schedulers (with slack updates).

  B2) Proof of correctness of the interference bound for work-conserving schedulers.

  B3) Definition of the interference bound for EDF scheduling (with slack updates).

  B4) Proof of correctness of the interference bound for EDF scheduling.

Response-time Bounds

  B5) Proof that any fixed point of Bertogna and Cirinei’s response-time recurrence for FP scheduling is a safe response-time bound.

  B6) Definition of Bertogna and Cirinei’s RTA for FP scheduling.

  B7) Proof of correctness of Bertogna and Cirinei’s RTA for FP scheduling.

  B8) Proof that any fixed point of Bertogna and Cirinei’s response-time recurrence for EDF scheduling is a safe response-time bound.

  B9) Definition of Strategy 2 of Bertogna and Cirinei’s RTA for EDF scheduling.

  B10) Proof of correctness of Strategy 2 of Bertogna and Cirinei’s RTA for EDF scheduling.

  B11) Proof that Strategy 2 of Bertogna and Cirinei’s response-time recurrence for EDF computes the least fixed point and thus dominates any other search strategy.

Implementation of Concrete Scheduler for Testing

  B12) Implementation of a periodic job arrival sequence. (Note that this implementation is just for testing the RTA procedures; all the schedulability analyses we verified apply to sporadic tasks.)

  B13) Implementation of a work-conserving scheduler.

  B14) Example of applying EDF RTA on a task set with three tasks. The absence of hypotheses in the proof of schedulability implies that there are no contradictory assumptions.

Sporadic Task Model with Release Jitter (J)

This model is similar to the sporadic task model, but with the additional constraint that each job incurs release jitter.

Interference Bounds

  J1) Definition of a jitter-aware interference bound for work-conserving schedulers (with slack updates).

  J2) Proof of correctness of the jitter-aware interference bound for work-conserving schedulers.

  J3) Definition of a jitter-aware interference bound for EDF scheduling (with slack updates).

  J4) Proof of correctness of the jitter-aware interference bound for EDF scheduling.

Response-time Bounds

  J5) Proof that any fixed point of jitter-aware Bertogna and Cirinei’s response-time recurrence for FP scheduling is a safe response-time bound.

  J6) Definition of jitter-aware Bertogna and Cirinei’s RTA for FP scheduling.

  J7) Proof of correctness of jitter-aware Bertogna and Cirinei’s RTA for FP scheduling.

  J8) Proof that any fixed point of jitter-aware Bertogna and Cirinei’s response-time recurrence for EDF scheduling is a safe response-time bound.

  J9) Definition of jitter-aware Bertogna and Cirinei’s RTA for EDF scheduling (similar to Strategy 2 of the basic analysis).

  J10) Proof of correctness of jitter-aware Bertogna and Cirinei’s RTA for EDF scheduling (similar to Strategy 2 of the basic analysis).

  J11) Proof that jitter-aware Bertogna and Cirinei’s RTA for EDF computes the least fixed point and thus dominates any other search strategy.

Implementation of Concrete Scheduler for Testing

  J12) Implementation of a periodic job arrival sequence that always incurs worst-case jitter. (Note that this implementation is just for testing the RTA procedures; all the schedulability analyses we verified apply to sporadic tasks.)

  J13) Implementation of a work-conserving scheduler.

  J14) Example of applying jitter-aware EDF RTA on a task set with three tasks. The absence of hypotheses in the proof of schedulability implies that there are no contradictory assumptions.

Sporadic Task Model with Parallel Jobs (P)

Differently from the basic task model, this model does not assume the constraint of job sequentiality.

Interference Bounds

  P1) Definition of a simplified interference bound for work-conserving schedulers with parallel jobs (with slack updates).

  P2) Proof of correctness of the interference bound for work-conserving schedulers with parallel jobs.

  P3) Definition of a simplified interference bound for EDF scheduling with parallel jobs (with slack updates).

  P4) Proof of correctness of the interference bound for EDF scheduling with parallel jobs.

Response-time Bounds

  P5) Proof that any fixed point of Bertogna and Cirinei’s response-time recurrence for FP scheduling with parallel jobs is a safe response-time bound.

  P6) Definition of Bertogna and Cirinei’s RTA for FP scheduling with parallel jobs.

  P7) Proof of correctness of Bertogna and Cirinei’s RTA for FP scheduling with parallel jobs.

  P8) Proof that any fixed point of Bertogna and Cirinei’s response-time recurrence for EDF scheduling with parallel jobs is a safe response-time bound.

  P9) Definition of Bertogna and Cirinei’s RTA for EDF scheduling with parallel jobs (similar to Strategy 2 of the basic analysis).

  P10) Proof of correctness Bertogna and Cirinei’s RTA for EDF scheduling with parallel jobs (similar to Strategy 2 of the basic analysis).

  P11) Proof that Bertogna and Cirinei’s RTA for EDF for parallel jobs computes the least fixed point and thus dominates any other search strategy.

5. Identifying Hypotheses

Another benefit of mechanized proofs is the complete control over the assumptions in each proof. As discussed in the paper, we favor fine-grained assumptions as a means to improve clarity and simplify future extensions (e.g., when working with different task models). Moreover, this fine granularity also allows the assumptions to be easily located.

To show how to visualize the assumptions in Prosa, we’ll search for those used in the correctness proof of Bertogna and Cirinei’s RTA for EDF scheduling. For this tutorial, we will do a manual search, but in the next releases of Prosa we plan to include in the distribution some dependency graph generator to automate this process (e.g., dpdgraph).

We begin by presenting the assumptions used in the RTA for the basic sporadic task model. After that, we discuss how those assumptions were changed to consider release jitter and parallel jobs.

Assumptions for Bertogna and Cirinei’s RTA for EDF

To locate the assumptions in the RTA for EDF scheduling, we just need to search the code for Hypothesis. But note that hypotheses only hold within the scope of the section enclosing each lemma/theorem statement. Based on that, you can now open the EDF RTA proof file in the section MainProof and notice the following assumptions for the analysis.

• Assumption 1: Jobs are not allowed to execute before their arrival times.

• Assumption 2: Jobs are not allowed to execute after completion.

• Assumption 3: All tasks in the task set have valid parameters (e.g., WCET and relative deadline both greater than zero).

• Assumption 4: The jobs in the arrival sequence also have valid parameters (e.g., Job ACET ≤ Task WCET).

• Assumption 5: There is at least one processor (recall that we need to divide the task interference by ‘m’).

• Assumption 6: Jobs are sequential (i.e., a single job cannot use multiple processors).

• Assumption 7: The scheduler is work-conserving (i.e., no processor remains idle if there are pending jobs).

• Assumption 8: The scheduler enforces EDF priority.

• Assumption 9: Since we implement the task set as a list, we assume it does not have duplicates.

• Assumption 10: All tasks have constrained deadlines.

• Assumption 11: All jobs in the schedule come from the task set (i.e., there are no other unexpected jobs to be scheduled).

• Assumption 12: Jobs have sporadic arrival times.

• Assumption 13: Since the RTA is a sufficient test, we only prove schedulability if the test succeeds.

Extension 1: Assuming that Jobs Incur Release Jitter

In order to incorporate release jitter into Bertogna and Cirinei’s RTA for EDF scheduling, we had to modify the following hypotheses from the basic task model (shown in the previous section). For context, please refer to the corresponding proof file.

• Assumption 1 was updated to enforce the constraint that jobs are only allowed to execute after the jitter has passed.

• Assumption 4 was updated to add job properties related to jitter (e.g., Job actual jitter ≤ Task worst-case jitter).

• Assumptions 7 and 8 were updated because the notions of work conservation and priority enforcement depend on the definition of pending job, which now considers release jitter.

Extension 2: Assuming Parallel Jobs

As can be seen in the proof file, the RTA for EDF scheduling with parallel jobs has exactly the same hypotheses as in the basic task model, except for Assumption 6 of job sequentiality.