Built with Alectryon, running Coq+SerAPI v8.14.0+0.14.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.

A Tutorial on Prosa

Introduction

Prosa [Prosa] is a framework for formulating and validating definitions and proofs that have been developed in the context of the real-time scheduling theory. Prosa was proposed by the MPI-SWS institute, and the foundations of the framework have been implemented by this group. It was first introduced in the academic setting in 2016 [prosa_paper]. Prosa is now being improved and developed further as part of the RT-Proofs project [rt_proofs].

Prosa is based on the Coq proof assistant developed by INRIA [coq] and uses its functionalities to express and prove constructs from the real-time scheduling theory.

The main motivation for Prosa is the fact that many definitions and proofs that are available in the real-time scheduling theory are based on intuition and lack formal steps. As such, these constructs may have flaws. One of the most famous examples is related to the CAN bus analysis [Davis_CAN]. By using proof assistants, as in Prosa, the number of flaws in the real-time scheduling theory can be significantly reduced. Formal developments also offer other major advantages: for instance it is easier to build on top of proofs, they give a better understanding of assumptions and they dramatically ease the process of trying to remove a thought useless assumption, or even help discover them.

Therefore, it is in the common interest of the real-time community to use proof libraries such as Prosa. To that aim, the awareness of the real-time community regarding the existence of such tools should be raised. In this tutorial-style document, the first user experience of a researcher with a real-time background, but neither Coq nor Prosa background, will be documented. The aim of this document is twofold. First, it should help new Prosa users to become familiar with the tool and some of its features, so as to be able to understand and follow Prosa artifacts, as well as to be able to develop their own Prosa extensions. Second, it should help the Prosa developers to better understand the challenges that the new users might face, and take that into consideration when refactoring existing and developing new functionalities.

The description of Prosa constructs will be performed in such a way that each item will be covered after its constituting components were introduced. Therefore, in this tutorial description of Prosa, we first start with basic items, and then cover more complex ones. The content covered should be sufficient for readers to become familiar with Prosa, and after completing this document, readers should be able to understand and follow other Prosa artifacts that are not covered here. Readers interested in more advanced aspects of the scheduling theory and their implementation in Prosa should consult the Prosa source code itself which is highly documented in a literate programming style.

Audience

Real-Time specialist not familiar with Coq constitue the main audience of this document. It should also be of interest for readers acquainted to Coq but with less knowledge about real-time, although this is not the main audience.

Getting Started

In a first reading, it is possible to skip this part and go directly to the next one However, for a deeper understanding of the Prosa library, it is advisable to install the Coq system and interactively replay the examples proposed in this document. The current section thus provides some minimal information to get a working Coq environment. A priori knowledge of Coq is welcome but should not be needed to understand the current document as main concepts will be introduced on the fly.

Installing Coq

The easiest solution is to resort on the binary installers/packages provided by the Coq platform for Linux, MacOS and Windows. This will install both Coq and some common libraries, including all Prosa dependencies.

TODO: see whether we need to recommend installing Msys2 on Windows.

Installing a Coq interface

Coq programs/proofs are files, with the extension .v, that can be compiled by the Coq compiler coqc but Coq proof scripts are usually developped in an interactive way. Thus, one needs an editor or IDE with some Coq support. The user of Visual Studio Code can install its VSCoq extension whereas Emacs' users will enjoy the Proof General mode. Users not familiar with any of these editors can simply rely on the coqide tool installed by the Coq platform. A more detailled list of interfaces is available on Coq's website.

Learning about Coq

A priori knowledge of Coq should not be needed to understand the current document. However, the reader interested in going further and developing its own proofs will need some experience with the ssreflect tactic language used in Prosa. A good first reading is Part1 of the Mathematical Components book.

Getting Prosa

You can download the code of Prosa using git

git clone https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs.git

Compilation then proceeds as follows

./create_makefile.sh --without_classic
make
make install

Reading this Tutorial

This tutorial is actually a Coq file that can be downloaded at (TODO URL) so one can step through it with Coq and thus replay the examples and experiment with them while reading the tutorial. When Coq is installed, it is then advisable to download this file and step through it in your editor/IDE (essential keyboard shortcuts are C-c C-n, C-c C-u and C-c RET to go down, up ot to the cursor under Emacs, Alt-down, Alt-up or Alt-right under VSCode).

It is first needed to load a few libraries.

From mathcomp Require Import all_ssreflect.
Require Import prosa.util.notation.

Architecture of Prosa

Th code of the Prosa library is split in a few main directories:

  • behavior/ defines the behavior of real-time systems, as used in the remaining of the library. This set of basic definitions is meant to remain as small as possible and will be exhaustively covered in the behavior Section below.
  • model/ provides common specifications used by the real-time analyses proved in the remaining of the library. This is already larger and will be partially covered in the model Section below. Enough will be presented for this document to remain self contained.
  • analysis/ contains the proofs of real-time analyses themselves. This contains a lot of often very generic results.
  • results/ instantiates some of the above results in well known settings. That's the place to look to understand what kind of results are in Prosa or find your favorite analysis. The current document will focus on a specific analysis, namely fixed priority tasks on a fully preemptive uniprocessor.
  • implementation/ instantiates the above results for concrete inputs.
  • util/ contains generic mathematical results useful in the remaining of the library.
  • classic/ contains an old version of the library. Some results are not yet ported to the new version and remains available there. This part is outside the scope fo the current document.

Note that the following description and code listings correspond to the current version of Prosa publicly available on its git repository.

Behavior

The behavior/ directory of Prosa defines the behavior of real-time systems, as used in the remaining of the library. This set of basic definitions is meant to remain as small as possible, thus we exhaustively cover it here.

Notion of Time

A concept of time is vital in the real-time scheduling theory, and there exist two approaches:

  1. discrete time domain, and
  2. continuous time domain.

In the former approach, it is assumed a smallest atomic unit of time (typically assigned an integer value of 1), and all other timing constructs are specified as multiples of that atomic unit. In the latter approach, the premise of the atomic unit does not exist, and each process can have an arbitrary duration.

In Prosa, a concept of time is introduced in the file behavior/time.v in which one can read

Definition duration := nat.
Definition instant  := nat.

This means the notions of duration and time instant are both defined as the type nat of natural integers from the Coq standard library.

If one tries

Inductive nat : Set := O : nat | S : nat -> nat. Arguments S _%nat_scope

one can see that a natural number is inductively defined as O or the successor S of a natural number. For instance, 2 is defined as S (S O).

Set Printing All.
S (S O) : nat
Unset Printing All.

Note

The Set Printing All command allows to see the underlying representation, otherwise the much more convenient notation 2 is used.

Thus, in Prosa, time is discrete (1.). At each observable moment (instant), the time has an exact integer value. Moreover, the duration of any process can be described as a multiple of atomic time instants, where the value is equal to the difference between the time instant when the process finished and the time instant when the process started.

Jobs

In real-time theory, and in Prosa, jobs represent an instantaneous arrival of an amount of workload that has to be executed upon a selected resource. In the context of the uniprocessor scheduling theory (the focus of this tutorial), that would be a computation performed on a processor. In Prosa, the definition is stated in behavior/job.v.

Note

In Coq syntax, everything between (* and *) is a comment, ignored by Coq.

This file is reproduced below.

(** * Notion of a Job Type *)

(** Throughout the library we assume that jobs
    have decidable equality. *)
Definition JobType := eqType.

(** * Notion of Work *)

(** We define 'work' to denote the unit of service received or needed.
    In a real system, this corresponds to the number
    of processor cycles. *)
Definition work  := nat.

(** * Basic Job Parameters — Cost, Arrival Time,
    and Absolute Deadline *)

(** Definition of a generic type of parameter relating jobs
    to a discrete cost. *)
Class JobCost (Job : JobType) := job_cost : Job -> work.

(** Definition of a generic type of parameter for job_arrival. *)
Class JobArrival (Job : JobType) := job_arrival : Job -> instant.

(** Definition of a generic type of parameter relating jobs
    to an absolute deadline. *)
Class JobDeadline (Job : JobType) := job_deadline : Job -> instant.

TODO : very short explanation about Class and typeclasses

From the above listing we can see that job is an entity with several parameters:

  1. job_arrival is the time instant when the job arrived to the system,
  2. job_cost is the amount of time that a job requires to be fully processed (a computation time in the context of uniprocessors), also called the job execution time,
  3. job_deadline is a deadline of a job.

Job Arrivals

The arrival of jobs to the system is covered in behavior/arrival_sequence.v. Of importance is the definition of arrival_sequence.

Let's first introduce here the Section mechanism of Coq, when typing

Section ArrivalSequence.

Coq starts a Section (called ArrivalSequence here, but that name only serves a documentation purpose) in which one can add variables

  (** Given any job type with decidable equality, ... *)
  Variable Job: JobType.

which can be used in further definitions in the section

  (** ..., an arrival sequence is a mapping from any time to a (finite)
      sequence of jobs. *)
  Definition arrival_sequence := instant -> seq Job.

note that currently, arrival sequence is exactly the stated definition

  
arrival_sequence = instant -> seq Job : Type

At some point, the section can be closed

End ArrivalSequence.

The section variables no longer exist.

The command has indeed failed with message: The reference Job was not found in the current environment.

But all objects defined in the section remain accessible as they are automatically generalized with respect to the section variables they refer to.

arrival_sequence = fun Job : JobType => instant -> seq Job : JobType -> Type

Note that Job is now a parameter of arrival_sequence.

Arrival sequences map individual time instants to finite sequences of jobs, where each sequence, associated to some time instant t, contains all jobs that arrive at t. In the context of individual jobs, several definitions are available

Section JobProperties.

  (** Consider any job arrival sequence. *)
  Context {Job: JobType}.
  Variable arr_seq: arrival_sequence Job.

  (** First, we define the sequence of jobs arriving at time t. *)
  Definition arrivals_at (t : instant) := arr_seq t.

  (** Next, we say that job j arrives at a given time t
      iff it belongs to the corresponding sequence. *)
  Definition arrives_at (j : Job) (t : instant) := j \in arrivals_at t.

  (** Similarly, we define whether job j arrives at some (unknown)
      time t, i.e., whether it belongs to the arrival sequence. *)
  Definition arrives_in (j : Job) := exists t, j \in arrivals_at t.

End JobProperties.

TODO short explanation on Context and implicit arguments

We've seen above that a function JobArrival can map any job to its arrival time, we thus need a way to state that an arrival sequence is consistent with such a function. This is expressed by the following definitions:

Section ValidArrivalSequence.

  (** Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (** Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

  (** We say that arrival times are consistent if any job that arrives
      in the sequence has the corresponding arrival time. *)
  Definition consistent_arrival_times :=
    forall j t,
      arrives_at arr_seq j t -> job_arrival j = t.

  (** We say that the arrival sequence is a set iff it doesn't contain
      duplicate jobs at any given time. *)
  Definition arrival_sequence_uniq :=
    forall t, uniq (arrivals_at arr_seq t).

  (** We say that the arrival sequence is valid iff it is a set
      and arrival times are consistent *)
  Definition valid_arrival_sequence :=
    consistent_arrival_times /\ arrival_sequence_uniq.

End ValidArrivalSequence.

For a given JobArrival, one can state a few additional definitions about individual jobs.

Section ArrivalTimeProperties.

  (** Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (** Let j be any job. *)
  Variable j: Job.

  (** We say that job j has arrived at time t iff it arrives
      at some time t_0 with t_0 <= t. *)
  Definition has_arrived (t : instant) := job_arrival j <= t.

  (** Next, we say that job j arrived before t iff it arrives
      at some time t_0 with t_0 < t. *)
  Definition arrived_before (t : instant) := job_arrival j < t.

  (** Finally, we say that job j arrives between t1 and t2
      iff it arrives at some time t with t1 <= t < t2. *)
  Definition arrived_between (t1 t2 : instant) :=
    t1 <= job_arrival j < t2.

End ArrivalTimeProperties.

Whereas when given an arrival_sequence, one can extract sequences of jobs arriving in some time interval.

Section ArrivalSequencePrefix.

  (** Assume that job arrival times are known. *)
  Context {Job: JobType}.
  Context `{JobArrival Job}.

  (** Consider any job arrival sequence. *)
  Variable arr_seq: arrival_sequence Job.

  (** By concatenation, we construct the list of jobs that arrived
      in the interval <<[t1, t2)>>. *)
  Definition arrivals_between (t1 t2 : instant) :=
    \cat_(t1 <= t < t2) arrivals_at arr_seq t.

  (** Based on that, we define the list of jobs that arrived
      up to time t, ...*)
  Definition arrivals_up_to (t : instant) := arrivals_between 0 t.+1.

  (** ... the list of jobs that arrived strictly before time t, ... *)
  Definition arrivals_before (t : instant) := arrivals_between 0 t.

  (** ... and the list of jobs that arrive in the interval
      <<[t1, t2)>> and satisfy a certain predicate [P]. *)
  Definition arrivals_between_P (P : Job -> bool) (t1 t2 : instant) :=
    [seq j <- arrivals_between t1 t2 | P j].

End ArrivalSequencePrefix.

Schedule

As already mentioned, jobs execute upon resources. In our uniprocessor case, that would relate to jobs executing on a processor. Since there may exist multiple jobs that require execution, while a processor can provide service to only one of them, job executions must be scheduled. In the context of job scheduling, jobs pass through different states. For example, a job can be not released yet, or released but without any service received from the processor yet, fully executed, etc.

The file behavior/schedule.v. defines a very generic notion of ProcessorState and schedule. It is worth noting that a schedule is a function from time instants to processor states.

Require Import prosa.behavior.schedule.

schedule = fun PState : Type => instant -> PState : Type -> Type Arguments schedule _%type_scope

Processor states returned by the schedule can then be inspected to know whether a given job is scheduled in this state

scheduled_in : ?Job -> ?State -> bool where ?Job : [ |- JobType] ?State : [ |- Type] ?H : [ |- ProcessorState ?Job ?State]

The above means that given a job j of some type ?Job, a processor state s of some type ?State such that there is some proof ?H that ?State is a processor state, then scheduled_in j s is a boolean telling whether the job j is scheduled in state s. In practice, the proof ?H will be automagically infered through the typeclass mechanism of Coq.

The amount of service given to a job is a processor state is defined similarly

service_in : ?Job -> ?State -> work where ?Job : [ |- JobType] ?State : [ |- Type] ?H : [ |- ProcessorState ?Job ?State]

Service

Equipped with this definitions, the file behavior/service.v gives basic definitions on the service received by a job.

Section Service.

  (** * Service of a Job *)

  (** Consider any kind of jobs and any kind of processor state. *)
  Context {Job : JobType} {PState : Type}.
  Context `{ProcessorState Job PState}.

  (** Consider any schedule. *)
  Variable sched : schedule PState.

  (** First, we define whether a job [j] is scheduled
      at time [t], ... *)
  Definition scheduled_at (j : Job) (t : instant) :=
    scheduled_in j (sched t).

  (** ... and the instantaneous service received by job j
      at time t. *)
  Definition service_at (j : Job) (t : instant) :=
    service_in j (sched t).

  (** Based on the notion of instantaneous service, we define the
      cumulative service received by job j during any interval from [t1]
      until (but not including) [t2]. *)
  Definition service_during (j : Job) (t1 t2 : instant) :=
    \sum_(t1 <= t < t2) service_at j t.

  (** Using the previous definition, we define the cumulative service
      received by job [j] up to (but not including) time [t]. *)
  Definition service (j : Job) (t : instant) := service_during j 0 t.

as well as the notion of completion of a job

  (** In the following, consider jobs that have a cost, a deadline,
      and an arbitrary arrival time. *)
  Context `{JobCost Job}.
  Context `{JobDeadline Job}.
  Context `{JobArrival Job}.

  (** We say that job [j] has completed by time [t] if it received all
      required service in the interval from [0] until
      (but not including) [t]. *)
  Definition completed_by (j : Job) (t : instant) :=
    service j t >= job_cost j.

  (** We say that job [j] completes at time [t] if it has completed
      by time [t] but not by time [t - 1]. *)
  Definition completes_at (j : Job) (t : instant) :=
    ~~ completed_by j t.-1 && completed_by j t.

of response time bound

  (** We say that a constant [R] is a response time bound of a job [j]
      if [j] has completed by [R] units after its arrival. *)
  Definition job_response_time_bound (j : Job) (R : duration) :=
    completed_by j (job_arrival j + R).

  (** We say that a job meets its deadline if it completes by
      its absolute deadline. *)
  Definition job_meets_deadline (j : Job) :=
    completed_by j (job_deadline j).

and of pending jobs

  (** Job [j] is pending at time [t] iff it has arrived
      but has not yet completed. *)
  Definition pending (j : Job) (t : instant) :=
    has_arrived j t && ~~ completed_by j t.

  (** Job [j] is pending earlier and at time [t] iff it has arrived
      before time [t] and has not been completed yet. *)
  Definition pending_earlier_and_at (j : Job) (t : instant) :=
    arrived_before j t && ~~ completed_by j t.

  (** Let's define the remaining cost of job [j] as the amount
      of service that has yet to be received for it to complete. *)
  Definition remaining_cost j t :=
    job_cost j - service j t.

End Service.

Similarly, one can find in file behavior/ready.v the definitions of ready and backlogged jobs as well as a characterization of valid schedules with respect to job arrivals costs and arrival sequences.

Finally, the behavior/all.v file provides a simple way to load all the above definitions by just typing

Require Import prosa.behavior.all.

Model

The model/ directory of Prosa provides common specifications used by the real-time analyses proved in the remaining of the library. This directory is larger than the pprevious behavior/ directory. It will then be only partially covered here, so that this document remains self-contained. The material detailled below should however be enough to get a good grasp of the kind of things formalized in this model/ directory.

Ideal Uniprocessor

The file model/processor/ideal.v defines ideal uniprocessors as processors that are at each instant either idle or executing a single job. To do this, a processor state, as introduced in schedule above, is defined using the option type of Coq's standard library

Require Import prosa.model.processor.ideal.

processor_state = fun Job : JobType => option Job : JobType -> Type
Inductive option (A : Type) : Type := Some : A -> option A | None : option A. Arguments option _%type_scope Arguments Some {A}%type_scope a (where some original arguments have been renamed) Arguments None {A}%type_scope

A value of type option Job is either Some j with j of type Job or None, respectively meaning that the processor is executing job j or idle. The function is_idle

is_idle : schedule (processor_state ?Job) -> instant -> bool where ?Job : [ |- JobType]

is then defined as the function which, given a schedule and an instant, tells whether the processor is idle in the given schedule at the given instant.

Concept of Task

The file model/task/concept.v defines the concept of task. A task is simply defined as a type with decidable equality.

Require Import model.task.concept.

TaskType = eqType : Type

Then, a few typeclasses are defined to be able to express the main characteristics of tasks. First, each job can be assigned to a task

JobTask = fun (Job : JobType) (Task : TaskType) => Job -> Task : JobType -> TaskType -> Type

Three other classes are defined for task deadlines, cost and minimum cost.

TaskDeadline = fun Task : TaskType => Task -> duration : TaskType -> Type
TaskCost = fun Task : TaskType => Task -> duration : TaskType -> Type
TaskMinCost = fun Task : TaskType => Task -> duration : TaskType -> Type

Then a bunch of validity hypothesis that usually apply to the above definitions are defined. For instance,

task_cost_positive = fun (Task : TaskType) (H : TaskCost Task) (tsk : Task) => 0 < task_cost tsk : forall Task : TaskType, TaskCost Task -> Task -> bool Arguments task_cost_positive {Task H} _

One can look at the ModelValidity Section in model/task/concept.v for the complete list. Those hypothesis usually need to be assumed whenever assuming any instance of the above typeclasses, otherwise they usually don't mean anything.

Finally, task sets are defined are sequences of tasks. This is used to express the fact that all jobs in an arrival sequence come from a given finite set of tasks.

all_jobs_from_taskset = fun (Task : TaskType) (Job : JobType) (H0 : JobTask Job Task) (arr_seq : arrival_sequence Job) (ts : TaskSet Task) => forall j : Job, arrives_in arr_seq j -> job_task j \in ts : forall (Task : TaskType) (Job : JobType), JobTask Job Task -> arrival_sequence Job -> TaskSet Task -> Prop Arguments all_jobs_from_taskset {Task Job H0} _ _

Task Arrivals

The file model/priority/classes.v provides a few basic definitions about ariivals of job of a given task. For instance, given an arrival sequence arr_seq, a task tsk and two instants t1 and t2, then task_arrivals_between arr_seq tsk t1 t2 is the set of all jobs of task tsk arriving between t1 and t2 in arr_seq.

Require Import prosa.model.task.arrivals.

task_arrivals_between = fun (Job : JobType) (Task : TaskType) (H : JobTask Job Task) (arr_seq : arrival_sequence Job) (tsk : Task) (t1 t2 : instant) => [seq j <- arrivals_between arr_seq t1 t2 | job_of_task tsk j] : forall (Job : JobType) (Task : TaskType), JobTask Job Task -> arrival_sequence Job -> Task -> instant -> instant -> seq Job Arguments task_arrivals_between {Job Task H} _ _ _ _

Task Sequentiality

The file model/task/sequentiality.v defines the notion of sequential tasks. A task is called sequential when all its jobs execute in a non overlapping manner. This is formally defined in

Require Import prosa.model.task.sequentiality.

sequential_tasks = fun (Job : JobType) (Task : TaskType) (H : JobTask Job Task) (H0 : JobArrival Job) (H1 : JobCost Job) (PState : Type) (H2 : ProcessorState Job PState) (arr_seq : arrival_sequence Job) (sched : schedule PState) => forall (j1 j2 : Job) (t : instant), arrives_in arr_seq j1 -> arrives_in arr_seq j2 -> same_task j1 j2 -> job_arrival j1 < job_arrival j2 -> scheduled_at sched j2 t -> completed_by sched j1 t : forall (Job : JobType) (Task : TaskType), JobTask Job Task -> JobArrival Job -> JobCost Job -> forall PState : Type, ProcessorState Job PState -> arrival_sequence Job -> schedule PState -> Prop Arguments sequential_tasks {Job Task H H0 H1} {PState}%type_scope {H2} _ _

Priority Classes

The file model/priority/classes.v defines main classes of priority policies. In this document, we are interested in Fixed Priority (FP) policies, defined by the typeclass

Require Import prosa.model.priority.classes.

FP_policy = fun Task : TaskType => rel Task : TaskType -> Type

A fixed priority policy is indeed defined as a relation on tasks. The relation is called

hep_task : rel ?Task where ?Task : [ |- TaskType] ?FP_policy : [ |- FP_policy ?Task]

for Higher or Equal Priority. If tsk1 and tsk2 are tasks, then hep_task tsk1 tsk2 means that tsk1 has higher (or equal) priority than tsk2.

The two other classes provided are Job Level Fixed Priority (JLFP) and Job Level Dynamic Priority (JLDP).

JLFP_policy = fun Job : JobType => rel Job : JobType -> Type
JLDP_policy = fun Job : JobType => instant -> rel Job : JobType -> Type

The first one is a relation between jobs, whereas the second one associates to each instant a (potentially) different relation.

Two type class instances are then defined to automatically build a JLFP from a FP (associating the same priority for all jobs in a same task) and to build a JLDP from a JLFP (associating the same relation to each instant).

The remaining of the file provides the definitions of some common hypotheses on priority policies, in particular reflexivity and transitivity or the fact that a priority is total.

Preemption

The file model/preemption/parameter.v defines the notion of preemption.

In Prosa, the various preemption models are represented with a single predicate

Require Import prosa.model.preemption.parameter.

JobPreemptable = fun Job : JobType => Job -> work -> bool : JobType -> Type

that indicates, given a job and a degree of progress, whether the job is preemptable at its current point of execution.

The validity conditions of a preemption model are then defined

valid_preemption_model = fun (Job : JobType) (H0 : JobCost Job) (H1 : JobPreemptable Job) (PState : Type) (H3 : ProcessorState Job PState) (arr_seq : arrival_sequence Job) (sched : schedule PState) => forall j : Job, arrives_in arr_seq j -> job_cannot_become_nonpreemptive_before_execution j /\ job_cannot_be_nonpreemptive_after_completion j /\ not_preemptive_implies_scheduled sched j /\ execution_starts_with_preemption_point sched j : forall Job : JobType, JobCost Job -> JobPreemptable Job -> forall PState : Type, ProcessorState Job PState -> arrival_sequence Job -> schedule PState -> Prop Arguments valid_preemption_model {Job H0 H1} {PState}%type_scope {H3} _ _

A fully preemptive job is then defined as a job that is always preemptable in file model/preemption/fully_preemptive.v.

The preemption model for tasks is slightly more elaborate. The details can be found in file model/task/preemption/parameters.v. and the fully preemptive implementation lies in model/task/preemption/fully_preemptive.v.

Arrival Curves

The file model/task/arrival/curves.v.

The typeclass MaxArrivals gives the type of arrival curves.

Require Import prosa.model.task.arrival.curves.

MaxArrivals = fun Task : TaskType => Task -> duration -> nat : TaskType -> Type

Arrivals curves associate to each task and duration a natural number. This number will be the maximum number of jobs of the given task that can arrive in any interval of time of the given duration.

Valid arrival curves are the functions that start at 0 and are monotone

valid_arrival_curve = fun num_arrivals : duration -> nat => num_arrivals 0 = 0 /\ monotone leq num_arrivals : (duration -> nat) -> Prop Arguments valid_arrival_curve _%function_scope

Finally, the semantics of arrival curves, is given by

respects_max_arrivals = fun (Task : TaskType) (Job : JobType) (H : JobTask Job Task) (arr_seq : arrival_sequence Job) (tsk : Task) (max_arrivals : duration -> nat) => forall t1 t2 : instant, t1 <= t2 -> number_of_task_arrivals arr_seq tsk t1 t2 <= max_arrivals (t2 - t1) : forall (Task : TaskType) (Job : JobType), JobTask Job Task -> arrival_sequence Job -> Task -> (duration -> nat) -> Prop Arguments respects_max_arrivals {Task Job H} _ _ _%function_scope

In the same file, one can find similar definitions for minimal arrival curves, as well as min and max separations.

Schedule Model

In file model/schedule/preemption_time.v, the notion of preemption time in a schedule is defined according to the scheduled job at each instant, if any.

Require Import prosa.model.schedule.preemption_time.

preemption_time = fun (Job : JobType) (H : JobPreemptable Job) (sched : schedule (processor_state Job)) (t : instant) => match sched t with | Some j => job_preemptable j (service sched j t) | None => true end : forall Job : JobType, JobPreemptable Job -> schedule (processor_state Job) -> instant -> bool Arguments preemption_time {Job H} _ _

This allows to, finally, define what it means for a schedule to respect a given priority policy in file model/schedule/priority_driven.v

Require Import prosa.model.schedule.priority_driven.

respects_policy_at_preemption_point = fun (Job : JobType) (H2 : JobPreemptable Job) (H3 : ProcessorState Job (processor_state Job)) (H4 : JobCost Job) (H5 : JobArrival Job) (H6 : JobReady Job (processor_state Job)) (arr_seq : arrival_sequence Job) (sched : schedule (processor_state Job)) (H7 : JLDP_policy Job) => forall (j j_hp : Job) (t : instant), arrives_in arr_seq j -> preemption_time sched t -> backlogged sched j t -> scheduled_at sched j_hp t -> hep_job_at t j_hp j : forall Job : JobType, JobPreemptable Job -> forall (H3 : ProcessorState Job (processor_state Job)) (H4 : JobCost Job) (H5 : JobArrival Job), JobReady Job (processor_state Job) -> arrival_sequence Job -> schedule (processor_state Job) -> JLDP_policy Job -> Prop Arguments respects_policy_at_preemption_point {Job H2 H3 H4 H5 H6} _ _ {H7}

This means that when a job j is backlogged at some preemption instant, all scheduled jobs at that instant have higher or equal priority.

Analysis

The analysis/ directory contains the proofs of real-time analyses themselves. Even more than pen&paper proofs, formal proofs need to be appropriately factored out into small reusable lemmas. Thus, the analysis/ directory also contains many basic lemmas about all the definitions introduced above. Since this document only attempts to present a specific analysis, namely fixed priority tasks on a fully preemptive uniprocessor, we only introduce here the lemmas used in that analysis. However, at the end of the section, the reader should be able to navigate herself through all the lemmas of the directory.

First Lemmas

Some definitions are used only internally into analysis/, thus they aren't located in behavior/ nor model/. Among them, let's mention

Require Import prosa.analysis.definitions.job_properties.

job_cost_positive = fun (Job : JobType) (H : JobCost Job) (j : Job) => 0 < job_cost j : forall Job : JobType, JobCost Job -> Job -> bool Arguments job_cost_positive {Job H} _

and

Require Import prosa.analysis.definitions.schedule_prefix.

identical_prefix = fun (PState : Type) (sched sched' : schedule PState) (horizon : instant) => forall t : nat, t < horizon -> sched t = sched' t : forall PState : Type, schedule PState -> schedule PState -> instant -> Prop Arguments identical_prefix {PState}%type_scope _ _ _

Equipped with all these definitions, we can finally introduce our first lemmas. The files in the directory analysis/facts/behavior/ contain many lemmas establishing basic facts about all the definitions introduced in the behavior section above. The user can load all those lemmas by simply requiring

Require Import prosa.analysis.facts.behavior.all.

The files in analysis/facts/behavior/ are developed in a literate programming style like the remaining of Prosa. Thus, they can be read ine xtenso like any other file in the library. However, lemmas are mostly made to be used inside proofs and such reading is a very ineffective way to find the lemma one needs when carrying a proof. Indeed, once one gets a Coq interface up and running, it is much more convenient to just load the files with the above Require command and use the Search utility of Coq. For instance, to find all lemmas about scheduled_at and service_at, one can type

service_at_implies_scheduled_at: forall {Job : JobType} {PState : Type} {H : ProcessorState Job PState} (sched : schedule PState) (j : Job) (t : instant), 0 < service_at sched j t -> scheduled_at sched j t
not_scheduled_implies_no_service: forall {Job : JobType} {PState : Type} {H : ProcessorState Job PState} (sched : schedule PState) (j : Job) (t : instant), ~~ scheduled_at sched j t -> service_at sched j t = 0
no_service_not_scheduled: forall {Job : JobType} {PState : Type} {H : ProcessorState Job PState} (sched : schedule PState) (j : Job), ideal_progress_proc_model PState -> forall t : instant, ~~ scheduled_at sched j t <-> service_at sched j t = 0

The Search command can also be used with a pattern, for instance to look for lemmas of the shape service at some point <= service at some other point, one can type

service_monotonic: forall {Job : JobType} {PState : Type} {H : ProcessorState Job PState} (sched : schedule PState) (j : Job) (t1 t2 : nat), t1 <= t2 -> service sched j t1 <= service sched j t2

The Search command is even more powerful, as documented in Coq's reference manual.

Note

The reference manual of Coq is of high quality nowadays. It is a good first place to learn about the details of any Coq feature.

Back to the service_monotonic lemma found above, if one looks in the file analysis/facts/behavior/service.v, one will find the following text

(** We establish a basic fact about the monotonicity of service. *)
Section Monotonicity.

  (** Consider any job type and any processor model. *)
  Context {Job: JobType}.
  Context {PState: Type}.
  Context `{ProcessorState Job PState}.

  (** Consider any given schedule... *)
  Variable sched: schedule PState.

  (** ...and a given job that is to be scheduled. *)
  Variable j: Job.

  (** We observe that the amount of service received
      is monotonic by definition. *)
  
Job: JobType
PState: Type
H: ProcessorState Job PState
sched: schedule PState
j: Job

forall t1 t2 : nat, t1 <= t2 -> service sched j t1 <= service sched j t2
Job: JobType
PState: Type
H: ProcessorState Job PState
sched: schedule PState
j: Job

forall t1 t2 : nat, t1 <= t2 -> service sched j t1 <= service sched j t2
by move=> t1 t2 ?; rewrite -(service_cat _ _ t1 t2)// leq_addr. Qed. End Monotonicity.

The whole Section business should now be familiar to the reader. The Lemma keyword is new. It is used to introduce a lemma, followed by its name, a colon sign and the statement of the result itself, ending with a dot, as any Coq sentence. The cryptic line between Proof and Qed can be ignored for now. It instructs Coq how to perform the proof of the previously stated lemma. The only thing to notice is that this proof is terminated by a Qed (for the latin words "Quod Erat Demonstrandum") meaning that, if Coq can compile the Qed it managed to check the proof and the new lemma is now available for use in future proofs.

Note

Naming lemmas is a delicate business. Some libraries have very specific and elaborated naming schemes, usually based on the statement of the theorem itself. Although there is no such strict naming scheme in Prosa, one can find a few generic advices in doc/guidelines.md.

Note

Coq has many synonyms of Lemma. The commands Lemma, Theorem, Fact, Remark, Corollary and Proposition all behave in the exact same way. The user is free to choose any of them to better comment her code.

Similarly to behavior, the files ideal_schedule.v, task_arrivals.v, sequential.v, service_of_jobs.v, preemption.v and workload.v, in the analysis/facts/model/ directory provide basic lemmas about definitions introduced in the model section above.

The files job/preemptive.v, task/preemptive.v, rtc_threshold/job_preemptable.v and rtc_threshold/preemptive.v, in the analysis/facts/preemption/ directory provide basic lemmas about preemption.

Readiness

The file analysis/definitions/readiness.v contains definitions of nonclairvoyant_readiness and nonpreemptive_readiness while the file analysis/definitions/work_bearing_readiness.v defines work_bearing_readiness. Basic facts about the sequential task readiness model can be found in analysis/facts/readiness/sequential.v.

Busy Intervals

Busy Intervals constitute a central tool in classic real time analyses. They are defined in definitions/busy_interval.v and definitions/priority_inversion.v and basic lemmas about them are to be found in facts/busy_interval/busy_interval.v and facts/busy_interval/priority_inversion.v.

Abstract RTA

The directory analysis/abstract/ contains proofs of classic real time analyses in a setting as abstract as possible. These proofs will later be instantiated in more concrete settings.

First, a few more definitions are needed and can be found in the file analysis/abstract/definitions.v

Then the notion of search space is exploited to refine the set of behaviors that can exhibit worst case response times. These results can be found in analysis/abstract/search_space.v

The fact that jobs that run to completion are non preemptive is studied in analysis/abstract/run_to_completion.v

The schedulability of tasks is defined in analysis/definitions/schedulability.v which enables to state and prove the main theorem uniprocessor_response_time_bound in analysis/abstract/abstract_rta.v. Basically, this theorem states that under a bunch of hypotheses, if some R satisfies the inequality in hypothesis H_R_is_maximum, then R is a response time bound.

The file analysis/abstract/abstract_seq_rta.v. offers a more precise theorem uniprocessor_response_time_bound_seq for sequential tasks.

Finally, the file analysis/abstract/ideal_jlfp_rta.v. provides lemmas for Job Level Fixed Priority policies for ideal uniprocessors.

Results

The results/ directory instantiates some of the above results in well known settings. The current document will focus on a specific analysis, namely fixed priority tasks on a fully preemptive uniprocessor. The main result lies in the file results/fixed_priority/rta/fully_preemptive.v. After about hundred lines to state the fixed priority fully preemptive setting on ideal uniprocessors (this could probably be way shorter, were the definitions more structured, but Prosa choses a flat model with lot of individual hypotheses, so they have to be all stated oone by one), the main hypothesis are the ones about L and R and they enable to prove the theorem uniprocessor_response_time_bound_fully_preemptive_fp that simply states that R is a response time bound.

Contributing

The reader should now be able to navigate through the extensive documentation of the Prosa library. The library being developped in a literate programming style, one can simply read the source files, although when looking for precise results, the querying commands of Coq Check, Print, About and Search can be of great help (particularly considering that Prosa makes extensive use of the Section mechanism which may sometimes obfuscate what are the exact hypotheses of a given lemma).

Prosa follows an open source development process. Contributions are welcomed, as stated at the end of its README.

References

[Prosa]MPI-SWS Germany. Formally proven schedulability analysis PROSA. http://prosa.mpi-sws.org/
[prosa_paper]
  1. Cerqueira, F. Stutz, and B. B. Brandenburg. PROSA: A Case for Readable Mechanized Schedulability Analysis. In ECRTS 2016, 2016.
[coq]Inria France. The Coq Proof Assistant. http://coq.inria.fr/
[Davis_CAN]Robert I. Davis, Alan Burns, Reinder J. Bril, and Johan J. Lukkien. Controller Area Network (CAN) schedulability analysis: Refuted, revisited and revised. Real-Time Systems, 2007.
[rt_proofs]INRIA, MPI-SWS, Onera, TU Braunschweig, and Verimag. RT-Proofs Formal Proofs for Real-Time Systems. Funded by ANR/DFG, 2018 - 2020. http://rt-proofs.inria.fr/