From 22a76ba8ff70443e504570e9a4c60e54edbd6b0d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?=
Date: Mon, 2 Dec 2019 13:41:47 +0100
Subject: [PATCH] address spell-checking issues in model module
---
.../model/aggregate/service_of_jobs.v | 16 +++++----
restructuring/model/aggregate/task_arrivals.v | 17 +++++----
restructuring/model/aggregate/workload.v | 16 +++++----
restructuring/model/arrival/arrival_curves.v | 36 ++++++++++---------
.../model/preemption/fully_preemptive.v | 2 +-
restructuring/model/preemption/parameter.v | 4 +--
restructuring/model/priority/classes.v | 2 +-
restructuring/model/readiness/basic.v | 2 +-
restructuring/model/readiness/jitter.v | 2 +-
.../model/schedule/work_conserving.v | 15 ++++----
restructuring/model/task/concept.v | 10 +++---
.../task/preemption/floating_nonpreemptive.v | 2 +-
.../task/preemption/limited_preemptive.v | 4 +--
.../model/task/preemption/parameters.v | 22 ++++++------
scripts/wordlist.pws | 1 +
15 files changed, 84 insertions(+), 67 deletions(-)
diff --git a/restructuring/model/aggregate/service_of_jobs.v b/restructuring/model/aggregate/service_of_jobs.v
index d22cedb..e3156c1 100644
--- a/restructuring/model/aggregate/service_of_jobs.v
+++ b/restructuring/model/aggregate/service_of_jobs.v
@@ -59,13 +59,15 @@ Section ServiceOfJobs.
(** Let jobs denote any (finite) set of jobs. *)
Variable jobs : seq Job.
- (** Let tsk be the task to be analyzed. *)
+ (** Let [tsk] be the task to be analyzed. *)
Variable tsk : Task.
- (** Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
+ (** Based on the definition of jobs of higher or equal priority
+ (with respect to task [tsk]), ... *)
Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.
- (** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
+ (** ...we define the service received during [[t1, t2)] by jobs of
+ higher or equal priority. *)
Definition service_of_higher_or_equal_priority_tasks (t1 t2 : instant) :=
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
@@ -87,7 +89,7 @@ Section ServiceOfJobs.
(** Based on the definition of jobs of higher or equal priority, ... *)
Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.
- (** ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
+ (** ...we define the service received during [[t1, t2)] by jobs of higher or equal priority. *)
Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
@@ -96,14 +98,14 @@ Section ServiceOfJobs.
(** In this section, we define the notion of workload for sets of jobs. *)
Section ServiceOfTask.
- (** Let tsk be the task to be analyzed... *)
+ (** Let [tsk] be the task to be analyzed... *)
Variable tsk : Task.
(** ... and let jobs denote any (finite) set of jobs. *)
Variable jobs : seq Job.
- (** We define the cumulative task service received by
- the jobs from the task within time interval [t1, t2). *)
+ (** We define the cumulative task service received by the jobs
+ from the task within time interval [[t1, t2)]. *)
Definition task_service_of_jobs_in t1 t2 :=
service_of_jobs (job_of_task tsk) jobs t1 t2.
diff --git a/restructuring/model/aggregate/task_arrivals.v b/restructuring/model/aggregate/task_arrivals.v
index 9216784..4d3c18b 100644
--- a/restructuring/model/aggregate/task_arrivals.v
+++ b/restructuring/model/aggregate/task_arrivals.v
@@ -12,22 +12,24 @@ Section TaskArrivals.
Section Definitions.
- (** Let tsk be any task. *)
+ (** Let [tsk] be any task. *)
Variable tsk : Task.
- (** We define the sequence of jobs of tsk arriving at time t. *)
+ (** We define the sequence of jobs of task [tsk] arriving at time t. *)
Definition task_arrivals_at (t : instant) : seq Job :=
[seq j <- arrivals_at arr_seq t | job_task j == tsk].
- (** By concatenation, we construct the list of jobs of tsk that arrived in the
- interval [t1, t2). *)
+ (** By concatenation, we construct the list of jobs of task [tsk]
+ that arrived in the interval [[t1, t2)]. *)
Definition task_arrivals_between (t1 t2 : instant) :=
[seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
- (** Based on that, we define the list of jobs of tsk that arrived up to time t, ...*)
+ (** Based on that, we define the list of jobs of task [tsk] that
+ arrived up to time t, ...*)
Definition task_arrivals_up_to (t : instant) := task_arrivals_between 0 t.+1.
- (** ...and the list of jobs of tsk that arrived strictly before time t ... *)
+ (** ...and the list of jobs of task [tsk] that arrived strictly
+ before time t ... *)
Definition task_arrivals_before (t : instant) := task_arrivals_between 0 t.
(** ... and also count the number of job arrivals. *)
@@ -36,7 +38,8 @@ Section TaskArrivals.
End Definitions.
- (** We define a predicate for arrival sequences for which jobs come from a taskset. *)
+ (** We define a predicate for arrival sequences in which all jobs
+ come from a given task set. *)
Definition arrivals_come_from_taskset (ts : seq Task) :=
forall j, arrives_in arr_seq j -> job_task j \in ts.
diff --git a/restructuring/model/aggregate/workload.v b/restructuring/model/aggregate/workload.v
index 9040dbb..6a3bea2 100644
--- a/restructuring/model/aggregate/workload.v
+++ b/restructuring/model/aggregate/workload.v
@@ -41,7 +41,7 @@ Section WorkloadOfJobs.
higher or equal priority. *)
Variable higher_eq_priority : FP_policy Task.
- (** Let tsk be the task to be analyzed. *)
+ (** Let [tsk] be the task to be analyzed. *)
Variable tsk : Task.
(** Recall the notion of a job of higher or equal priority. *)
@@ -49,7 +49,7 @@ Section WorkloadOfJobs.
higher_eq_priority (job_task j) tsk.
(** Then, we define the workload of all jobs of tasks with
- higher-or-equal priority than tsk. *)
+ higher-or-equal priority than task [tsk]. *)
Definition workload_of_higher_or_equal_priority_tasks :=
workload_of_jobs of_higher_or_equal_priority.
@@ -60,7 +60,7 @@ Section WorkloadOfJobs.
Section PerJobPriority.
(** Consider any JLFP policy that indicates whether a job has
- higher or equal priority. *)
+ higher or equal priority. *)
Variable higher_eq_priority : JLFP_policy Job.
(** Let j be the job to be analyzed. *)
@@ -79,16 +79,18 @@ Section WorkloadOfJobs.
(** We also define workload of a task. *)
Section TaskWorkload.
- (** Let tsk be the task to be analyzed. *)
+ (** Let [tsk] be the task to be analyzed. *)
Variable tsk : Task.
- (** We define the task workload as the workload of jobs of task tsk. *)
+ (** We define the task workload as the workload of jobs of task
+ [tsk]. *)
Definition task_workload jobs := workload_of_jobs (job_of_task tsk) jobs.
- (** Next, we recall the definition of the task workload in interval [t1, t2). *)
+ (** Next, we recall the definition of the task workload in
+ interval [[t1, t2)]. *)
Definition task_workload_between (t1 t2 : instant) :=
task_workload (arrivals_between arr_seq t1 t2).
End TaskWorkload.
-End WorkloadOfJobs.
\ No newline at end of file
+End WorkloadOfJobs.
diff --git a/restructuring/model/arrival/arrival_curves.v b/restructuring/model/arrival/arrival_curves.v
index f89c3df..b69fe73 100644
--- a/restructuring/model/arrival/arrival_curves.v
+++ b/restructuring/model/arrival/arrival_curves.v
@@ -1,8 +1,8 @@
Require Export rt.util.rel.
Require Export rt.restructuring.model.aggregate.task_arrivals.
-(** In this section, we define the notion of arrival curves, which
- can be used to reason about the frequency of job arrivals. *)
+(** In this section, we define the notion of arrival curves, which can
+ be used to reason about the frequency of job arrivals. *)
Section ArrivalCurves.
(** Consider any type of tasks ... *)
@@ -18,15 +18,17 @@ Section ArrivalCurves.
(** First, we define what constitutes an arrival bound for a task. *)
Section ArrivalCurves.
- (** We say that num_arrivals is a valid arrival curve for task tsk iff
- [num_arrivals] is a monotonic function that equals 0 for the empty
- interval delta = 0. *)
+ (** We say that [num_arrivals] is a valid arrival curve for task
+ [tsk] iff [num_arrivals] is a monotonic function that equals 0
+ for the empty interval [delta = 0]. *)
Definition valid_arrival_curve (tsk : Task) (num_arrivals : duration -> nat) :=
num_arrivals 0 = 0 /\
monotone num_arrivals leq.
- (** We say that max_arrivals is an upper arrival bound for tsk iff, for any interval [t1, t2),
- [max_arrivals (t2 - t1)] bounds the number of jobs of tsk that arrive in that interval. *)
+ (** We say that [max_arrivals] is an upper arrival bound for task
+ [tsk] iff, for any interval [[t1, t2)], [max_arrivals (t2 -
+ t1)] bounds the number of jobs of [tsk] that arrive in that
+ interval. *)
Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
forall (t1 t2 : instant),
t1 <= t2 ->
@@ -42,15 +44,16 @@ Section ArrivalCurves.
Section SeparationBound.
- (** Then, we say that min_separation is a lower separation bound iff, for any number of jobs
- of tsk, min_separation lower-bounds the minimum interval length in which that number
- of jobs can be spawned. *)
+ (** Then, we say that [min_separation] is a lower separation bound
+ iff, for any number of jobs of task [tsk], [min_separation]
+ lower-bounds the minimum interval length in which that number
+ of jobs can be spawned. *)
Definition respects_min_separation (tsk : Task) (min_separation: nat -> duration) :=
forall t1 t2,
t1 <= t2 ->
min_separation (number_of_task_arrivals arr_seq tsk t1 t2) <= t2 - t1.
- (** We define in the same way upper separation bounds *)
+ (** We define in the same way upper separation bounds. *)
Definition respects_max_separation (tsk : Task) (max_separation: nat -> duration):=
forall t1 t2,
t1 <= t2 ->
@@ -87,16 +90,17 @@ Section ArrivalCurvesModel.
`{MaxSeparation Task}
`{MinSeparation Task}.
- (** Let ts be an arbitrary task set. *)
+ (** Let [ts] be an arbitrary task set. *)
Variable ts : seq Task.
- (** We say that arrivals is a valid arrival curve for a taskset if it is valid for any task
- in the taskset *)
+ (** We say that [arrivals] is a valid arrival curve for a task set
+ if it is valid for any task in the task set *)
Definition valid_taskset_arrival_curve (arrivals : Task -> duration -> nat) :=
forall (tsk : Task), tsk \in ts -> valid_arrival_curve tsk (arrivals tsk).
- (** We say that max_arrivals is an arrival bound for taskset ts *)
- (** iff max_arrival is an arrival bound for any task from ts. *)
+ (** We say that [max_arrivals] is an arrival bound for a task set
+ [ts] iff [max_arrivals] is an arrival bound for any task in
+ [ts]. *)
Definition taskset_respects_max_arrivals :=
forall (tsk : Task), tsk \in ts -> respects_max_arrivals arr_seq tsk (max_arrivals tsk).
diff --git a/restructuring/model/preemption/fully_preemptive.v b/restructuring/model/preemption/fully_preemptive.v
index 9f8e026..da8401b 100644
--- a/restructuring/model/preemption/fully_preemptive.v
+++ b/restructuring/model/preemption/fully_preemptive.v
@@ -1,6 +1,6 @@
Require Export rt.restructuring.model.preemption.parameter.
-(** * Platform for Fully Premptive Model *)
+(** * Fully Preemptive Model *)
(** In this section, we instantiate [job_preemptable] for the fully
preemptive model. *)
Section FullyPreemptiveModel.
diff --git a/restructuring/model/preemption/parameter.v b/restructuring/model/preemption/parameter.v
index 20a26f0..0bb7e5c 100644
--- a/restructuring/model/preemption/parameter.v
+++ b/restructuring/model/preemption/parameter.v
@@ -76,8 +76,8 @@ Section MaxAndLastNonpreemptiveSegment.
End MaxAndLastNonpreemptiveSegment.
(** * Platform with limited preemptions *)
-(** In the follwoing, we define properties that any reasonable job preemption
- model must satisfy. *)
+(** In the following, we define properties that any reasonable job
+ preemption model must satisfy. *)
Section PreemptionModel.
(** Consider any type of jobs... *)
diff --git a/restructuring/model/priority/classes.v b/restructuring/model/priority/classes.v
index 138496c..f8323bd 100644
--- a/restructuring/model/priority/classes.v
+++ b/restructuring/model/priority/classes.v
@@ -86,7 +86,7 @@ Section Priorities.
(** Consider any FP policy. *)
Context `{FP_policy Task}.
- (** We define whether the policy is antisymmetric over a taskset ts. *)
+ (** We define whether the policy is antisymmetric over a task set [ts]. *)
Definition antisymmetric_over_taskset (ts : seq Task) :=
antisymmetric_over_list hep_task ts.
diff --git a/restructuring/model/readiness/basic.v b/restructuring/model/readiness/basic.v
index d1ac1a6..9f133b1 100644
--- a/restructuring/model/readiness/basic.v
+++ b/restructuring/model/readiness/basic.v
@@ -12,7 +12,7 @@ Section LiuAndLaylandReadiness.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (** Supose jobs have an arrival time and a cost. *)
+ (** Suppose jobs have an arrival time and a cost. *)
Context `{JobArrival Job} `{JobCost Job}.
(** In the basic Liu & Layland model, a job is ready iff it is pending. *)
diff --git a/restructuring/model/readiness/jitter.v b/restructuring/model/readiness/jitter.v
index 1f80f3f..6079837 100644
--- a/restructuring/model/readiness/jitter.v
+++ b/restructuring/model/readiness/jitter.v
@@ -17,7 +17,7 @@ Section ReadinessOfJitteryJobs.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (** Supose jobs have an arrival time, a cost, and a release jitter bound. *)
+ (** Suppose jobs have an arrival time, a cost, and a release jitter bound. *)
Context `{JobArrival Job} `{JobCost Job} `{JobJitter Job}.
(** We say that a job is released at a time after its arrival if the job's
diff --git a/restructuring/model/schedule/work_conserving.v b/restructuring/model/schedule/work_conserving.v
index 503a68a..3f39cd5 100644
--- a/restructuring/model/schedule/work_conserving.v
+++ b/restructuring/model/schedule/work_conserving.v
@@ -1,11 +1,14 @@
Require Export rt.restructuring.behavior.all.
-(** In this file, we introduce a restrictive definition of work conserving
- uniprocessor schedules. The definition is restrictive because it does not
- allow for effects such as jitter or self-suspensions that affect whether a
- job can be scheduled at a given point in time. A more general notion of work
- conservation that is "readiness-aware", as well as a variant that covers
- global scheduling, is TBD. *)
+(** In this file, we introduce a restrictive definition of work
+ conserving schedules. The definition is restrictive because it
+ does not yet cover multiprocessor scheduling (there are plans to
+ address this in future work). The definition does however cover
+ effects such as jitter or self-suspensions that affect whether a
+ job can be scheduled at a given point in time because it is based
+ on the general notion of a job being [backlogged] (i.e., ready and
+ not executing), which is parametric in any given job readiness
+ model. *)
Section WorkConserving.
(** Consider any type of job associated with any type of tasks... *)
diff --git a/restructuring/model/task/concept.v b/restructuring/model/task/concept.v
index b47041b..ad82dad 100644
--- a/restructuring/model/task/concept.v
+++ b/restructuring/model/task/concept.v
@@ -20,10 +20,12 @@ Section SameTask.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
- (** ... we say that two jobs j1 and j2 are from the same task iff job_task j1 is equal to job_task j2, ... *)
+ (** ... we say that two jobs [j1] and [j2] are from the same task iff
+ [job_task j1] is equal to [job_task j2], ... *)
Definition same_task (j1 j2 : Job) := job_task j1 == job_task j2.
- (** ... we also say that job j is a job of task tsk iff job_task j is equal to tsk. *)
+ (** ... we also say that job [j] is a job of task [tsk] iff
+ [job_task j] is equal to [tsk]. *)
Definition job_of_task (tsk : Task) (j : Job) := job_task j == tsk.
End SameTask.
@@ -36,7 +38,7 @@ Section PropertesOfTask.
Context `{TaskCost Task}.
Context `{TaskDeadline Task}.
- (** Next we intrdoduce attributes of a valid sporadic task. *)
+ (** Next we introduce attributes of a valid sporadic task. *)
Section ValidTask.
(** Consider an arbitrary task. *)
@@ -115,7 +117,7 @@ Section PropertesOfTaskSet.
tsk \in ts ->
task_cost_positive tsk.
- (** All jobs in the arrival sequence come from the taskset. *)
+ (** All jobs in the arrival sequence come from the task set. *)
Definition all_jobs_from_taskset :=
forall j,
arrives_in arr_seq j ->
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 26b5730..953f071 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -23,7 +23,7 @@ Section ModelWithFloatingNonpreemptiveRegions.
Variable arr_seq : arrival_sequence Job.
(** We require [task_max_nonpreemptive_segment (job_task j)] to be
- an upper bound of the lenght of the max nonpreemptive segment of
+ an upper bound of the length of the max nonpreemptive segment of
job [j]. *)
Definition job_max_np_segment_le_task_max_np_segment :=
forall (j : Job),
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 3458aa5..e3ba898 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -37,7 +37,7 @@ Section ModelWithFixedPreemptionPoints.
forall tsk, tsk \in ts -> last0 (task_preemption_points tsk) = task_cost tsk.
(** (3) We require the sequence of preemption points
- to be a nondecreasing sequence. *)
+ to be a non-decreasing sequence. *)
Definition task_preemption_points_is_nondecreasing_sequence :=
forall tsk, tsk \in ts -> nondecreasing_sequence (task_preemption_points tsk).
@@ -51,7 +51,7 @@ Section ModelWithFixedPreemptionPoints.
size (job_preemption_points j) = size (task_preemption_points (job_task j)).
(** (5) We require lengths of nonpreemptive segments of a job to be bounded
- by lenghts of the corresponding segments of its task. *)
+ by lengths of the corresponding segments of its task. *)
Definition lengths_of_task_segments_bound_length_of_job_segments :=
forall j n,
arrives_in arr_seq j ->
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index 1c0b7fd..d1b9edd 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -3,7 +3,7 @@ Require Export rt.restructuring.model.task.concept.
(** * Static information about preemption points *)
(** Definition of a generic type of parameter relating a task
- to the length of the maximum nonpreeptive segment. *)
+ to the length of the maximum nonpreemptive segment. *)
Class TaskMaxNonpreemptiveSegment (Task : TaskType) :=
task_max_nonpreemptive_segment : Task -> work.
@@ -98,7 +98,7 @@ Section PreemptionModel.
bounded length. I.e., for any progress [ρ] of job [j] there
exists a preemption point [pp] such that [ρ <= pp <= ρ +
(job_max_nps j - ε)]. That is, in any time interval of length
- [job_max_nps j], there exists a preeemption point which lies
+ [job_max_nps j], there exists a preemption point which lies
in this interval. *)
Definition nonpreemptive_regions_have_bounded_length (j : Job) :=
forall (ρ : duration),
@@ -148,7 +148,7 @@ Section ValidTaskRunToCompletionThreshold.
Context `{JobCost Job}.
(** In addition, we assume existence of a function
- maping jobs to theirs preemption points ... *)
+ mapping jobs to theirs preemption points ... *)
Context `{JobPreemptable Job}.
(** ...and a function mapping tasks to theirs
@@ -169,10 +169,10 @@ Section ValidTaskRunToCompletionThreshold.
Definition task_run_to_completion_threshold_le_task_cost tsk :=
task_run_to_completion_threshold tsk <= task_cost tsk.
- (** We say that the run-to-completion threshold of a task tsk bounds
- the job run-to-completionthreshold iff for any job j of task tsk
- the job run-to-completion threshold is less than or equal to the
- task run-to-completion threshold. *)
+ (** We say that the run-to-completion threshold of a task [tsk]
+ bounds the job run-to-completion threshold iff for any job [j]
+ of task [tsk] the job's run-to-completion threshold is less than
+ or equal to the task's run-to-completion threshold. *)
Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
forall j,
arrives_in arr_seq j ->
@@ -180,11 +180,11 @@ Section ValidTaskRunToCompletionThreshold.
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
(** We say that task_run_to_completion_threshold is a valid task
- run-to-completion threshold for a task tsk iff
+ run-to-completion threshold for a task [tsk] iff
[task_run_to_completion_threshold tsk] is (1) no bigger than
- tsk's cost, (2) for any job of task tsk
- job_run_to_completion_threshold is bounded by
- task_run_to_completion_threshold. *)
+ [tsk]'s cost, (2) for any job of task [tsk]
+ [job_run_to_completion_threshold] is bounded by
+ [task_run_to_completion_threshold]. *)
Definition valid_task_run_to_completion_threshold tsk :=
task_run_to_completion_threshold_le_task_cost tsk /\
task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index ce46294..5da88c6 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -22,6 +22,7 @@ namespace
nonpreemptive
preemptive
preemptable
+preemptions
EDF
FP
JLFP
--
GitLab