Improve documentation in restructuring/behavior

Use coqdoc's header feature to make it easier to find key concepts and
improve/tweak a few comments.

README.md

@@ -4,6 +4,12 @@ This repository contains the main Coq specification & proof development of the [
 
 <center><img alt="RT-Proofs logo" src="http://prosa.mpi-sws.org/figures/rt-proofs-logo.png" width="300px"></center>
 
+## Documentation
+
+Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+
+- <https://prosa.mpi-sws.org/branches>
+
 ## Publications
 
 Please see the [list of publications](http://prosa.mpi-sws.org/documentation.html#publications) on the Prosa project's homepage. 
@@ -46,11 +52,6 @@ Second, compile the library.
 make -j
 ```
 
-## Documentation
-
-Up-to-date documentation for all branches of the main Prosa repository is available at <https://prosa.mpi-sws.org/branches>.
-
-
 ## Generating HTML Documentation
 
 The Coqdoc documentation (as shown on the [webpage](http://prosa.mpi-sws.org/documentation.html)) can be easily generated with the provided `Makefile`:

restructuring/behavior/arrival_sequence.v

@@ -2,7 +2,10 @@ From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
 From rt.restructuring.behavior Require Export time job.
 From rt.util Require Import notation.
 
-(** Definitions and properties of job arrival sequences. *)
+(** This module contains basic definitions and properties of job arrival
+    sequences. *)
+
+(** * Notion of an Arrival Sequence *)
 
 (** We begin by defining a job arrival sequence. *)
 Section ArrivalSequence.
@@ -15,6 +18,8 @@ Section ArrivalSequence.
 
 End ArrivalSequence.
 
+(** * Arrival of a Job *)
+
 (** Next, we define properties of jobs in a given arrival sequence. *)
 Section JobProperties.
 
@@ -35,6 +40,8 @@ Section JobProperties.
 
 End JobProperties.
 
+(** * Validity of an Arrival Sequence *)
+
 (** Next, we define valid arrival sequences. *)
 Section ValidArrivalSequence.
 
@@ -62,6 +69,8 @@ Section ValidArrivalSequence.
 
 End ValidArrivalSequence.
 
+(** * Arrival Time Predicates *)
+
 (** Next, we define properties of job arrival times. *)
 Section ArrivalTimeProperties.
 
@@ -86,6 +95,8 @@ Section ArrivalTimeProperties.
 
 End ArrivalTimeProperties.
 
+(** * Finite Arrival Sequence Prefixes *)
+
 (** In this section, we define arrival sequence prefixes, which are useful to
    define (computable) properties over sets of jobs in the schedule. *)
 Section ArrivalSequencePrefix.

restructuring/behavior/job.v

 From rt.restructuring.behavior Require Export time.
 From mathcomp Require Export eqtype ssrnat.
 
+(** * Notion of a Job Type *)
+
 (** Throughout the library we assume that jobs have decidable equality. *)
 Definition JobType := eqType.
 
+(** * Unit 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.
 

restructuring/behavior/ready.v

 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export service.
 
+(** * Readiness of a Job *)
 
 (** We define a general notion of readiness of a job: a job can be
    scheduled only when it is ready, as determined by the predicate
@@ -19,6 +20,8 @@ Class JobReady (Job : JobType) (PState : Type)
     _ : forall sched j t, job_ready sched j t -> pending sched j t;
   }.
 
+(** * Backlogged Jobs *)
+
 (** Based on the general notion of readiness, we define what it means to be
    backlogged, i.e., ready to run but not executing. *)
 Section Backlogged.
@@ -36,9 +39,11 @@ Section Backlogged.
 End Backlogged.
 
 
+(** * Validity of a Schedule *)
+
 (** With the readiness concept in place, we define the notion of valid schedules. *)
 Section ValidSchedule.
-  (** Consider any kinds of jobs and any kind of processor state. *)
+  (** Consider any kind of jobs and any kind of processor state. *)
   Context {Job : JobType} {PState : Type}.
   Context `{ProcessorState Job PState}.
 

restructuring/behavior/schedule.v

 From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export arrival_sequence.
 
-(** We define the notion of a generic processor state. The processor state type
-   determines aspects of the execution environment are modeled (e.g., overheads, spinning).
-   In the most simple case (i.e., Ideal.processor_state), at any time,
-   either a particular job is either scheduled or it is idle. *)
+(** * Generic Processor State *)
+
+(** Rather than choosing a specific schedule representation up front, we define
+    the notion of a generic processor state, which allows us to state general
+    definitions of core concepts (such as "how much service has a job
+    received") that work across many possble scenarios (e.g., ideal
+    uniprocessor schedules, schedules with overheads, variable-speed
+    processors, multiprocessors, etc.).
+
+    A concrete processor state type precisely determines how all relevant
+    aspects of the execution environment are modeled (e.g., scheduled jobs,
+    overheads, spinning). Here, we define just the common interface of all
+    possible concrete processor states by means of a "type class", i.e., we
+    define a few generic predicates and an invariant that must be defined by
+    all concrete processor state types.
+
+    In the most simple case (i.e., an ideal uniprocessor state), at any time,
+    either a particular job is scheduled or the processor is idle. *)
 Class ProcessorState (Job : JobType) (State : Type) :=
   {
     (** A [ProcessorState] instance provides a finite set of cores on which
@@ -31,7 +45,13 @@ Class ProcessorState (Job : JobType) (State : Type) :=
       forall j s, ~~ scheduled_in j s -> service_in j s = 0
   }.
 
-(** A schedule maps an instant to a processor state *)
+(** * Schedule Representation *)
+
+(** In Prosa, schedules are represented as functions, which allows us to model
+    potentially infinite schedules. More specifically, a schedule simply maps
+    each instant to a processor state, which reflects state of the computing
+    platform at the specific time (e.g., which job is presently scheduled). *)
+
 Definition schedule (PState : Type) := instant -> PState.
 
 (** The following line instructs Coq to not let proofs use knowledge of how

restructuring/behavior/service.v

@@ -2,58 +2,69 @@ From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 From rt.restructuring.behavior Require Export schedule.
 
 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, ... *)
+  (** 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. *)
+  (** ... 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 [t1, t2). *)
+  (** 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 time t, i.e., during interval [0, 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.
 
+  (** * Job Completion and Response Time *)
+
+  (** 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}.
 
-  (** Next, we say that job j has completed by time t if it received enough
-           service in the interval [0, t). *)
+  (** 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 *)
+  (** 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.
 
-  (** We say that R is a response time bound of a job j if j has completed
-     by R units after its arrival *)
+  (** 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 *)
+  (** 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).
 
-  (** Job j is pending at time t iff it has arrived but has not yet completed. *)
+  (** * Pending or Incomplete 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. *)
+  (** 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 to be received for its completion. *)
+  (** 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.
 

restructuring/behavior/time.v

-(** Time is defined as a natural number. *)
+(** * Model of Time *)
 
+(** Prosa is based on a discrete model of time. Thus, time is simply defined by
+    the natural numbers. To aid readability, we distinguish between time values
+    that represent durations and time values that represent specific
+    instants. *)
 Definition duration := nat.
 Definition instant  := nat.