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.

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.

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:

Coq successfully compiles the code only if every proof is correct, and
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:

incomplete proofs can be assumed to hold by calling the admit or Admitted commands, and
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:

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

B13) Implementation of a work-conserving scheduler.

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

J13) Implementation of a work-conserving scheduler.

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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

[Show code snippet]

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

[Show code snippet]

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.

[Show code snippet]

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.

Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.

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

Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.

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

Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.

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

Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

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

Hypothesis H_at_least_one_cpu : num_cpus > 0.

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

Hypothesis H_sequential_jobs: sequential_jobs sched.

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

Hypothesis H_work_conserving: work_conserving job_cost sched.

Assumption 8: The scheduler enforces EDF priority.

Hypothesis H_edf_policy: enforces_JLDP_policy job_cost sched (EDF job_deadline).

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

Hypothesis H_ts_is_a_set: uniq ts.

Assumption 10: All tasks have constrained deadlines.

Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.

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

Hypothesis H_all_jobs_from_taskset:
∀ (j: JobIn arr_seq), job_task j \in ts.

Assumption 12: Jobs have sporadic arrival times.

Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.

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

Hypothesis H_test_succeeds: edf_schedulable ts.

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.

Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter job_jitter sched.

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

Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.

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.

Hypothesis H_work_conserving: work_conserving job_cost job_jitter sched.
Hypothesis H_edf_policy: enforces_JLDP_policy job_cost job_jitter sched (EDF job_deadline).

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.