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.

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.

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

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.

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.

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.

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.

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.

```
$ 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
```

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.

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.

This corresponds to the sporadic task model from the literature.

**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]

**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]

**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]

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

**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]

**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]

**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]

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

**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]

**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]

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.

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

Hypothesis H_valid_job_parameters:

∀ (j: JobIn arr_seq),

valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

∀ (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’).

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

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

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.

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

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

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