From fbcbb9973368e0eebaacfdc6279c8ffb15834bd3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 2 Dec 2019 13:52:41 +0100
Subject: [PATCH] address spell-checking issues in EDF optimality proof
---
.../analysis/facts/transform/edf_opt.v | 60 ++++++++++---------
.../analysis/facts/transform/replace_at.v | 32 +++++-----
.../analysis/facts/transform/swaps.v | 6 +-
restructuring/analysis/transform/edf_trans.v | 46 +++++++-------
4 files changed, 74 insertions(+), 70 deletions(-)
diff --git a/restructuring/analysis/facts/transform/edf_opt.v b/restructuring/analysis/facts/transform/edf_opt.v
index 2536c0ca6..8bc9b823f 100644
--- a/restructuring/analysis/facts/transform/edf_opt.v
+++ b/restructuring/analysis/facts/transform/edf_opt.v
@@ -7,9 +7,9 @@ Require Export rt.restructuring.analysis.facts.readiness.basic.
(** This file contains the main argument of the EDF optimality proof,
starting with an analysis of the individual functions that drive
- the "EDF-ication" of a given reference schedule and ending with
- the proofs of individual properties of the obtained EDF
- schedule. *)
+ the piece-wise transformation of a given reference schedule in an
+ EDF schedule, and ending with proofs of individual properties of
+ the obtained EDF schedule. *)
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
@@ -170,7 +170,7 @@ End FindSwapCandidateFacts.
(** In the next section, we analyze properties of [make_edf_at], which
- we abbreviate as "mea" in the following. *)
+ we abbreviate as "[mea]" in the following. *)
Section MakeEDFAtFacts.
(** For any given type of jobs... *)
@@ -279,13 +279,14 @@ Section MakeEDFAtFacts.
(** Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
- sched'. As this is a larger argument, we proceed by case analysis and
+ [sched']. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section GuaranteeCaseAnalysis.
- (** Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
- denote the job scheduled in sched' at time t_edf, and let j' denote any
- job scheduled in sched' at some time t' after t_edf... *)
+ (** Let [j_orig] denote the job scheduled in [sched] at time
+ [t_edf], let [j_edf] denote the job scheduled in [sched'] at
+ time [t_edf], and let [j'] denote any job scheduled in
+ [sched'] at some time [t'] after [t_edf]... *)
Variable j_orig j_edf j': Job.
Variable t': instant.
@@ -295,18 +296,18 @@ Section MakeEDFAtFacts.
Hypothesis H_sched_edf: scheduled_at sched' j_edf t_edf.
Hypothesis H_sched': scheduled_at sched' j' t'.
- (** ... and that arrives before time t_edf. *)
+ (** ... and that arrives before time [t_edf]. *)
Hypothesis H_arrival_j' : job_arrival j' <= t_edf.
(** We begin by observing three simple facts that will be used repeatedly in
- the case analysis. *)
+ the case analysis. *)
- (** First, the deadline of j_orig is later than t_edf. *)
+ (** First, the deadline of [j_orig] is later than [t_edf]. *)
Fact mea_guarantee_dl_orig: t_edf < job_deadline j_orig.
Proof. by apply (scheduled_job_in_sched_has_later_deadline j_orig t_edf H_sched_orig). Qed.
- (** Second, by the definition of sched', j_edf is scheduled in sched at the time
- returned by [find_swap_candidate]. *)
+ (** Second, by the definition of [sched'], [j_edf] is scheduled in
+ [sched] at the time returned by [find_swap_candidate]. *)
Fact mea_guarantee_fsc_is_j_edf: sched (find_swap_candidate sched t_edf j_orig) = Some j_edf.
Proof.
move: (H_sched_orig). rewrite scheduled_at_def => /eqP SCHED.
@@ -317,7 +318,8 @@ Section MakeEDFAtFacts.
- by rewrite ifT // => /eqP.
Qed.
- (** Third, the deadline of j_edf is no later than the deadline of j_orig. *)
+ (** Third, the deadline of [j_edf] is no later than the deadline
+ of [j_orig]. *)
Fact mea_guarantee_deadlines: job_deadline j_edf <= job_deadline j_orig.
Proof.
apply: (fsc_no_later_deadline sched _ _ t_edf) => //.
@@ -327,11 +329,12 @@ Section MakeEDFAtFacts.
(** With the setup in place, we are now ready to begin the case analysis. *)
- (** First, we consider the simpler case where t' is no earlier than the
- deadline of j_orig. This case is simpler because t' being no earlier
- than j_orig's deadline implies that j' has deadline no earlier than
- j_orig (since no scheduled job in sched misses a deadline), which in
- turn has a deadline no earlier than j_edf. *)
+ (** First, we consider the simpler case where [t'] is no earlier
+ than the deadline of [j_orig]. This case is simpler because
+ [t'] being no earlier than [j_orig]'s deadline implies that
+ [j'] has deadline no earlier than [j_orig] (since no scheduled
+ job in [sched] misses a deadline), which in turn has a
+ deadline no earlier than [j_edf]. *)
Lemma mea_guarantee_case_t'_past_deadline:
job_deadline j_orig <= t' ->
job_deadline j_edf <= job_deadline j'.
@@ -343,8 +346,8 @@ Section MakeEDFAtFacts.
by apply ltnW.
Qed.
- (** Next, we consider the more difficult case, where t' is before the
- deadline of j_orig. *)
+ (** Next, we consider the more difficult case, where [t'] is
+ before the deadline of [j_orig]. *)
Lemma mea_guarantee_case_t'_before_deadline:
t' < job_deadline j_orig ->
job_deadline j_edf <= job_deadline j'.
@@ -378,8 +381,9 @@ Section MakeEDFAtFacts.
End GuaranteeCaseAnalysis.
- (** Finally, putting the preceding case analysis together, we obtain the
- result that [make_edf_at] establishes [EDF_at] at time [t_edf]. *)
+ (** Finally, putting the preceding cases together, we obtain the
+ result that [make_edf_at] establishes [EDF_at] at time
+ [t_edf]. *)
Lemma make_edf_at_guarantee:
EDF_at sched' t_edf.
Proof.
@@ -394,8 +398,8 @@ Section MakeEDFAtFacts.
by apply: (mea_guarantee_case_t'_past_deadline j_orig j_edf j' t').
Qed.
- (** We observe that [make_edf_at] maintains the property that jobs must arrive
- to execute. *)
+ (** We observe that [make_edf_at] maintains the property that jobs
+ must arrive to execute. *)
Lemma mea_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
Proof.
@@ -535,7 +539,7 @@ Section EDFPrefixFacts.
(** Consider any point in time, denoted [horizon], and... *)
Variable horizon: instant.
- (** ...let [sched'] denote the schedule obtained by EDF-ifying
+ (** ...let [sched'] denote the schedule obtained by transforming
[sched] up to the horizon. *)
Let sched' := edf_transform_prefix sched horizon.
@@ -707,8 +711,8 @@ Section EDFPrefixInclusion.
End EDFPrefixInclusion.
-(** In the following section, we finally establish properties of the overall
- EDF-ication operation [edf_transform]. *)
+(** In the following section, we finally establish properties of the
+ overall EDF transformation[edf_transform]. *)
Section EDFTransformFacts.
(** For any given type of jobs... *)
diff --git a/restructuring/analysis/facts/transform/replace_at.v b/restructuring/analysis/facts/transform/replace_at.v
index 20a2fe23b..29a4d8805 100644
--- a/restructuring/analysis/facts/transform/replace_at.v
+++ b/restructuring/analysis/facts/transform/replace_at.v
@@ -21,12 +21,12 @@ Section ReplaceAtFacts.
(** ...and a replacement state [state]. *)
Variable nstate: PState.
- (** In the following, let sched' denote the schedule with replacement at time
+ (** In the following, let [sched'] denote the schedule with replacement at time
t'. *)
Let sched' := replace_at sched t' nstate.
(** We begin with the trivial observation that the schedule doesn't change at
- other times. *)
+ other times. *)
Lemma rest_of_schedule_invariant:
forall t, t <> t' -> sched' t = sched t.
Proof.
@@ -36,8 +36,8 @@ Section ReplaceAtFacts.
by move/eqP in TT; rewrite TT in DIFF; contradiction.
Qed.
- (** As a result, the service in intervals that do not intersect with t' is
- invariant, too. *)
+ (** As a result, the service in intervals that do not intersect with
+ [t'] is invariant, too. *)
Lemma service_at_other_times_invariant:
forall t1 t2,
t2 <= t' \/ t' < t1 ->
@@ -54,10 +54,10 @@ Section ReplaceAtFacts.
apply /andP; by split.
Qed.
- (** Next, we consider the amount of service received in intervals that do span
- across the replacement point. We can relate the service received in the
- original and the new schedules by adding the service in the respective
- "missing" state... *)
+ (** Next, we consider the amount of service received in intervals
+ that do span across the replacement point. We can relate the
+ service received in the original and the new schedules by adding
+ the service in the respective "missing" state... *)
Lemma service_delta:
forall t1 t2,
t1 <= t' < t2 ->
@@ -82,10 +82,11 @@ Section ReplaceAtFacts.
service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.
Proof. move => t1 t2 ORDER j. by rewrite service_delta// addnK. Qed.
- (** As another simple invariant (useful for case analysis), we observe that if
- a job is scheduled neither in the replaced nor in the new state, then at
- any time it receives exactly the same amount of service in the new
- schedule with replacements as in the original schedule. *)
+ (** As another simple invariant (useful for case analysis), we
+ observe that if a job is scheduled neither in the replaced nor
+ in the new state, then at any time it receives exactly the same
+ amount of service in the new schedule with replacements as in
+ the original schedule. *)
Lemma service_at_of_others_invariant (j: Job):
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
@@ -99,9 +100,10 @@ Section ReplaceAtFacts.
- rewrite rest_of_schedule_invariant//.
Qed.
- (** Based on the previous observation, we can trivially lift the invariant
- that jobs not involved in the replacement receive equal service to the
- cumulative service received in any interval. *)
+ (** Based on the previous observation, we can trivially lift the
+ invariant that jobs not involved in the replacement receive
+ equal service to the cumulative service received in any
+ interval. *)
Corollary service_during_of_others_invariant (j: Job):
~~ scheduled_in j (sched' t') ->
~~ scheduled_in j (sched t') ->
diff --git a/restructuring/analysis/facts/transform/swaps.v b/restructuring/analysis/facts/transform/swaps.v
index 7529e887a..1b27adf6b 100644
--- a/restructuring/analysis/facts/transform/swaps.v
+++ b/restructuring/analysis/facts/transform/swaps.v
@@ -295,11 +295,11 @@ Section SwappedScheduleProperties.
Hypothesis H_order: t1 <= t2.
(** We let [sched'] denote the schedule in which the allocations at
- [t1] and [t2] have been swapped. *)
+ [t1] and [t2] have been swapped. *)
Let sched' := swapped sched t1 t2.
- (** First, we observe that if jobs never accomulate more service than
- required, then that's still the case after the swap. *)
+ (** First, we observe that if jobs never accumulate more service than
+ required, then that's still the case after the swap. *)
Lemma swapped_service_bound:
(forall j t, service sched j t <= job_cost j) ->
(forall j t, service sched' j t <= job_cost j).
diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 65ed0841b..0d6a78dd1 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -1,8 +1,9 @@
Require Export rt.restructuring.analysis.transform.prefix.
Require Export rt.restructuring.analysis.transform.swap.
-(** In this file we define the "EDF-ification" of a schedule, the
- operation at the core of the EDF optimality proof. *)
+(** In this file we define the EDF transformation of a schedule, which turns a
+ (finite prefix of a) schedule into an EDF schedule. This operation is at
+ the core of the EDF optimality proof. *)
Section EDFTransformation.
(** Consider any given type of jobs... *)
@@ -12,37 +13,34 @@ Section EDFTransformation.
Let PState := ideal.processor_state Job.
Let SchedType := schedule (PState).
- (** We say that a state s1 "has an earlier or equal deadline" than a
- state s2 if the job scheduled in state s1 has has an earlier or
- equal deadline than the job scheduled in state s2. This function
- is never used on idle states, so the default values are
- irrelevant. *)
+ (** We say that a state [s1] "has an earlier or equal deadline" than a state
+ [s2] if the job scheduled in state [s1] has has an earlier or equal
+ deadline than the job scheduled in state [s2]. This function is never
+ used on idle states, so the default values are irrelevant. *)
Definition earlier_deadline (s1 s2: PState) :=
(oapp job_deadline 0 s1) <= (oapp job_deadline 0 s2).
- (** We say that a state is relevant (for the purpose of the
- transformation) if it is not idle and if the job scheduled in it
- has arrived prior to some given reference time. *)
+ (** We say that a state is relevant (for the purpose of the transformation)
+ if it is not idle and if the job scheduled in it has arrived prior to
+ some given reference time. *)
Definition relevant_pstate (reference_time: instant) (s: PState) :=
match s with
| None => false
| Some j' => job_arrival j' <= reference_time
end.
- (** Next, we define a central element of the "EDF-ification"
- procedure: given a job scheduled at a time t1, find a later time
- t2 before the job's deadlineat which a job with an
- earlier-or-equal deadline is scheduled. In other words, find a
- job that causes the [EDF_at] property to be violated at time
- t1. *)
+ (** Next, we define a central element of the EDF transformation procedure:
+ given a job scheduled at a time [t1], find a later time [t2] before the
+ job's deadline at which a job with an earlier-or-equal deadline is
+ scheduled. In other words, find a job that causes the [EDF_at] property
+ to be violated at time [t1]. *)
Definition find_swap_candidate (sched: SchedType) (t1: instant) (j: Job) :=
if search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j) is Some t
then t
else 0.
- (** The point-wise EDF-ification procedure: given a schedule and a
- time t1, ensure that the schedule satisfies [EDF_at] at time
- t1. *)
+ (** The point-wise EDF transformation procedure: given a schedule and a time
+ [t1], ensure that the schedule satisfies [EDF_at] at time [t1]. *)
Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
match sched t1 with
| None => sched (* leave idle instants alone *)
@@ -53,14 +51,14 @@ Section EDFTransformation.
end.
(** To transform a finite prefix of a given reference schedule, apply
- [make_edf_at] to every point up to the given finite horizon. *)
+ [make_edf_at] to every point up to the given finite horizon. *)
Definition edf_transform_prefix (sched: SchedType) (horizon: instant): SchedType :=
prefix_map sched make_edf_at horizon.
- (** Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
- at any time) is obtained by first computing an EDF prefix up to
- and including the requested time t, and by then looking at the
- last point of the prefix. *)
+ (** Finally, a full EDF schedule (i.e., one that satisfies [EDF_at] at any
+ time) is obtained by first computing an EDF prefix up to and including
+ the requested time [t], and by then looking at the last point of the
+ prefix. *)
Definition edf_transform (sched: SchedType) (t: instant): ideal.processor_state Job :=
let
edf_prefix := edf_transform_prefix sched t.+1
--
GitLab