diff --git a/restructuring/analysis/abstract/abstract_rta.v b/restructuring/analysis/abstract/abstract_rta.v
index 088b34a7f838d397d488c73933854b1b7a63fca0..3912dd54cdf031a28f7efd1d01da9a1b20a61796 100644
--- a/restructuring/analysis/abstract/abstract_rta.v
+++ b/restructuring/analysis/abstract/abstract_rta.v
@@ -6,9 +6,9 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Abstract Response-Time Analysis *)
(** In this module, we propose the general framework for response-time analysis (RTA)
- of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
+ of uni-processor scheduling of real-time tasks with arbitrary arrival models. *)
(** We prove that the maximum (with respect to the set of offsets) among the solutions
- of the response-time bound recurrence is a response time bound for tsk. Note that
+ of the response-time bound recurrence is a response time bound for [tsk]. Note that
in this section we do not rely on any hypotheses about job sequentiality. *)
Section Abstract_RTA.
@@ -29,7 +29,7 @@ Section Abstract_RTA.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
- (** Next, consider any uniprocessor schedule of this arrival sequence...*)
+ (** Next, consider any uni-processor schedule of this arrival sequence...*)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
@@ -44,7 +44,7 @@ Section Abstract_RTA.
(** Consider a task set ts... *)
Variable ts : list Task.
- (** ... and a task tsk of ts that is to be analyzed. *)
+ (** ... and a task [tsk] of ts that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
@@ -53,8 +53,8 @@ Section Abstract_RTA.
valid_preemption_model arr_seq sched.
(** ...and a valid task run-to-completion threshold function. That is,
- [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
+ [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. *)
Hypothesis H_valid_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
@@ -77,13 +77,13 @@ Section Abstract_RTA.
Let busy_interval := busy_interval sched interference interfering_workload.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
- (** Let L be a constant which bounds any busy interval of task tsk. *)
+ (** Let L be a constant which bounds any busy interval of task [tsk]. *)
Variable L : duration.
Hypothesis H_busy_interval_exists:
busy_intervals_are_bounded_by interference interfering_workload L.
(** Next, assume that interference_bound_function is a bound on
- the interference incurred by jobs of task tsk. *)
+ the interference incurred by jobs of task [tsk]. *)
Variable interference_bound_function : Task -> duration -> duration -> duration.
Hypothesis H_job_interference_is_bounded:
job_interference_is_bounded_by
@@ -92,9 +92,9 @@ Section Abstract_RTA.
(** For simplicity, let's define a local name for the search space. *)
Let is_in_search_space A := is_in_search_space tsk L interference_bound_function A.
- (** Consider any value R that upper-bounds the solution of each response-time recurrence,
+ (** Consider any value [R] that upper-bounds the solution of each response-time recurrence,
i.e., for any relative arrival time A in the search space, there exists a corresponding
- solution F such that F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R. *)
+ solution [F] such that [F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R]. *)
Variable R: nat.
Hypothesis H_R_is_maximum:
forall A,
@@ -105,10 +105,10 @@ Section Abstract_RTA.
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
(** In this section we show a detailed proof of the main theorem
- that establishes that R is a response-time bound of task tsk. *)
+ that establishes that R is a response-time bound of task [tsk]. *)
Section ProofOfTheorem.
- (** Consider any job j of tsk with positive cost. *)
+ (** Consider any job j of [tsk] with positive cost. *)
Variable j: Job.
Hypothesis H_j_arrives: arrives_in arr_seq j.
Hypothesis H_job_of_tsk: job_task j = tsk.
@@ -123,29 +123,29 @@ Section Abstract_RTA.
(** In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum.
Note that the relative arrival time (A) is not necessarily from the search space. However,
- earlier we have proven that for any A there exists another A_sp from the search space that
- shares the same IBF value. Moreover, we've also shown that there exists an F_sp such that
- F_sp is a solution of the response time recurrence for parameter A_sp. Thus, despite the
+ earlier we have proven that for any A there exists another [A_sp] from the search space that
+ shares the same IBF value. Moreover, we've also shown that there exists an [F_sp] such that
+ [F_sp] is a solution of the response time recurrence for parameter [A_sp]. Thus, despite the
fact that the relative arrival time may not lie in the search space, we can still use
the assumption H_R_is_maximum. *)
- (** More formally, consider any A_sp and F_sp such that:.. *)
+ (** More formally, consider any [A_sp] and [F_sp] such that:.. *)
Variable A_sp F_sp : duration.
- (** (a) A_sp is less than or equal to A... *)
+ (** (a) [A_sp] is less than or equal to [A]... *)
Hypothesis H_A_gt_Asp : A_sp <= A.
- (** (b) interference_bound_function(A, x) is equal to
- interference_bound_function(A_sp, x) for all x less than L... *)
+ (** (b) [interference_bound_function(A, x)] is equal to
+ [interference_bound_function(A_sp, x)] for all [x] less than [L]... *)
Hypothesis H_equivalent :
are_equivalent_at_values_less_than
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) L.
- (** (c) A_sp is in the search space, ... *)
+ (** (c) [A_sp] is in the search space, ... *)
Hypothesis H_Asp_is_in_search_space : is_in_search_space A_sp.
- (** (d) [A_sp + F_sp] is a solution of the response time reccurence... *)
+ (** (d) [A_sp + F_sp] is a solution of the response time recurrence... *)
Hypothesis H_Asp_Fsp_fixpoint :
A_sp + F_sp = task_run_to_completion_threshold tsk + interference_bound_function tsk A_sp (A_sp + F_sp).
@@ -162,7 +162,7 @@ Section Abstract_RTA.
(** 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. *)
+ (** Then we prove that [job_arrival j + R] is no less than [t2]. *)
Lemma t2_le_arrival_plus_R:
t2 <= job_arrival j + R.
Proof.
@@ -197,32 +197,32 @@ Section Abstract_RTA.
Hypothesis H_small_fixpoint_solution : t1 + (A_sp + F_sp) < t2.
(** Next, let's consider two other cases: *)
- (** CASE 1: the value of the fixpoint is no less than the relative arrival time of job j. *)
+ (** CASE 1: the value of the fix-point is no less than the relative arrival time of job [j]. *)
Section FixpointIsNoLessThanArrival.
- (** Suppose that [A_sp + F_sp] is no less than relative arrival of job j. *)
+ (** Suppose that [A_sp + F_sp] is no less than relative arrival of job [j]. *)
Hypothesis H_fixpoint_is_no_less_than_relative_arrival_of_j : A <= A_sp + F_sp.
- (** In this section, we prove that the fact that job j is not completed by
+ (** In this section, we prove that the fact that job [j] is not completed by
time [job_arrival j + R] leads to a contradiction. Which in turn implies
- that the opposite is true -- job j completes by time [job_arrival j + R]. *)
+ that the opposite is true -- job [j] completes by time [job_arrival j + R]. *)
Section ProofByContradiction.
- (** Recall that by lemma "solution_for_A_exists" there is a solution F
- of the response-time recurrence for the given relative arrival time A
+ (** Recall that by lemma "solution_for_A_exists" there is a solution [F]
+ of the response-time recurrence for the given relative arrival time [A]
(which is not necessarily from the search space). *)
- (** Thus, consider a constant F such that:.. *)
+ (** Thus, consider a constant [F] such that:.. *)
Variable F : duration.
- (** (a) the sum of A_sp and F_sp is equal to the sum of A and F... *)
+ (** (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 most F_sp... *)
+ (** (b) [F] is at mo1st [F_sp]... *)
Hypothesis H_F_le_Fsp : F <= F_sp.
- (** (c) and [A + F] is a solution for the response-time recurrence for A. *)
+ (** (c) and [A + F] is a solution for the response-time recurrence for [A]. *)
Hypothesis H_A_F_fixpoint:
A + F = task_run_to_completion_threshold tsk + interference_bound_function tsk A (A + F).
- (** Next, we assume that job j is not completed by time [job_arrival j + R]. *)
+ (** Next, we assume that job [j] is not completed by time [job_arrival j + R]. *)
Hypothesis H_j_not_completed : ~~ completed_by sched j (job_arrival j + R).
(** Some additional reasoning is required since the term [task_cost tsk - task_run_to_completion_threshold tsk]
@@ -233,25 +233,25 @@ Section Abstract_RTA.
in the case of floating non-preemptive sections).
In this case we cannot directly apply lemma "j_receives_at_least_run_to_completion_threshold". Therefore
- we introduce two temporal notions of the last nonpreemptive region of job j and an execution
+ we introduce two temporal notions of the last non-preemptive region of job j and an execution
optimism. We use these notions inside this proof, so we define them only locally. *)
- (** Let the last nonpreemptive region of job j (last) be the difference between the cost of the job
- and the j's run-to-completion threshold (i.e. [job_cost j - job_run_to_completion_threshold j]).
+ (** Let the last non-preemptive region of job [j] (last) be the difference between the cost of the job
+ and the [j]'s run-to-completion threshold (i.e. [job_cost j - job_run_to_completion_threshold j]).
We know that after j has reached its run-to-completion threshold, it will additionally be executed
[job_last j] units of time. *)
Let job_last := job_cost j - job_run_to_completion_threshold j.
- (** And let execution optimism (optimism) be the difference between the tsk's
- run-to-completion threshold and the j's run-to-completion threshold (i.e.
+ (** And let execution optimism (optimism) be the difference between the [tsk]'s
+ run-to-completion threshold and the [j]'s run-to-completion threshold (i.e.
[task_run_to_completion_threshold - job_run_to_completion_threshold]).
Intuitively, optimism is how much earlier job j has received its
run-to-completion threshold than it could at worst. *)
Let optimism := task_run_to_completion_threshold tsk - job_run_to_completion_threshold j.
- (** From lemma "j_receives_at_least_run_to_completion_threshold" with parametetrs [progress_of_job :=
- job_run_to_completion_threshold j] and [delta := (A + F) - optimism)] we know that service of j
- by time [t1 + (A + F) - optimism] is no less than [job_run_to_completion_threshold j]. Hence, job j
+ (** From lemma "j_receives_at_least_run_to_completion_threshold" with parameters [progress_of_job :=
+ job_run_to_completion_threshold j] and [delta := (A + F) - optimism)] we know that service of [j]
+ by time [t1 + (A + F) - optimism] is no less than [job_run_to_completion_threshold j]. Hence, job [j]
is completed by time [t1 + (A + F) - optimism + last]. *)
Lemma j_is_completed_by_t1_A_F_optimist_last :
completed_by sched j (t1 + (A + F - optimism) + job_last).
@@ -295,10 +295,10 @@ Section Abstract_RTA.
So, for example [a + (b - c) = a + b - c] only if [b ≥ c]. *)
Section AuxiliaryInequalities.
- (** Recall that we consider a busy interval of a job j, and j has arrived A time units
+ (** Recall that we consider a busy interval of a job [j], and [j] has arrived [A] time units
after the beginning the busy interval. From basic properties of a busy interval it
- follows that job j incurrs interference at any time instant t ∈ [t1, t1 + A).
- Therefore interference_bound_function(tsk, A, A + F) is at least A. *)
+ follows that job [j] incurs interference at any time instant t ∈ [t1, t1 + A).
+ Therefore [interference_bound_function(tsk, A, A + F)] is at least [A]. *)
Lemma relative_arrival_le_interference_bound:
A <= interference_bound_function tsk A (A + F).
Proof.
@@ -342,7 +342,7 @@ Section Abstract_RTA.
Qed.
(** As two trivial corollaries, we show that
- tsk's run-to-completion threshold is at most F_sp... *)
+ [tsk]'s run-to-completion threshold is at most [F_sp]... *)
Corollary tsk_run_to_completion_threshold_le_Fsp :
task_run_to_completion_threshold tsk <= F_sp.
Proof.
@@ -354,7 +354,7 @@ Section Abstract_RTA.
apply leq_trans with F; auto.
Qed.
- (** ... and optimism is at most F. *)
+ (** ... and optimism is at most [F]. *)
Corollary optimism_le_F :
optimism <= F.
Proof.
@@ -371,13 +371,13 @@ Section Abstract_RTA.
(** Next we show that [t1 + (A + F) - optimism + last] is at most [job_arrival j + R],
which is easy to see from the following sequence of inequalities:
- t1 + (A + F) - optimism + last
- ≤ job_arrival j + (F - optimism) + job_last
- ≤ job_arrival j + (F_sp - optimism) + job_last
- ≤ job_arrival j + F_sp + (job_last - optimism)
- ≤ job_arrival j + F_sp + job_cost j - task_run_to_completion_threshold tsk
- ≤ job_arrival j + F_sp + task_cost tsk - task_run_to_completion_threshold tsk
- ≤ job_arrival j + R. *)
+ [t1 + (A + F) - optimism + last]
+ [≤ job_arrival j + (F - optimism) + job_last]
+ [≤ job_arrival j + (F_sp - optimism) + job_last]
+ [≤ job_arrival j + F_sp + (job_last - optimism)]
+ [≤ job_arrival j + F_sp + job_cost j - task_run_to_completion_threshold tsk]
+ [≤ job_arrival j + F_sp + task_cost tsk - task_run_to_completion_threshold tsk]
+ [≤ job_arrival j + R]. *)
Lemma t1_A_F_optimist_last_le_arrival_R :
t1 + (A + F - optimism) + job_last <= job_arrival j + R.
Proof.
@@ -406,7 +406,7 @@ Section Abstract_RTA.
}
Qed.
- (** ... which contradicts the initial assumption about j is not
+ (** ... which contradicts the initial assumption about [j] is not
completed by time [job_arrival j + R]. *)
Lemma j_is_completed_earlier_contradiction : False.
Proof.
@@ -417,7 +417,7 @@ Section Abstract_RTA.
End ProofByContradiction.
- (** Putting everything together, we conclude that j is completed by [job_arrival j + R]. *)
+ (** Putting everything together, we conclude that [j] is completed by [job_arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_2:
completed_by sched j (job_arrival j + R).
Proof.
@@ -445,9 +445,9 @@ Section Abstract_RTA.
End FixpointIsNoLessThanArrival.
- (** CASE 2: the value of the fixpoint is less than the relative arrival time of
- job j (which turns out to be impossible, i.e. the solution of the responce-time
- recurrense is always equal to or greater than the relative arrival time). *)
+ (** CASE 2: the value of the fix-point is less than the relative arrival time of
+ job j (which turns out to be impossible, i.e. the solution of the response-time
+ recurrence is always equal to or greater than the relative arrival time). *)
Section FixpointCannotBeSmallerThanArrival.
(** Assume that [A_sp + F_sp] is less than A. *)
@@ -497,8 +497,8 @@ Section Abstract_RTA.
by rewrite {2}H_Asp_Fsp_fixpoint leq_add //; apply H_valid_run_to_completion_threshold.
Qed.
- (** However, this is a contradiction. Since job j has not yet arrived, its service
- is equal to 0. However, run-to-completion threshold is always positive. *)
+ (** However, this is a contradiction. Since job [j] has not yet arrived, its service
+ is equal to [0]. However, run-to-completion threshold is always positive. *)
Lemma relative_arrival_time_is_no_less_than_fixpoint:
False.
Proof.
@@ -518,7 +518,7 @@ Section Abstract_RTA.
End ProofOfTheorem.
- (** Using the lemmas above, we prove that R is a response-time bound. *)
+ (** Using the lemmas above, we prove that [R] is a response-time bound. *)
Theorem uniprocessor_response_time_bound:
response_time_bounded_by tsk R.
Proof.
diff --git a/restructuring/analysis/abstract/abstract_seq_rta.v b/restructuring/analysis/abstract/abstract_seq_rta.v
index 41c01f68161f5efa43e2344b9168bd86091cda32..3effc1a50c581bb04d0bf0f34cc50cc60227e43d 100644
--- a/restructuring/analysis/abstract/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/abstract_seq_rta.v
@@ -8,11 +8,11 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Abstract Response-Time Analysis with sequential tasks *)
(** In this section we propose the general framework for response-time analysis (RTA)
- of uniprocessor scheduling of real-time tasks with arbitrary arrival models
+ of uni-processor scheduling of real-time tasks with arbitrary arrival models
and sequential tasks. *)
(** We prove that the maximum among the solutions of the response-time bound
- recurrence for some set of parameters is a response-time bound for tsk.
+ recurrence for some set of parameters is a response-time bound for [tsk].
Note that in this section we _do_ rely on the hypothesis about task
sequentiality. This allows us to provide a more precise response-time
bound function, since jobs of the same task will be executed strictly
@@ -51,7 +51,7 @@ Section Sequential_Abstract_RTA.
(** Consider an arbitrary task set. *)
Variable ts : list Task.
- (** Let tsk be any task in ts that is to be analyzed. *)
+ (** Let [tsk] be any task in ts that is to be analyzed. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
@@ -60,15 +60,15 @@ Section Sequential_Abstract_RTA.
valid_preemption_model arr_seq sched.
(** ...and a valid task run-to-completion threshold function. That is,
- [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. *)
+ [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]. *)
Hypothesis H_valid_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
- (** 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 delta = 0. *)
+ (** 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 [delta = 0]. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
@@ -92,7 +92,7 @@ Section Sequential_Abstract_RTA.
(** When assuming sequential tasks, we can introduce an additional hypothesis that
ensures that the values of interference and workload remain consistent. It states
- that any of tsk's job, that arrived before the busy interval, should be
+ that any of [tsk]'s job, that arrived before the busy interval, should be
completed by the beginning of the busy interval. *)
Definition interference_and_workload_consistent_with_sequential_tasks :=
forall (j : Job) (t1 t2 : instant),
@@ -102,11 +102,11 @@ Section Sequential_Abstract_RTA.
busy_interval j t1 t2 ->
task_workload_between 0 t1 = task_service_of_jobs_in (arrivals_between 0 t1) 0 t1.
- (** Next we introduce the notion of task interference. Intuitively, task tsk incurs
- interference when some of the jobs of task tsk incur interference. As a result,
- tsk cannot make any progress. More formally, task tsk experiences interference at
- a time instant time t, if at time t task tsk is not scheduled and there exists
- a job of tsk that (1) experiences interference and (2) has arrived before some
+ (** Next we introduce the notion of task interference. Intuitively, task [tsk] incurs
+ interference when some of the jobs of task [tsk] incur interference. As a result,
+ [tsk] cannot make any progress. More formally, task [tsk] experiences interference at
+ a time instant time [t], if at time t task [tsk] is not scheduled and there exists
+ a job of [tsk] that (1) experiences interference and (2) has arrived before some
time instant [upper_bound].
It is important to note two subtle points: according to our semantics of the
@@ -115,7 +115,7 @@ Section Sequential_Abstract_RTA.
is why we use the term [~~ task_scheduled_at tsk t].
Moreover, in order to make the definition constructive, we introduce an upper bound
- on the arrival time of jobs from task tsk. As a result, we need to consider only a
+ on the arrival time of jobs from task [tsk]. As a result, we need to consider only a
finite number of jobs. For the function to produce the correct values it is enough
to specify a sufficiently large upper_bound. Usually as upper_bound one can use the
end of the corresponding busy interval. *)
@@ -127,11 +127,11 @@ Section Sequential_Abstract_RTA.
Definition cumul_task_interference tsk upper_bound t1 t2 :=
\sum_(t1 <= t < t2) task_interference_received_before tsk upper_bound t.
- (** We say that task interference is bounded by task_interference_bound_function (tIBF)
- iff for any job j of task tsk cumulative _task_ interference within the interval
- [t1, t1 + R) is bounded by function tIBF(tsk, A, R).
+ (** We say that task interference is bounded by task_interference_bound_function ([tIBF])
+ iff for any job [j] of task [tsk] cumulative _task_ interference within the interval
+ [t1, t1 + R) is bounded by function [tIBF(tsk, A, R)].
Note that this definition is almost the same as the definition of job_interference_is_bounded_by
- from the non-nesessary-sequential case. However, in this case we ignore the
+ from the non-necessary-sequential case. However, in this case we ignore the
interference that comes from jobs from the same task. *)
Definition task_interference_is_bounded_by
(task_interference_bound_function : Task -> duration -> duration -> duration) :=
@@ -147,7 +147,7 @@ Section Sequential_Abstract_RTA.
End Definitions.
(** In this section, we prove that the maximum among the solutions of the
- response-time bound recurrence is a response-time bound for tsk. *)
+ response-time bound recurrence is a response-time bound for [tsk]. *)
Section ResponseTimeBound.
(** For simplicity, let's define some local names. *)
@@ -166,7 +166,7 @@ Section Sequential_Abstract_RTA.
Hypothesis H_interference_and_workload_consistent_with_sequential_tasks:
interference_and_workload_consistent_with_sequential_tasks.
- (** Assume we have a constant L which bounds the busy interval of any of tsk's jobs. *)
+ (** Assume we have a constant L which bounds the busy interval of any of [tsk]'s jobs. *)
Variable L : duration.
Hypothesis H_busy_interval_exists:
busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
@@ -176,12 +176,12 @@ Section Sequential_Abstract_RTA.
Hypothesis H_task_interference_is_bounded:
task_interference_is_bounded_by task_interference_bound_function.
- (** Given any job j of task tsk that arrives exactly A units after the beginning of the busy
- interval, the bound on the total interference incurred by j within an interval of length Δ
+ (** Given any job [j] of task [tsk] that arrives exactly [A] units after the beginning of the busy
+ interval, the bound on the total interference incurred by [j] within an interval of length [Δ]
is no greater than [task_rbf (A + ε) - task_cost tsk + task's IBF Δ]. Note that in case of
sequential tasks the bound consists of two parts: (1) the part that bounds the interference
- received from other jobs of task tsk -- [task_rbf (A + ε) - task_cost tsk] and (2) any other
- interferece that is bounded by task_IBF(tsk, A, Δ). *)
+ received from other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost tsk] and (2) any other
+ interference that is bounded by [task_IBF(tsk, A, Δ)]. *)
Let total_interference_bound (tsk : Task) (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A Δ.
@@ -191,14 +191,14 @@ Section Sequential_Abstract_RTA.
[total_interference_bound (tsk, A, Δ) ≠total_interference_bound (tsk, A + ε, Δ)]. *)
Let is_in_search_space_seq := is_in_search_space tsk L total_interference_bound.
- (** Consider any value R, and assume that for any relative arrival time A from the search
- space there is a solution F of the response-time recurrence that is bounded by R. In
+ (** Consider any value [R], and assume that for any relative arrival time [A] from the search
+ space there is a solution [F] of the response-time recurrence that is bounded by [R]. In
contrast to the formula in "non-sequential" Abstract RTA, assuming that tasks are
sequential leads to a more precise response-time bound. Now we can explicitly express
the interference caused by other jobs of the task under consideration.
- To understand the right part of the fixpoint in the equation it is helpful to note
- that the bound on the total interference (bound_of_total_interference) is equal to
+ To understand the right part of the fix-point in the equation it is helpful to note
+ that the bound on the total interference ([bound_of_total_interference]) is equal to
[task_rbf (A + ε) - task_cost tsk + tIBF tsk A Δ]. Besides, a job must receive
enough service to become non-preemptive [task_lock_in_service tsk]. The sum of
these two quantities is exactly the right-hand side of the equation. *)
@@ -215,7 +215,7 @@ Section Sequential_Abstract_RTA.
considering the busy interval of the job under consideration. *)
Section CompletionOfJobsFromSameTask.
- (** Consider any two jobs j1 j2 of tsk. *)
+ (** Consider any two jobs [j1] [j2] of [tsk]. *)
Variable j1 j2 : Job.
Hypothesis H_j1_arrives: arrives_in arr_seq j1.
Hypothesis H_j2_arrives: arrives_in arr_seq j2.
@@ -227,7 +227,7 @@ Section Sequential_Abstract_RTA.
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j1 t1 t2.
- (** We prove that if a job from task tsk arrived before the beginning of the busy
+ (** We prove that if a job from task [tsk] arrived before the beginning of the busy
interval, then it must be completed before the beginning of the busy interval *)
Lemma completed_before_beginning_of_busy_interval:
job_arrival j2 < t1 ->
@@ -270,10 +270,10 @@ Section Sequential_Abstract_RTA.
fact that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
(** In this section we show that there exists a bound for cumulative interference for any
- job of task tsk, i.e., the hypothesis H_job_interference_is_bounded holds. *)
+ job of task [tsk], i.e., the hypothesis [H_job_interference_is_bounded] holds. *)
Section BoundOfCumulativeJobInterference.
- (** Consider any job j of tsk. *)
+ (** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
@@ -295,9 +295,9 @@ Section Sequential_Abstract_RTA.
(** In this section, 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). Note that the task workload is computed
+ interference of [j]'s task in the interval [t1, t1 + x). Note that the task workload is computed
only on the interval [t1, t1 + A + ε). Thanks to the hypothesis about sequential tasks, jobs of
- task tsk that arrive after [t1 + A + ε] cannot interfere with j. *)
+ task [tsk] that arrive after [t1 + A + ε] cannot interfere with j. *)
Section TaskInterferenceBoundsInterference.
(** We start by proving a simpler analog of the lemma which states that at
@@ -314,13 +314,13 @@ Section Sequential_Abstract_RTA.
Section Case1.
- (** Assume the processor is idle at time t. *)
+ (** Assume the processor is idle at time [t]. *)
Hypothesis H_idle : sched t = None.
(** In case when the processor is idle, one can show that
[interference j t = 1, scheduled_at j t = 0]. But since
- interference doesn't come from a job of task tsk
- [task_interferece tsk = 1]. Which reduces to [1 ≤ 1]. *)
+ interference doesn't come from a job of task [tsk]
+ [task_interference tsk = 1]. Which reduces to [1 ≤ 1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_idle:
interference j t + scheduled_at sched j t <=
service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t +
@@ -344,15 +344,15 @@ Section Sequential_Abstract_RTA.
Section Case2.
- (** Assume a job j' from another task is scheduled at time t. *)
+ (** Assume a job [j'] from another task is scheduled at time [t]. *)
Variable j' : Job.
Hypothesis H_sched : sched t = Some j'.
Hypothesis H_not_job_of_tsk : job_task j' != tsk.
- (** If a job j' from another task is scheduled at time t,
+ (** If a job [j]' from another task is scheduled at time [t],
then [interference j t = 1, scheduled_at j t = 0]. But
- since interference doesn't come from a job of task tsk
- [task_interferece tsk = 1]. Which reduces to [1 ≤ 1]. *)
+ since interference doesn't come from a job of task [tsk]
+ [task_interference tsk = 1]. Which reduces to [1 ≤ 1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_task:
interference j t + scheduled_at sched j t <=
service_of_jobs_at (job_of_task tsk) (arrivals_between t1 (t1 + A + ε)) t +
@@ -384,15 +384,15 @@ Section Sequential_Abstract_RTA.
Section Case3.
- (** Assume a job j' (different from j) of task tsk is scheduled at time t. *)
+ (** Assume a job [j'] (different from j) of task [tsk] is scheduled at time [t]. *)
Variable j' : Job.
Hypothesis H_sched : sched t = Some j'.
Hypothesis H_not_job_of_tsk : job_task j' == tsk.
Hypothesis H_j_neq_j' : j != j'.
- (** If a job j' (different from j) of task tsk is scheduled at time t, then
+ (** If a job [j'] (different from [j]) of task [tsk] is scheduled at time [t], then
[interference j t = 1, scheduled_at j t = 0]. Moreover, since interference
- comes from a job of the same task [task_interferece tsk = 0]. However,
+ comes from a job of the same task [task_interference tsk = 0]. However,
in this case [service_of_jobs of tsk = 1]. Which reduces to [1 ≤ 1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_job:
interference j t + scheduled_at sched j t <=
@@ -444,10 +444,10 @@ Section Sequential_Abstract_RTA.
Section Case4.
- (** Assume that job j is scheduled at time t. *)
+ (** Assume that job [j] is scheduled at time [t]. *)
Hypothesis H_sched : sched t = Some j.
- (** If job j is scheduled at time t, then [interference = 0, scheduled_at = 1], but
+ (** If job [j] is scheduled at time [t], then [interference = 0, scheduled_at = 1], but
note that [service_of_jobs of tsk = 1], therefore inequality reduces to [1 ≤ 1]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference_j:
interference j t + scheduled_at sched j t <=
@@ -551,7 +551,7 @@ Section Sequential_Abstract_RTA.
(** 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). *)
+ 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)
@@ -569,8 +569,8 @@ Section Sequential_Abstract_RTA.
(** In order to obtain a more convenient bound of the cumulative interference, we need to
abandon the actual workload in favor of a bound which depends on task parameters only.
- So, we show that actual workload of the task excluding workload of any job j is no
- greater than bound of workload excluding the cost of job j's task. *)
+ So, we show that actual workload of the task excluding workload of any job [j] is no
+ greater than bound of workload excluding the cost of job [j]'s task. *)
Lemma task_rbf_excl_tsk_bounds_task_workload_excl_j:
task_workload_between t1 (t1 + A + ε) - job_cost j <= task_rbf (A + ε) - task_cost tsk.
Proof.
@@ -615,7 +615,7 @@ Section Sequential_Abstract_RTA.
Qed.
(** Finally, we use the lemmas above to obtain the bound on
- interference in terms of task_rbf and task_interfere. *)
+ [interference] in terms of [task_rbf] and [task_interference]. *)
Lemma cumulative_job_interference_bound:
cumul_interference j t1 (t1 + x)
<= (task_rbf (A + ε) - task_cost tsk) + cumul_task_interference t2 t1 (t1 + x).
@@ -637,7 +637,7 @@ Section Sequential_Abstract_RTA.
(** In this section, we prove that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
Section MaxInSeqHypothesisImpMaxInNonseqHypothesis.
- (** Consider any job j of tsk. *)
+ (** Consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
diff --git a/restructuring/analysis/abstract/definitions.v b/restructuring/analysis/abstract/definitions.v
index 59fe51b6e3952473e69937e258d1d292371ddff6..3d3d5c05e1473b65a3f5abb0df284aa68b78d017 100644
--- a/restructuring/analysis/abstract/definitions.v
+++ b/restructuring/analysis/abstract/definitions.v
@@ -1,12 +1,12 @@
Require Export rt.restructuring.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
(** * Definitions for Abstract Response-Time Analysis *)
(** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA)
- of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
+ of uni-processor scheduling of real-time tasks with arbitrary arrival models. *)
Section AbstractRTADefinitions.
(** In this section, we introduce all the abstract notions required by the analysis. *)
@@ -24,18 +24,18 @@ Section AbstractRTADefinitions.
(** Consider any arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
- (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+ (** ... and any ideal uni-processor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
- (** Let tsk be any task that is to be analyzed *)
+ (** Let [tsk] be any task that is to be analyzed *)
Variable tsk : Task.
(** For simplicity, let's define some local names. *)
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by sched.
- (** Recall that a job j is pending_earlier_and_at a time instant t iff job
- j arrived before time t and is still not completed by time t. *)
+ (** Recall that a job [j] is pending_earlier_and_at a time instant [t] iff job
+ [j] arrived before time [t] and is still not completed by time [t]. *)
Let job_pending_earlier_and_at := pending_earlier_and_at sched.
(** We are going to introduce two main variables of the analysis:
@@ -46,29 +46,29 @@ Section AbstractRTADefinitions.
factors (preemption by higher-priority jobs, jitter, black-out periods in hierarchical
scheduling, lack of budget, etc.), which we call interference.
- Besides, note that even the n’th activation of a task can suffer from interference at
- the beggining of its busy interval (despite the fact that this job hasn’t even arrived
+ Besides, note that even the subsequent activation of a task can suffer from interference at
+ the beginning of its busy interval (despite the fact that this job hasn’t even arrived
at that moment!). Thus, it makes more sense (at least for the current busy-interval
analysis) to think about interference of a job as any interference within the
corresponding busy interval, and not after release of the job.
- Based on that, assume a predicate that expresses whether a job j under consideration
- incurs interference at a given time t (in the context of the schedule under consideration).
- This will be used later to upper-bound job j's response time. Note that a concrete
+ Based on that, assume a predicate that expresses whether a job [j] under consideration
+ incurs interference at a given time [t] (in the context of the schedule under consideration).
+ This will be used later to upper-bound job [j]'s response time. Note that a concrete
realization of the function may depend on the schedule, but here we do not require this
for the sake of simplicity and generality. *)
Variable interference : Job -> instant -> bool.
(** b) Interfering Workload *)
- (** In addition to interference, the analysis assumes that at any time t, we know an upper
+ (** In addition to interference, the analysis assumes that at any time [t], we know an upper
bound on the potential cumulative interference that can be incurred in the future by any
job (i.e., the total remaining potential delays). Based on that, assume a function
- interfering_workload that indicates for any job j, at any time t, the amount of potential
- interference for job j that is introduced into the system at time t. This function will be
+ interfering_workload that indicates for any job [j], at any time [t], the amount of potential
+ interference for job [j] that is introduced into the system at time [t]. This function will be
later used to upper-bound the length of the busy window of a job.
- One example of workload function is the "total cost of jobs that arrive at time t and
+ One example of workload function is the "total cost of jobs that arrive at time [t] and
have higher-or-equal priority than job j". In some task models, this function expresses
- the amount of the potential interference on job j that "arrives" in the system at time t. *)
+ the amount of the potential interference on job [j] that "arrives" in the system at time [t]. *)
Variable interfering_workload : Job -> instant -> duration.
(** In order to bound the response time of a job, we must to consider the cumulative
@@ -82,20 +82,20 @@ Section AbstractRTADefinitions.
incur interference. In this section, we provide a definition of an abstract busy interval. *)
Section BusyInterval.
- (** We say that time instant t is a quiet time for job j iff two conditions hold.
- First, the cumulative interference at time t must be equal to the cumulative
+ (** We say that time instant [t] is a quiet time for job [j] iff two conditions hold.
+ First, the cumulative interference at time [t] must be equal to the cumulative
interfering workload, to indicate that the potential interference seen so far
has been fully "consumed" (i.e., there is no more higher-priority work or other
- kinds of delay pending). Second, job j cannot be pending at any time earlier
- than t _and_ at time instant t (i.e., either it was pending earlier but is no
+ kinds of delay pending). Second, job [j] cannot be pending at any time earlier
+ than [t] _and_ at time instant [t] (i.e., either it was pending earlier but is no
longer pending now, or it was previously not pending and may or may not be
- released now), to ensure that the busy window captures the execution of job j. *)
+ released now), to ensure that the busy window captures the execution of job [j]. *)
Definition quiet_time (j : Job) (t : instant) :=
cumul_interference j 0 t = cumul_interfering_workload j 0 t /\
~~ job_pending_earlier_and_at j t.
(** Based on the definition of quiet time, we say that interval [t1, t2) is
- a (potentially unbounded) busy-interval prefix w.r.t. job j iff the
+ a (potentially unbounded) busy-interval prefix w.r.t. job [j] iff the
interval (a) contains the arrival of job j, (b) starts with a quiet
time and (c) remains non-quiet. *)
Definition busy_interval_prefix (j : Job) (t1 t2 : instant) :=
@@ -159,9 +159,9 @@ Section AbstractRTADefinitions.
busy interval that are fundamental for the analysis. *)
Section BusyIntervalProperties.
- (** We say that a schedule is "work_conserving" iff for any job j from task tsk and
- at any time t within a busy interval, there are only two options:
- either (a) interference(j, t) holds or (b) job j is scheduled at time t. *)
+ (** We say that a schedule is "work_conserving" iff for any job [j] from task [tsk] and
+ at any time [t] within a busy interval, there are only two options:
+ either (a) interference(j, t) holds or (b) job [j] is scheduled at time [t]. *)
Definition work_conserving :=
forall j t1 t2 t,
arrives_in arr_seq j ->
@@ -171,8 +171,8 @@ Section AbstractRTADefinitions.
t1 <= t < t2 ->
~ interference j t <-> job_scheduled_at j t.
- (** Next, we say that busy intervals of task tsk are bounded by L iff, for any job j of task
- tsk, there exists a busy interval with length at most L. Note that the existence of such a
+ (** Next, we say that busy intervals of task [tsk] are bounded by [L] iff, for any job [j] of task
+ [tsk], there exists a busy interval with length at most L. Note that the existence of such a
bounded busy interval is not guaranteed if the schedule is overloaded with work.
Therefore, in the later concrete analyses, we will have to introduce an additional
condition that prevents overload. *)
@@ -191,14 +191,14 @@ Section AbstractRTADefinitions.
issue, we define the notion of an interference bound. Note that according to the definition of
a work conserving schedule, interference does _not_ include execution of a job itself. Therefore,
an interference bound is not obliged to take into account the execution of this job. We say that
- the job interference is bounded by an interference_bound_function (IBF) iff for any job j of
- task tsk the cumulative interference incurred by j in the subinterval [t1, t1 + delta) of busy
- interval [t1, t2) does not exceed interference_bound_function(tsk, A, delta), where A is a
- relative arrival time of job j (with respect to time t1). *)
+ the job interference is bounded by an interference_bound_function ([IBF]) iff for any job [j] of
+ task [tsk] the cumulative interference incurred by [j] in the sub-interval [t1, t1 + delta) of busy
+ interval [t1, t2) does not exceed [interference_bound_function(tsk, A, delta)], where [A] is a
+ relative arrival time of job [j] (with respect to time [t1]). *)
Definition job_interference_is_bounded_by (interference_bound_function: Task -> duration -> duration -> duration) :=
(** Let's examine this definition in more detail. *)
forall t1 t2 delta j,
- (** First, we require j to be a job of task tsk. *)
+ (** First, we require [j] to be a job of task [tsk]. *)
arrives_in arr_seq j ->
job_task j = tsk ->
(** Next, we require the IBF to bound the interference only within the interval [t1, t1 + delta). *)
@@ -208,7 +208,7 @@ Section AbstractRTADefinitions.
completed, after which the function can behave arbitrarily. *)
~~ job_completed_by j (t1 + delta) ->
(** And finally, the IBF function might depend not only on the length
- of the interval, but also on the relative arrival time of job j (offset). *)
+ of the interval, but also on the relative arrival time of job [j] (offset). *)
(** While the first three conditions are needed for discarding excessive cases, offset adds
flexibility to the IBF, which is important, for instance, when analyzing EDF scheduling. *)
let offset := job_arrival j - t1 in
diff --git a/restructuring/analysis/abstract/ideal_jlfp_rta.v b/restructuring/analysis/abstract/ideal_jlfp_rta.v
index 535e0b06cd37893e51884e301ce457cad276b6b3..8ac9d7343caa72631bfc80dde5d90eba9d727329 100644
--- a/restructuring/analysis/abstract/ideal_jlfp_rta.v
+++ b/restructuring/analysis/abstract/ideal_jlfp_rta.v
@@ -31,7 +31,7 @@ Section JLFPInstantiation.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set: arrival_sequence_uniq arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
@@ -55,7 +55,7 @@ Section JLFPInstantiation.
earlier-arrived jobs of the same task. *)
Hypothesis H_JLFP_respects_sequential_tasks : policy_respects_sequential_tasks.
- (** Let tsk be any task in ts that is to be analyzed. *)
+ (** Let [tsk] be any task in ts that is to be analyzed. *)
Variable tsk : Task.
(** For simplicity, let's define some local names. *)
@@ -72,13 +72,13 @@ Section JLFPInstantiation.
of a job, we need to distinguish interference received from other
jobs of the same task and jobs of other tasks. In that regard, we
introduce two additional relations. The first relation defines
- whether job j1 has a higher-than-or-equal-priority than job j2
- and j1 is not equal to j2... *)
+ whether job [j1] has a higher-than-or-equal-priority than job [j2]
+ and [j1] is not equal to [j2]... *)
Let another_hep_job: JLFP_policy Job :=
fun j1 j2 => higher_eq_priority j1 j2 && (j1 != j2).
- (** ...and the second relation defines whether a job j1 has a higher-or-equal-priority than
- job j2 and the task of j1 is not equal to task of j2. *)
+ (** ...and the second relation defines whether a job [j1] has a higher-or-equal-priority than
+ job [j2] and the task of [j1] is not equal to task of [j2]. *)
Let hep_job_from_another_task: JLFP_policy Job :=
fun j1 j2 => higher_eq_priority j1 j2 && (job_task j1 != job_task j2).
@@ -99,7 +99,7 @@ Section JLFPInstantiation.
is_priority_inversion sched higher_eq_priority j t.
(** Next, we say that job j is incurring interference from another job with higher or equal
- priority at time t, if there exists job jhp (different from j) with a higher or equal priority
+ priority at time t, if there exists job [jhp] (different from j) with a higher or equal priority
that executes at time t. *)
Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=
if sched t is Some jhp then
@@ -107,7 +107,7 @@ Section JLFPInstantiation.
else false.
(** Similarly, we say that job j is incurring interference from a job with higher or
- equal priority of another task at time t, if there exists a job jhp (of a different task)
+ equal priority of another task at time t, if there exists a job [jhp] (of a different task)
with higher or equal priority that executes at time t. *)
Definition is_interference_from_hep_job_from_another_task (j : Job) (t : instant) :=
if sched t is Some jhp then
@@ -182,7 +182,7 @@ Section JLFPInstantiation.
interfering workload) and definitions corresponding to the conventional concepts.
As it was mentioned previously, instantiated functions of interference and
- interfering workload usually do not have any useful lemmas about them. Hovewer,
+ interfering workload usually do not have any useful lemmas about them. However,
it is possible to prove their equivalence to the more conventional notions like
service or workload. Next we prove the equivalence between the instantiations
and conventional notions. *)
@@ -214,10 +214,10 @@ Section JLFPInstantiation.
}
Qed.
- (** Let j be any job of task tsk, and let upp_t be any time instant after job j's arrival.
- Then for any time interval lying before upp_t, the cumulative interference received by tsk
- is equal to the sum of the cumulative priority inversion of job j and the cumulative interference
- incurred by task tsk due to other tasks. *)
+ (** Let [j] be any job of task [tsk], and let [upp_t] be any time instant after job [j]'s arrival.
+ Then for any time interval lying before [upp_t], the cumulative interference received by [tsk]
+ is equal to the sum of the cumulative priority inversion of job [j] and the cumulative interference
+ incurred by task [tsk] due to other tasks. *)
Lemma cumulative_task_interference_split:
forall j t1 t2 upp_t,
job_task j = tsk ->
@@ -275,7 +275,7 @@ Section JLFPInstantiation.
(** Let [t1,t2) be any time interval. *)
Variables t1 t2 : instant.
- (** Consider any job j of tsk. *)
+ (** Consider any job j of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
@@ -424,7 +424,7 @@ Section JLFPInstantiation.
the conventional, concrete definition of busy interval for JLFP scheduling. *)
Section BusyIntervalEquivalence.
- (** Consider any job j of tsk. *)
+ (** Consider any job j of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
diff --git a/restructuring/analysis/abstract/run_to_completion.v b/restructuring/analysis/abstract/run_to_completion.v
index 63f0ef08d9f68ec655b8a0ed44c7f4d0bc7555e4..822f65ccab2ba08ef2c0eaa5d90f9f8c61675863 100644
--- a/restructuring/analysis/abstract/run_to_completion.v
+++ b/restructuring/analysis/abstract/run_to_completion.v
@@ -5,13 +5,13 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Run-to-Completion Threshold of a job *)
(** In this module, we provide a sufficient condition under which a job
- receives enough service to become nonpreemptive. *)
+ receives enough service to become non-preemptive. *)
(** Previously we defined the notion of run-to-completion threshold (see file
abstract.run_to_completion_threshold.v). Run-to-completion threshold is the
amount of service after which a job cannot be preempted until its completion.
In this section we prove that if cumulative interference inside a busy interval
is bounded by a certain constant then a job executes long enough to reach its
- run-to-completion threshold and become nonpreemptive. *)
+ run-to-completion threshold and become non-preemptive. *)
Section AbstractRTARunToCompletionThreshold.
(** Consider any type of tasks ... *)
@@ -25,20 +25,20 @@ Section AbstractRTARunToCompletionThreshold.
Context `{JobCost Job}.
(** In addition, we assume existence of a function
- maping jobs to their preemption points. *)
+ mapping jobs to their preemption points. *)
Context `{JobPreemptable Job}.
(** Consider any arrival sequence with consistent arrivals... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
(** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_jobs_respect_taskset_costs : cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
- (** Let tsk be any task that is to be analyzed. *)
+ (** Let [tsk] be any task that is to be analyzed. *)
Variable tsk : Task.
(** Assume we are provided with abstract functions for interference and interfering workload. *)
@@ -54,17 +54,17 @@ Section AbstractRTARunToCompletionThreshold.
(** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving: work_conserving interference interfering_workload.
- (** Let j be any job of task tsk with positive cost. *)
+ (** Let [j] be any job of task [tsk] with positive cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
Hypothesis H_job_cost_positive : job_cost_positive j.
- (** Next, consider any busy interval [t1, t2) of job j. *)
+ (** Next, consider any busy interval [t1, t2) of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j t1 t2.
- (** First, we prove that job j completes by the end of the busy interval.
+ (** 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. *)
@@ -79,10 +79,10 @@ Section AbstractRTARunToCompletionThreshold.
Qed.
(** In this section we show that the cumulative interference is a complement to
- the total time where job j is scheduled inside the busy interval. *)
+ the total time where job [j] is scheduled inside the busy interval. *)
Section InterferenceIsComplement.
- (** Consider any subinterval [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.
@@ -108,7 +108,7 @@ Section AbstractRTARunToCompletionThreshold.
End InterferenceIsComplement.
- (** In this section, we prove a sufficient condition under which job j receives enough service. *)
+ (** In this section, we prove a sufficient condition under which job [j] receives enough service. *)
Section InterferenceBoundedImpliesEnoughService.
(** Let progress_of_job be the desired service of job j. *)
@@ -162,7 +162,7 @@ Section AbstractRTARunToCompletionThreshold.
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
- (** Then, job j must complete in [job_cost j - job_run_to_completion_threshold j] time
+ (** Then, job [j] must complete in [job_cost j - job_run_to_completion_threshold j] time
units after it reaches run-to-completion threshold. *)
Lemma job_completes_after_reaching_run_to_completion_threshold:
forall t,
diff --git a/restructuring/analysis/abstract/search_space.v b/restructuring/analysis/abstract/search_space.v
index ec0e022492c71dfdc2635b3f3246b40ba2ce346c..f40ecc21a4f455a2eddf07768494574255d7d49f 100644
--- a/restructuring/analysis/abstract/search_space.v
+++ b/restructuring/analysis/abstract/search_space.v
@@ -3,16 +3,16 @@ Require Import rt.util.tactics.
Require Import rt.restructuring.model.task.concept.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** * Reduction of the serach space for Abstract RTA *)
+(** * Reduction of the search space for Abstract RTA *)
(** In this file, we prove that in order to calculate the worst-case response time
- it is sufficient to consider only values of A that lie in the search space defined below. *)
+ it is sufficient to consider only values of [A] that lie in the search space defined below. *)
Section AbstractRTAReduction.
(** The response-time analysis we are presenting in this series of documents is based on searching
- over all possible values of A, the relative arrival time of the job respective to the beginning
+ over all possible values of [A], the relative arrival time of the job respective to the beginning
of the busy interval. However, to obtain a practically useful response-time bound, we need to
- constrain the search space of values of A. In this section, we define an approach to
+ constrain the search space of values of [A]. In this section, we define an approach to
reduce the search space. *)
Context {Task : TaskType}.
@@ -20,65 +20,65 @@ Section AbstractRTAReduction.
(** First, we provide a constructive notion of equivalent functions. *)
Section EquivalentFunctions.
- (** Consider an arbitrary type T... *)
+ (** Consider an arbitrary type [T]... *)
Context {T : eqType}.
- (** ...and two function from nat to T. *)
+ (** ...and two function from [nat] to [T]. *)
Variables f1 f2 : nat -> T.
- (** Let B be an arbitrary constant. *)
+ (** Let [B] be an arbitrary constant. *)
Variable B : nat.
- (** Then we say that f1 and f2 are equivalent at values less than B iff
- for any natural number x less than B [f1 x] is equal to [f2 x]. *)
+ (** Then we say that [f1] and [f2] are equivalent at values less than [B] iff
+ for any natural number [x] less than [B] [f1 x] is equal to [f2 x]. *)
Definition are_equivalent_at_values_less_than :=
forall x, x < B -> f1 x = f2 x.
- (** And vice versa, we say that f1 and f2 are not equivalent at values
- less than B iff there exists a natural number x less than B such
+ (** And vice versa, we say that [f1] and [f2] are not equivalent at values
+ less than [B] iff there exists a natural number [x] less than [B] such
that [f1 x] is not equal to [f2 x]. *)
Definition are_not_equivalent_at_values_less_than :=
exists x, x < B /\ f1 x <> f2 x.
End EquivalentFunctions.
- (** Let tsk be any task that is to be analyzed *)
+ (** Let [tsk] be any task that is to be analyzed *)
Variable tsk : Task.
- (** To ensure that the analysis procedure terminates, we assume an upper bound B on
- the values of A that must be checked. The existence of B follows from the assumption
+ (** To ensure that the analysis procedure terminates, we assume an upper bound [B] on
+ the values of [A] that must be checked. The existence of [B] follows from the assumption
that the system is not overloaded (i.e., it has bounded utilization). *)
Variable B : duration.
(** Instead of searching for the maximum interference of each individual job, we
assume a per-task interference bound function [IBF(tsk, A, x)] that is parameterized
- by the relative arrival time A of a potential job (see abstract_RTA.definitions.v file). *)
+ by the relative arrival time [A] of a potential job (see abstract_RTA.definitions.v file). *)
Variable interference_bound_function : Task -> duration -> duration -> duration.
- (** Recall the definition of ε, which defines the neighborhood of a point in the timeline.
- Note that epsilon = 1 under discrete time. *)
- (** To ensure that the search converges more quickly, we only check values of A in the interval
- [0, B) for which the interference bound function changes, i.e., every point x in which
- interference_bound_function (A - ε, x) is not equal to interference_bound_function (A, x). *)
+ (** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
+ Note that [ε = 1] under discrete time. *)
+ (** To ensure that the search converges more quickly, we only check values of [A] in the interval
+ [[0, B)] for which the interference bound function changes, i.e., every point [x] in which
+ [interference_bound_function (A - ε, x)] is not equal to [interference_bound_function (A, x)]. *)
Definition is_in_search_space A :=
A = 0 \/
0 < A < B /\ are_not_equivalent_at_values_less_than
(interference_bound_function tsk (A - ε)) (interference_bound_function tsk A) B.
- (** In this section we prove that for every A there exists a smaller A_sp
- in the search space such that interference_bound_function(A_sp,x) is
- equal to interference_bound_function(A, x). *)
+ (** In this section we prove that for every [A] there exists a smaller [A_sp]
+ in the search space such that [interference_bound_function(A_sp,x)] is
+ equal to [interference_bound_function(A, x)]. *)
Section ExistenceOfRepresentative.
- (** Let A be any constant less than B. *)
+ (** Let [A] be any constant less than [B]. *)
Variable A : duration.
Hypothesis H_A_less_than_B : A < B.
- (** We prove that there exists a constant A_sp such that:
- (a) A_sp is no greater than A, (b) interference_bound_function(A_sp, x) is
- equal to interference_bound_function(A, x) and (c) A_sp is in the search space.
- In other words, either A is already inside the search space, or we can go
- to the "left" until we reach A_sp, which will be inside the search space. *)
+ (** We prove that there exists a constant [A_sp] such that:
+ (a) [A_sp] is no greater than [A], (b) [interference_bound_function(A_sp, x)] is
+ equal to [interference_bound_function(A, x)] and (c) [A_sp] is in the search space.
+ In other words, either [A] is already inside the search space, or we can go
+ to the "left" until we reach [A_sp], which will be inside the search space. *)
Lemma representative_exists:
exists A_sp,
A_sp <= A /\
@@ -125,18 +125,18 @@ Section AbstractRTAReduction.
End ExistenceOfRepresentative.
(** In this section we prove that any solution of the response-time recurrence for
- a given point A_sp in the search space also gives a solution for any point
+ a given point [A_sp] in the search space also gives a solution for any point
A that shares the same interference bound. *)
Section FixpointSolutionForAnotherA.
- (** Suppose A_sp + F_sp is a "small" solution (i.e. less than B) of the response-time recurrence. *)
+ (** Suppose [A_sp + F_sp] is a "small" solution (i.e. less than [B]) of the response-time recurrence. *)
Variables A_sp F_sp : duration.
Hypothesis H_less_than : A_sp + F_sp < B.
Hypothesis H_fixpoint : A_sp + F_sp = interference_bound_function tsk A_sp (A_sp + F_sp).
- (** Next, let A be any point such that: (a) A_sp <= A <= A_sp + F_sp and
- (b) interference_bound_function(A, x) is equal to
- interference_bound_function(A_sp, x) for all x less than B. *)
+ (** Next, let [A] be any point such that: (a) [A_sp <= A <= A_sp + F_sp] and
+ (b) [interference_bound_function(A, x)] is equal to
+ [interference_bound_function(A_sp, x)] for all [x] less than [B]. *)
Variable A : duration.
Hypothesis H_bounds_for_A : A_sp <= A <= A_sp + F_sp.
Hypothesis H_equivalent :
@@ -144,8 +144,8 @@ Section AbstractRTAReduction.
(interference_bound_function tsk A)
(interference_bound_function tsk A_sp) B.
- (** We prove that there exists a consant F such that [A + F] is equal to [A_sp + F_sp]
- and [A + F] is a solution for the response-time recurrence for A. *)
+ (** We prove that there exists a constant [F] such that [A + F] is equal to [A_sp + F_sp]
+ and [A + F] is a solution for the response-time recurrence for [A]. *)
Lemma solution_for_A_exists:
exists F,
A_sp + F_sp = A + F /\
@@ -162,5 +162,4 @@ Section AbstractRTAReduction.
End FixpointSolutionForAnotherA.
-End AbstractRTAReduction.
-
+End AbstractRTAReduction.
\ No newline at end of file
diff --git a/restructuring/analysis/concepts/priority_inversion.v b/restructuring/analysis/concepts/priority_inversion.v
index bc5271e686528297e428ad187a5746a9272377b2..04770f758c33ca8c2dfe00628160104fd412d884 100644
--- a/restructuring/analysis/concepts/priority_inversion.v
+++ b/restructuring/analysis/concepts/priority_inversion.v
@@ -3,7 +3,7 @@ Require Export rt.restructuring.analysis.concepts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * Cumulative Priority Inversion for JLFP-models *)
-(** In this module we define the notion of cumulative priority inversion for uniprocessor for JLFP schedulers. *)
+(** In this module we define the notion of cumulative priority inversion for uni-processor for JLFP schedulers. *)
Section CumulativePriorityInversion.
(** Consider any type of tasks ... *)
@@ -32,7 +32,7 @@ Section CumulativePriorityInversion.
(** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
- (** Consider any job j of tsk. *)
+ (** Consider any job j of [tsk]. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_task : job_of_task tsk j.
@@ -52,8 +52,8 @@ Section CumulativePriorityInversion.
Definition cumulative_priority_inversion (t1 t2 : instant) :=
\sum_(t1 <= t < t2) is_priority_inversion t.
- (** We say that priority inversion of job j is bounded by a constant B iff cumulative
- priority inversion within any busy inverval prefix is bounded by B. *)
+ (** We say that priority inversion of job [j] is bounded by a constant [B] iff cumulative
+ priority inversion within any busy interval prefix is bounded by [B]. *)
Definition priority_inversion_of_job_is_bounded_by (B : duration) :=
forall (t1 t2 : instant),
busy_interval_prefix arr_seq sched higher_eq_priority j t1 t2 ->
@@ -64,10 +64,10 @@ Section CumulativePriorityInversion.
(** In this section, we define a notion of the bounded priority inversion for task. *)
Section TaskPriorityInversionBound.
- (** Consider an arbitrary task tsk. *)
+ (** Consider an arbitrary task [tsk]. *)
Variable tsk : Task.
- (** We say that task tsk has bounded priority inversion if all
+ (** We say that task [tsk] has bounded priority inversion if all
its jobs have bounded cumulative priority inversion. *)
Definition priority_inversion_is_bounded_by (B : duration) :=
forall (j : Job),
diff --git a/restructuring/analysis/concepts/request_bound_function.v b/restructuring/analysis/concepts/request_bound_function.v
index f4401de560019e50f3624c3a81f4d3e14ebefbcf..d70b44f75a4802b10c17277940ca8c339e6121e6 100644
--- a/restructuring/analysis/concepts/request_bound_function.v
+++ b/restructuring/analysis/concepts/request_bound_function.v
@@ -1,7 +1,7 @@
Require Export rt.restructuring.model.arrival.arrival_curves.
Require Export rt.restructuring.model.priority.classes.
-(** The following definitions assume ideal uniprocessor schedules. This
+(** The following definitions assume ideal uni-processor schedules. This
restriction exists for historic reasons; the defined concepts could be
generalized in future work. *)
Require Import rt.restructuring.analysis.facts.behavior.ideal_schedule.
@@ -25,24 +25,24 @@ Section TaskWorkloadBoundedByArrivalCurves.
Context `{JobTask Job Task}.
Context `{JobCost Job}.
- (** Consider any ideal uniprocessor schedule of these jobs... *)
+ (** Consider any ideal uni-processor schedule of these jobs... *)
Variable sched : schedule (ideal.processor_state Job).
(** ... and an FP policy that indicates a higher-or-equal priority
relation. *)
Variable higher_eq_priority : FP_policy Task.
- (** Let MaxArrivals denote any function that takes a task and an interval length
+ (** Let [MaxArrivals] denote any function that takes a task and an interval length
and returns the associated number of job arrivals of the task. *)
Context `{MaxArrivals Task}.
(** ** RBF of a Single Task *)
(** In this section, we define a bound for the workload of a single task
- under uniprocessor FP scheduling. *)
+ under uni-processor FP scheduling. *)
Section SingleTask.
- (** Consider any task tsk that is to be scheduled in an interval of length delta. *)
+ (** Consider any task [tsk] that is to be scheduled in an interval of length delta. *)
Variable tsk : Task.
Variable delta : duration.
@@ -59,7 +59,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
(** Consider a task set ts... *)
Variable ts : list Task.
- (** ...and let tsk be any task in task set. *)
+ (** ...and let [tsk] be any task in task set. *)
Variable tsk : Task.
(** Let delta be the length of the interval of interest. *)
@@ -77,14 +77,14 @@ Section TaskWorkloadBoundedByArrivalCurves.
\sum_(tsk <- ts) task_request_bound_function tsk delta.
(** Similarly, we define the following bound for the total workload of
- tasks of higher-or-equal priority (with respect to tsk) in any interval
+ tasks of higher-or-equal priority (with respect to [tsk]) in any interval
of length delta. *)
Definition total_hep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_hep_task tsk_other)
task_request_bound_function tsk_other delta.
(** We also define a bound for the total workload of higher-or-equal
- priority tasks other than tsk in any interval of length delta. *)
+ priority tasks other than [tsk] in any interval of length delta. *)
Definition total_ohep_request_bound_function_FP :=
\sum_(tsk_other <- ts | is_other_hep_task tsk_other)
task_request_bound_function tsk_other delta.
diff --git a/restructuring/analysis/concepts/schedulability.v b/restructuring/analysis/concepts/schedulability.v
index eaa3f136be86bc98009404b739cab8a893d6f75c..8ecedc8d006518ae90fd9304c8b2a963c8df0a24 100644
--- a/restructuring/analysis/concepts/schedulability.v
+++ b/restructuring/analysis/concepts/schedulability.v
@@ -17,14 +17,14 @@ Section Task.
(** ...and any schedule of these jobs. *)
Variable sched: schedule PState.
- (** Let tsk be any task that is to be analyzed. *)
+ (** Let [tsk] be any task that is to be analyzed. *)
Variable tsk: Task.
- (** Then, we say that R is a response-time bound of tsk in this schedule ... *)
+ (** Then, we say that R is a response-time bound of [tsk] in this schedule ... *)
Variable R: duration.
- (** ... iff any job j of tsk in this arrival sequence has
- completed by (job_arrival j + R). *)
+ (** ... iff any job [j] of [tsk] in this arrival sequence has
+ completed by [job_arrival j + R]. *)
Definition task_response_time_bound :=
forall j,
arrives_in arr_seq j ->
@@ -83,16 +83,16 @@ Section Schedulability.
(** Assume that jobs don't execute after completion. *)
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (** Let tsk be any task that is to be analyzed. *)
+ (** Let [tsk] be any task that is to be analyzed. *)
Variable tsk: Task.
- (** Given a response-time bound of tsk in this schedule no larger than its deadline, ... *)
+ (** Given a response-time bound of [tsk] in this schedule no larger than its deadline, ... *)
Variable R: duration.
Hypothesis H_R_le_deadline: R <= task_deadline tsk.
Hypothesis H_response_time_bounded: task_response_time_bound arr_seq sched tsk R.
- (** ...then tsk is schedulable. *)
+ (** ...then [tsk] is schedulable. *)
Lemma schedulability_from_response_time_bound:
schedulable_task arr_seq sched tsk.
Proof.
diff --git a/restructuring/analysis/definitions/carry_in.v b/restructuring/analysis/definitions/carry_in.v
index 252ab2794425bc10f5fa19d84bc8ef931ec1b81d..ac0eee1afe00ebdbd149de9403d732fdde794284 100644
--- a/restructuring/analysis/definitions/carry_in.v
+++ b/restructuring/analysis/definitions/carry_in.v
@@ -5,7 +5,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Import rt.restructuring.model.processor.ideal.
(** * No Carry-In *)
-(** In this module we define the notion of no carry-in time for uniprocessor schedulers. *)
+(** In this module we define the notion of no carry-in time for uni-processor schedulers. *)
Section NoCarryIn.
(** Consider any type of tasks ... *)
@@ -22,7 +22,7 @@ Section NoCarryIn.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence. *)
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
(** The processor has no carry-in at time t iff every job (regardless of priority)
diff --git a/restructuring/analysis/definitions/task_schedule.v b/restructuring/analysis/definitions/task_schedule.v
index abd2757e60b7bdc36bca2613f23b3f62817c37f6..a5ee28f9793dd8eafa7cf40a1bce419293a17802 100644
--- a/restructuring/analysis/definitions/task_schedule.v
+++ b/restructuring/analysis/definitions/task_schedule.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.facts.behavior.ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Due to historical reasons this file defines the notion of a schedule of
- a task for the ideal uniprocessor model. This is not a fundamental limitation
+ a task for the ideal uni-processor model. This is not a fundamental limitation
and the notion can be further generalized to an arbitrary model. *)
(** * Schedule of task *)
@@ -21,15 +21,15 @@ Section ScheduleOfTask.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (** Let sched be any ideal uniprocessor schedule. *)
+ (** Let [sched] be any ideal uni-processor schedule. *)
Variable sched : schedule (ideal.processor_state Job).
Section TaskProperties.
- (** Let tsk be any task. *)
+ (** Let [tsk] be any task. *)
Variable tsk : Task.
- (** Next we define whether a task is scheduled at time t, ... *)
+ (** Next we define whether a task is scheduled at time [t], ... *)
Definition task_scheduled_at (t : instant) :=
if sched t is Some j then
job_task j == tsk
@@ -39,11 +39,11 @@ Section ScheduleOfTask.
Definition task_service_at (t : instant) := task_scheduled_at t.
(** Based on the notion of instantaneous service, we define the
- cumulative service received by tsk during any interval [t1, t2)... *)
+ cumulative service received by [tsk] during any interval [t1, t2)... *)
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
- (** ...and the cumulative service received by tsk up to time t2,
+ (** ...and the cumulative service received by [tsk] up to time t2,
i.e., in the interval [0, t2). *)
Definition task_service (t2 : instant) := task_service_during 0 t2.
diff --git a/restructuring/analysis/facts/behavior/ideal_schedule.v b/restructuring/analysis/facts/behavior/ideal_schedule.v
index 2435af2fcbd058eeb9db7bf1f13052130b381a3b..ee7d8f7051eaa911508a19f1a63009e93e8e41b4 100644
--- a/restructuring/analysis/facts/behavior/ideal_schedule.v
+++ b/restructuring/analysis/facts/behavior/ideal_schedule.v
@@ -3,13 +3,13 @@ Require Export rt.util.all.
Require Export rt.restructuring.model.processor.platform_properties.
Require Export rt.restructuring.analysis.facts.behavior.service.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
(** Note: we do not re-export the basic definitions to avoid littering the global
namespace with type class instances. *)
-(** In this section we estlish the classes to which an ideal schedule belongs. *)
+(** In this section we establish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.
Local Transparent service_in scheduled_in scheduled_on.
@@ -18,7 +18,7 @@ Section ScheduleClass.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (** We note that the ideal processor model is indeed a uniprocessor
+ (** We note that the ideal processor model is indeed a uni-processor
model. *)
Lemma ideal_proc_model_is_a_uniprocessor_model:
uniprocessor_model (processor_state Job).
@@ -96,8 +96,8 @@ Hint Resolve ideal_proc_model_is_a_uniprocessor_model
(** We also provide tactics for case analysis on ideal processor state. *)
-(** The first tactic generates two subgoals: one with idle processor and
- the other with processor executing a job named JobName. *)
+(** The first tactic generates two sub-goals: one with idle processor and
+ the other with processor executing a job named [JobName]. *)
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
let Idle := fresh "Idle" in
let Sched := fresh "Sched_" JobName in
@@ -115,7 +115,7 @@ Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
| move: (Sched); simpl; move => /eqP SchedEq; rewrite ?SchedEq].
(** * Incremental Service in Ideal Schedule *)
-(** In the following section we prove a few facts about service in ideal schedeule. *)
+(** In the following section we prove a few facts about service in ideal schedule. *)
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
Section IncrementalService.
@@ -127,7 +127,7 @@ Section IncrementalService.
(** ... any arrival sequence, ... *)
Variable arr_seq : arrival_sequence Job.
- (** ... and any ideal uniprocessor schedule of this arrival sequence. *)
+ (** ... and any ideal uni-processor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
(** As a base case, we prove that if a job j receives service in
diff --git a/restructuring/analysis/facts/behavior/service.v b/restructuring/analysis/facts/behavior/service.v
index 77d36351f9c5b45e37b3b6245daf5bc5152404c3..1d84947bcface00604bfdcb36a1c212b4ee45b59 100644
--- a/restructuring/analysis/facts/behavior/service.v
+++ b/restructuring/analysis/facts/behavior/service.v
@@ -42,8 +42,8 @@ Section Composition.
rewrite /service service_during_geq //.
Qed.
- (** Trivially, an interval consiting of one time unit is equivalent to
- service_at. *)
+ (** Trivially, an interval consisting of one time unit is equivalent to
+ [service_at]. *)
Lemma service_during_instant:
forall t,
service_during sched j t t.+1 = service_at sched j t.
@@ -375,7 +375,7 @@ Section RelationToScheduled.
by apply (IS_ZERO t); apply /andP; split => //.
Qed.
- (** If a job is scheduled at some point in an interval, it receivees
+ (** If a job is scheduled at some point in an interval, it receives
positive cumulative service during the interval... *)
Lemma scheduled_implies_cumulative_service:
forall t1 t2,
@@ -407,7 +407,7 @@ Section RelationToScheduled.
End GuaranteedService.
Section AfterArrival.
- (** Futhermore, if we know that jobs are not released early, then we can
+ (** Furthermore, if we know that jobs are not released early, then we can
narrow the interval during which they must have been scheduled. *)
Context `{JobArrival Job}.
diff --git a/restructuring/analysis/facts/behavior/service_of_jobs.v b/restructuring/analysis/facts/behavior/service_of_jobs.v
index 706ff2a146063b4f8d6c6c673c752b834ec179ef..5e3bfb7ab96ef4114744855d3b2b558eb27ab0d6 100644
--- a/restructuring/analysis/facts/behavior/service_of_jobs.v
+++ b/restructuring/analysis/facts/behavior/service_of_jobs.v
@@ -50,7 +50,7 @@ Section GenericModelLemmas.
(** Let jobs denote any (finite) set of jobs. *)
Variable jobs : seq Job.
- (** Assume that the processor model is a unit service moodel. I.e.,
+ (** Assume that the processor model is a unit service model. I.e.,
no job ever receives more than one unit of service at any time. *)
Hypothesis H_unit_service : unit_service_proc_model PState.
@@ -122,7 +122,7 @@ Section GenericModelLemmas.
End GenericModelLemmas.
(** In this section, we prove some properties about service
- of sets of jobs for ideal uniprocessor model. *)
+ of sets of jobs for ideal uni-processor model. *)
Section IdealModelLemmas.
(** Consider any type of tasks ... *)
@@ -138,7 +138,7 @@ Section IdealModelLemmas.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
@@ -192,13 +192,13 @@ Section IdealModelLemmas.
is upper-bounded by the corresponding interval length. *)
Section ServiceOfJobsIsBoundedByLength.
- (** Let jobs denote any (finite) set of jobs. *)
+ (** Let [jobs] denote any (finite) set of jobs. *)
Variable jobs : seq Job.
- (** Assume that the sequence of jobs is a set. *)
+ (** Assume that the sequence of [jobs] is a set. *)
Hypothesis H_no_duplicate_jobs : uniq jobs.
- (** We prove that the overall service of jobs at a single time instant is at most 1. *)
+ (** We prove that the overall service of [jobs] at a single time instant is at most [1]. *)
Lemma service_of_jobs_le_1:
forall t, \sum_(j <- jobs | P j) service_at sched j t <= 1.
Proof.
@@ -282,13 +282,13 @@ Section IdealModelLemmas.
Variable t_compl : instant.
(** And state the proposition that all jobs are completed by time
- t_compl. Next we show that this proposition is equivalent to
+ [t_compl]. Next we show that this proposition is equivalent to
the fact that [workload of jobs = service of jobs]. *)
Let all_jobs_completed_by t_compl :=
forall j, j \in jobs -> P j -> completed_by j t_compl.
(** First, we prove that if the workload of [jobs] is equal to the service
- of [jobs], then any job in [jobs] is completed by time t_compl. *)
+ of [jobs], then any job in [jobs] is completed by time [t_compl]. *)
Lemma workload_eq_service_impl_all_jobs_have_completed:
workload_of_jobs P jobs =
service_of_jobs sched P jobs t1 t_compl ->
@@ -318,7 +318,7 @@ Section IdealModelLemmas.
}
Qed.
- (** And vice versa, the fact that any job in [jobs] is completed by time t_compl
+ (** And vice versa, the fact that any job in [jobs] is completed by time [t_compl]
implies that the workload of [jobs] is equal to the service of [jobs]. *)
Lemma all_jobs_have_completed_impl_workload_eq_service:
all_jobs_completed_by t_compl ->
diff --git a/restructuring/analysis/facts/behavior/task_arrivals.v b/restructuring/analysis/facts/behavior/task_arrivals.v
index 67cb0aea835b350e8f1ae42d3122883eec7eb9fb..74b882bd5e8d6571950c31d65919220731812fb2 100644
--- a/restructuring/analysis/facts/behavior/task_arrivals.v
+++ b/restructuring/analysis/facts/behavior/task_arrivals.v
@@ -11,7 +11,7 @@ Section TaskArrivals.
(** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (** Let tsk be any task. *)
+ (** Let [tsk] be any task. *)
Variable tsk : Task.
(** We show that the number of arrivals of task can be split into disjoint intervals. *)
diff --git a/restructuring/analysis/facts/busy_interval.v b/restructuring/analysis/facts/busy_interval.v
index 739f2f4922d42021f7b9113c898436f120857b05..dc9cdabce22aa23653285c3be6307a9c632a6e5a 100644
--- a/restructuring/analysis/facts/busy_interval.v
+++ b/restructuring/analysis/facts/busy_interval.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.analysis.concepts.priority_inversion.
Require Export rt.restructuring.analysis.facts.behavior.all.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
@@ -12,7 +12,7 @@ Require Import rt.restructuring.model.readiness.basic.
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
- busy intervals for uniprocessor for JLFP schedulers. *)
+ busy intervals for uni-processor for JLFP schedulers. *)
Section ExistsBusyIntervalJLFP.
(** Consider any type of tasks ... *)
@@ -29,7 +29,7 @@ Section ExistsBusyIntervalJLFP.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
@@ -95,7 +95,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_not_quiet : ~ quiet_time t2.
(** Then, we prove that there is a job pending at time t2
- that has higher or equal priority (with respect of tsk). *)
+ that has higher or equal priority (with respect of [tsk]). *)
Lemma not_quiet_implies_exists_pending_job:
exists j_hp,
arrives_in arr_seq j_hp /\
@@ -141,7 +141,7 @@ Section ExistsBusyIntervalJLFP.
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix t1 t2.
- (** We prove that if the processot is idle at a time instant t, then
+ (** We prove that if the processor is idle at a time instant t, then
the next time instant [t+1] will be a quiet time. *)
Lemma idle_time_implies_quiet_time_at_the_next_time_instant:
forall (t : instant),
@@ -337,7 +337,7 @@ Section ExistsBusyIntervalJLFP.
End QuietTimeAndServiceOfJobs.
(** In this section, we show that the length of any busy interval
- is bounded, as long as there is enough supply to accomodate
+ is bounded, as long as there is enough supply to accommodate
the workload of tasks with higher or equal priority. *)
Section BoundingBusyInterval.
diff --git a/restructuring/analysis/facts/preemption/job/limited.v b/restructuring/analysis/facts/preemption/job/limited.v
index 909f35c5cb7f15ba326c215b8a5ab749c9baed75..64de8667f7cb8b70b3deeae28f4e88e090af9ef7 100644
--- a/restructuring/analysis/facts/preemption/job/limited.v
+++ b/restructuring/analysis/facts/preemption/job/limited.v
@@ -27,7 +27,7 @@ Section ModelWithLimitedPreemptions.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (** Next, consider any limited ideal uniprocessor schedule of this arrival sequence ... *)
+ (** Next, consider any limited ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions:
valid_schedule_with_limited_preemptions arr_seq sched.
@@ -84,8 +84,8 @@ Section ModelWithLimitedPreemptions.
by apply list_of_preemption_point_is_not_empty.
Qed.
- (** As a corollary, we prove that the sequence of nonpreemptive
- points of a job with poisitive cost contains at least 2
+ (** As a corollary, we prove that the sequence of non-preemptive
+ points of a job with positive cost contains at least 2
points. *)
Corollary number_of_preemption_points_at_least_two:
job_cost_positive j ->
@@ -107,8 +107,8 @@ Section ModelWithLimitedPreemptions.
- by rewrite EQ; apply job_cost_in_nonpreemptive_points.
Qed.
- (** Next we prove that "antidensity" property (from
- preemption.util file) holds for [job_preemption_point j]. *)
+ (** Next we prove that "anti-density" property (from
+ [preemption.util] file) holds for [job_preemption_point j]. *)
Lemma antidensity_of_preemption_points:
forall (Ï : work),
Ï <= job_cost j ->
@@ -157,7 +157,7 @@ Section ModelWithLimitedPreemptions.
Qed.
(** Recall that file [job.parameters] also defines notion of
- preemption poins. And note that
+ preemption points. And note that
[job.parameter.job_preemption_points] cannot have a
duplicating preemption points. Therefore, we need additional
lemmas to relate [job.parameter.job_preemption_points] and
diff --git a/restructuring/analysis/facts/preemption/job/preemptive.v b/restructuring/analysis/facts/preemption/job/preemptive.v
index f5f56bdef2dc9fcc15651e854c2b28a6a04556a0..f2af28e1f4eff982ec6b35dd379be17c5d92f0ef 100644
--- a/restructuring/analysis/facts/preemption/job/preemptive.v
+++ b/restructuring/analysis/facts/preemption/job/preemptive.v
@@ -1,7 +1,7 @@
Require Export rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.fully_preemptive.
-(** * Preemptions in Fully Premptive Model *)
+(** * Preemptions in Fully Preemptive Model *)
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully preemptive model indeed defines
a valid preemption model. *)
diff --git a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index ef91d3329a2b4301664bba6b4245ba26ad2fe718..03dd0428bb31662eeeef19a764a13d849b91ce42 100644
--- a/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/restructuring/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -4,7 +4,7 @@ Require Export rt.restructuring.model.task.preemption.parameters.
(** * Run-to-Completion Threshold *)
(** In this section, we provide a few basic properties
- of run-to-completion-threshold-compilant schedules. *)
+ of run-to-completion-threshold-compliant schedules. *)
Section RunToCompletionThreshold.
(** Consider any type of jobs. *)
@@ -13,7 +13,7 @@ Section RunToCompletionThreshold.
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}.
(** Consider any kind of processor state model, ... *)
@@ -117,7 +117,7 @@ Section RunToCompletionThreshold.
+ by apply A2.
Qed.
- (** Last nonpreemptive segment of a positive-cost job has positive length. *)
+ (** Last non-preemptive segment of a positive-cost job has positive length. *)
Lemma job_last_nonpreemptive_segment_positive:
job_cost_positive j ->
0 < job_last_nonpreemptive_segment j.
diff --git a/restructuring/analysis/facts/preemption/task/floating.v b/restructuring/analysis/facts/preemption/task/floating.v
index 28c39720c8b18f77bd73eb9ca95c1c7c69c8c439..14bf9d381e49fd7ea6f80f464003db7b137ebbe1 100644
--- a/restructuring/analysis/facts/preemption/task/floating.v
+++ b/restructuring/analysis/facts/preemption/task/floating.v
@@ -5,12 +5,12 @@ Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-(** * Platform for Floating Non-Premptive Regions Model *)
+(** * Platform for Floating Non-Preemptive Regions Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the model
with floating non-preemptive regions indeed defines a valid
preemption model with bounded non-preemptive regions. *)
-Section FloatingNonPremptiveRegionsModel.
+Section FloatingNonPreemptiveRegionsModel.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
@@ -33,7 +33,7 @@ Section FloatingNonPremptiveRegionsModel.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (** Next, consider any ideal uniprocessor preemption-aware schedule
+ (** Next, consider any ideal uni-processor preemption-aware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule:
@@ -44,13 +44,13 @@ Section FloatingNonPremptiveRegionsModel.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Next, we assume that preemption points are defined by the model
- with floating nonpreemptive regions. *)
+ with floating non-preemptive regions. *)
Hypothesis H_valid_model_with_floating_nonpreemptive_regions:
valid_model_with_floating_nonpreemptive_regions arr_seq.
(** Then, we prove that the [job_preemptable and
task_max_nonpreemptive_segment] functions define
- a model with bounded nonpremtive regions. *)
+ a model with bounded non-preemptive regions. *)
Lemma floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
@@ -105,7 +105,7 @@ Section FloatingNonPremptiveRegionsModel.
- apply floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions.
Qed.
-End FloatingNonPremptiveRegionsModel.
+End FloatingNonPreemptiveRegionsModel.
Hint Resolve
valid_fixed_preemption_points_model_lemma
diff --git a/restructuring/analysis/facts/preemption/task/limited.v b/restructuring/analysis/facts/preemption/task/limited.v
index a3d9a686274ea4402a9231702b51c130dd85da58..2b11f7560dffe1a12ff4c083462cdef5408589ba 100644
--- a/restructuring/analysis/facts/preemption/task/limited.v
+++ b/restructuring/analysis/facts/preemption/task/limited.v
@@ -28,7 +28,7 @@ Section LimitedPreemptionsModel.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (** Next, consider any ideal uniprocessor preemption-aware schedule
+ (** Next, consider any ideal uni-processor preemption-aware schedule
of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_valid_schedule_with_limited_preemptions:
@@ -47,7 +47,7 @@ Section LimitedPreemptionsModel.
valid_fixed_preemption_points_model arr_seq ts.
(** Then we prove that functions [job_preemptable and
- task_preemption_points] define a model with bounded nonpremtive
+ task_preemption_points] define a model with bounded non-preemptive
regions. *)
Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq .
diff --git a/restructuring/analysis/facts/preemption/task/nonpreemptive.v b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
index fd3ba3548d369adfd1ef531269faf27602e8d384..899a8f9ab4dc669284329e13c046a88db04ae380 100644
--- a/restructuring/analysis/facts/preemption/task/nonpreemptive.v
+++ b/restructuring/analysis/facts/preemption/task/nonpreemptive.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-(** * Platform for Fully Non-Premptive Model *)
+(** * Platform for Fully Non-Preemptive Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the fully
non-preemptive model indeed defines a valid preemption model with
@@ -26,7 +26,7 @@ Section FullyNonPreemptiveModel.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (** Next, consider any ideal non-preemptive uniprocessor schedule of this arrival sequence... *)
+ (** Next, consider any ideal non-preemptive uni-processor schedule of this arrival sequence... *)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.
@@ -39,7 +39,7 @@ Section FullyNonPreemptiveModel.
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
(** Then we prove that [fully_nonpreemptive_model] function
- defines a model with bounded nonpremtive regions.*)
+ defines a model with bounded non-preemptive regions.*)
Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
diff --git a/restructuring/analysis/facts/preemption/task/preemptive.v b/restructuring/analysis/facts/preemption/task/preemptive.v
index f04b0de7e803af1d52e60fb4a1b1fd6362933aa4..f7ed78564d82c32aa01a55a5ca49ab6427cf50c0 100644
--- a/restructuring/analysis/facts/preemption/task/preemptive.v
+++ b/restructuring/analysis/facts/preemption/task/preemptive.v
@@ -3,7 +3,7 @@ Require Export rt.restructuring.analysis.facts.preemption.job.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-(** * Platform for Fully Premptive Model *)
+(** * Platform for Fully Preemptive Model *)
(** In this section, we prove that instantiation of functions
[job_preemptable and task_max_nonpreemptive_segment] to the fully
preemptive model indeed defines a valid preemption model with
@@ -31,7 +31,7 @@ Section FullyPreemptiveModel.
Variable sched : schedule PState.
(** We prove that [fully_preemptive_model] function
- defines a model with bounded nonpremtive regions.*)
+ defines a model with bounded non-preemptive regions.*)
Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
model_with_bounded_nonpreemptive_segments arr_seq.
Proof.
diff --git a/restructuring/analysis/facts/priority_inversion.v b/restructuring/analysis/facts/priority_inversion.v
index 16e07b07b757e698f18f5f17f0b1863a90935900..b24ece23584b0ce2479e8a07deb52b6df4fbdee5 100644
--- a/restructuring/analysis/facts/priority_inversion.v
+++ b/restructuring/analysis/facts/priority_inversion.v
@@ -7,7 +7,7 @@ Require Export rt.restructuring.analysis.concepts.busy_interval.
Require Export rt.restructuring.analysis.facts.busy_interval.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
(** Throughout the file we assume for the classic Liu & Layland model
@@ -144,11 +144,11 @@ Section PriorityInversionIsBounded.
Let job_completed_by := completed_by sched.
(** Finally, we introduce the notion of the maximal length of
- (potential) priority inversion at a time instant t, which is
+ (potential) priority inversion at a time instant [t], which is
defined as the maximum length of nonpreemptive segments among
all jobs that arrived so far. Note that the value
- [job_max_nonpreemptive_segment j_lp] is at least ε for any job
- j_lp, so the maximal length of priority inversion cannot be
+ [job_max_nonpreemptive_segment j_lp] is at least [ε] for any job
+ [j_lp], so the maximal length of priority inversion cannot be
negative. *)
Definition max_length_of_priority_inversion (j : Job) (t : instant) :=
\max_(j_lp <- arrivals_before arr_seq t | ~~ higher_eq_priority j_lp j)
@@ -163,7 +163,7 @@ Section PriorityInversionIsBounded.
different scheduler and/or task models. Thus, we don't define
such a bound in this module. *)
- (** Consider any job j of tsk with positive job cost. *)
+ (** Consider any job [j] of [tsk] with positive job cost. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
@@ -196,9 +196,6 @@ Section PriorityInversionIsBounded.
intros Idle.
by exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
Qed.
-
- (** Note for Björn: This should be a local lemma, but
- "gallinahtml" removes all "Local" lemmas (html and htmlpretty are fine). *)
(** Next we consider two cases: (1) when [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *)
Lemma t_lt_t2_or_t_eq_t2:
@@ -250,7 +247,7 @@ Section PriorityInversionIsBounded.
Qed.
(** In case when [t = t2 - 1], we cannot use the same proof
- sinse [t+1 = t2], but [t2] is a quiet time. So we do a
+ since [t+1 = t2], but [t2] is a quiet time. So we do a
similar case analysis on the fact that [t1 = t ∨ t1 < t]. *)
Lemma scheduled_at_preemption_time_implies_higher_or_equal_priority_eq:
t = t2.-1 ->
@@ -310,9 +307,9 @@ Section PriorityInversionIsBounded.
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority_eq.
Qed.
- (** Sinse a job that is scheduled at time [t] has higher-or-equal priority,
+ (** Since a job that is scheduled at time [t] has higher-or-equal priority,
by properties of a busy interval it cannot arrive before time instant [t1]. *)
- Lemma scheduled_at_preemption_time_implies_arriwed_between_within_busy_interval:
+ Lemma scheduled_at_preemption_time_implies_arrived_between_within_busy_interval:
forall jhp,
scheduled_at sched jhp t ->
arrived_between jhp t1 t2.
@@ -347,7 +344,7 @@ Section PriorityInversionIsBounded.
{ by exfalso; apply instant_t_is_not_idle. }
exists jhp.
repeat split.
- - by apply scheduled_at_preemption_time_implies_arriwed_between_within_busy_interval.
+ - by apply scheduled_at_preemption_time_implies_arrived_between_within_busy_interval.
- by apply scheduled_at_preemption_time_implies_higher_or_equal_priority.
- by done.
Qed.
@@ -481,7 +478,7 @@ Section PriorityInversionIsBounded.
(** * Preemption Time Exists *)
(** In this section we prove that the function [max_length_of_priority_inversion]
indeed upper bounds the priority inversion length. *)
- Section PreemprionTimeExists.
+ Section PreemptionTimeExists.
(** First we prove that if a job with higher-or-equal priority is scheduled at
a quiet time [t+1] then this is the first time when this job is scheduled. *)
@@ -563,7 +560,7 @@ Section PriorityInversionIsBounded.
(** Thus, there must be a preemption time in the interval [t1, t1
+ max_priority_inversion t1]. That is, if a job with
higher-or-equal priority is scheduled at time instant t1, then
- t1 is a preemprion time. Otherwise, if a job with lower
+ t1 is a preemption time. Otherwise, if a job with lower
priority is scheduled at time t1, then this jobs also should
be scheduled before the beginning of the busy interval. So,
the next preemption time will be no more than
@@ -645,7 +642,7 @@ Section PriorityInversionIsBounded.
job_preemptable jlp Ï ->
service sched jlp t1 + fpt <= Ï.
- (** For convinience we also assume the following inequality holds. *)
+ (** For convenience we also assume the following inequality holds. *)
Hypothesis H_progr_le_max_nonp_segment:
progr_t1 <= progr_t1 + fpt <= progr_t1 + (job_max_nonpreemptive_segment jlp - ε).
@@ -666,7 +663,7 @@ Section PriorityInversionIsBounded.
Qed.
(** Thanks to the fact that the scheduler respects the notion of preemption points
- we show that [jlp] is continuously scheduled in time interval [t1, t1 + fpt). *)
+ we show that [jlp] is continuously scheduled in time interval [[t1, t1 + fpt)]. *)
Lemma continuously_scheduled_between_preemption_points:
forall t',
t1 <= t' < t1 + fpt ->
@@ -819,6 +816,6 @@ Section PriorityInversionIsBounded.
by rewrite -eqbF_neg; apply /eqP.
Qed.
- End PreemprionTimeExists.
+ End PreemptionTimeExists.
End PriorityInversionIsBounded.
diff --git a/restructuring/analysis/facts/rbf.v b/restructuring/analysis/facts/rbf.v
index 93dad5fd070428715469310251ac83d45db6c5ca..90ee17c3d39360cedbe03082ec118ae61fb46dce 100644
--- a/restructuring/analysis/facts/rbf.v
+++ b/restructuring/analysis/facts/rbf.v
@@ -7,10 +7,8 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Facts about Request Bound Functions (RBFs) *)
-
(** In this file, we prove some lemmas about request bound functions. *)
-
(** ** RBF is a Bound on Workload *)
(** First, we show that a task's RBF is indeed an upper bound on its
@@ -32,7 +30,7 @@ Section ProofWorkloadBound.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
- (** ... and any ideal uniprocessor schedule of this arrival sequence.*)
+ (** ... and any ideal uni-processor schedule of this arrival sequence.*)
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
@@ -43,7 +41,7 @@ Section ProofWorkloadBound.
(** Consider a task set ts... *)
Variable ts : list Task.
- (** ...and let tsk be any task in ts. *)
+ (** ...and let [tsk] be any task in ts. *)
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.
@@ -54,7 +52,7 @@ Section ProofWorkloadBound.
(** Next, we assume that all jobs come from the task set. *)
Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
- (** Let max_arrivals be any arrival bound for taskset ts. *)
+ (** Let max_arrivals be any arrival bound for task-set [ts]. *)
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
@@ -64,13 +62,13 @@ Section ProofWorkloadBound.
Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
- (** Next, we consider any job j of tsk. *)
+ (** Next, we consider any job [j] of [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
- (** Next, we say that two jobs j1 and j2 are in relation
- other_higher_eq_priority, iff j1 has higher or equal priority than j2 and
+ (** Next, we say that two jobs [j1] and [j2] are in relation
+ [other_higher_eq_priority], iff [j1] has higher or equal priority than [j2] and
is produced by a different task. *)
Let other_higher_eq_priority j1 j2 := jlfp_higher_eq_priority j1 j2 && (~~ same_task j1 j2).
@@ -97,7 +95,7 @@ Section ProofWorkloadBound.
Variable t : instant.
Variable delta : instant.
- (** First, we show that workload of task tsk is bounded by the number of
+ (** First, we show that workload of task [tsk] is bounded by the number of
arrivals of the task times the cost of the task. *)
Lemma task_workload_le_num_of_arrivals_times_cost:
task_workload t (t + delta)
@@ -252,11 +250,11 @@ Section RequestBoundFunctions.
Hypothesis H_arrival_times_are_consistent:
consistent_arrival_times arr_seq.
- (** Let tsk be any task. *)
+ (** Let [tsk] be any task. *)
Variable tsk : Task.
- (** 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
+ (** 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 delta = 0. *)
Context `{MaxArrivals Task}.
Hypothesis H_valid_arrival_curve : valid_arrival_curve tsk (max_arrivals tsk).
@@ -274,7 +272,7 @@ Section RequestBoundFunctions.
by move: H_valid_arrival_curve => [T1 T2].
Qed.
- (** We prove that task_rbf is monotone. *)
+ (** We prove that [task_rbf] is monotone. *)
Lemma task_rbf_monotone:
monotone task_rbf leq.
Proof.
@@ -284,13 +282,13 @@ Section RequestBoundFunctions.
by move: H_valid_arrival_curve => [_ T]; apply T.
Qed.
- (** Consider any job j of tsk. This guarantees that there exists at least one
- job of task tsk. *)
+ (** Consider any job j of [tsk]. This guarantees that there exists at least one
+ job of task [tsk]. *)
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_task j = tsk.
- (** Then we prove that task_rbf 1 is greater than or equal to task cost. *)
+ (** Then we prove that [task_rbf 1] is greater than or equal to task cost. *)
Lemma task_rbf_1_ge_task_cost:
task_rbf 1 >= task_cost tsk.
Proof.
diff --git a/restructuring/analysis/facts/readiness/basic.v b/restructuring/analysis/facts/readiness/basic.v
index 29eb01ede9a7984ec12dd96e10d2a551e5f77036..a58055a1853de74d40930747a37f9a4480f1d717 100644
--- a/restructuring/analysis/facts/readiness/basic.v
+++ b/restructuring/analysis/facts/readiness/basic.v
@@ -11,7 +11,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 schedule satisfies that only ready
diff --git a/restructuring/analysis/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 0d6a78dd16ef662ffd6159df681229d2b44a8e99..1fd663234a6ba0ca211e11f772be2624f942fe4b 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -9,7 +9,7 @@ Section EDFTransformation.
(** Consider any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (** ... and ideal uniprocessor schedules. *)
+ (** ... and ideal uni-processor schedules. *)
Let PState := ideal.processor_state Job.
Let SchedType := schedule (PState).