From 6a20581c17d85a1a3d61c7333c8e7970a36c2b23 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 8 Aug 2022 15:18:12 +0200
Subject: [PATCH] fix spelling and markup issues uncovered by `hunspell`
---
analysis/abstract/abstract_rta.v | 8 ++--
analysis/abstract/abstract_seq_rta.v | 14 +++----
analysis/abstract/definitions.v | 2 +-
analysis/abstract/run_to_completion.v | 8 ++--
analysis/facts/behavior/arrivals.v | 12 +++---
analysis/facts/behavior/service.v | 2 +-
analysis/facts/model/rbf.v | 6 +--
analysis/facts/preemption/job/preemptive.v | 2 +-
.../preemption/rtc_threshold/nonpreemptive.v | 2 +-
analysis/facts/transform/edf_opt.v | 2 +-
analysis/facts/transform/edf_wc.v | 2 +-
analysis/facts/transform/swaps.v | 38 +++++++++----------
behavior/arrival_sequence.v | 10 ++---
implementation/refinements/arrival_curve.v | 2 +-
implementation/refinements/task.v | 2 +-
model/schedule/edf.v | 4 +-
model/task/preemption/fully_nonpreemptive.v | 2 +-
model/task/preemption/fully_preemptive.v | 2 +-
results/edf/rta/bounded_pi.v | 8 ++--
results/fixed_priority/rta/bounded_pi.v | 4 +-
util/list.v | 2 +-
util/setoid.v | 2 +-
util/sum.v | 2 +-
util/tactics.v | 8 ++--
24 files changed, 73 insertions(+), 73 deletions(-)
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index 61267573c..eac93f193 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -123,7 +123,7 @@ Section Abstract_RTA.
Variable t1 t2: instant.
Hypothesis H_busy_interval: busy_interval j t1 t2.
- (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+ (** Let's define [A] as a relative arrival time of job [j] (with respect to time [t1]). *)
Let A := job_arrival j - t1.
(** In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum.
@@ -164,7 +164,7 @@ Section Abstract_RTA.
interval remains completed. *)
Section FixpointOutsideBusyInterval.
- (** By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
+ (** By assumption, suppose that [t2] is less than or equal to [t1 + A_sp + F_sp]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + (A_sp + F_sp).
(** Then we prove that [job_arrival j + R] is no less than [t2]. *)
@@ -198,7 +198,7 @@ Section Abstract_RTA.
[t1 + A_sp + F_sp] lies inside the busy interval. *)
Section FixpointInsideBusyInterval.
- (** So, assume that [t1 + A_sp + F_sp] is less than t2. *)
+ (** So, assume that [t1 + A_sp + F_sp] is less than [t2]. *)
Hypothesis H_small_fixpoint_solution : t1 + (A_sp + F_sp) < t2.
(** Next, let's consider two other cases: *)
@@ -221,7 +221,7 @@ Section Abstract_RTA.
Variable F : duration.
(** (a) the sum of [A_sp] and [F_sp] is equal to the sum of [A] and [F]... *)
Hypothesis H_Asp_Fsp_eq_A_F : A_sp + F_sp = A + F.
- (** (b) [F] is at mo1st [F_sp]... *)
+ (** (b) [F] is at most [F_sp]... *)
Hypothesis H_F_le_Fsp : F <= F_sp.
(** (c) and [A + F] is a solution for the response-time recurrence for [A]. *)
Hypothesis H_A_F_fixpoint:
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index 0cf81e00b..6b7ac5618 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -220,7 +220,7 @@ Section Sequential_Abstract_RTA.
Hypothesis H_j2_from_tsk: job_of_task tsk j2.
Hypothesis H_j1_cost_positive: job_cost_positive j1.
- (** Consider the busy interval <<[t1, t2)>> of job j1. *)
+ (** Consider the busy interval <<[t1, t2)>> of job [j1]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j1 t1 t2.
@@ -241,7 +241,7 @@ Section Sequential_Abstract_RTA.
Qed.
(** Next we prove that if a job is pending after the beginning
- of the busy interval <<[t1, t2)>> then it arrives after t1. *)
+ of the busy interval <<[t1, t2)>> then it arrives after [t1]. *)
Lemma arrives_after_beginning_of_busy_interval:
forall t,
t1 <= t ->
@@ -280,14 +280,14 @@ Section Sequential_Abstract_RTA.
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j t1 t2.
- (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+ (** Let's define [A] as a relative arrival time of job [j] (with respect to time [t1]). *)
Let A : duration := job_arrival j - t1.
(** Consider an arbitrary time x ... *)
Variable x : duration.
- (** ... such that (t1 + x) is inside the busy interval... *)
+ (** ... such that [(t1 + x)] is inside the busy interval... *)
Hypothesis H_inside_busy_interval : t1 + x < t2.
- (** ... and job j is not completed by time (t1 + x). *)
+ (** ... and job [j] is not completed by time [(t1 + x)]. *)
Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + x).
(** In this section, we show that the cumulative interference of job j in the interval <<[t1, t1 + x)>>
@@ -549,8 +549,8 @@ Section Sequential_Abstract_RTA.
Qed.
(** Finally, we show that the cumulative interference of job j in the interval <<[t1, t1 + x)>>
- is bounded by the sum of the task workload in the interval [t1, t1 + A + ε) and
- the cumulative interference of [j]'s task in the interval [t1, t1 + x). *)
+ is bounded by the sum of the task workload in the interval <<[t1, t1 + A + ε)>> and
+ the cumulative interference of [j]'s task in the interval <<[t1, t1 + x)>>. *)
Lemma cumulative_job_interference_le_task_interference_bound:
cumul_interference j t1 (t1 + x)
<= (task_workload_between t1 (t1 + A + ε) - job_cost j)
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index a37648ea5..19dd3d45f 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -96,7 +96,7 @@ Section AbstractRTADefinitions.
(forall t, t1 < t < t2 -> ~ quiet_time j t).
(** Next, we say that an interval <<[t1, t2)>> is a busy interval iff
- [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
+ <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet time. *)
Definition busy_interval (j : Job) (t1 t2 : instant) :=
busy_interval_prefix j t1 t2 /\
quiet_time j t2.
diff --git a/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
index 2d442f5fc..281ac45a5 100644
--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -57,9 +57,9 @@ Section AbstractRTARunToCompletionThreshold.
Hypothesis H_busy_interval : busy_interval j t1 t2.
(** First, we prove that job [j] completes by the end of the busy interval.
- Note that the busy interval contains the execution of job j, in addition
- time instant t2 is a quiet time. Thus by the definition of a quiet time
- the job should be completed before time t2. *)
+ Note that the busy interval contains the execution of job j, in addition
+ time instant [t2] is a quiet time. Thus by the definition of a quiet time
+ the job should be completed before time [t2]. *)
Lemma job_completes_within_busy_interval:
completed_by sched j t2.
Proof.
@@ -74,7 +74,7 @@ Section AbstractRTARunToCompletionThreshold.
the total time where job [j] is scheduled inside the busy interval. *)
Section InterferenceIsComplement.
- (** Consider any sub-interval <<[t, t + delta)>> inside the busy interval [t1, t2). *)
+ (** Consider any sub-interval <<[t, t + delta)>> inside the busy interval <<[t1, t2)>>. *)
Variables (t : instant) (delta : duration).
Hypothesis H_greater_than_or_equal : t1 <= t.
Hypothesis H_less_or_equal: t + delta <= t2.
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index e15e96e89..46d814e23 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -275,7 +275,7 @@ Section ArrivalSequencePrefix.
Qed.
(** Next, we prove that if a job belongs to the prefix
- (jobs_arrived_before t), then it arrives in the arrival
+ [(jobs_arrived_before t)], then it arrives in the arrival
sequence. *)
Lemma in_arrivals_implies_arrived:
forall j t1 t2,
@@ -291,16 +291,16 @@ Section ArrivalSequencePrefix.
Proof. by move=> t ? ?; exists t. Qed.
(** Next, we prove that if a job belongs to the prefix
- (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
- t2. *)
+ [(jobs_arrived_between t1 t2)], then it indeed arrives between [t1] and
+ [t2]. *)
Lemma in_arrivals_implies_arrived_between:
forall j t1 t2,
j \in arrivals_between arr_seq t1 t2 ->
arrived_between j t1 t2.
Proof. by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed.
- (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
- then it indeed arrives before time t. *)
+ (** Similarly, if a job belongs to the prefix [(jobs_arrived_before t)],
+ then it indeed arrives before time [t]. *)
Lemma in_arrivals_implies_arrived_before:
forall j t,
j \in arrivals_before arr_seq t ->
@@ -308,7 +308,7 @@ Section ArrivalSequencePrefix.
Proof. by move=> ? ? /in_arrivals_implies_arrived_between. Qed.
(** Similarly, we prove that if a job from the arrival sequence arrives
- before t, then it belongs to the sequence (jobs_arrived_before t). *)
+ before t, then it belongs to the sequence [(jobs_arrived_before t)]. *)
Lemma arrived_between_implies_in_arrivals:
forall j t1 t2,
arrives_in arr_seq j ->
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index 14d7654b3..856c10e7a 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -94,7 +94,7 @@ Section Composition.
Proof. move=> ?; exact: service_during_last_plus_before. Qed.
(** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
- into the service at a midpoint t2 and the service in the intervals before
+ into the service at a midpoint [t2] and the service in the intervals before
and after. *)
Lemma service_split_at_point:
forall t1 t2 t3,
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index a68197ec3..0e21acfde 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -242,7 +242,7 @@ Section RequestBoundFunctions.
(** Let [max_arrivals] be a family of valid arrival curves, i.e., for any task [tsk] in [ts]
[max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
- that equals 0 for the empty interval Δ = 0. *)
+ that equals 0 for the empty interval [Δ = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
@@ -388,10 +388,10 @@ Section TotalRBFMonotonic.
End TotalRBFMonotonic.
-(** ** RBFs Equal to Zero for Duration ε *)
+(** ** RBFs Equal to Zero for Duration [ε] *)
(** In the following section, we derive simple properties that follow in
- the pathological case of an RBF that yields zero for duration ε. *)
+ the pathological case of an RBF that yields zero for duration [ε]. *)
Section DegenerateTotalRBFs.
(** Consider a set of tasks characterized by WCETs and arrival curves ... *)
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index 8e58895ae..cf1436775 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -45,7 +45,7 @@ Section FullyPreemptiveModel.
by rewrite H1; compute.
Qed.
- (** ... or ε when [job_cost j > 0]. *)
+ (** ... or [ε] when [job_cost j > 0]. *)
Lemma job_max_nps_is_ε:
forall j,
job_cost j > 0 ->
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 6b7ae3a73..1b1634fde 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -47,7 +47,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
by rewrite H3; compute.
Qed.
- (** ... and ε otherwise. *)
+ (** ... and [ε] otherwise. *)
Fact job_rtc_threshold_is_ε:
forall j,
job_cost j > 0 ->
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index ee45e95f1..b5a3a903d 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -97,7 +97,7 @@ Section FindSwapCandidateFacts.
(** Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
- that it arrives not later than at time t1. *)
+ that it arrives not later than at time [t1]. *)
Corollary fsc_found_job_arrival:
forall j2,
scheduled_at sched j2 (find_swap_candidate sched t1 j1) ->
diff --git a/analysis/facts/transform/edf_wc.v b/analysis/facts/transform/edf_wc.v
index 9976ec343..e51360d26 100644
--- a/analysis/facts/transform/edf_wc.v
+++ b/analysis/facts/transform/edf_wc.v
@@ -219,7 +219,7 @@ Section FSCWorkConservationLemmas.
- by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
- case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ'].
+ by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
- + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET]. (* t <> t2 *)
+ + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET].
* move: NOT_BET; move/orP => [] => NOT_BET.
{ by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }
{ by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }
diff --git a/analysis/facts/transform/swaps.v b/analysis/facts/transform/swaps.v
index c8cd39e47..e6b360903 100644
--- a/analysis/facts/transform/swaps.v
+++ b/analysis/facts/transform/swaps.v
@@ -18,11 +18,11 @@ Section SwappedFacts.
Variable t1 t2: instant.
(** In the following, let [sched'] denote the schedule in which the
- allocations at [t1] and [t2] have been swapped. *)
+ allocations at [t1] and [t2] have been swapped. *)
Let sched' := swapped sched t1 t2.
- (** First, we note that the trivial case where t1 == t2 is not interesting
- because then the two schedules are identical. *)
+ (** First, we note that the trivial case where [t1 == t2] is not interesting
+ because then the two schedules are identical. *)
Lemma trivial_swap:
t1 = t2 ->
forall t,
@@ -58,8 +58,8 @@ Section SwappedFacts.
by rewrite /sched' /swapped !rest_of_schedule_invariant //.
Qed.
- (** By definition, if a job is scheduled at t2 in the original
- schedule, then it is found at t1 in the new schedule. *)
+ (** By definition, if a job is scheduled at [t2] in the original
+ schedule, then it is found at [t1] in the new schedule. *)
Lemma swap_job_scheduled_t1:
forall j,
scheduled_at sched' j t1 =
@@ -72,8 +72,8 @@ Section SwappedFacts.
- by rewrite ifT.
Qed.
- (** Similarly, a job scheduled at t1 in the original schedule is
- scheduled at t2 after the swap. *)
+ (** Similarly, a job scheduled at [t1] in the original schedule is
+ scheduled at [t2] after the swap. *)
Lemma swap_job_scheduled_t2:
forall j,
scheduled_at sched' j t2 =
@@ -189,11 +189,11 @@ Section SwappedFacts.
service received. *)
(** To avoid dealing with symmetric cases, assume in the following
- that t1 and t2 are ordered. *)
+ that [t1] and [t2] are ordered. *)
Hypothesis H_well_ordered: t1 <= t2.
(** As another trivial invariant, we observe that nothing has changed
- before time t1. *)
+ before time [t1]. *)
Lemma swap_before_invariant:
forall t,
t < t1 ->
@@ -205,7 +205,7 @@ Section SwappedFacts.
[move: t_lt_t1|move: t_lt_t2]; rewrite ltnn.
Qed.
- (** Similarly, nothing has changed after time t2. *)
+ (** Similarly, nothing has changed after time [t2]. *)
Lemma swap_after_invariant:
forall t,
t2 < t ->
@@ -217,7 +217,7 @@ Section SwappedFacts.
[move: t1_lt_t|move: t2_lt_t]; rewrite ltnn.
Qed.
- (** Thus, we observe that, before t1, the two schedules are identical with
+ (** Thus, we observe that, before [t1], the two schedules are identical with
regard to the service received by any job because they are identical. *)
Corollary service_before_swap_invariant:
forall t,
@@ -232,7 +232,7 @@ Section SwappedFacts.
by apply ltnW.
Qed.
- (** Likewise, we observe that, *after* t2, the swapped schedule again does not
+ (** Likewise, we observe that, *after* [t2], the swapped schedule again does not
differ with regard to the service received by any job. *)
Lemma service_after_swap_invariant:
forall t,
@@ -379,8 +379,8 @@ Section EDFSwap.
(** ...that are ordered. *)
Hypothesis H_well_ordered: t1 <= t2.
- (** Further, assume that, if there are jobs scheduled at times t1 and t2, then
- they either have the same deadline or violate EDF, ... *)
+ (** Further, assume that, if there are jobs scheduled at times [t1] and [t2], then
+ they either have the same deadline or violate EDF, ... *)
Hypothesis H_not_EDF:
forall j1 j2,
scheduled_at sched j1 t1 ->
@@ -388,14 +388,14 @@ Section EDFSwap.
job_deadline j1 >= job_deadline j2.
(** ...and that we don't move idle times or deadline misses earlier,
- i.e., if t1 is not an idle time, then neither is t2 and whatever
- job is scheduled at time t2 has not yet missed its deadline. *)
+ i.e., if [t1] is not an idle time, then neither is [t2] and whatever
+ job is scheduled at time [t2] has not yet missed its deadline. *)
Hypothesis H_no_idle_time_at_t2:
forall j1,
scheduled_at sched j1 t1 ->
exists j2, scheduled_at sched j2 t2 /\ job_deadline j2 > t2.
- (** Consider the schedule obtained from swapping the allocations at times t1 and t2. *)
+ (** Consider the schedule obtained from swapping the allocations at times [t1] and [t2]. *)
Let sched' := swapped sched t1 t2.
(** The key property of this transformation is that, for any job that
@@ -423,7 +423,7 @@ Section EDFSwap.
Qed.
(** Next, we observe that a swap is unproblematic for the job scheduled at
- time t2. *)
+ time [t2]. *)
Lemma moved_earlier_implies_deadline_met:
scheduled_at sched j t2 ->
job_meets_deadline sched' j.
@@ -453,7 +453,7 @@ Section EDFSwap.
(** From the above case analysis, we conclude that no deadline misses
are introduced in the schedule obtained from swapping the
- allocations at times t1 and t2. *)
+ allocations at times [t1] and [t2]. *)
Theorem edf_swap_no_deadline_misses_introduced:
forall j, job_meets_deadline sched j -> job_meets_deadline sched' j.
Proof.
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ad..d45221c39 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -81,16 +81,16 @@ Section ArrivalTimeProperties.
(** 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. *)
+ (** 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. *)
+ 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. *)
+ (** 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.
diff --git a/implementation/refinements/arrival_curve.v b/implementation/refinements/arrival_curve.v
index ca61002ec..e69429ef9 100644
--- a/implementation/refinements/arrival_curve.v
+++ b/implementation/refinements/arrival_curve.v
@@ -15,7 +15,7 @@ Definition get_horizon_of_task (tsk : Task) : duration :=
Definition get_time_steps_of_task (tsk : Task) : seq duration :=
time_steps_of (get_arrival_curve_prefix tsk).
-(** ... a function that yields the same time steps, offset by δ, ...**)
+(** ... a function that yields the same time steps, offset by [δ], ...**)
Definition time_steps_with_offset tsk δ := [seq t + δ | t <- get_time_steps_of_task tsk].
(** ... and a generalization of the previous function that repeats the time
diff --git a/implementation/refinements/task.v b/implementation/refinements/task.v
index a8f89b5c3..6926932fc 100644
--- a/implementation/refinements/task.v
+++ b/implementation/refinements/task.v
@@ -84,7 +84,7 @@ Section Definitions.
Definition get_time_steps_of_task_T (tsk : task_T) : seq T :=
time_steps_of_T (get_extrapolated_arrival_curve_T tsk).
- (** ... a function that yields the same time steps, offset by δ, ... *)
+ (** ... a function that yields the same time steps, offset by [δ], ... *)
Definition time_steps_with_offset_T tsk δ :=
[seq t + δ | t <- get_time_steps_of_task_T tsk]%C.
diff --git a/model/schedule/edf.v b/model/schedule/edf.v
index 947d79c58..411de8328 100644
--- a/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -7,8 +7,8 @@ Require Export prosa.behavior.all.
"EDF schedule".
Note that the "proper" way to define an EDF schedule in Prosa is to use the
- EDF priority policy defined in model.priority.edf and the notion of
- priority-compliant schedules defined in model.schedule.priority_driven, as
+ EDF priority policy defined in [model.priority.edf] and the notion of
+ priority-compliant schedules defined in [model.schedule.priority_driven], as
well as the general notion of work-conservation provided in
model.schedule.work_conserving, which will have the benefit of taking into
account issues such as various readiness models (e.g., jitter) and diverse
diff --git a/model/task/preemption/fully_nonpreemptive.v b/model/task/preemption/fully_nonpreemptive.v
index 249dc0685..1a7e9f7b4 100644
--- a/model/task/preemption/fully_nonpreemptive.v
+++ b/model/task/preemption/fully_nonpreemptive.v
@@ -30,7 +30,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
(** In the fully non-preemptive model, no job can be preempted prior to its
completion. In other words, once a job starts running, it is guaranteed
to finish. Thus, we can set the task-level run-to-completion threshold
- to ε. *)
+ to [ε]. *)
Definition fully_nonpreemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
fun tsk : Task => ε.
diff --git a/model/task/preemption/fully_preemptive.v b/model/task/preemption/fully_preemptive.v
index f3d48b5fe..942442f80 100644
--- a/model/task/preemption/fully_preemptive.v
+++ b/model/task/preemption/fully_preemptive.v
@@ -11,7 +11,7 @@ Section FullyPreemptiveModel.
Context {Task : TaskType}.
(** In the fully preemptive model, any job can be preempted at any
- time. Thus, the maximal non-preemptive segment has length at most ε
+ time. Thus, the maximal non-preemptive segment has length at most [ε]
(i.e., one time unit such as a processor cycle). *)
Definition fully_preemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
fun tsk : Task => ε.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index ab4a9e5fb..d34ab0733 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -231,17 +231,17 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis H_busy_interval :
definitions.busy_interval sched interference interfering_workload j t1 t2.
- (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+ (** Let's define A as a relative arrival time of job j (with respect to time [t1]). *)
Let A := job_arrival j - t1.
- (** Consider an arbitrary shift Δ inside the busy interval ... *)
+ (** Consider an arbitrary offset [Δ] inside the busy interval ... *)
Variable Δ : duration.
Hypothesis H_Δ_in_busy : t1 + Δ < t2.
(** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
- (** We define a predicate [EDF_from tsk].Predicate [EDF_from tsk]
+ (** We define a predicate [EDF_from tsk]. The predicate [EDF_from tsk]
holds true for any job [jo] of task [tsk] such that
[job_deadline jo <= job_deadline j]. *)
Let EDF_from (tsk : Task) := fun (jo : Job) => EDF jo j && (job_task jo == tsk).
@@ -355,7 +355,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
- interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
+ interval of length [Δ] is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
Let total_interference_bound tsk (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + IBF_other A Δ.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 9bacf139f..1773ba209 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -199,7 +199,7 @@ Section AbstractRTAforFPwithArrivalCurves.
Recall that in module abstract_seq_RTA hypothesis task_interference_is_bounded_by expects
to receive a function that maps some task t, the relative arrival time of a job j of task t,
and the length of the interval to the maximum amount of interference (for more details see
- files limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
+ the modules [limited.abstract_RTA.definitions] and [limited.abstract_RTA.abstract_seq_rta]).
However, in this module we analyze only one task -- [tsk], therefore it is “hard-codedâ€
inside the interference bound function [IBF_other]. Moreover, in case of a model with fixed
@@ -253,7 +253,7 @@ Section AbstractRTAforFPwithArrivalCurves.
(** Given any job j of task [tsk] that arrives exactly A units after the beginning of
the busy interval, the bound of the total interference incurred by j within an
- interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other Δ]. *)
+ interval of length [Δ] is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other Δ]. *)
Let total_interference_bound tsk A Δ :=
task_rbf (A + ε) - task_cost tsk + IBF_other Δ.
diff --git a/util/list.v b/util/list.v
index 0bc795711..ce4d329a6 100644
--- a/util/list.v
+++ b/util/list.v
@@ -157,7 +157,7 @@ Section Max0.
Proof. by intros; rewrite !max0_cons maxnA [maxn x1 x2]maxnE subnKC. Qed.
(** We prove that [max0] of a sequence [xs]
- is equal to [max0] of sequence [xs] without 0s. *)
+ is equal to [max0] of [xs] without any zeros. *)
Lemma max0_rem0 :
forall xs,
max0 ([seq x <- xs | 0 < x]) = max0 xs.
diff --git a/util/setoid.v b/util/setoid.v
index 9e9cc4f3d..b0ba96f69 100644
--- a/util/setoid.v
+++ b/util/setoid.v
@@ -1,5 +1,5 @@
(** Setoid Rewriting with boolean inequalities of ssreflect. Solution
- suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016) *)
+ suggested by Georges Gonthier (ssreflect mailing list @ 18.12.2016) *)
From Coq Require Import Basics Setoid Morphisms.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
diff --git a/util/sum.v b/util/sum.v
index dbc969c9a..896580e7d 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -214,7 +214,7 @@ End SumsOverSequences.
(** In this section, we prove a variety of properties of sums performed over ranges. *)
Section SumsOverRanges.
- (** First, we prove that the sum of Δ ones is equal to Δ . *)
+ (** First, we prove that the sum of [Δ] ones is equal to [Δ]. *)
Lemma sum_of_ones:
forall t Δ,
\sum_(t <= x < t + Δ) 1 = Δ.
diff --git a/util/tactics.v b/util/tactics.v
index 603bb587d..b8ba3b152 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -72,12 +72,12 @@ Ltac feed H :=
end.
(* Generalization of feed for multiple hypotheses.
- feed_n is useful for accessing conclusions of long implications.
+ [feed_n[ is useful for accessing conclusions of long implications.
- Usage: feed_n 3 H.
- H: P1 -> P2 -> P3 -> Q.
+ Usage: <<feed_n 3 H.>>
+ <<H: P1 -> P2 -> P3 -> Q.>>
- We'll be asked to prove P1, P2 and P3, so that Q can be inferred. *)
+ We'll be asked to prove [P1], [P2] and [P3], so that Q can be inferred. *)
Ltac feed_n n H := match constr:(n) with
| O => idtac
| (S ?m) => feed H ; [| feed_n m H]
--
GitLab