From 8f172d18e8d89389b537e771c1b815255f32f45b Mon Sep 17 00:00:00 2001
From: =?UTF8?q?Bj=C3=B6rn=20Brandenburg?=
Date: Mon, 18 Nov 2019 16:33:27 +0100
Subject: [PATCH] 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  11 ++
restructuring/behavior/arrival_sequence.v  13 +++++
restructuring/behavior/job.v  6 +++
restructuring/behavior/ready.v  7 +++
restructuring/behavior/schedule.v  30 +++++++++++
restructuring/behavior/service.v  49 ++++++++++++++
restructuring/behavior/time.v  6 ++
7 files changed, 90 insertions(+), 32 deletions()
diff git a/README.md b/README.md
index 66f4967..befa2f0 100644
 a/README.md
+++ b/README.md
@@ 4,6 +4,12 @@ This repository contains the main Coq specification & proof development of the [
+## Documentation
+
+Uptodate documentation for all branches of the main Prosa repository is available on the Prosa homeage:
+
+
+
## Publications
Please see the [list of publications](http://prosa.mpisws.org/documentation.html#publications) on the Prosa project's homepage.
@@ 46,11 +52,6 @@ Second, compile the library.
make j
```
## Documentation

Uptodate documentation for all branches of the main Prosa repository is available at .


## Generating HTML Documentation
The Coqdoc documentation (as shown on the [webpage](http://prosa.mpisws.org/documentation.html)) can be easily generated with the provided `Makefile`:
diff git a/restructuring/behavior/arrival_sequence.v b/restructuring/behavior/arrival_sequence.v
index 976c015..6f913ff 100644
 a/restructuring/behavior/arrival_sequence.v
+++ b/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.
diff git a/restructuring/behavior/job.v b/restructuring/behavior/job.v
index 26ae4c6..6a152cc 100644
 a/restructuring/behavior/job.v
+++ b/restructuring/behavior/job.v
@@ 1,13 +1,19 @@
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.
diff git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index a2a5d2e..30587b0 100644
 a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ 1,6 +1,7 @@
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}.
diff git a/restructuring/behavior/schedule.v b/restructuring/behavior/schedule.v
index ea6e917..2958f87 100644
 a/restructuring/behavior/schedule.v
+++ b/restructuring/behavior/schedule.v
@@ 1,10 +1,24 @@
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, variablespeed
+ 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
diff git a/restructuring/behavior/service.v b/restructuring/behavior/service.v
index e42f353..24bc015 100644
 a/restructuring/behavior/service.v
+++ b/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.
diff git a/restructuring/behavior/time.v b/restructuring/behavior/time.v
index 662292c..54dd8b2 100644
 a/restructuring/behavior/time.v
+++ b/restructuring/behavior/time.v
@@ 1,4 +1,8 @@
(** 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.

2.24.1