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-refinements
make
make install

Stepping through this Tutorial

This tutorial is actually a Coq file that can be found in the doc/tutorial.v file of Prosa's sources (as downloaded by the git command just above). So one can step through it with Coq and thus replay the examples and experiment with them while reading the tutorial. Once 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.

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

Print nat.
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.
Check 2.
S (S O)
     : nat
Unset Printing All.

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.

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.

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

  Print arrival_sequence.
arrival_sequence = instant -> seq Job
     : Type

At some point, the section can be closed

End ArrivalSequence.

The section variables no longer exist.

Fail Check Job.
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.

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

Note that Job is now a parameter of arrival_sequence. This Section mechanism is extensively used in Prosa to share common variables between multiple definitions.

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.

We've seen above that a function job_arrival 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 {ja : 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 {ja : 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 {ja : 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.

Print schedule.
schedule = 
fun (Job : JobType) (PState : ProcessorState Job) =>
instant -> PState
     : forall Job : JobType,
       ProcessorState Job -> Type

Arguments schedule {Job} _

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

Check scheduled_in.
scheduled_in
     : ?Job -> ?State -> bool
where
?Job : [ |- JobType]
?State : [ |- ProcessorState ?Job]

The above means that given a job j of some type ?Job, a processor state s of some type ?State, then scheduled_in j s is a boolean telling whether the job j is scheduled in state s.

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

Check service_in.
service_in
     : ?Job -> ?State -> work
where
?Job : [ |- JobType]
?State : [ |- ProcessorState ?Job]

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 : ProcessorState Job}.

  (** 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 {jc : JobCost Job}.
  Context {jd : JobDeadline Job}.
  Context {ja : 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.

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.

Print processor_state.
processor_state = 
fun Job : JobType =>
{|
  State := option Job;
  Core := unit_finType;
  scheduled_on :=
    fun (j : Job) (s : option Job) =>
    fun=> s == Some j;
  service_on :=
    fun (j : Job) (s : option Job) =>
    fun=> (if s == Some j then 1 else 0);
  service_on_implies_scheduled_on :=
    fun (j : Job) (s : option Job) =>
    fun=> [eta ideal.processor_state_obligation_1 Job
                 j s]
|}
     : forall Job : JobType, ProcessorState Job

Print option.
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 is idle. The function is_idle

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

Print TaskType.
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

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

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

Print TaskDeadline.
TaskDeadline = 
fun Task : TaskType => Task -> duration
     : TaskType -> Type
Print TaskCost.
TaskCost = 
fun Task : TaskType => Task -> duration
     : TaskType -> Type
Print TaskMinCost.
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,

Print task_cost_positive.
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 as 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.

Print all_jobs_from_taskset.
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/task/arrivals.v provides a few basic definitions about arrivals of jobs 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.

Print task_arrivals_between.
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.

Print sequential_tasks.
sequential_tasks = 
fun (Job : JobType) (Task : TaskType)
  (H : JobTask Job Task) (H0 : JobArrival Job)
  (H1 : JobCost Job) (PState : ProcessorState Job)
  (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 : ProcessorState Job,
       arrival_sequence Job -> schedule PState -> Prop

Arguments sequential_tasks {Job Task H H0 H1 PState} _
  _

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.

Print FP_policy.
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

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

Print JLFP_policy.
JLFP_policy = 
fun Job : JobType => rel Job
     : JobType -> Type
Print JLDP_policy.
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.

Print JobPreemptable.
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

Print valid_preemption_model.
valid_preemption_model = 
fun (Job : JobType) (H0 : JobCost Job)
  (H1 : JobPreemptable Job)
  (PState : ProcessorState Job)
  (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 : ProcessorState Job,
       arrival_sequence Job -> schedule PState -> Prop

Arguments valid_preemption_model {Job H0 H1 PState} _
  _

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 defines (min and max) arrival curves. The typeclass MaxArrivals gives the type of arrival curves.

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

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

Arrival 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

Print valid_arrival_curve.
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

Print respects_max_arrivals.
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.

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

Print respects_JLDP_policy_at_preemption_point.
respects_JLDP_policy_at_preemption_point = 
fun (Job : JobType) (H0 : JobArrival Job)
  (H1 : JobCost Job) (H2 : JobPreemptable Job)
  (jr : JobReady Job (processor_state Job))
  (arr_seq : arrival_sequence Job)
  (sched : schedule (processor_state Job))
  (policy : 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) (H0 : JobArrival Job)
         (H1 : JobCost Job),
       JobPreemptable Job ->
       JobReady Job (processor_state Job) ->
       arrival_sequence Job ->
       schedule (processor_state Job) ->
       JLDP_policy Job -> Prop

Arguments respects_JLDP_policy_at_preemption_point
  {Job H0 H1 H2 jr} _ _ _

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

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.

Print job_cost_positive.
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.

Print identical_prefix.
identical_prefix = 
fun (Job : JobType) (PState : ProcessorState Job)
  (sched sched' : schedule PState) (horizon : instant)
=> forall t : nat, t < horizon -> sched t = sched' t
     : forall (Job : JobType)
         (PState : ProcessorState Job),
       schedule PState ->
       schedule PState -> instant -> Prop

Arguments identical_prefix {Job PState} _ _ _

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 inextenso 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

Search scheduled_at service_at.
service_at_implies_scheduled_at:
  forall {Job : JobType} {PState : ProcessorState Job}
    (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 : ProcessorState Job}
    (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 : ProcessorState Job}
    (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

Search (service _ _ _ <= service _ _ _).
service_monotonic:
  forall {Job : JobType} {PState : ProcessorState Job}
    (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.

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} {PState : ProcessorState Job}.

  (** 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. *)
  Lemma service_monotonic : forall t1 t2, t1 <= t2 ->
    service sched j t1 <= service sched j t2.
Job: JobType
PState: ProcessorState Job
sched: schedule PState
j: Job
forall t1 t2 : nat,
t1 <= t2 -> service sched j t1 <= service sched j t2
  Proof.
Job: JobType
PState: ProcessorState Job
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.

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 jobs with bounded interference receive at least some amount of service is proved in analysis/abstract/lower_bound_on_service.v

The response time of tasks is defined as task_response_time_bound 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/ideal/abstract_seq_rta.v. offers a more precise theorem uniprocessor_response_time_bound_seq for sequential tasks.

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