A Generic Coq Proof of Typical Worst-Case Analysis

1. Overview

We present here the Coq definitions and proofs corresponding to our paper “A Generic Coq Proof of Typical Worst-Case Analysis” to be presented at RTSS’18. The paper presents a generic proof of Typical Worst-Case Analysis (TWCA), an analysis technique for weakly-hard real-time uniprocessor systems. Our generic analysis is based on an abstract model that characterizes the exact properties needed to make TWCA applicable.

Note that our work is built to be as compatible as possible with the Prosa library: we structure and document our development following the Prosa guidelines, we share the relevant parts of the formalization (as described in the Prosa paper) and tried to reuse proofs as much as possible. Our goal is to integrate our work to the library in the near future. In the meantime, we provide a self-contained version of our contributions. The parts of our development taken, or adapted, from Prosa are documented as such in proof scripts.

2. Setting up the Coq formalization

In order to download and check our definitions and proofs, you have two options: manual installation or using a virtual machine (VM). Unless you are familiar with Coq, we advise you to use the VM.

A. Using a Virtual Machine
  • First, you need VirtualBox to be installed on your system. If this is not the case, you can download it on the VirtualBox website.
  • You then need to download the packaged VM, available at https://files.inria.fr/spades/twcaproofs/GTWCA.ova.
  • In order to set up the VM you just have to double-click on the ova file. If this doesn’t work you can open the “File->Import Appliance” functionality of the VirtualBox GUI.
  • VirtualBox will then allow you to change the settings before importing the VM. The default settings (2048 MB of RAM and 1 CPU) are adequate to check the proofs. Clicking the import button will add the VM to your list of VirtualBox VMs.
  • You can now launch the VM from the VirtualBox GUI.
B. Alternative: Manual installation

You can also directly download the proof scripts and the generated documentation here. These proof scripts were written for the Coq proof assistant version 8.7.2 using the Mathematical Components library version 1.6.4. After extracting the files you should run the following command to generate the Makefile needed to check the proofs:

coq_makefile -f _CoqProject -o Makefile

3. Reading the Coq specification

The “src” folder (reachable through the “Proofs” shortcut on the desktop of the provided VM) contains the proof scripts (.v files) which can be opened and stepped through using the “coqide” tool. In order to read the specification you will need to understand the structure of sectioned proof scripts. The section mechanism of Coq allows us to present our results in a format closer to scientific prose. As an example, consider the following code snippet :

Section example.
  Variable x : nat.
  Hypothesis Hx : x > 2.
  Lemma xpos : x > 0.
  Proof.
    ...
  Qed.
End example.

This proof script contains a proof named “xpos” that for any natural number x, if x > 2 then x > 0. The ellipsis between “Proof.” and “Qed.” contains the proof of “xpos” which is checked by Coq.

Structure of the archive

The formalization is structured as follows:

  • util.v : Notations and arithmetic lemmas from the Prosa library
  • model.v : Definitions for traces, compatible with the definitions of Prosa
  • fpp.v : Definition and analysis of the system model used in Section II
  • typical.v : The generic TWCA presented in Section III
  • typical_fpp.v : Instantiation of TWCA to FPP as in Section IV

The documentation is automatically generated from the proof scripts using “coqdoc” and follows the same structure. The documentation files contain the whole specifications and theorem statements from the development but proofs are omitted for readability. The entry point to the documentation is the file html/toc.html (or using the “Documentation” link on the VM), also available online : https://files.inria.fr/spades/twcaproofs/toc.html

You can now locate the main results of the paper in the following locations.

Main results of the paper

The main results of the paper are the files typical.v and typical_fpp.v.

typical.v: This file contains the formal results related to the Generic Typical Worst Case Analysis (GTWCA)

  • The formalization of analyzable windows (Hypothesis 1) is given (for a task tsk) as 
    Variable aw : instant -> instant -> Prop.
Variable aw_left : instant -> instant.
Variable aw_right : instant -> instant.
Hypothesis aw_correct : forall t, aw (aw_left t) (aw_right t).
Hypothesis leq_aw_left : forall t, aw_left t <= t.
Hypothesis ltn_aw_right : forall t, t < aw_right t.
Hypothesis aw_uniq : forall t t1 t2 t1' t2',
  t1 <= t < t2 ->
  t1' <= t < t2' ->
  aw t1 t2 -> aw t1' t2' ->
  t1 = t1' /\ t2 = t2'.
  • The specification of the local analysis (Hypothesis 2) is 
    Definition local_bound_correct (N : local_bound) := forall t,
  count (deadline_miss sched) (task_arrivals_between arrs tsk (aw_left t) (aw_right t))
  <= N (c t).
  • The specification of the set of possible combinations (Hypothesis 3) is 
    Definition combinations_correct (Cs : combinations) := forall t,
  c t \in Cs.

    where c t is the analyzable window around time t

  • Theorem 1 (Deadline miss bound) is Lemma dm_correct 
    Lemma dm_correct : count (deadline_miss sched) Iarrs <= dm N Cs (C_occs t1 t2).
  • The specification of the constraint on abstract scenarios (Hypothesis 4) is 
    Hypothesis HP : forall t1 t2, P (t2 - t1) (C_occs t1 t2).

    where “C_occs t1 t2” is the analyzable window cover of interval [t1;t2[

  • Theorem 3 is Theorem dmm_bound 
    Theorem dmm_bound : forall (t : instant),
  count (deadline_miss sched) (task_arrivals_between arrs tsk t (dt + t)) 
  <= \sup_(X | P dt X) dm N Cs X.

typical_fpp.v: This file contains the instantiation of GTWCA to the Fixed Priority Preemptive scheduling policy with arrival curves as activation model.

  • The hypotheses related to the arrival model are 
    Hypothesis wcet_correct : wcet_correct task_wcet job_cost job_task arrs.
Hypothesis arrival_model :
  (forall tsk,
    tsk \in ts ->
    eta_plus_correct eta_plus job_task arrs tsk) /\
  (forall tsk,
    tsk \in ts ->
    typical_task tsk ->
    delta_plus_correct delta_plus job_task arrs tsk).
  • The hypotheses related to the scheduling policy are 
    Hypothesis work_conserving : work_conserving job_arrival job_cost arrs sched.
Hypothesis sched_fp : sched_fp hp job_task job_arrival job_cost arrs sched.
  • The main result is Theorem dmm_fpp 
    Theorem dmm_fpp : forall (t : instant) (dt : duration),
  size (task_arrivals_between tsk t (dt + t)) = k ->
  count deadline_miss (task_arrivals_between tsk t (dt + t)) <=
  \sup_( X | P tsk (delta_plus tsk k) X) dm ts (N tsk) (C_candidates tsk) X.

4. Checking the Coq proofs

A. Inside the Virtual Machine

From the “twca” folder you can run the following commands to have Coq check the proofs and print out any axioms used in our development and its dependencies.

make clean
make validate

After a few minutes you should only see a list of axioms from the Mathematical Components library as indicated by their “mathcomp” prefix. For more details about checking the validity of the proofs we refer the reader to the Prosa paper artifact evaluation section on checking the correctness of Coq proofs.

B. With a manual installation

To compile the proofs, after extracting the contents of the archive, run:

make

To regenerate the documentation :

make gallinahtml

You can then follow the instructions for the VM above for additional checks on the proofs.

Comments are closed.