diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index cab1b614c6fe128b865e8eff5e1997c1856ca69e..f2176d5ba312efa9b45132d9d0e027cdbe6d90df 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -11,92 +11,92 @@ 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. *)
-(* We prove that the maximum (with respect to the set of offsets) among the solutions
+(** 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
in this section we do not rely on any hypotheses about job sequentiality. *)
Section Abstract_RTA.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
- (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+ (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
Variable arr_seq : arrival_sequence Job.
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 uniprocessor 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.
- (* ... where jobs do not execute before their arrival nor after completion. *)
+ (** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
- (* Assume that the job costs are no larger than the task costs. *)
+ (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
- (* Consider a task set ts... *)
+ (** 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.
- (* Consider a valid preemption model... *)
+ (** Consider a valid preemption model... *)
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
- (* ...and a valid task run-to-completion threshold function. That is,
+ (** ...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. *)
Hypothesis H_valid_run_to_completion_threshold:
valid_task_run_to_completion_threshold arr_seq tsk.
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let work_conserving := work_conserving arr_seq sched tsk.
Let busy_intervals_are_bounded_by := busy_intervals_are_bounded_by arr_seq sched tsk.
Let job_interference_is_bounded_by := job_interference_is_bounded_by arr_seq sched tsk.
- (* Assume we are provided with abstract functions for interference and interfering workload. *)
+ (** Assume we are provided with abstract functions for interference and interfering workload. *)
Variable interference : Job -> instant -> bool.
Variable interfering_workload : Job -> instant -> duration.
- (* We assume that the scheduler is work-conserving. *)
+ (** We assume that the scheduler is work-conserving. *)
Hypothesis H_work_conserving : work_conserving interference interfering_workload.
- (* For simplicity, let's define some local names. *)
+ (** For simplicity, let's define some local names. *)
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
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
+ (** Next, assume that interference_bound_function is a bound on
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
interference interfering_workload interference_bound_function.
- (* For simplicity, let's define a local name for the search space. *)
+ (** 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. *)
Variable R: nat.
@@ -108,24 +108,24 @@ Section Abstract_RTA.
+ interference_bound_function tsk A (A + F) /\
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
- (* In this section we show a detailed proof of the main theorem
+ (** In this section we show a detailed proof of the main theorem
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.
Hypothesis H_job_cost_positive: job_cost_positive j.
- (* Assume we have a busy interval [t1, t2) of job j that is bounded by L. *)
+ (** Assume we have a busy interval [t1, t2) of job j that is bounded by L. *)
Variable t1 t2: instant.
Hypothesis H_busy_interval: busy_interval j t1 t2.
- (* Let's define A as a relative arrival time of job j (with respect to time t1). *)
+ (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
Let A := job_arrival j - t1.
- (* In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum.
+ (** 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
@@ -133,40 +133,40 @@ Section Abstract_RTA.
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
+ (** (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 reccurence... *)
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).
- (* (e) and finally, [F_sp + (task_last - ε)] is no greater than R. *)
+ (** (e) and finally, [F_sp + (task_last - ε)] is no greater than R. *)
Hypothesis H_R_gt_Fsp : F_sp + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
- (* In this section, we consider the case where the solution is so large
+ (** In this section, we consider the case where the solution is so large
that the value of [t1 + A_sp + F_sp] goes beyond the busy interval.
Although this case may be impossible in some scenarios, it can be
easily proven, since any job that completes by the end of the busy
interval remains completed. *)
Section FixpointOutsideBusyInterval.
- (* By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
+ (** By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
Hypothesis H_big_fixpoint_solution : t2 <= t1 + (A_sp + F_sp).
- (* Then we prove that [job_arrival j + R] is no less than t2. *)
+ (** 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.
@@ -180,7 +180,7 @@ Section Abstract_RTA.
first rewrite leq_addr.
Qed.
- (* But since we know that the job is completed by the end of its busy interval,
+ (** But since we know that the job is completed by the end of its busy interval,
we can show that job j is completed by [job arrival j + R]. *)
Lemma job_completed_by_arrival_plus_R_1:
completed_by sched j (job_arrival j + R).
@@ -193,43 +193,43 @@ Section Abstract_RTA.
End FixpointOutsideBusyInterval.
- (* In this section, we consider the complementary case where
+ (** In this section, we consider the complementary case where
[t1 + A_sp + F_sp] lies inside the busy interval. *)
Section FixpointInsideBusyInterval.
- (* So, assume that [t1 + A_sp + F_sp] is less than t2. *)
+ (** So, assume that [t1 + A_sp + F_sp] is less than t2. *)
Hypothesis H_small_fixpoint_solution : t1 + (A_sp + F_sp) < t2.
- (* Next, let's consider two other cases: *)
- (* CASE 1: the value of the fixpoint is no less than the relative arrival time of job j. *)
+ (** 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. *)
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]. *)
Section ProofByContradiction.
- (* Recall that by lemma "solution_for_A_exists" there is a solution F
+ (** 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 most F_sp... *)
Hypothesis H_F_le_Fsp : F <= F_sp.
- (* (c) and [A + F] is a solution for the response-time recurrence for A. *)
+ (** (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]
+ (** Some additional reasoning is required since the term [task_cost tsk - task_run_to_completion_threshold tsk]
does not necessarily bound the term [job_cost j - job_run_to_completion_threshold j]. That is, a job can
have a small run-to-completion threshold, thereby becoming non-preemptive much earlier than guaranteed
according to task run-to-completion threshold, while simultaneously executing the last non-preemptive
@@ -240,20 +240,20 @@ Section Abstract_RTA.
we introduce two temporal notions of the last nonpreemptive 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
+ (** 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]).
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
+ (** 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 :=
+ (** 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
is completed by time [t1 + (A + F) - optimism + last]. *)
@@ -293,13 +293,13 @@ Section Abstract_RTA.
eapply job_completes_after_reaching_run_to_completion_threshold with (arr_seq0 := arr_seq); eauto 2.
Qed.
- (* However, [t1 + (A + F) - optimism + last ≤ job_arrival j + R]!
+ (** However, [t1 + (A + F) - optimism + last ≤ job_arrival j + R]!
To prove this fact we need a few auxiliary inequalities that are
needed because we use the truncated subtraction in our development.
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. *)
@@ -345,7 +345,7 @@ Section Abstract_RTA.
}
Qed.
- (* As two trivial corollaries, we show that
+ (** As two trivial corollaries, we show that
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.
@@ -358,7 +358,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.
@@ -372,7 +372,7 @@ Section Abstract_RTA.
End AuxiliaryInequalities.
- (* Next we show that [t1 + (A + F) - optimism + last] is at most [job_arrival j + R],
+ (** 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
@@ -410,7 +410,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.
@@ -421,7 +421,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.
@@ -449,15 +449,15 @@ Section Abstract_RTA.
End FixpointIsNoLessThanArrival.
- (* CASE 2: the value of the fixpoint is less than the relative arrival time of
+ (** 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). *)
Section FixpointCannotBeSmallerThanArrival.
- (* Assume that [A_sp + F_sp] is less than A. *)
+ (** Assume that [A_sp + F_sp] is less than A. *)
Hypothesis H_fixpoint_is_less_that_relative_arrival_of_j: A_sp + F_sp < A.
- (* Note that the relative arrival time of job j is less than L. *)
+ (** Note that the relative arrival time of job j is less than L. *)
Lemma relative_arrival_is_bounded: A < L.
Proof.
rewrite /A.
@@ -469,7 +469,7 @@ Section Abstract_RTA.
by apply ltn_sub2r; first apply leq_ltn_trans with (job_arrival j).
Qed.
- (* We can use [j_receives_at_least_run_to_completion_threshold] to prove that the service
+ (** We can use [j_receives_at_least_run_to_completion_threshold] to prove that the service
received by j by time [t1 + (A_sp + F_sp)] is no less than run-to-completion threshold. *)
Lemma service_of_job_ge_run_to_completion_threshold:
service sched j (t1 + (A_sp + F_sp)) >= job_run_to_completion_threshold j.
@@ -501,7 +501,7 @@ 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
+ (** 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.
@@ -522,7 +522,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/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 08d40389f42ac1cd1feec4288d3a3dc7d4f6f87e..a1d86dbb4ca80a4ee873abc934822c89a2fc1abf 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -17,7 +17,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models
and sequential jobs. *)
- (* We prove that the maximum among the solutions of the response-time bound
+ (** 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.
Note that in this section we _do_ rely on the hypothesis about job
sequentiality. This allows us to provide a more precise response-time
@@ -25,65 +25,65 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
in the order they arrive. *)
Section Sequential_Abstract_RTA.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskRunToCompletionThreshold Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobPreemptable Job}.
- (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+ (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
Variable arr_seq : arrival_sequence Job.
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 uniprocessor 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.
- (* ... where jobs do not execute before their arrival nor after completion. *)
+ (** ... where jobs do not execute before their arrival nor after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
- (* Assume that the job costs are no larger than the task costs. *)
+ (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost:
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
- (* Consider an arbitrary task set. *)
+ (** 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.
- (* Consider a valid preemption model... *)
+ (** Consider a valid preemption model... *)
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
- (* ...and a valid task run-to-completion threshold function. That is,
+ (** ...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. *)
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
+ (** 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.
- (* Assume we are provided with abstract functions for interference and interfering workload. *)
+ (** Assume we are provided with abstract functions for interference and interfering workload. *)
Variable interference : Job -> instant -> bool.
Variable interfering_workload : Job -> instant -> duration.
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let busy_interval := busy_interval sched interference interfering_workload.
Let arrivals_between := arrivals_between arr_seq.
@@ -92,11 +92,11 @@ Section Sequential_Abstract_RTA.
Let task_service_of_jobs_in := task_service_of_jobs_in sched tsk.
Let response_time_bounded_by := task_response_time_bound arr_seq sched.
- (* In this section, we introduce a few new definitions to make it easier
+ (** In this section, we introduce a few new definitions to make it easier
to express the new bound of the worst-case execution time. *)
Section Definitions.
- (* When assuming sequential jobs, we can introduce an additional hypothesis that
+ (** When assuming sequential jobs, 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
completed by the beginning of the busy interval. *)
@@ -108,7 +108,7 @@ 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
+ (** 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
@@ -129,11 +129,11 @@ Section Sequential_Abstract_RTA.
(~~ task_scheduled_at sched tsk t)
&& has (fun j => interference j t) (task_arrivals_before arr_seq tsk upper_bound).
- (* Next we define the cumulative task interference. *)
+ (** Next we define the cumulative task interference. *)
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)
+ (** 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
@@ -152,37 +152,37 @@ Section Sequential_Abstract_RTA.
End Definitions.
- (* In this section, we prove that the maximum among the solutions of the
+ (** In this section, we prove that the maximum among the solutions of the
response-time bound recurrence is a response-time bound for tsk. *)
Section ResponseTimeBound.
- (* For simplicity, let's define some local names. *)
+ (** For simplicity, let's define some local names. *)
Let cumul_interference := cumul_interference interference.
Let cumul_workload := cumul_interfering_workload interfering_workload.
Let cumul_task_interference := cumul_task_interference tsk.
- (* We assume that the schedule is work-conserving. *)
+ (** We assume that the schedule is work-conserving. *)
Hypothesis H_work_conserving:
work_conserving arr_seq sched tsk interference interfering_workload.
- (* Unlike the previous theorem [uniprocessor_response_time_bound], we assume
+ (** Unlike the previous theorem [uniprocessor_response_time_bound], we assume
that (1) jobs are sequential, moreover (2) functions interference and
interfering_workload are consistent with the hypothesis of sequential jobs. *)
Hypothesis H_sequential_jobs : sequential_jobs sched.
Hypothesis H_interference_and_workload_consistent_with_sequential_jobs:
interference_and_workload_consistent_with_sequential_jobs.
- (* 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.
- (* Next, we assume that task_interference_bound_function is a bound on interference incurred by the task. *)
+ (** Next, we assume that task_interference_bound_function is a bound on interference incurred by the task. *)
Variable task_interference_bound_function : Task -> duration -> duration -> duration.
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
+ (** 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 jobs the bound consists of two parts: (1) the part that bounds the interference
@@ -191,13 +191,13 @@ Section Sequential_Abstract_RTA.
Let total_interference_bound (tsk : Task) (A Δ : duration) :=
task_rbf (A + ε) - task_cost tsk + task_interference_bound_function tsk A Δ.
- (* Note that since we consider the modified interference bound function, the search space has
+ (** Note that since we consider the modified interference bound function, the search space has
also changed. One can see that the new search space is guaranteed to include any A for which
[task_rbf (A) ≠task_rbf (A + ε)], since this implies the fact that
[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
+ (** 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 jobs are
sequential leads to a more precise response-time bound. Now we can explicitly express
@@ -217,11 +217,11 @@ Section Sequential_Abstract_RTA.
+ task_interference_bound_function tsk A (A + F) /\
F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
- (* In this section we prove a few simple lemmas about the completion of jobs from the task
+ (** In this section we prove a few simple lemmas about the completion of jobs from the task
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.
@@ -229,11 +229,11 @@ Section Sequential_Abstract_RTA.
Hypothesis H_j2_from_tsk: job_task j2 = tsk.
Hypothesis H_j1_cost_positive: job_cost_positive j1.
- (* Consider the busy interval [t1, t2) of job j1. *)
+ (** Consider the busy interval [t1, t2) of job j1. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j1 t1 t2.
- (* 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 ->
@@ -249,7 +249,7 @@ Section Sequential_Abstract_RTA.
by apply arrived_between_implies_in_arrivals.
Qed.
- (* Next we prove that if a job is pending after the beginning
+ (** Next we prove that if a job is pending after the beginning
of the busy interval [t1, t2) then it arrives after t1. *)
Lemma arrives_after_beginning_of_busy_interval:
forall t,
@@ -269,61 +269,61 @@ Section Sequential_Abstract_RTA.
End CompletionOfJobsFromSameTask.
- (* Since we are going to use the [uniprocessor_response_time_bound] theorem to prove
+ (** Since we are going to use the [uniprocessor_response_time_bound] theorem to prove
the theorem of this section, we have to show that all the hypotheses are satisfied.
Namely, we need to show that hypotheses [H_sequential_jobs, H_i_w_are_task_consistent
and H_task_interference_is_bounded_by] imply [H_job_interference_is_bounded], and the
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
+ (** 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. *)
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.
Hypothesis H_job_cost_positive : job_cost_positive j.
- (* Consider the busy interval [t1, t2) of job j. *)
+ (** Consider the busy interval [t1, t2) of job j. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval j t1 t2.
- (* Let's define A as a relative arrival time of job j (with respect to time t1). *)
+ (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
Let A : duration := job_arrival j - t1.
- (* Consider an arbitrary time x ... *)
+ (** Consider an arbitrary time x ... *)
Variable x : duration.
- (* ... such that (t1 + x) is inside the busy interval... *)
+ (** ... such that (t1 + x) is inside the busy interval... *)
Hypothesis H_inside_busy_interval : t1 + x < t2.
- (* ... and job j is not completed by time (t1 + x). *)
+ (** ... and job j is not completed by time (t1 + x). *)
Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + x).
- (* In this section, we show that the cumulative interference of job j in the interval [t1, t1 + x)
+ (** 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
only on the interval [t1, t1 + A + ε). Thanks to the hypothesis about sequential jobs, jobs of
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
+ (** We start by proving a simpler analog of the lemma which states that at
any time instant t ∈ [t1, t1 + x) the sum of [interference j t] and
[scheduled_at j t] is no larger than the sum of [the service received
by jobs of task tsk at time t] and [task_iterference tsk t]. *)
- (* Next we consider 4 cases. *)
+ (** Next we consider 4 cases. *)
Section CaseAnalysis.
- (* Consider an arbitrary time instant t ∈ [t1, t1 + x). *)
+ (** Consider an arbitrary time instant t ∈ [t1, t1 + x). *)
Variable t : instant.
Hypothesis H_t_in_interval : t1 <= t < t1 + x.
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
+ (** 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]. *)
@@ -351,12 +351,12 @@ 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]. *)
@@ -391,13 +391,13 @@ 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,
in this case [service_of_jobs of tsk = 1]. Which reduces to [1 ≤ 1]. *)
@@ -451,10 +451,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 <=
@@ -484,7 +484,7 @@ Section Sequential_Abstract_RTA.
End Case4.
- (* We use the above case analysis to prove that any time instant
+ (** We use the above case analysis to prove that any time instant
t ∈ [t1, t1 + x) the sum of [interference j t] and [scheduled_at j t]
is no larger than the sum of [the service received by jobs of task
tsk at time t] and [task_iterference tsk t]. *)
@@ -508,7 +508,7 @@ Section Sequential_Abstract_RTA.
End CaseAnalysis.
- (* Next we prove cumulative version of the lemma above. *)
+ (** Next we prove cumulative version of the lemma above. *)
Lemma cumul_interference_plus_sched_le_serv_of_task_plus_cumul_task_interference:
cumul_interference j t1 (t1 + x)
<= (task_service_of_jobs_in (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
@@ -531,7 +531,7 @@ Section Sequential_Abstract_RTA.
by apply interference_plus_sched_le_serv_of_task_plus_task_interference.
Qed.
- (* On the other hand, the service terms in the inequality
+ (** On the other hand, the service terms in the inequality
above can be upper-bound by the workload terms. *)
Lemma serv_of_task_le_workload_of_task_plus:
task_service_of_jobs_in (arrivals_between t1 (t1 + A + ε)) t1 (t1 + x)
@@ -555,7 +555,7 @@ Section Sequential_Abstract_RTA.
by apply service_of_jobs_le_workload; auto using ideal_proc_model_provides_unit_service.
Qed.
- (* Finally, we show that the cumulative interference of job j in the interval [t1, t1 + x)
+ (** 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). *)
Lemma cumulative_job_interference_le_task_interference_bound:
@@ -573,7 +573,7 @@ Section Sequential_Abstract_RTA.
End TaskInterferenceBoundsInterference.
- (* In order to obtain a more convenient bound of the cumulative interference, we need to
+ (** 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. *)
@@ -620,7 +620,7 @@ Section Sequential_Abstract_RTA.
by rewrite -TSK2; apply H_job_cost_le_task_cost; exists (t1 + A); apply rem_in in ARR'.
Qed.
- (* Finally, we use the lemmas above to obtain the bound on
+ (** Finally, we use the lemmas above to obtain the bound on
interference in terms of task_rbf and task_interfere. *)
Lemma cumulative_job_interference_bound:
cumul_interference j t1 (t1 + x)
@@ -640,19 +640,19 @@ Section Sequential_Abstract_RTA.
End BoundOfCumulativeJobInterference.
- (* In this section, we prove that [H_R_is_maximum_seq] implies [H_R_is_maximum]. *)
+ (** 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.
- (* For simplicity, let's define a local name for the search space. *)
+ (** For simplicity, let's define a local name for the search space. *)
Let is_in_search_space A :=
is_in_search_space tsk L total_interference_bound A.
- (* We prove that [H_R_is_maximum] holds. *)
+ (** We prove that [H_R_is_maximum] holds. *)
Lemma max_in_seq_hypothesis_implies_max_in_nonseq_hypothesis:
forall (A : duration),
is_in_search_space A ->
@@ -680,7 +680,7 @@ Section Sequential_Abstract_RTA.
End MaxInSeqHypothesisImpMaxInNonseqHypothesis.
- (* Finally, we apply the [uniprocessor_response_time_bound] theorem, and using the
+ (** Finally, we apply the [uniprocessor_response_time_bound] theorem, and using the
lemmas above, we prove that all the requirements are satisfied. So, R is a response
time bound. *)
Theorem uniprocessor_response_time_bound_seq:
diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index 56e6d79bebf4ca910c14d7f023b520e79ecabc45..dd1fcb2a05bcbc1ff3d72123735666bf7f007b73 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -9,40 +9,40 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
of uniprocessor scheduling of real-time tasks with arbitrary arrival models. *)
Section AbstractRTADefinitions.
- (* In this section, we introduce all the abstract notions required by the analysis. *)
+ (** In this section, we introduce all the abstract notions required by the analysis. *)
Section Definitions.
- (* Consider any type of job associated with any type of tasks... *)
+ (** Consider any type of job associated with any type of tasks... *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
- (* ... with arrival times and costs. *)
+ (** ... with arrival times and costs. *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Consider any arrival sequence... *)
+ (** Consider any arrival sequence... *)
Variable arr_seq : arrival_sequence Job.
- (* ... and any ideal uniprocessor schedule of this arrival sequence. *)
+ (** ... and any ideal uniprocessor 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. *)
+ (** 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
+ (** 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:
+ (** We are going to introduce two main variables of the analysis:
(a) interference, and (b) interfering workload. *)
(** a) Interference *)
- (* Execution of a job may be postponed by the environment and/or the system due to different
+ (** Execution of a job may be postponed by the environment and/or the system due to different
factors (preemption by higher-priority jobs, jitter, black-out periods in hierarchical
scheduling, lack of budget, etc.), which we call interference.
@@ -60,7 +60,7 @@ Section AbstractRTADefinitions.
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
@@ -71,18 +71,18 @@ Section AbstractRTADefinitions.
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
+ (** In order to bound the response time of a job, we must to consider the cumulative
interference and cumulative interfering workload. *)
Definition cumul_interference j t1 t2 := \sum_(t1 <= t < t2) interference j t.
Definition cumul_interfering_workload j t1 t2 := \sum_(t1 <= t < t2) interfering_workload j t.
(** Definition of Busy Interval *)
- (* Further analysis will be based on the notion of a busy interval. The overall idea of the
+ (** Further analysis will be based on the notion of a busy interval. The overall idea of the
busy interval is to take into account the workload that cause a job under consideration to
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.
+ (** 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
@@ -94,7 +94,7 @@ Section AbstractRTADefinitions.
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
+ (** 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
interval (a) contains the arrival of job j, (b) starts with a quiet
time and (c) remains non-quiet. *)
@@ -103,13 +103,13 @@ Section AbstractRTADefinitions.
quiet_time j t1 /\
(forall t, t1 < t < t2 -> ~ quiet_time j t).
- (* Next, we say that an interval [t1, t2) is a busy interval iff
+ (** Next, we say that an interval [t1, t2) is a busy interval iff
[t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
Definition busy_interval (j : Job) (t1 t2 : instant) :=
busy_interval_prefix j t1 t2 /\
quiet_time j t2.
- (* Note that the busy interval, if it exists, is unique. *)
+ (** Note that the busy interval, if it exists, is unique. *)
Lemma busy_interval_is_unique:
forall j t1 t2 t1' t2',
busy_interval j t1 t2 ->
@@ -155,11 +155,11 @@ Section AbstractRTADefinitions.
End BusyInterval.
- (* In this section, we introduce some assumptions about the
+ (** In this section, we introduce some assumptions about the
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
+ (** 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 :=
@@ -171,7 +171,7 @@ 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
+ (** 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
@@ -186,7 +186,7 @@ Section AbstractRTADefinitions.
t2 <= t1 + L /\
busy_interval j t1 t2.
- (* Although we have defined the notion of cumulative interference of a job, it cannot be used in
+ (** Although we have defined the notion of cumulative interference of a job, it cannot be used in
a response-time analysis because of the variability of job parameters. To address this
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,
@@ -196,20 +196,20 @@ Section AbstractRTADefinitions.
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. *)
+ (** 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). *)
+ (** Next, we require the IBF to bound the interference only within the interval [t1, t1 + delta). *)
busy_interval j t1 t2 ->
t1 + delta < t2 ->
- (* Next, we require the IBF to bound the interference only until the job is
+ (** Next, we require the IBF to bound the interference only until the job is
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
+ (** 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). *)
- (* While the first three conditions are needed for discarding excessive cases, offset adds
+ (** 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
cumul_interference j t1 (t1 + delta) <= interference_bound_function tsk offset delta.
diff --git a/restructuring/analysis/abstract/core/reduction_of_search_space.v b/restructuring/analysis/abstract/core/reduction_of_search_space.v
index 1c8833a6601a56a82217314607f8e0fa55486748..e24eb8f49d2aeadca8b53031b02f6002fe8ee926 100644
--- a/restructuring/analysis/abstract/core/reduction_of_search_space.v
+++ b/restructuring/analysis/abstract/core/reduction_of_search_space.v
@@ -9,7 +9,7 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
Section AbstractRTAReduction.
- (* The response-time analysis we are presenting in this series of documents is based on searching
+ (** 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
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
@@ -17,24 +17,24 @@ Section AbstractRTAReduction.
Context {Task : TaskType}.
- (* First, we provide a constructive notion of equivalent functions. *)
+ (** 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
+ (** 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
+ (** 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 :=
@@ -42,22 +42,22 @@ Section AbstractRTAReduction.
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
+ (** 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
+ (** 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). *)
Variable interference_bound_function : Task -> duration -> duration -> duration.
- (* Recall the definition of ε, which defines the neighborhood of a point in the timeline.
+ (** 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
+ (** 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 :=
@@ -65,16 +65,16 @@ Section AbstractRTAReduction.
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 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:
+ (** 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
@@ -124,17 +124,17 @@ Section AbstractRTAReduction.
End ExistenceOfRepresentative.
- (* In this section we prove that any solution of the response-time recurrence for
+ (** 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 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
+ (** 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.
@@ -144,7 +144,7 @@ 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]
+ (** 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. *)
Lemma solution_for_A_exists:
exists F,
diff --git a/restructuring/analysis/abstract/core/run_to_completion_threshold.v b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
index 3df959fd19444805f380e6d80ae7d09e4e45f268..191d43eb50714ddec8b7341f411805cbbc7bf7f8 100644
--- a/restructuring/analysis/abstract/core/run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/run_to_completion_threshold.v
@@ -10,43 +10,43 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
of run-to-completion-threshold-compilant schedules. *)
Section RunToCompletionThreshold.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* In addition, we assume existence of a function
+ (** In addition, we assume existence of a function
maping jobs to theirs preemption points ... *)
Context `{JobPreemptable Job}.
- (* ...and a function mapping tasks to theirs
+ (** ...and a function mapping tasks to theirs
run-to-completion threshold. *)
Context `{TaskRunToCompletionThreshold Task}.
- (* Consider any kind of processor state model, ... *)
+ (** Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (* ... any job arrival sequence, ... *)
+ (** ... any job arrival sequence, ... *)
Variable arr_seq: arrival_sequence Job.
- (* ... and any given schedule. *)
+ (** ... and any given schedule. *)
Variable sched: schedule PState.
- (* In this section we define the notion of a run-to-completion threshold for a job. *)
+ (** In this section we define the notion of a run-to-completion threshold for a job. *)
Section JobRunToCompletionThreshold.
- (* We define the notion of job's run-to-completion threshold: run-to-completion threshold
+ (** We define the notion of job's run-to-completion threshold: run-to-completion threshold
is the amount of service after which a job cannot be preempted until its completion. *)
Definition runs_to_completion_from (j : Job) (Ï : duration) :=
all (fun (δ : duration) => ~~ job_preemptable j δ) (index_iota Ï (job_cost j)).
- (* Note that a run-to-completion threshold exists for any job. *)
+ (** Note that a run-to-completion threshold exists for any job. *)
Lemma eventually_runs_to_completion:
forall (j : Job), exists (Ï : duration), runs_to_completion_from j Ï.
Proof.
@@ -56,24 +56,24 @@ Section RunToCompletionThreshold.
by move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
Qed.
- (* We define run-to-completion threshold of a job as the minimal progress
+ (** We define run-to-completion threshold of a job as the minimal progress
the job should reach to become non-preemptive until completion. *)
Definition job_run_to_completion_threshold (j : Job) : duration :=
ex_minn (eventually_runs_to_completion j).
- (* In this section we prove a few simple lemmas
+ (** In this section we prove a few simple lemmas
about run-to-completion threshold for a job. *)
Section Lemmas.
- (* Assume that the preemption model is valid. *)
+ (** Assume that the preemption model is valid. *)
Hypothesis H_valid_preemption_model:
valid_preemption_model arr_seq sched.
- (* Consider an arbitrary job j from the arrival sequence. *)
+ (** Consider an arbitrary job j from the arrival sequence. *)
Variable j : Job.
Hypothesis H_j_in_arrival_seq : arrives_in arr_seq j.
- (* First, we prove that a job cannot be preempted
+ (** First, we prove that a job cannot be preempted
during execution of the last segment. *)
Lemma job_cannot_be_preempted_within_last_segment:
forall (Ï : duration),
@@ -87,7 +87,7 @@ Section RunToCompletionThreshold.
by apply RUNS; rewrite mem_index_iota; apply/andP; split.
Qed.
- (* We prove that the run-to-completion threshold is positive for any job. I.e., in order
+ (** We prove that the run-to-completion threshold is positive for any job. I.e., in order
to become non-preemptive a job must receive at least one unit of service. *)
Lemma job_run_to_completion_threshold_positive:
job_cost_positive j ->
@@ -104,7 +104,7 @@ Section RunToCompletionThreshold.
by apply H_valid_preemption_model.
Qed.
- (* Next we show that the run-to-completion threshold
+ (** Next we show that the run-to-completion threshold
is at most the cost of a job. *)
Lemma job_run_to_completion_threshold_le_job_cost:
job_cost_positive j ->
@@ -117,7 +117,7 @@ Section RunToCompletionThreshold.
by move: GE; rewrite leqNgt; move => /negP GE; apply: GE.
Qed.
- (* In order to get a consistent schedule, the scheduler should respect
+ (** In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion. *)
@@ -139,7 +139,7 @@ Section RunToCompletionThreshold.
End JobRunToCompletionThreshold.
- (* Since a task model may not provide exact information about preemption point of
+ (** Since a task model may not provide exact information about preemption point of
a task run-to-completion, task's run-to-completion threshold cannot be defined in
terms of preemption points of a task (unlike job's run-to-completion threshold).
Therefore, one can assume the existence of a function that maps a task to
@@ -147,11 +147,11 @@ Section RunToCompletionThreshold.
of a valid run-to-completion threshold of a task. *)
Section ValidTaskRunToCompletionThreshold.
- (* A task's run-to-completion threshold should be at most the cost of the task. *)
+ (** A task's run-to-completion threshold should be at most the cost of the task. *)
Definition task_run_to_completion_threshold_le_task_cost tsk :=
task_run_to_completion_threshold tsk <= task_cost tsk.
- (* We say that the run-to-completion threshold of a task tsk
+ (** We say that the run-to-completion threshold of a task tsk
bounds the job run-to-completionthreshold iff for any job j
of task tsk the job run-to-completion threshold is less than
or equal to the task run-to-completion threshold. *)
@@ -161,7 +161,7 @@ Section RunToCompletionThreshold.
job_task j = tsk ->
job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
- (* We say that task_run_to_completion_threshold is a valid task run-to-completion
+ (** We say that task_run_to_completion_threshold is a valid task run-to-completion
threshold for a task tsk iff [task_run_to_completion_threshold tsk] is (1) no
bigger than tsk's cost, (2) for any job of task tsk job_run_to_completion_threshold
is bounded by task_run_to_completion_threshold. *)
diff --git a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
index bf6fa2b342977cd56901b4cdb93c8d632d283024..41275bfc19f664100c1ed0e00cf8d0f7ab28c274 100644
--- a/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
+++ b/restructuring/analysis/abstract/core/sufficient_condition_for_run_to_completion_threshold.v
@@ -9,7 +9,7 @@ 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. *)
-(* Previously we defined the notion of run-to-completion threshold (see file
+(** 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
@@ -17,57 +17,57 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
run-to-completion threshold and become nonpreemptive. *)
Section AbstractRTARunToCompletionThreshold.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* In addition, we assume existence of a function
+ (** In addition, we assume existence of a function
maping jobs to their preemption points. *)
Context `{JobPreemptable Job}.
- (* Consider any arrival sequence with consistent arrivals... *)
+ (** 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 uniprocessor schedule of this arrival sequence. *)
Variable sched : schedule (ideal.processor_state Job).
- (* Assume that the job costs are no larger than the task costs. *)
+ (** 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. *)
+ (** Assume we are provided with abstract functions for interference and interfering workload. *)
Variable interference : Job -> instant -> bool.
Variable interfering_workload : Job -> instant -> duration.
- (* For simplicity, let's define some local names. *)
+ (** For simplicity, let's define some local names. *)
Let work_conserving := work_conserving arr_seq sched tsk.
Let cumul_interference := cumul_interference interference.
Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.
Let busy_interval := busy_interval sched interference interfering_workload.
- (* We assume that the schedule is work-conserving. *)
+ (** 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. *)
@@ -81,16 +81,16 @@ Section AbstractRTARunToCompletionThreshold.
by rewrite Bool.negb_involutive in QT2.
Qed.
- (* In this section we show that the cumulative interference is a complement to
+ (** 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. *)
Section InterferenceIsComplement.
- (* Consider any subinterval [t, t + delta) inside the busy interval [t1, t2). *)
+ (** Consider any subinterval [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.
- (* We prove that sum of cumulative service and cumulative interference
+ (** We prove that sum of cumulative service and cumulative interference
in the interval [t, t + delta) is equal to delta. *)
Lemma interference_is_complement_to_schedule:
service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.
@@ -124,20 +124,20 @@ 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. *)
+ (** Let progress_of_job be the desired service of job j. *)
Variable progress_of_job : duration.
Hypothesis H_progress_le_job_cost : progress_of_job <= job_cost j.
- (* Assume that for some delta, the sum of desired progress and cumulative
+ (** Assume that for some delta, the sum of desired progress and cumulative
interference is bounded by delta (i.e., the supply). *)
Variable delta : duration.
Hypothesis H_total_workload_is_bounded:
progress_of_job + cumul_interference j t1 (t1 + delta) <= delta.
- (* Then, it must be the case that the job has received no less service than progress_of_job. *)
+ (** Then, it must be the case that the job has received no less service than progress_of_job. *)
Theorem j_receives_at_least_run_to_completion_threshold:
service sched j (t1 + delta) >= progress_of_job.
Proof.
@@ -166,19 +166,19 @@ Section AbstractRTARunToCompletionThreshold.
End InterferenceBoundedImpliesEnoughService.
- (* In this section we prove a simple lemma about completion of
+ (** In this section we prove a simple lemma about completion of
a job after is reaches run-to-completion threshold. *)
Section CompletionOfJobAfterRunToCompletionThreshold.
- (* Assume that completed jobs do not execute ... *)
+ (** Assume that completed jobs do not execute ... *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute sched.
- (* .. and the preemption model is valid. *)
+ (** .. and the preemption model is valid. *)
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/arrival/rbf.v b/restructuring/analysis/arrival/rbf.v
index 6159f10d3064651f182ce6e9a9f64f6aa7a89583..e67260e5096628c1314f3302ec47f0afa643e5ff 100644
--- a/restructuring/analysis/arrival/rbf.v
+++ b/restructuring/analysis/arrival/rbf.v
@@ -11,34 +11,34 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** In this section, we prove some properties of Request Bound Functions (RBF). *)
Section RequestBoundFunctions.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
- (* Consider any arrival sequence. *)
+ (** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
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
+ (** 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).
Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
- (* We prove that [task_rbf 0] is equal to 0. *)
+ (** We prove that [task_rbf 0] is equal to 0. *)
Lemma task_rbf_0_zero:
task_rbf 0 = 0.
Proof.
@@ -47,7 +47,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.
@@ -57,13 +57,13 @@ Section RequestBoundFunctions.
by move: H_valid_arrival_curve => [_ T]; apply T.
Qed.
- (* Consider any job j of tsk. This guarantees that
+ (** 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/arrival/workload_bound.v b/restructuring/analysis/arrival/workload_bound.v
index 11d998ccee1332e5d97d1db5c932444b1366fe97..0ab32d35f4eed91461da177dcc31605792e5fe89 100644
--- a/restructuring/analysis/arrival/workload_bound.v
+++ b/restructuring/analysis/arrival/workload_bound.v
@@ -11,81 +11,81 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
(** * Task Workload Bounded by Arrival Curves *)
Section TaskWorkloadBoundedByArrivalCurves.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Consider any arrival sequence with consistent, non-duplicate arrivals... *)
+ (** Consider any arrival sequence with consistent, non-duplicate arrivals... *)
Variable arr_seq : arrival_sequence Job.
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 uniprocessor 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.
- (* Consider an FP policy that indicates a higher-or-equal priority relation. *)
+ (** Consider an FP policy that indicates a higher-or-equal priority relation. *)
Variable higher_eq_priority : FP_policy Task.
Let jlfp_higher_eq_priority := FP_to_JLFP Job Task.
- (* For simplicity, let's define some local names. *)
+ (** For simplicity, let's define some local names. *)
Let arrivals_between := arrivals_between arr_seq.
- (* We define the notion of request bound function. *)
+ (** We define the notion of request bound function. *)
Section RequestBoundFunction.
- (* 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}.
- (* In this section, we define a bound for the workload of a single task
+ (** In this section, we define a bound for the workload of a single task
under uniprocessor 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.
- (* We define the following workload bound for the task. *)
+ (** We define the following workload bound for the task. *)
Definition task_request_bound_function := task_cost tsk * max_arrivals tsk delta.
End SingleTask.
- (* In this section, we define a bound for the workload of multiple tasks. *)
+ (** In this section, we define a bound for the workload of multiple tasks. *)
Section AllTasks.
- (* Consider a task set ts... *)
+ (** 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. *)
+ (** Let delta be the length of the interval of interest. *)
Variable delta : duration.
- (* Recall the definition of higher-or-equal-priority task and
+ (** Recall the definition of higher-or-equal-priority task and
the per-task workload bound for FP scheduling. *)
Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
Let is_other_hep_task tsk_other := higher_eq_priority tsk_other tsk && (tsk_other != tsk).
- (* Using the sum of individual workload bounds, we define the following bound
+ (** Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks in any interval of length delta. *)
Definition total_request_bound_function :=
\sum_(tsk <- ts) task_request_bound_function tsk delta.
- (* Similarly, we define the following bound for the total workload of tasks of
+ (** Similarly, we define the following bound for the total workload of 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
+ (** We also define a bound for the total workload of higher-or-equal
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)
@@ -95,66 +95,66 @@ Section TaskWorkloadBoundedByArrivalCurves.
End RequestBoundFunction.
- (* In this section we prove some lemmas about request bound functions. *)
+ (** In this section we prove some lemmas about request bound functions. *)
Section ProofWorkloadBound.
- (* Consider a task set ts... *)
+ (** 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.
- (* Assume that the job costs are no larger than the task costs. *)
+ (** Assume that the job costs are no larger than the task costs. *)
Hypothesis H_job_cost_le_task_cost :
cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
- (* Next, we assume that all jobs come from the task set. *)
+ (** 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 taskset ts. *)
Context `{MaxArrivals Task}.
Hypothesis H_is_arrival_bound : taskset_respects_max_arrivals arr_seq ts.
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let task_rbf := task_request_bound_function tsk.
Let total_rbf := total_request_bound_function ts.
Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
Let total_ohep_rbf := total_ohep_request_bound_function_FP 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
+ (** 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).
- (* Next, we recall the notions of total workload of jobs... *)
+ (** Next, we recall the notions of total workload of jobs... *)
Let total_workload t1 t2 := workload_of_jobs predT (arrivals_between t1 t2).
- (* ...notions of workload of higher or equal priority jobs... *)
+ (** ...notions of workload of higher or equal priority jobs... *)
Let total_hep_workload t1 t2 :=
workload_of_jobs (fun j_other => jlfp_higher_eq_priority j_other j) (arrivals_between t1 t2).
- (* ... workload of other higher or equal priority jobs... *)
+ (** ... workload of other higher or equal priority jobs... *)
Let total_ohep_workload t1 t2 :=
workload_of_jobs (fun j_other => other_higher_eq_priority j_other j) (arrivals_between t1 t2).
- (* ... and the workload of jobs of the same task as job j. *)
+ (** ... and the workload of jobs of the same task as job j. *)
Let task_workload t1 t2 :=
workload_of_jobs (job_of_task tsk) (arrivals_between t1 t2).
- (* In this section we prove that the workload of any jobs is
+ (** In this section we prove that the workload of any jobs is
no larger than the request bound function. *)
Section WorkloadIsBoundedByRBF.
- (* Consider any time t and any interval of length delta. *)
+ (** Consider any time t and any interval of length delta. *)
Variable t : instant.
Variable delta : instant.
- (* First, we show that workload of task tsk is bounded by
+ (** 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)
@@ -168,7 +168,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
by apply H_job_cost_le_task_cost.
Qed.
- (* As a corollary, we prove that workload of task is
+ (** As a corollary, we prove that workload of task is
no larger the than task request bound function. *)
Corollary task_workload_le_task_rbf:
task_workload t (t + delta) <= task_rbf delta.
@@ -181,7 +181,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
by apply H_is_arrival_bound; last rewrite leq_addr.
Qed.
- (* Next, we prove that total workload of other tasks with
+ (** Next, we prove that total workload of other tasks with
higher-or-equal priority is no larger than the total
request bound function. *)
Lemma total_workload_le_total_rbf:
@@ -217,7 +217,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
}
Qed.
- (* Next, we prove that total workload of tasks with higher-or-equal
+ (** Next, we prove that total workload of tasks with higher-or-equal
priority is no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf':
total_hep_workload t (t + delta) <= total_hep_rbf delta.
@@ -252,7 +252,7 @@ Section TaskWorkloadBoundedByArrivalCurves.
}
Qed.
- (* Next, we prove that total workload of tasks is
+ (** Next, we prove that total workload of tasks is
no larger than the total request bound function. *)
Lemma total_workload_le_total_rbf'':
total_workload t (t + delta) <= total_rbf delta.
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 361c73159fcc1d9fa2872e852f5755f976208f52..3b0c19700c3f8037bb53fc2cdd94866b3d25f9c0 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -1,22 +1,22 @@
From rt.restructuring.behavior Require Export all.
From rt.util Require Import all.
-(* In this section, we relate job readiness to [has_arrived]. *)
+(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
- (* Consider any kinds of jobs and any kind of processor state. *)
+ (** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
- (* Consider any schedule... *)
+ (** Consider any schedule... *)
Variable sched : schedule PState.
- (* ...and suppose that jobs have a cost, an arrival time, and a notion of
+ (** ...and suppose that jobs have a cost, an arrival time, and a notion of
readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
- (* We observe that a given job must have arrived to be ready... *)
+ (** We observe that a given job must have arrived to be ready... *)
Lemma ready_implies_arrived:
forall j t, job_ready sched j t -> has_arrived j t.
Proof.
@@ -25,7 +25,7 @@ Section Arrived.
by rewrite /pending => /andP [ARR _].
Qed.
- (* ...and lift this observation also to the level of whole schedules. *)
+ (** ...and lift this observation also to the level of whole schedules. *)
Lemma jobs_must_arrive_to_be_ready:
jobs_must_be_ready_to_execute sched ->
jobs_must_arrive_to_execute sched.
@@ -38,23 +38,23 @@ Section Arrived.
End Arrived.
-(* In this section, we establish useful facts about arrival sequence prefixes. *)
+(** In this section, we establish useful facts about arrival sequence prefixes. *)
Section ArrivalSequencePrefix.
- (* Assume that job arrival times are known. *)
+ (** Assume that job arrival times are known. *)
Context {Job: JobType}.
Context `{JobArrival Job}.
- (* Consider any job arrival sequence. *)
+ (** Consider any job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
- (* In this section, we prove some lemmas about arrival sequence prefixes. *)
+ (** In this section, we prove some lemmas about arrival sequence prefixes. *)
Section Lemmas.
- (* We begin with basic lemmas for manipulating the sequences. *)
+ (** We begin with basic lemmas for manipulating the sequences. *)
Section Composition.
- (* First, we show that the set of arriving jobs can be split
+ (** First, we show that the set of arriving jobs can be split
into disjoint intervals. *)
Lemma arrivals_between_cat:
forall t1 t t2,
@@ -66,7 +66,7 @@ Section ArrivalSequencePrefix.
by rewrite (@big_cat_nat _ _ _ t).
Qed.
- (* Second, the same observation applies to membership in the set of
+ (** Second, the same observation applies to membership in the set of
arrived jobs. *)
Lemma arrivals_between_mem_cat:
forall j t1 t t2,
@@ -78,7 +78,7 @@ Section ArrivalSequencePrefix.
by intros j t1 t t2 GE LE; rewrite (arrivals_between_cat _ t).
Qed.
- (* Third, we observe that we can grow the considered interval without
+ (** Third, we observe that we can grow the considered interval without
"losing" any arrived jobs, i.e., membership in the set of arrived jobs
is monotonic. *)
Lemma arrivals_between_sub:
@@ -100,14 +100,14 @@ Section ArrivalSequencePrefix.
End Composition.
- (* Next, we relate the arrival prefixes with job arrival times. *)
+ (** Next, we relate the arrival prefixes with job arrival times. *)
Section ArrivalTimes.
- (* Assume that job arrival times are consistent. *)
+ (** Assume that job arrival times are consistent. *)
Hypothesis H_consistent_arrival_times:
consistent_arrival_times arr_seq.
- (* First, we prove that if a job belongs to the prefix
+ (** First, we prove that if a job belongs to the prefix
(jobs_arrived_before t), then it arrives in the arrival sequence. *)
Lemma in_arrivals_implies_arrived:
forall j t1 t2,
@@ -121,7 +121,7 @@ Section ArrivalSequencePrefix.
by exists arr.
Qed.
- (* Next, we prove that if a job belongs to the prefix
+ (** Next, we prove that if a job belongs to the prefix
(jobs_arrived_between t1 t2), then it indeed arrives between t1 and
t2. *)
Lemma in_arrivals_implies_arrived_between:
@@ -136,7 +136,7 @@ Section ArrivalSequencePrefix.
by apply CONS in IN; rewrite /arrived_between IN.
Qed.
- (* Similarly, if a job belongs to the prefix (jobs_arrived_before t),
+ (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
then it indeed arrives before time t. *)
Lemma in_arrivals_implies_arrived_before:
forall j t,
@@ -148,7 +148,7 @@ Section ArrivalSequencePrefix.
by rewrite /arrived_between /=.
Qed.
- (* Similarly, we prove that if a job from the arrival sequence arrives
+ (** Similarly, we prove that if a job from the arrival sequence arrives
before t, then it belongs to the sequence (jobs_arrived_before t). *)
Lemma arrived_between_implies_in_arrivals:
forall j t1 t2,
@@ -162,7 +162,7 @@ Section ArrivalSequencePrefix.
by apply mem_bigcat_nat with (j := (job_arrival j)).
Qed.
- (* Next, we prove that if the arrival sequence doesn't contain duplicate
+ (** Next, we prove that if the arrival sequence doesn't contain duplicate
jobs, the same applies for any of its prefixes. *)
Lemma arrivals_uniq :
arrival_sequence_uniq arr_seq ->
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index 4263486dd97836b340e41508eed68dcfa518b0a9..eeec87ba7467579b65c7c88fdb428b99a2a58dab 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -6,21 +6,21 @@ From rt.util Require Import nat.
(** In this file, we establish basic facts about job completions. *)
Section CompletionFacts.
- (* Consider any job type,...*)
+ (** Consider any job type,...*)
Context {Job: JobType}.
Context `{JobCost Job}.
- (* ...any kind of processor model,... *)
+ (** ...any kind of processor model,... *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* ...and a given schedule. *)
+ (** ...and a given schedule. *)
Variable sched: schedule PState.
- (* Let j be any job that is to be scheduled. *)
+ (** Let j be any job that is to be scheduled. *)
Variable j: Job.
- (* We prove that after job j completes, it remains completed. *)
+ (** We prove that after job j completes, it remains completed. *)
Lemma completion_monotonic:
forall t t',
t <= t' ->
@@ -32,7 +32,7 @@ Section CompletionFacts.
by apply service_monotonic.
Qed.
- (* We observe that being incomplete is the same as not having received
+ (** We observe that being incomplete is the same as not having received
sufficient service yet... *)
Lemma less_service_than_cost_is_incomplete:
forall t,
@@ -43,7 +43,7 @@ Section CompletionFacts.
move=> t. by split; rewrite /completed_by; [rewrite -ltnNge // | rewrite ltnNge //].
Qed.
- (* ...which is also the same as having positive remaining cost. *)
+ (** ...which is also the same as having positive remaining cost. *)
Lemma incomplete_is_positive_remaining_cost:
forall t,
~~ completed_by sched j t
@@ -53,11 +53,11 @@ Section CompletionFacts.
move=> t. by split; rewrite /remaining_cost -less_service_than_cost_is_incomplete subn_gt0 //.
Qed.
- (* Assume that completed jobs do not execute. *)
+ (** Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute sched.
- (* Further, we note that if a job receives service at some time t, then its
+ (** Further, we note that if a job receives service at some time t, then its
remaining cost at this time is positive. *)
Lemma serviced_implies_positive_remaining_cost:
forall t,
@@ -70,14 +70,14 @@ Section CompletionFacts.
by apply service_at_implies_scheduled_at.
Qed.
- (* Consequently, if we have a have processor model where scheduled jobs
+ (** Consequently, if we have a have processor model where scheduled jobs
* necessarily receive service, we can conclude that scheduled jobs have
* remaining positive cost. *)
- (* Assume a scheduled job always receives some positive service. *)
+ (** Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* Then a scheduled job has positive remaining cost. *)
+ (** Then a scheduled job has positive remaining cost. *)
Corollary scheduled_implies_positive_remaining_cost:
forall t,
scheduled_at sched j t ->
@@ -87,7 +87,7 @@ Section CompletionFacts.
by apply: serviced_implies_positive_remaining_cost; rewrite /service_at; apply: H_scheduled_implies_serviced.
Qed.
- (* We also prove that a completed job cannot be scheduled... *)
+ (** We also prove that a completed job cannot be scheduled... *)
Lemma completed_implies_not_scheduled:
forall t,
completed_by sched j t ->
@@ -100,7 +100,7 @@ Section CompletionFacts.
by rewrite less_service_than_cost_is_incomplete.
Qed.
- (* ... and that a scheduled job cannot be completed. *)
+ (** ... and that a scheduled job cannot be completed. *)
Lemma scheduled_implies_not_completed:
forall t,
scheduled_at sched j t ->
@@ -120,28 +120,28 @@ Section ServiceAndCompletionFacts.
but are also related to completion and rely on some of the above lemmas.
Hence they are in this file rather than in the service facts file. *)
- (* Consider any job type,...*)
+ (** Consider any job type,...*)
Context {Job: JobType}.
Context `{JobCost Job}.
- (* ...any kind of processor model,... *)
+ (** ...any kind of processor model,... *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* ...and a given schedule. *)
+ (** ...and a given schedule. *)
Variable sched: schedule PState.
- (* Assume that completed jobs do not execute. *)
+ (** Assume that completed jobs do not execute. *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute sched.
- (* Let j be any job that is to be scheduled. *)
+ (** Let j be any job that is to be scheduled. *)
Variable j: Job.
- (* Assume that a scheduled job receives exactly one time unit of service. *)
+ (** Assume that a scheduled job receives exactly one time unit of service. *)
Hypothesis H_unit_service: unit_service_proc_model.
- (* To begin with, we establish that the cumulative service never exceeds a
+ (** To begin with, we establish that the cumulative service never exceeds a
job's total cost if service increases only by one at each step since
completed jobs don't execute. *)
Lemma service_at_most_cost:
@@ -162,7 +162,7 @@ Section ServiceAndCompletionFacts.
by apply H_unit_service.
Qed.
- (* This lets us conclude that [service] and [remaining_cost] are complements
+ (** This lets us conclude that [service] and [remaining_cost] are complements
of one another. *)
Lemma service_cost_invariant:
forall t,
@@ -173,7 +173,7 @@ Section ServiceAndCompletionFacts.
by apply service_at_most_cost.
Qed.
- (* We show that the service received by job j in any interval is no larger
+ (** We show that the service received by job j in any interval is no larger
than its cost. *)
Lemma cumulative_service_le_job_cost:
forall t t',
@@ -185,7 +185,7 @@ Section ServiceAndCompletionFacts.
rewrite /service. rewrite -(service_during_cat sched j 0 t t') // leq_addl //.
Qed.
- (* If a job isn't complete at time t, it can't be completed at time (t +
+ (** If a job isn't complete at time t, it can't be completed at time (t +
remaining_cost j t - 1). *)
Lemma job_doesnt_complete_before_remaining_cost:
forall t,
@@ -205,14 +205,14 @@ Section ServiceAndCompletionFacts.
Section GuaranteedService.
- (* Assume a scheduled job always receives some positive service. *)
+ (** Assume a scheduled job always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* Assume that jobs are not released early. *)
+ (** Assume that jobs are not released early. *)
Context `{JobArrival Job}.
Hypothesis H_jobs_must_arrive: jobs_must_arrive_to_execute sched.
- (* We show that if job j is scheduled, then it must be pending. *)
+ (** We show that if job j is scheduled, then it must be pending. *)
Lemma scheduled_implies_pending:
forall t,
scheduled_at sched j t ->
@@ -233,30 +233,30 @@ Section PositiveCost.
(** In this section, we establish facts that on jobs with non-zero costs that
must arrive to execute. *)
- (* Consider any type of jobs with cost and arrival-time attributes,...*)
+ (** Consider any type of jobs with cost and arrival-time attributes,...*)
Context {Job: JobType}.
Context `{JobCost Job}.
Context `{JobArrival Job}.
- (* ...any kind of processor model,... *)
+ (** ...any kind of processor model,... *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* ...and a given schedule. *)
+ (** ...and a given schedule. *)
Variable sched: schedule PState.
- (* Let j be any job that is to be scheduled. *)
+ (** Let j be any job that is to be scheduled. *)
Variable j: Job.
- (* We assume that job j has positive cost, from which we can
+ (** We assume that job j has positive cost, from which we can
infer that there always is a time in which j is pending, ... *)
Hypothesis H_positive_cost: job_cost j > 0.
- (* ...and that jobs must arrive to execute. *)
+ (** ...and that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
- (* Then, we prove that the job with a positive cost
+ (** Then, we prove that the job with a positive cost
must be scheduled to be completed. *)
Lemma completed_implies_scheduled_before:
forall t,
@@ -272,7 +272,7 @@ Section PositiveCost.
by apply: positive_service_implies_scheduled_since_arrival; assumption.
Qed.
- (* We also prove that the job is pending at the moment of its arrival. *)
+ (** We also prove that the job is pending at the moment of its arrival. *)
Lemma job_pending_at_arrival:
pending sched j (job_arrival j).
Proof.
@@ -285,20 +285,20 @@ Section PositiveCost.
End PositiveCost.
Section CompletedJobs.
- (* Consider any kinds of jobs and any kind of processor state. *)
+ (** Consider any kinds of jobs and any kind of processor state. *)
Context {Job : JobType} {PState : Type}.
Context `{ProcessorState Job PState}.
- (* Consider any schedule... *)
+ (** Consider any schedule... *)
Variable sched : schedule PState.
- (* ...and suppose that jobs have a cost, an arrival time, and a notion of
+ (** ...and suppose that jobs have a cost, an arrival time, and a notion of
readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
Context `{JobReady Job PState}.
- (* We observe that a given job is ready only if it is also incomplete... *)
+ (** We observe that a given job is ready only if it is also incomplete... *)
Lemma ready_implies_incomplete:
forall j t, job_ready sched j t -> ~~ completed_by sched j t.
Proof.
@@ -307,7 +307,7 @@ Section CompletedJobs.
by rewrite /pending => /andP [_ INCOMPLETE].
Qed.
- (* ...and lift this observation also to the level of whole schedules. *)
+ (** ...and lift this observation also to the level of whole schedules. *)
Lemma completed_jobs_are_not_ready:
jobs_must_be_ready_to_execute sched ->
completed_jobs_dont_execute sched.
@@ -319,7 +319,7 @@ Section CompletedJobs.
by apply ready_implies_incomplete.
Qed.
- (* We further observe that completed jobs don't execute if scheduled jobs
+ (** We further observe that completed jobs don't execute if scheduled jobs
always receive non-zero service and cumulative service never exceeds job
costs. *)
Lemma ideal_progress_completed_jobs:
diff --git a/restructuring/analysis/basic_facts/deadlines.v b/restructuring/analysis/basic_facts/deadlines.v
index 7fe7696ffa8c84970516fa9c471c72deb7daa785..40b86d777565533bc079b30838fc2d08add8a6b2 100644
--- a/restructuring/analysis/basic_facts/deadlines.v
+++ b/restructuring/analysis/basic_facts/deadlines.v
@@ -5,9 +5,9 @@ From rt.restructuring.analysis.basic_facts Require Export service completion.
model w.r.t. deadlines. *)
Section DeadlineFacts.
- (* Consider any given type of jobs with costs and deadlines... *)
+ (** Consider any given type of jobs with costs and deadlines... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
- (* ... any given type of processor states. *)
+ (** ... any given type of processor states. *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
@@ -15,16 +15,16 @@ Section DeadlineFacts.
always receive service. *)
Section IdealProgressSchedules.
- (* Consider a given reference schedule... *)
+ (** Consider a given reference schedule... *)
Variable sched: schedule PState.
- (* ...in which complete jobs don't execute... *)
+ (** ...in which complete jobs don't execute... *)
Hypothesis H_completed_jobs: completed_jobs_dont_execute sched.
- (* ...and scheduled jobs always receive service. *)
+ (** ...and scheduled jobs always receive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* We observe that, if a job is known to meet its deadline, then
+ (** We observe that, if a job is known to meet its deadline, then
its deadline must be later than any point at which it is
scheduled. That is, if a job that meets its deadline is
scheduled at time t, we may conclude that its deadline is at a
@@ -52,10 +52,10 @@ Section DeadlineFacts.
both schedules or none. *)
Section EqualProgress.
- (* Consider any two schedules [sched] and [sched']. *)
+ (** Consider any two schedules [sched] and [sched']. *)
Variable sched sched': schedule PState.
- (* We observe that, if the service is invariant at the time of a
+ (** We observe that, if the service is invariant at the time of a
job's absolute deadline, and if the job meets its deadline in one of the schedules,
then it meets its deadline also in the other schedule. *)
Lemma service_invariant_implies_deadline_met:
diff --git a/restructuring/analysis/basic_facts/ideal_schedule.v b/restructuring/analysis/basic_facts/ideal_schedule.v
index 993ed6a6002010a6e7475d6e8640c9bdbcf1fe98..f74ecf24627d61013ea5db0a8edf704004c8d17b 100644
--- a/restructuring/analysis/basic_facts/ideal_schedule.v
+++ b/restructuring/analysis/basic_facts/ideal_schedule.v
@@ -1,13 +1,13 @@
From rt.restructuring.model.processor Require Import ideal platform_properties.
-(* Note: we do not re-export the basic definitions to avoid littering the global
+(** 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 estlish the classes to which an ideal schedule belongs. *)
Section ScheduleClass.
- (* Consider any job type and the ideal processor model. *)
+ (** Consider any job type and the ideal processor model. *)
Context {Job: JobType}.
- (* We note that the ideal processor model is indeed a uniprocessor
+ (** We note that the ideal processor model is indeed a uniprocessor
model. *)
Lemma ideal_proc_model_is_a_uniprocessor_model:
@uniprocessor_model _ (processor_state Job) _.
@@ -16,7 +16,7 @@ Section ScheduleClass.
by rewrite /scheduled_at=> /eqP-> /eqP[->].
Qed.
- (* We observe that the ideal processor model falls into the category
+ (** We observe that the ideal processor model falls into the category
of ideal-progress models, i.e., a scheduled job always receives
service. *)
Lemma ideal_proc_model_ensures_ideal_progress:
@@ -26,7 +26,7 @@ Section ScheduleClass.
by rewrite /service_in /pstate_instance SOME.
Qed.
- (* The ideal processor model is a unit-service model. *)
+ (** The ideal processor model is a unit-service model. *)
Lemma ideal_proc_model_provides_unit_service:
@unit_service_proc_model _ (processor_state Job) _.
Proof.
diff --git a/restructuring/analysis/basic_facts/sequential.v b/restructuring/analysis/basic_facts/sequential.v
index 1750f84635a2893f1594ced15265f46724869797..3ea1d588879cf9be4bf191ccb7f94648e7dc49cd 100644
--- a/restructuring/analysis/basic_facts/sequential.v
+++ b/restructuring/analysis/basic_facts/sequential.v
@@ -1,27 +1,27 @@
From rt.restructuring.model Require Export schedule.sequential.
Section ExecutionOrder.
- (* Consider any type of job associated with any type of tasks... *)
+ (** Consider any type of job associated with any type of tasks... *)
Context {Job: JobType}.
Context {Task: TaskType}.
Context `{JobTask Job Task}.
- (* ... with arrival times and costs ... *)
+ (** ... with arrival times and costs ... *)
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* ... and any kind of processor state model. *)
+ (** ... and any kind of processor state model. *)
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* Assume a schedule ... *)
+ (** Assume a schedule ... *)
Variable sched: schedule PState.
- (* in which the sequential jobs hypothesis holds. *)
+ (** in which the sequential jobs hypothesis holds. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
- (* A simple corollary of this hypothesis is that the scheduler
+ (** A simple corollary of this hypothesis is that the scheduler
executes a job with the earliest arrival time. *)
Corollary scheduler_executes_job_with_earliest_arrival:
forall j1 j2 t,
diff --git a/restructuring/analysis/basic_facts/service.v b/restructuring/analysis/basic_facts/service.v
index 9c01810c7fe34e247a1cbed69b0974b117cecf6e..533c860f1f1a445d0be7f1fbad62959fbc5ddfca 100644
--- a/restructuring/analysis/basic_facts/service.v
+++ b/restructuring/analysis/basic_facts/service.v
@@ -10,21 +10,21 @@ Section Composition.
(** To begin with, we provide some simple but handy rewriting rules for
[service] and [service_during]. *)
- (* Consider any job type and any processor state. *)
+ (** Consider any job type and any processor state. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* For any given schedule... *)
+ (** For any given schedule... *)
Variable sched: schedule PState.
- (* ...and any given job... *)
+ (** ...and any given job... *)
Variable j: Job.
- (* ...we establish a number of useful rewriting rules that decompose
+ (** ...we establish a number of useful rewriting rules that decompose
the service received during an interval into smaller intervals. *)
- (* As a trivial base case, no job receives any service during an empty
+ (** As a trivial base case, no job receives any service during an empty
interval. *)
Lemma service_during_geq:
forall t1 t2,
@@ -34,14 +34,14 @@ Section Composition.
rewrite /service_during big_geq //.
Qed.
- (* Equally trivially, no job has received service prior to time zero. *)
+ (** Equally trivially, no job has received service prior to time zero. *)
Corollary service0:
service sched j 0 = 0.
Proof.
rewrite /service service_during_geq //.
Qed.
- (* Trivially, an interval consiting of one time unit is equivalent to
+ (** Trivially, an interval consiting of one time unit is equivalent to
service_at. *)
Lemma service_during_instant:
forall t,
@@ -51,7 +51,7 @@ Section Composition.
by rewrite /service_during big_nat_recr ?big_geq //.
Qed.
- (* Next, we observe that we can look at the service received during an
+ (** Next, we observe that we can look at the service received during an
interval [t1, t3) as the sum of the service during [t1, t2) and [t2, t3)
for any t2 \in [t1, t3]. (The "_cat" suffix denotes the concatenation of
the two intervals.) *)
@@ -65,7 +65,7 @@ Section Composition.
by rewrite /service_during -big_cat_nat /=.
Qed.
- (* Since [service] is just a special case of [service_during], the same holds
+ (** Since [service] is just a special case of [service_during], the same holds
for [service]. *)
Lemma service_cat:
forall t1 t2,
@@ -77,7 +77,7 @@ Section Composition.
rewrite /service service_during_cat //.
Qed.
- (* As a special case, we observe that the service during an interval can be
+ (** As a special case, we observe that the service during an interval can be
decomposed into the first instant and the rest of the interval. *)
Lemma service_during_first_plus_later:
forall t1 t2,
@@ -91,7 +91,7 @@ Section Composition.
by rewrite -service_during_instant //.
Qed.
- (* Symmetrically, we have the same for the end of the interval. *)
+ (** Symmetrically, we have the same for the end of the interval. *)
Lemma service_during_last_plus_before:
forall t1 t2,
t1 <= t2 ->
@@ -103,7 +103,7 @@ Section Composition.
rewrite service_during_instant //.
Qed.
- (* And hence also for [service]. *)
+ (** And hence also for [service]. *)
Corollary service_last_plus_before:
forall t,
(service sched j t) + (service_at sched j t)
@@ -113,7 +113,7 @@ Section Composition.
rewrite /service. rewrite -service_during_last_plus_before //.
Qed.
- (* Finally, we deconstruct the service received during an interval [t1, t3)
+ (** Finally, we deconstruct the service received during an interval [t1, t3)
into the service at a midpoint t2 and the service in the intervals before
and after. *)
Lemma service_split_at_point:
@@ -134,28 +134,28 @@ Section UnitService.
(** As a common special case, we establish facts about schedules in which a
job receives either 1 or 0 service units at all times. *)
- (* Consider any job type and any processor state. *)
+ (** Consider any job type and any processor state. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* Let's consider a unit-service model... *)
+ (** Let's consider a unit-service model... *)
Hypothesis H_unit_service: unit_service_proc_model.
- (* ...and a given schedule. *)
+ (** ...and a given schedule. *)
Variable sched: schedule PState.
- (* Let j be any job that is to be scheduled. *)
+ (** Let j be any job that is to be scheduled. *)
Variable j: Job.
- (* First, we prove that the instantaneous service cannot be greater than 1, ... *)
+ (** First, we prove that the instantaneous service cannot be greater than 1, ... *)
Lemma service_at_most_one:
forall t, service_at sched j t <= 1.
Proof.
by move=> t; rewrite /service_at.
Qed.
- (* ...which implies that the cumulative service received by job j in any
+ (** ...which implies that the cumulative service received by job j in any
interval of length delta is at most delta. *)
Lemma cumulative_service_le_delta:
forall t delta,
@@ -169,7 +169,7 @@ Section UnitService.
Section ServiceIsAStepFunction.
- (* We show that the service received by any job j is a step function. *)
+ (** We show that the service received by any job j is a step function. *)
Lemma service_is_a_step_function:
is_step_function (service sched j).
Proof.
@@ -178,15 +178,15 @@ Section UnitService.
apply service_at_most_one.
Qed.
- (* Next, consider any time t... *)
+ (** Next, consider any time t... *)
Variable t: instant.
- (* ...and let s0 be any value less than the service received
+ (** ...and let s0 be any value less than the service received
by job j by time t. *)
Variable s0: duration.
Hypothesis H_less_than_s: s0 < service sched j t.
- (* Then, we show that there exists an earlier time t0 where job j had s0
+ (** Then, we show that there exists an earlier time t0 where job j had s0
units of service. *)
Corollary exists_intermediate_service:
exists t0,
@@ -207,18 +207,18 @@ End UnitService.
Section Monotonicity.
(** We establish a basic fact about the monotonicity of service. *)
- (* Consider any job type and any processor model. *)
+ (** Consider any job type and any processor model. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* Consider any given schedule... *)
+ (** Consider any given schedule... *)
Variable sched: schedule PState.
- (* ...and a given job that is to be scheduled. *)
+ (** ...and a given job that is to be scheduled. *)
Variable j: Job.
- (* We observe that the amount of service received is monotonic by definition. *)
+ (** We observe that the amount of service received is monotonic by definition. *)
Lemma service_monotonic:
forall t1 t2,
t1 <= t2 ->
@@ -231,18 +231,18 @@ Section Monotonicity.
End Monotonicity.
Section RelationToScheduled.
- (* Consider any job type and any processor model. *)
+ (** Consider any job type and any processor model. *)
Context {Job: JobType}.
Context {PState: Type}.
Context `{ProcessorState Job PState}.
- (* Consider any given schedule... *)
+ (** Consider any given schedule... *)
Variable sched: schedule PState.
- (* ...and a given job that is to be scheduled. *)
+ (** ...and a given job that is to be scheduled. *)
Variable j: Job.
- (* We observe that a job that isn't scheduled cannot possibly receive service. *)
+ (** We observe that a job that isn't scheduled cannot possibly receive service. *)
Lemma not_scheduled_implies_no_service:
forall t,
~~ scheduled_at sched j t -> service_at sched j t = 0.
@@ -252,7 +252,7 @@ Section RelationToScheduled.
rewrite service_implies_scheduled //.
Qed.
- (* Conversely, if a job receives service, then it must be scheduled. *)
+ (** Conversely, if a job receives service, then it must be scheduled. *)
Lemma service_at_implies_scheduled_at:
forall t,
service_at sched j t > 0 -> scheduled_at sched j t.
@@ -262,7 +262,7 @@ Section RelationToScheduled.
rewrite not_scheduled_implies_no_service // negbT //.
Qed.
- (* Thus, if the cumulative amount of service changes, then it must be
+ (** Thus, if the cumulative amount of service changes, then it must be
scheduled, too. *)
Lemma service_delta_implies_scheduled:
forall t,
@@ -273,7 +273,7 @@ Section RelationToScheduled.
apply: service_at_implies_scheduled_at.
Qed.
- (* We observe that a job receives cumulative service during some interval iff
+ (** We observe that a job receives cumulative service during some interval iff
it receives services at some specific time in the interval. *)
Lemma service_during_service_at:
forall t1 t2,
@@ -310,7 +310,7 @@ Section RelationToScheduled.
}
Qed.
- (* Thus, any job that receives some service during an interval must be
+ (** Thus, any job that receives some service during an interval must be
scheduled at some point during the interval... *)
Corollary cumulative_service_implies_scheduled:
forall t1 t2,
@@ -326,7 +326,7 @@ Section RelationToScheduled.
by apply: service_at_implies_scheduled_at.
Qed.
- (* ...which implies that any job with positive cumulative service must have
+ (** ...which implies that any job with positive cumulative service must have
been scheduled at some point. *)
Corollary positive_service_implies_scheduled_before:
forall t,
@@ -339,13 +339,13 @@ Section RelationToScheduled.
Qed.
Section GuaranteedService.
- (* If we can assume that a scheduled job always receives service, we can
+ (** If we can assume that a scheduled job always receives service, we can
further prove the converse. *)
- (* Assume j always receives some positive service. *)
+ (** Assume j always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* In other words, not being scheduled is equivalent to receiving zero
+ (** In other words, not being scheduled is equivalent to receiving zero
service. *)
Lemma no_service_not_scheduled:
forall t,
@@ -358,7 +358,7 @@ Section RelationToScheduled.
by rewrite -eqn0Ngt; apply /eqP => //.
Qed.
- (* Then, if a job does not receive any service during an interval, it
+ (** Then, if a job does not receive any service during an interval, it
is not scheduled. *)
Lemma no_service_during_implies_not_scheduled:
forall t1 t2,
@@ -373,7 +373,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 receivees
positive cumulative service during the interval... *)
Lemma scheduled_implies_cumulative_service:
forall t1 t2,
@@ -389,7 +389,7 @@ Section RelationToScheduled.
by apply (H_scheduled_implies_serviced j (sched t')).
Qed.
- (* ...which again applies to total service, too. *)
+ (** ...which again applies to total service, too. *)
Corollary scheduled_implies_nonzero_service:
forall t,
(exists t',
@@ -405,16 +405,16 @@ Section RelationToScheduled.
End GuaranteedService.
Section AfterArrival.
- (* Futhermore, if we know that jobs are not released early, then we can
+ (** Futhermore, 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}.
- (* Assume that jobs must arrive to execute. *)
+ (** Assume that jobs must arrive to execute. *)
Hypothesis H_jobs_must_arrive:
jobs_must_arrive_to_execute sched.
- (* We prove that any job with positive cumulative service at time [t] must
+ (** We prove that any job with positive cumulative service at time [t] must
have been scheduled some time since its arrival and before time [t]. *)
Lemma positive_service_implies_scheduled_since_arrival:
forall t,
@@ -438,7 +438,7 @@ Section RelationToScheduled.
rewrite /has_arrived -ltnNge //.
Qed.
- (* We show that job j does not receive service at any time t prior to its
+ (** We show that job j does not receive service at any time t prior to its
arrival. *)
Lemma service_before_job_arrival_zero:
forall t,
@@ -449,7 +449,7 @@ Section RelationToScheduled.
rewrite not_scheduled_implies_no_service // not_scheduled_before_arrival //.
Qed.
- (* Note that the same property applies to the cumulative service. *)
+ (** Note that the same property applies to the cumulative service. *)
Lemma cumulative_service_before_job_arrival_zero :
forall t1 t2 : instant,
t2 <= job_arrival j ->
@@ -465,7 +465,7 @@ Section RelationToScheduled.
by apply leq_trans with (n := t2); auto.
Qed.
- (* Hence, one can ignore the service received by a job before its arrival
+ (** Hence, one can ignore the service received by a job before its arrival
time... *)
Lemma ignore_service_before_arrival:
forall t1 t2,
@@ -479,7 +479,7 @@ Section RelationToScheduled.
by apply/andP; split; exact.
Qed.
- (* ... which we can also state in terms of cumulative service. *)
+ (** ... which we can also state in terms of cumulative service. *)
Corollary no_service_before_arrival:
forall t,
t <= job_arrival j -> service sched j t = 0.
@@ -494,16 +494,16 @@ Section RelationToScheduled.
(** In this section, we prove some lemmas about time instants with same
service. *)
- (* Consider any time instants t1 and t2... *)
+ (** Consider any time instants t1 and t2... *)
Variable t1 t2: instant.
- (* ...where t1 is no later than t2... *)
+ (** ...where t1 is no later than t2... *)
Hypothesis H_t1_le_t2: t1 <= t2.
- (* ...and where job j has received the same amount of service. *)
+ (** ...and where job j has received the same amount of service. *)
Hypothesis H_same_service: service sched j t1 = service sched j t2.
- (* First, we observe that this means that the job receives no service
+ (** First, we observe that this means that the job receives no service
during [t1, t2)... *)
Lemma constant_service_implies_no_service_during:
service_during sched j t1 t2 = 0.
@@ -513,7 +513,7 @@ Section RelationToScheduled.
by rewrite eqn_add2l => /eqP //.
Qed.
- (* ...which of course implies that it does not receive service at any
+ (** ...which of course implies that it does not receive service at any
point, either. *)
Lemma constant_service_implies_not_scheduled:
forall t,
@@ -525,7 +525,7 @@ Section RelationToScheduled.
apply IS_ZERO. apply /andP; split => //.
Qed.
- (* We show that job j receives service at some point t < t1 iff j receives
+ (** We show that job j receives service at some point t < t1 iff j receives
service at some point t' < t2. *)
Lemma same_service_implies_serviced_at_earlier_times:
[exists t: 'I_t1, service_at sched j t > 0] =
@@ -548,13 +548,13 @@ Section RelationToScheduled.
}
Qed.
- (* Then, under the assumption that scheduled jobs receives service,
+ (** Then, under the assumption that scheduled jobs receives service,
we can translate this into a claim about scheduled_at. *)
- (* Assume j always receives some positive service. *)
+ (** Assume j always receives some positive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* We show that job j is scheduled at some point t < t1 iff j is scheduled
+ (** We show that job j is scheduled at some point t < t1 iff j is scheduled
at some point t' < t2. *)
Lemma same_service_implies_scheduled_at_earlier_times:
[exists t: 'I_t1, scheduled_at sched j t] =
diff --git a/restructuring/analysis/basic_facts/service_of_jobs.v b/restructuring/analysis/basic_facts/service_of_jobs.v
index 4e84ffafe29b327ba3dd3f90f3aae7cb8fbfd9f4..dea898eb415295c56d2df1f2dbb933f538db30da 100644
--- a/restructuring/analysis/basic_facts/service_of_jobs.v
+++ b/restructuring/analysis/basic_facts/service_of_jobs.v
@@ -10,52 +10,52 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** * Lemmas about Service Received by Sets of Jobs *)
(** In this file, we establish basic facts about the service received by _sets_ of jobs. *)
-(* To begin with, we provide some basic properties of service
+(** To begin with, we provide some basic properties of service
of a set of jobs in case of a generic scheduling model. *)
Section GenericModelLemmas.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Consider any kind of processor state model, ... *)
+ (** Consider any kind of processor state model, ... *)
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (* ... any job arrival sequence with consistent arrivals, .... *)
+ (** ... any job arrival sequence with consistent arrivals, .... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
- (* ... and any schedule of this arrival sequence ...*)
+ (** ... and any schedule of this arrival sequence ...*)
Variable sched : schedule PState.
- (* ... where jobs do not execute before their arrival or after completion. *)
+ (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
- (* Let P be any predicate over jobs. *)
+ (** Let P be any predicate over jobs. *)
Variable P : Job -> bool.
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let arrivals_between := arrivals_between arr_seq.
- (* In this section, we prove that the service received by any set of jobs
+ (** In this section, we prove that the service received by any set of jobs
is upper-bounded by the corresponding workload. *)
Section ServiceBoundedByWorkload.
- (* Let jobs denote any (finite) set of jobs. *)
+ (** 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 moodel. I.e.,
no job ever receives more than one unit of service at any time. *)
Hypothesis H_unit_service : unit_service_proc_model.
- (* Then, we prove that the service received by those jobs is no larger than their workload. *)
+ (** Then, we prove that the service received by those jobs is no larger than their workload. *)
Lemma service_of_jobs_le_workload:
forall t1 t2,
service_of_jobs sched P jobs t1 t2 <= workload_of_jobs P jobs.
@@ -67,11 +67,11 @@ Section GenericModelLemmas.
End ServiceBoundedByWorkload.
- (* In this section we prove a few facts about splitting
+ (** In this section we prove a few facts about splitting
the total service of a set of jobs. *)
Section ServiceCat.
- (* We show that the total service of jobs released in a time interval [t1,t2)
+ (** We show that the total service of jobs released in a time interval [t1,t2)
during [t1,t2) is equal to the sum of:
(1) the total service of jobs released in time interval [t1, t) during time [t1, t)
(2) the total service of jobs released in time interval [t1, t) during time [t, t2)
@@ -101,7 +101,7 @@ Section GenericModelLemmas.
by move: ARR => /andP [N1 N2]; apply leq_trans with t.
Qed.
- (* We show that the total service of jobs released in a time interval [t1,t2)
+ (** We show that the total service of jobs released in a time interval [t1,t2)
during [t,t2) is equal to the sum of:
(1) the total service of jobs released in a time interval [t1,t) during [t,t2)
and (2) the total service of jobs released in a time interval [t,t2) during [t,t2). *)
@@ -122,48 +122,48 @@ Section GenericModelLemmas.
End GenericModelLemmas.
-(* In this section, we prove some properties about service
+(** In this section, we prove some properties about service
of sets of jobs for ideal uniprocessor model. *)
Section IdealModelLemmas.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Consider any arrival sequence with consistent arrivals. *)
+ (** 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 uniprocessor schedule of this arrival sequence ... *)
Variable sched : schedule (ideal.processor_state Job).
- (* ... where jobs do not execute before their arrival or after completion. *)
+ (** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
- (* Let P be any predicate over jobs. *)
+ (** Let P be any predicate over jobs. *)
Variable P : Job -> bool.
- (* Let's define some local names for clarity. *)
+ (** Let's define some local names for clarity. *)
Let arrivals_between := arrivals_between arr_seq.
Let completed_by := completed_by sched.
- (* In this section, we prove that the service received by any set of jobs
+ (** In this section, we prove that the service received by any set of jobs
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.
@@ -200,7 +200,7 @@ Section IdealModelLemmas.
}
Qed.
- (* Then, we prove that the service received by those jobs is no larger than their workload. *)
+ (** Then, we prove that the service received by those jobs is no larger than their workload. *)
Corollary service_of_jobs_le_length_of_interval:
forall (t : instant) (Δ : duration),
service_of_jobs sched P jobs t (t + Δ) <= Δ.
@@ -217,26 +217,26 @@ Section IdealModelLemmas.
End ServiceOfJobsIsBoundedByLength.
- (* In this section, we introduce a connection between the cumulative
+ (** In this section, we introduce a connection between the cumulative
service, cumulative workload, and completion of jobs. *)
Section WorkloadServiceAndCompletion.
- (* Consider an arbitrary time interval [t1, t2). *)
+ (** Consider an arbitrary time interval [t1, t2). *)
Variables t1 t2 : instant.
- (* Let jobs be a set of all jobs arrived during [t1, t2). *)
+ (** Let jobs be a set of all jobs arrived during [t1, t2). *)
Let jobs := arrivals_between t1 t2.
- (* Next, we consider some time instant [t_compl]. *)
+ (** Next, we consider some time instant [t_compl]. *)
Variable t_compl : instant.
- (* And state the proposition that all jobs are completed by time
+ (** And state the proposition that all jobs are completed by time
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
+ (** 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. *)
Lemma workload_eq_service_impl_all_jobs_have_completed:
workload_of_jobs P jobs =
@@ -267,7 +267,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 ->
@@ -307,7 +307,7 @@ Section IdealModelLemmas.
}
Qed.
- (* Using the lemmas above, we prove equivalence. *)
+ (** Using the lemmas above, we prove equivalence. *)
Corollary all_jobs_have_completed_equiv_workload_eq_service:
all_jobs_completed_by t_compl <->
workload_of_jobs P jobs =
diff --git a/restructuring/analysis/basic_facts/task_arrivals.v b/restructuring/analysis/basic_facts/task_arrivals.v
index 381fc6aa08a692ed5869faf3297cbd5800f10102..23478e2f02feae0ffe8f4054eea18cdebe133c1d 100644
--- a/restructuring/analysis/basic_facts/task_arrivals.v
+++ b/restructuring/analysis/basic_facts/task_arrivals.v
@@ -1,20 +1,20 @@
From rt.restructuring.model.aggregate Require Export task_arrivals.
-(* In this file we provide basic properties related to tasks on arrival sequences. *)
+(** In this file we provide basic properties related to tasks on arrival sequences. *)
Section TaskArrivals.
- (* Consider any type of job associated with any type of tasks. *)
+ (** Consider any type of job associated with any type of tasks. *)
Context {Job : JobType}.
Context {Task : TaskType}.
Context `{JobTask Job Task}.
- (* Consider any job arrival sequence. *)
+ (** 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. *)
+ (** We show that the number of arrivals of task can be split into disjoint intervals. *)
Lemma num_arrivals_of_task_cat:
forall t t1 t2,
t1 <= t <= t2 ->
diff --git a/restructuring/analysis/edf/optimality.v b/restructuring/analysis/edf/optimality.v
index 3e08e8d63d1be211e8b11a9100a96d803daeeb88..bed07c60cef893dd5b2236031899c7159daac751 100644
--- a/restructuring/analysis/edf/optimality.v
+++ b/restructuring/analysis/edf/optimality.v
@@ -7,14 +7,14 @@ From rt.restructuring.analysis Require Import schedulability transform.facts.edf
schedule in which all deadlines are met. *)
Section Optimality.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ... and any valid job arrival sequence. *)
+ (** ... and any valid job arrival sequence. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
- (* We observe that EDF is optimal in the sense that, if there exists
+ (** We observe that EDF is optimal in the sense that, if there exists
any schedule in which all jobs of arr_seq meet their deadline,
then there also exists an EDF schedule in which all deadlines are
met. *)
@@ -44,16 +44,16 @@ End Optimality.
that avoids a dependency on a given arrival sequence. *)
Section WeakOptimality.
- (* For any given type of jobs,... *)
+ (** For any given type of jobs,... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...if we have a well-behaved schedule in which no deadlines are missed,... *)
+ (** ...if we have a well-behaved schedule in which no deadlines are missed,... *)
Variable any_sched: schedule (ideal.processor_state Job).
Hypothesis H_must_arrive: jobs_must_arrive_to_execute any_sched.
Hypothesis H_completed_dont_execute: completed_jobs_dont_execute any_sched.
Hypothesis H_all_deadlines_met: all_deadlines_met any_sched.
- (* ...then there also exists a corresponding EDF schedule in which
+ (** ...then there also exists a corresponding EDF schedule in which
no deadlines are missed (and in which exactly the same set of
jobs is scheduled, as ensured by the last clause). *)
Theorem weak_EDF_optimality:
diff --git a/restructuring/analysis/schedulability.v b/restructuring/analysis/schedulability.v
index 0e332a9e319ec3e48a7e28df59547da3d81a65e7..c04eef66ddbbea198c2365342e0b2d0377922ad8 100644
--- a/restructuring/analysis/schedulability.v
+++ b/restructuring/analysis/schedulability.v
@@ -13,19 +13,19 @@ Section Task.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (* Consider any job arrival sequence... *)
+ (** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
- (* ...and any schedule of these jobs. *)
+ (** ...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
+ (** ... iff any job j of tsk in this arrival sequence has
completed by (job_arrival j + R). *)
Definition task_response_time_bound :=
forall j,
@@ -33,7 +33,7 @@ Section Task.
job_task j = tsk ->
job_response_time_bound sched j R.
- (* We say that a task is schedulable if all its jobs meet their deadline *)
+ (** We say that a task is schedulable if all its jobs meet their deadline *)
Definition schedulable_task :=
forall j,
arrives_in arr_seq j ->
@@ -53,19 +53,19 @@ Section TaskSet.
Variable ts : {set Task}.
- (* Consider any job arrival sequence... *)
+ (** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
- (* ...and any schedule of these jobs. *)
+ (** ...and any schedule of these jobs. *)
Variable sched: schedule PState.
- (* We say that a task set is schedulable if all its tasks are schedulable *)
+ (** We say that a task set is schedulable if all its tasks are schedulable *)
Definition schedulable_taskset :=
forall tsk, tsk \in ts -> schedulable_task arr_seq sched tsk.
End TaskSet.
Section Schedulability.
- (* We can infer schedulability from a response-time bound of a task. *)
+ (** We can infer schedulability from a response-time bound of a task. *)
Context {Task : TaskType}.
Context {Job: JobType}.
@@ -76,25 +76,25 @@ Section Schedulability.
Context {PState : Type}.
Context `{ProcessorState Job PState}.
- (* Consider any job arrival sequence... *)
+ (** Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
- (* ...and any schedule of these jobs. *)
+ (** ...and any schedule of these jobs. *)
Variable sched: schedule PState.
- (* Assume that jobs don't execute after completion. *)
+ (** 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.
@@ -115,14 +115,14 @@ End Schedulability.
arrival sequence. *)
Section AllDeadlinesMet.
- (* Consider any given type of jobs... *)
+ (** Consider any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ... any given type of processor states. *)
+ (** ... any given type of processor states. *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* We say that all deadlines are met if every job scheduled at some
+ (** We say that all deadlines are met if every job scheduled at some
point in the schedule meets its deadline. Note that this is a
relatively weak definition since an "empty" schedule that is idle
at all times trivially satisfies it (since the definition does
@@ -132,15 +132,15 @@ Section AllDeadlinesMet.
scheduled_at sched j t ->
job_meets_deadline sched j.
- (* To augment the preceding definition, we also define an alternate
+ (** To augment the preceding definition, we also define an alternate
notion of "all deadlines met" based on all jobs included in a
given arrival sequence. *)
Section DeadlinesOfArrivals.
- (* Given an arbitrary job arrival sequence ... *)
+ (** Given an arbitrary job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
- (* ... we say that all arrivals meet their deadline if every job
+ (** ... we say that all arrivals meet their deadline if every job
that arrives at some point in time meets its deadline. Note
that this definition does not preclude the existence of jobs in
a schedule that miss their deadline (e.g., if they stem from
@@ -152,7 +152,7 @@ Section AllDeadlinesMet.
End DeadlinesOfArrivals.
- (* We observe that the latter definition, assuming a schedule in
+ (** We observe that the latter definition, assuming a schedule in
which all jobs come from the arrival sequence, implies the former
definition. *)
Lemma all_deadlines_met_in_valid_schedule:
diff --git a/restructuring/analysis/task_schedule.v b/restructuring/analysis/task_schedule.v
index dd846c6e3a49d1ecef0c5dac7aec462fd1296c7b..d0d427d3de8bf215e97a131bad51bc976ed2064b 100644
--- a/restructuring/analysis/task_schedule.v
+++ b/restructuring/analysis/task_schedule.v
@@ -4,7 +4,7 @@ From rt.restructuring.analysis.basic_facts Require Import 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
+(** 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
and the notion can be further generalized to an arbitrary model. *)
@@ -12,39 +12,39 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** In this section we define properties of schedule of a task *)
Section ScheduleOfTask.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Let sched be any ideal uniprocessor schedule. *)
+ (** Let sched be any ideal uniprocessor 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
else false.
- (* ...which also corresponds to the instantaneous service it receives. *)
+ (** ...which also corresponds to the instantaneous service it receives. *)
Definition task_service_at (t : instant) := task_scheduled_at t.
- (* Based on the notion of instantaneous service, we define the
+ (** Based on the notion of instantaneous service, we define the
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/transform/edf_trans.v b/restructuring/analysis/transform/edf_trans.v
index 792a87409984dd8da2c2f0dec68fe5a3f472cb18..78853374502806ddae68bc933affc9afdf817e17 100644
--- a/restructuring/analysis/transform/edf_trans.v
+++ b/restructuring/analysis/transform/edf_trans.v
@@ -5,14 +5,14 @@ From rt.util Require Export search_arg.
operation at the core of the EDF optimality proof. *)
Section EDFTransformation.
- (* Consider any given type of jobs... *)
+ (** Consider any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ... and ideal uniprocessor schedules. *)
+ (** ... and ideal uniprocessor schedules. *)
Let PState := ideal.processor_state Job.
Let SchedType := schedule (PState).
- (* We say that a state s1 "has an earlier or equal deadline" than a
+ (** We say that a state s1 "has an earlier or equal deadline" than a
state s2 if the job scheduled in state s1 has has an earlier or
equal deadline than the job scheduled in state s2. This function
is never used on idle states, so the default values are
@@ -20,7 +20,7 @@ Section EDFTransformation.
Definition earlier_deadline (s1 s2: PState) :=
(oapp job_deadline 0 s1) <= (oapp job_deadline 0 s2).
- (* We say that a state is relevant (for the purpose of the
+ (** We say that a state is relevant (for the purpose of the
transformation) if it is not idle and if the job scheduled in it
has arrived prior to some given reference time. *)
Definition relevant_pstate (reference_time: instant) (s: PState) :=
@@ -29,7 +29,7 @@ Section EDFTransformation.
| Some j' => job_arrival j' <= reference_time
end.
- (* Next, we define a central element of the "EDF-ification"
+ (** Next, we define a central element of the "EDF-ification"
procedure: given a job scheduled at a time t1, find a later time
t2 before the job's deadlineat which a job with an
earlier-or-equal deadline is scheduled. In other words, find a
@@ -40,24 +40,24 @@ Section EDFTransformation.
then t
else 0.
- (* The point-wise EDF-ification procedure: given a schedule and a
+ (** The point-wise EDF-ification procedure: given a schedule and a
time t1, ensure that the schedule satisfies [EDF_at] at time
t1. *)
Definition make_edf_at (sched: SchedType) (t1: instant): SchedType :=
match sched t1 with
- | None => sched (* leave idle instants alone *)
+ | None => sched (** leave idle instants alone *)
| Some j =>
let
t2 := find_swap_candidate sched t1 j
in swapped sched t1 t2
end.
- (* To transform a finite prefix of a given reference schedule, apply
+ (** To transform a finite prefix of a given reference schedule, apply
[make_edf_at] to every point up to the given finite horizon. *)
Definition edf_transform_prefix (sched: SchedType) (horizon: instant): SchedType :=
prefix_map sched make_edf_at horizon.
- (* Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
+ (** Finally, a full EDF schedule (i.e., one that satisfies [EDF_at]
at any time) is obtained by first computing an EDF prefix up to
and including the requested time t, and by then looking at the
last point of the prefix. *)
diff --git a/restructuring/analysis/transform/facts/edf_opt.v b/restructuring/analysis/transform/facts/edf_opt.v
index c298caee9f8d08c62fe69fb7cc04e9312299697f..528467d907e59c947e34a741094b1b4029c493a2 100644
--- a/restructuring/analysis/transform/facts/edf_opt.v
+++ b/restructuring/analysis/transform/facts/edf_opt.v
@@ -11,39 +11,39 @@ From rt.util Require Import tactics nat.
the proofs of individual properties of the obtained EDF
schedule. *)
-(* Throughout this file, we assume ideal uniprocessor schedules. *)
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
From rt.restructuring.model.processor Require Export ideal.
-(* Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
From rt.restructuring.model.readiness Require Export basic.
(** We start by analyzing the helper function [find_swap_candidate],
which is a problem-specific wrapper around [search_arg]. *)
Section FindSwapCandidateFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...consider an ideal uniprocessor schedule... *)
+ (** ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ...that is well-behaved (i.e., in which jobs execute only after
+ (** ...that is well-behaved (i.e., in which jobs execute only after
having arrived and only if they are not yet complete). *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (* Suppose we are given a job [j1]... *)
+ (** Suppose we are given a job [j1]... *)
Variable j1: Job.
- (* ...and a point in time [t1]... *)
+ (** ...and a point in time [t1]... *)
Variable t1: instant.
- (* ...at which [j1] is scheduled... *)
+ (** ...at which [j1] is scheduled... *)
Hypothesis H_not_idle: scheduled_at sched j1 t1.
- (* ...and that is before its deadline. *)
+ (** ...and that is before its deadline. *)
Hypothesis H_deadline_not_missed: t1 < job_deadline j1.
- (* First, we observe that under these assumptions the processor
+ (** First, we observe that under these assumptions the processor
state at time [t1] is "relevant" according to the notion of
relevance underlying the EDF transformation, namely
[relevant_pstate]. *)
@@ -55,7 +55,7 @@ Section FindSwapCandidateFacts.
by apply SCHED_ARR.
Qed.
- (* Since [t1] is relevant, we conclude that a search for a relevant
+ (** Since [t1] is relevant, we conclude that a search for a relevant
state succeeds (if nothing else, it finds [t1]). *)
Lemma fsc_search_successful:
exists t, search_arg sched (relevant_pstate t1) earlier_deadline t1 (job_deadline j1) = Some t.
@@ -66,7 +66,7 @@ Section FindSwapCandidateFacts.
- by apply t1_relevant.
Qed.
- (* For rewriting purposes, we observe that the [search_arg]
+ (** For rewriting purposes, we observe that the [search_arg]
operation within [find_swap_candidate] yields the final result of
[find_swap_candidate]. *)
Corollary fsc_search_result:
@@ -76,7 +76,7 @@ Section FindSwapCandidateFacts.
by rewrite /find_swap_candidate FOUND.
Qed.
- (* There is a job that is scheduled at the time that
+ (** There is a job that is scheduled at the time that
[find_swap_candidate] returns, and that job arrives no later than
at time [t1]. *)
Lemma fsc_not_idle:
@@ -93,7 +93,7 @@ Section FindSwapCandidateFacts.
by apply /eqP.
Qed.
- (* Since we are considering a uniprocessor model, only one job is
+ (** Since we are considering a uniprocessor model, only one job is
scheduled at a time. Hence once we know that a job is scheduled
at the time that [find_swap_candidate] returns, we can conclude
that it arrives not later than at time t1. *)
@@ -107,19 +107,19 @@ Section FindSwapCandidateFacts.
by rewrite -(ideal_proc_model_is_a_uniprocessor_model _ _ _ _ SCHED_j' SCHED_j2).
Qed.
- (* We observe that [find_swap_candidate] returns a value within a
+ (** We observe that [find_swap_candidate] returns a value within a
known finite interval. *)
Lemma fsc_range:
t1 <= find_swap_candidate sched t1 j1 < job_deadline j1.
Proof. move: fsc_search_result. by apply search_arg_in_range. Qed.
- (* For convenience, since we often only require the lower bound on
+ (** For convenience, since we often only require the lower bound on
the interval, we re-state it as a corollary. *)
Corollary fsc_range1:
t1 <= find_swap_candidate sched t1 j1.
Proof. by move: fsc_range => /andP [LE _]. Qed.
- (* The following lemma is a key step of the overall proof: the job
+ (** The following lemma is a key step of the overall proof: the job
scheduled at the time found by [find_swap_candidate] has the
property that it has a deadline that is no later than that of any
other job in the window given by time [t1] and the deadline of
@@ -151,7 +151,7 @@ Section FindSwapCandidateFacts.
by move: ED; rewrite /earlier_deadline /oapp SCHED_j SCHED_j2.
Qed.
- (* As a special case of the above lemma, we observe that the job
+ (** As a special case of the above lemma, we observe that the job
scheduled at the time given by [find_swap_candidate] in
particular has a deadline no later than the job scheduled at time
[t1]. *)
@@ -173,20 +173,20 @@ End FindSwapCandidateFacts.
we abbreviate as "mea" in the following. *)
Section MakeEDFAtFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...consider an ideal uniprocessor schedule... *)
+ (** ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ...that is well-behaved... *)
+ (** ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (* ...and in which no scheduled job misses a deadline. *)
+ (** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
- (* Since we will require this fact repeatedly, we briefly observe
+ (** Since we will require this fact repeatedly, we briefly observe
that, since no scheduled job misses its deadline, if a job is
scheduled at some time [t], then its deadline is later than
[t]. *)
@@ -201,15 +201,15 @@ Section MakeEDFAtFacts.
- by apply (H_no_deadline_misses _ t).
Qed.
- (* We analyze [make_edf_at] applied to an arbitrary point in time,
+ (** We analyze [make_edf_at] applied to an arbitrary point in time,
which we denote [t_edf] in the following. *)
Variable t_edf: instant.
- (* For brevity, let [sched'] denote the schedule obtained from
+ (** For brevity, let [sched'] denote the schedule obtained from
[make_edf_at] applied to [sched] at time [t_edf]. *)
Let sched' := make_edf_at sched t_edf.
- (* First, we observe that in [sched'] jobs still don't execute past
+ (** First, we observe that in [sched'] jobs still don't execute past
completion. *)
Lemma mea_completed_jobs:
completed_jobs_dont_execute sched'.
@@ -225,7 +225,7 @@ Section MakeEDFAtFacts.
by apply scheduled_job_in_sched_has_later_deadline.
Qed.
- (* Importantly, [make_edf_at] does not introduce any deadline
+ (** Importantly, [make_edf_at] does not introduce any deadline
misses, which is a crucial step in the EDF optimality
argument. *)
Lemma mea_no_deadline_misses:
@@ -264,7 +264,7 @@ Section MakeEDFAtFacts.
}
Qed.
- (* As a result, we may conclude that any job scheduled at a time t has a deadline later than t. *)
+ (** As a result, we may conclude that any job scheduled at a time t has a deadline later than t. *)
Corollary mea_scheduled_job_has_later_deadline:
forall j t,
scheduled_at sched' j t ->
@@ -277,13 +277,13 @@ Section MakeEDFAtFacts.
- by apply mea_no_deadline_misses with (t := t).
Qed.
- (* Next comes a big step in the optimality proof: we observe that
+ (** Next comes a big step in the optimality proof: we observe that
[make_edf_at] indeed ensures that [EDF_at] holds at time [t_edf] in
sched'. As this is a larger argument, we proceed by case analysis and
first establish a couple of helper lemmas in the following section. *)
Section GuaranteeCaseAnalysis.
- (* Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
+ (** Let j_orig denote the job scheduled in sched at time t_edf, let j_edf
denote the job scheduled in sched' at time t_edf, and let j' denote any
job scheduled in sched' at some time t' after t_edf... *)
Variable j_orig j_edf j': Job.
@@ -295,17 +295,17 @@ Section MakeEDFAtFacts.
Hypothesis H_sched_edf: scheduled_at sched' j_edf t_edf.
Hypothesis H_sched': scheduled_at sched' j' t'.
- (* ... and that arrives before time t_edf. *)
+ (** ... and that arrives before time t_edf. *)
Hypothesis H_arrival_j' : job_arrival j' <= t_edf.
- (* We begin by observing three simple facts that will be used repeatedly in
+ (** We begin by observing three simple facts that will be used repeatedly in
the case analysis. *)
- (* First, the deadline of j_orig is later than t_edf. *)
+ (** First, the deadline of j_orig is later than t_edf. *)
Fact mea_guarantee_dl_orig: t_edf < job_deadline j_orig.
Proof. by apply (scheduled_job_in_sched_has_later_deadline j_orig t_edf H_sched_orig). Qed.
- (* Second, by the definition of sched', j_edf is scheduled in sched at the time
+ (** Second, by the definition of sched', j_edf is scheduled in sched at the time
returned by [find_swap_candidate]. *)
Fact mea_guarantee_fsc_is_j_edf: sched (find_swap_candidate sched t_edf j_orig) = Some j_edf.
Proof.
@@ -316,7 +316,7 @@ Section MakeEDFAtFacts.
- by rewrite ifT // => /eqP.
Qed.
- (* Third, the deadline of j_edf is no later than the deadline of j_orig. *)
+ (** Third, the deadline of j_edf is no later than the deadline of j_orig. *)
Fact mea_guarantee_deadlines: job_deadline j_edf <= job_deadline j_orig.
Proof.
apply: (fsc_no_later_deadline sched _ _ t_edf) => //.
@@ -324,9 +324,9 @@ Section MakeEDFAtFacts.
- by rewrite /scheduled_at mea_guarantee_fsc_is_j_edf //=.
Qed.
- (* With the setup in place, we are now ready to begin the case analysis. *)
+ (** With the setup in place, we are now ready to begin the case analysis. *)
- (* First, we consider the simpler case where t' is no earlier than the
+ (** First, we consider the simpler case where t' is no earlier than the
deadline of j_orig. This case is simpler because t' being no earlier
than j_orig's deadline implies that j' has deadline no earlier than
j_orig (since no scheduled job in sched misses a deadline), which in
@@ -342,7 +342,7 @@ Section MakeEDFAtFacts.
by apply ltnW.
Qed.
- (* Next, we consider the more difficult case, where t' is before the
+ (** Next, we consider the more difficult case, where t' is before the
deadline of j_orig. *)
Lemma mea_guarantee_case_t'_before_deadline:
t' < job_deadline j_orig ->
@@ -377,7 +377,7 @@ Section MakeEDFAtFacts.
End GuaranteeCaseAnalysis.
- (* Finally, putting the preceding case analysis together, we obtain the
+ (** Finally, putting the preceding case analysis together, we obtain the
result that [make_edf_at] establishes [EDF_at] at time [t_edf]. *)
Lemma make_edf_at_guarantee:
EDF_at sched' t_edf.
@@ -393,7 +393,7 @@ Section MakeEDFAtFacts.
by apply: (mea_guarantee_case_t'_past_deadline j_orig j_edf j' t').
Qed.
- (* We observe that [make_edf_at] maintains the property that jobs must arrive
+ (** We observe that [make_edf_at] maintains the property that jobs must arrive
to execute. *)
Lemma mea_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
@@ -421,7 +421,7 @@ Section MakeEDFAtFacts.
by rewrite /scheduled_at /scheduled_in /pstate_instance.
Qed.
- (* We connect the fact that a job is scheduled in [sched'] to the
+ (** We connect the fact that a job is scheduled in [sched'] to the
fact that it must be scheduled somewhere in [sched], too, since
[make_edf_at] does not introduce any new jobs. *)
Lemma mea_job_scheduled:
@@ -436,7 +436,7 @@ Section MakeEDFAtFacts.
by exact SCHED_j.
Qed.
- (* Conversely, if a job is scheduled in [sched], it is also
+ (** Conversely, if a job is scheduled in [sched], it is also
scheduled somewhere in [sched'] since [make_edf_at] does not lose
any jobs. *)
Lemma mea_job_scheduled':
@@ -452,17 +452,17 @@ Section MakeEDFAtFacts.
by exact SCHED_j.
Qed.
- (* Next, we observe that if all jobs in [sched] come from a given
+ (** Next, we observe that if all jobs in [sched] come from a given
arrival sequence, then that's still the case in [sched'], too. *)
Section ArrivalSequence.
- (* For given arrival sequence,... *)
+ (** For given arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
- (* ...if all jobs in [sched] come from the arrival sequence,... *)
+ (** ...if all jobs in [sched] come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
- (* ...then all jobs in [sched'] do, too. *)
+ (** ...then all jobs in [sched'] do, too. *)
Lemma mea_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
@@ -474,12 +474,12 @@ Section MakeEDFAtFacts.
End ArrivalSequence.
- (* For the final claim, assume that [EDF_at] already holds
+ (** For the final claim, assume that [EDF_at] already holds
everywhere prior to time [t_edf], i.e., that [sched] consists of
an EDF prefix. *)
Hypothesis H_EDF_prefix: forall t, t < t_edf -> EDF_at sched t.
- (* We establish a key property of [make_edf_at]: not only does it
+ (** We establish a key property of [make_edf_at]: not only does it
ensure [EDF_at] at time [t_edf], it also maintains the fact that
the schedule has an EDF prefix prior to time [t_edf]. In other
words, it grows the EDF prefix by one time unit. *)
@@ -518,27 +518,27 @@ End MakeEDFAtFacts.
(** In the following section, we establish properties of [edf_transform_prefix]. *)
Section EDFPrefixFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...consider an ideal uniprocessor schedule... *)
+ (** ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ...that is well-behaved... *)
+ (** ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (* ...and in which no scheduled job misses a deadline. *)
+ (** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
- (* Consider any point in time, denoted [horizon], and... *)
+ (** Consider any point in time, denoted [horizon], and... *)
Variable horizon: instant.
- (* ...let [sched'] denote the schedule obtained by EDF-ifying
+ (** ...let [sched'] denote the schedule obtained by EDF-ifying
[sched] up to the horizon. *)
Let sched' := edf_transform_prefix sched horizon.
- (* To start, we observe that [sched'] is still well-behaved and
+ (** To start, we observe that [sched'] is still well-behaved and
without deadline misses. *)
Lemma edf_prefix_well_formedness:
completed_jobs_dont_execute sched'
@@ -556,13 +556,13 @@ Section EDFPrefixFacts.
- apply mea_no_deadline_misses => //.
Qed.
- (* Because it is needed frequently, we extract the second clause of
+ (** Because it is needed frequently, we extract the second clause of
the above conjunction as a corollary. *)
Corollary edf_prefix_jobs_must_arrive:
jobs_must_arrive_to_execute sched'.
Proof. by move: edf_prefix_well_formedness => [_ [ARR _]]. Qed.
- (* We similarly observe that the absence of deadline misses implies
+ (** We similarly observe that the absence of deadline misses implies
that any scheduled job must have a deadline at a time later then
when it is scheduled. *)
Corollary edf_prefix_scheduled_job_has_later_deadline:
@@ -577,7 +577,7 @@ Section EDFPrefixFacts.
- by apply (DL_MET j t).
Qed.
- (* Since no jobs are lost or added to the schedule by
+ (** Since no jobs are lost or added to the schedule by
[edf_transform_prefix], we if a job is scheduled in the
transformed schedule, then it is also scheduled at some point in
the original schedule. *)
@@ -595,7 +595,7 @@ Section EDFPrefixFacts.
by apply: (EX t'''' SCHED'''').
Qed.
- (* Conversely, if a job is scheduled in the original schedule, it is
+ (** Conversely, if a job is scheduled in the original schedule, it is
also scheduled at some point in the transformed schedule. *)
Lemma edf_prefix_job_scheduled':
forall j t,
@@ -610,17 +610,17 @@ Section EDFPrefixFacts.
by exact SCHEDX_j.
Qed.
- (* Next, we note that [edf_transform_prefix] maintains the
+ (** Next, we note that [edf_transform_prefix] maintains the
property that all jobs stem from a given arrival sequence. *)
Section ArrivalSequence.
- (* For any arrival sequence,... *)
+ (** For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
- (* ...if all jobs in the original schedule come from the arrival sequence,... *)
+ (** ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
- (* ...then all jobs in the transformed schedule still come from
+ (** ...then all jobs in the transformed schedule still come from
the same arrival sequence. *)
Lemma edf_prefix_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
@@ -633,7 +633,7 @@ Section EDFPrefixFacts.
End ArrivalSequence.
- (* We establish the key property of [edf_transform_prefix]: that it indeed
+ (** We establish the key property of [edf_transform_prefix]: that it indeed
ensures that the resulting schedule ensures the EDF invariant up to the
given [horizon]. *)
Lemma edf_prefix_guarantee:
@@ -661,23 +661,23 @@ Section EDFPrefixFacts.
End EDFPrefixFacts.
-(* Finally, we observe that [edf_transform_prefix] is prefix-stable, which
+(** Finally, we observe that [edf_transform_prefix] is prefix-stable, which
allows us to replace an earlier horizon with a later horizon. Note: this is
in a separate section because we need [edf_prefix_jobs_must_arrive]
generalized for any schedule. *)
Section EDFPrefixInclusion.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...consider an ideal uniprocessor schedule... *)
+ (** ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ...that is well-behaved... *)
+ (** ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (* ...and in which no scheduled job misses a deadline. *)
+ (** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
Lemma edf_prefix_inclusion:
@@ -710,24 +710,24 @@ End EDFPrefixInclusion.
EDF-ication operation [edf_transform]. *)
Section EDFTransformFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ...consider an ideal uniprocessor schedule... *)
+ (** ...consider an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ...that is well-behaved... *)
+ (** ...that is well-behaved... *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute sched.
- (* ...and in which no scheduled job misses a deadline. *)
+ (** ...and in which no scheduled job misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
- (* In the following, let [sched_edf] denote the EDF schedule obtained by
+ (** In the following, let [sched_edf] denote the EDF schedule obtained by
transforming the given reference schedule. *)
Let sched_edf := edf_transform sched.
- (* We begin with the first key property: the resulting schedule is actually
+ (** We begin with the first key property: the resulting schedule is actually
an EDF schedule. *)
Theorem edf_transform_ensures_edf:
is_EDF_schedule sched_edf.
@@ -743,7 +743,7 @@ Section EDFTransformFacts.
by apply (EDF j SCHED_j t' j' LE_t_t').
Qed.
- (* Next, we observe that completed jobs still don't execute in the resulting
+ (** Next, we observe that completed jobs still don't execute in the resulting
EDF schedule. This observation is needed to establish that the resulting
EDF schedule is valid. *)
Lemma edf_transform_completed_jobs_dont_execute:
@@ -765,7 +765,7 @@ Section EDFTransformFacts.
by apply COMP.
Qed.
- (* Similarly, we observe that no job is scheduled prior to its arrival. *)
+ (** Similarly, we observe that no job is scheduled prior to its arrival. *)
Lemma edf_transform_jobs_must_arrive:
jobs_must_arrive_to_execute sched_edf.
Proof.
@@ -775,7 +775,7 @@ Section EDFTransformFacts.
by apply ARR.
Qed.
- (* We next establish the second key property: in the transformed EDF
+ (** We next establish the second key property: in the transformed EDF
schedule, no scheduled job misses a deadline. *)
Theorem edf_transform_deadlines_met:
all_deadlines_met sched_edf.
@@ -798,7 +798,7 @@ Section EDFTransformFacts.
by apply: (DL j t).
Qed.
- (* We observe that no new jobs are introduced: any job scheduled in the EDF
+ (** We observe that no new jobs are introduced: any job scheduled in the EDF
schedule were also present in the reference schedule. *)
Lemma edf_transform_job_scheduled:
forall j t, scheduled_at sched_edf j t -> exists t', scheduled_at sched j t'.
@@ -808,7 +808,7 @@ Section EDFTransformFacts.
by apply edf_prefix_job_scheduled.
Qed.
- (* Conversely, we observe that no jobs are lost: any job scheduled in the
+ (** Conversely, we observe that no jobs are lost: any job scheduled in the
reference schedule is also present in the EDF schedule. *)
Lemma edf_transform_job_scheduled':
forall j t, scheduled_at sched j t -> exists t', scheduled_at sched_edf j t'.
@@ -823,17 +823,17 @@ Section EDFTransformFacts.
by apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := job_deadline j).
Qed.
- (* Next, we note that [edf_transform] maintains the property that all jobs
+ (** Next, we note that [edf_transform] maintains the property that all jobs
stem from a given arrival sequence. *)
Section ArrivalSequence.
- (* For any arrival sequence,... *)
+ (** For any arrival sequence,... *)
Variable arr_seq: arrival_sequence Job.
- (* ...if all jobs in the original schedule come from the arrival sequence,... *)
+ (** ...if all jobs in the original schedule come from the arrival sequence,... *)
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
- (* ...then all jobs in the transformed EDF schedule still come from the
+ (** ...then all jobs in the transformed EDF schedule still come from the
same arrival sequence. *)
Lemma edf_transform_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched_edf arr_seq.
@@ -850,29 +850,29 @@ End EDFTransformFacts.
(** Finally, we state the theorems that jointly make up the EDF optimality claim. *)
Section Optimality.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ... consider an arbitrary valid job arrival sequence ... *)
+ (** ... consider an arbitrary valid job arrival sequence ... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arr_seq_valid: valid_arrival_sequence arr_seq.
- (* ... and an ideal uniprocessor schedule... *)
+ (** ... and an ideal uniprocessor schedule... *)
Variable sched: schedule (ideal.processor_state Job).
- (* ... that corresponds to the given arrival sequence. *)
+ (** ... that corresponds to the given arrival sequence. *)
Hypothesis H_sched_valid: valid_schedule sched arr_seq.
- (* In the following, let [equivalent_edf_schedule] denote the schedule that
+ (** In the following, let [equivalent_edf_schedule] denote the schedule that
results from the EDF transformation. *)
Let equivalent_edf_schedule := edf_transform sched.
Section AllDeadlinesMet.
- (* Suppose no job scheduled in the given reference schedule misses a deadline. *)
+ (** Suppose no job scheduled in the given reference schedule misses a deadline. *)
Hypothesis H_no_deadline_misses: all_deadlines_met sched.
- (* Then the resulting EDF schedule is a valid schedule for the given
+ (** Then the resulting EDF schedule is a valid schedule for the given
arrival sequence... *)
Theorem edf_schedule_is_valid:
valid_schedule equivalent_edf_schedule arr_seq.
@@ -887,7 +887,7 @@ Section Optimality.
- by apply edf_transform_completed_jobs_dont_execute.
Qed.
- (* ...and no scheduled job misses its deadline. *)
+ (** ...and no scheduled job misses its deadline. *)
Theorem edf_schedule_meets_all_deadlines:
all_deadlines_met equivalent_edf_schedule.
Proof.
@@ -899,16 +899,16 @@ Section Optimality.
End AllDeadlinesMet.
- (* Next, we strengthen the above "no deadline misses" claim by relating it
+ (** Next, we strengthen the above "no deadline misses" claim by relating it
not just to all scheduled jobs, but to all jobs in the given arrival
sequence. *)
Section AllDeadlinesOfArrivalsMet.
- (* Suppose no job that's part of the arrival sequence misses a deadline in
+ (** Suppose no job that's part of the arrival sequence misses a deadline in
the given reference schedule. *)
Hypothesis H_no_deadline_misses_of_arrivals: all_deadlines_of_arrivals_met arr_seq sched.
- (* Then no job that's part of the arrival sequence misses a deadline in the
+ (** Then no job that's part of the arrival sequence misses a deadline in the
EDF schedule, either. *)
Theorem edf_schedule_meets_all_deadlines_wrt_arrivals:
all_deadlines_of_arrivals_met arr_seq equivalent_edf_schedule.
diff --git a/restructuring/analysis/transform/facts/replace_at.v b/restructuring/analysis/transform/facts/replace_at.v
index 62c52ec27c855324db658ead963f33bc1b3ca909..2ad56400b402202e4a9068f89e9a75af10041ed9 100644
--- a/restructuring/analysis/transform/facts/replace_at.v
+++ b/restructuring/analysis/transform/facts/replace_at.v
@@ -6,27 +6,27 @@ From rt.util Require Import nat.
replacements. *)
Section ReplaceAtFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType}.
- (* ... and any given type of processor states, ... *)
+ (** ... and any given type of processor states, ... *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider any given reference schedule. *)
+ (** ...consider any given reference schedule. *)
Variable sched: schedule PState.
- (* Suppose we are given a specific time [t'] ... *)
+ (** Suppose we are given a specific time [t'] ... *)
Variable t': instant.
- (* ...and a replacement state [state]. *)
+ (** ...and a replacement state [state]. *)
Variable nstate: PState.
- (* In the following, let sched' denote the schedule with replacement at time
+ (** In the following, let sched' denote the schedule with replacement at time
t'. *)
Let sched' := replace_at sched t' nstate.
- (* We begin with the trivial observation that the schedule doesn't change at
+ (** We begin with the trivial observation that the schedule doesn't change at
other times. *)
Lemma rest_of_schedule_invariant:
forall t, t <> t' -> sched' t = sched t.
@@ -37,7 +37,7 @@ Section ReplaceAtFacts.
by move/eqP in TT; rewrite TT in DIFF; contradiction.
Qed.
- (* As a result, the service in intervals that do not intersect with t' is
+ (** As a result, the service in intervals that do not intersect with t' is
invariant, too. *)
Lemma service_at_other_times_invariant:
forall t1 t2,
@@ -54,7 +54,7 @@ Section ReplaceAtFacts.
eapply point_not_in_interval; eauto.
Qed.
- (* Next, we consider the amount of service received in intervals that do span
+ (** Next, we consider the amount of service received in intervals that do span
across the replacement point. We can relate the service received in the
original and the new schedules by adding the service in the respective
"missing" state... *)
@@ -72,7 +72,7 @@ Section ReplaceAtFacts.
by rewrite !service_at_other_times_invariant -/sched'; [ring | right | left].
Qed.
- (* ...which we can also rewrite as follows. *)
+ (** ...which we can also rewrite as follows. *)
Corollary service_in_replaced:
forall t1 t2,
t1 <= t' < t2 ->
@@ -82,7 +82,7 @@ Section ReplaceAtFacts.
service_during sched j t1 t2 + service_at sched' j t' - service_at sched j t'.
Proof. move => t1 t2 ORDER j. by rewrite service_delta// addnK. Qed.
- (* As another simple invariant (useful for case analysis), we observe that if
+ (** As another simple invariant (useful for case analysis), we observe that if
a job is scheduled neither in the replaced nor in the new state, then at
any time it receives exactly the same amount of service in the new
schedule with replacements as in the original schedule. *)
@@ -99,7 +99,7 @@ Section ReplaceAtFacts.
- rewrite rest_of_schedule_invariant//.
Qed.
- (* Based on the previous observation, we can trivially lift the invariant
+ (** Based on the previous observation, we can trivially lift the invariant
that jobs not involved in the replacement receive equal service to the
cumulative service received in any interval. *)
Corollary service_during_of_others_invariant (j: Job):
diff --git a/restructuring/analysis/transform/facts/swaps.v b/restructuring/analysis/transform/facts/swaps.v
index 5395156ae9fdab7310b6e3cf1da6d0a37cd942e2..b104c1093d5aa8274ea63a2d3257447b9b34f482 100644
--- a/restructuring/analysis/transform/facts/swaps.v
+++ b/restructuring/analysis/transform/facts/swaps.v
@@ -7,23 +7,23 @@ From rt.util Require Import nat.
classic EDF optimality proof. *)
Section SwappedFacts.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType}.
- (* ... any given type of processor states: *)
+ (** ... any given type of processor states: *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider any given reference schedule. *)
+ (** ...consider any given reference schedule. *)
Variable sched: schedule PState.
- (* Suppose we are given two specific times [t1] and [t2]. *)
+ (** Suppose we are given two specific times [t1] and [t2]. *)
Variable t1 t2: instant.
- (* In the following, let [sched'] denote the schedule in which the
+ (** In the following, let [sched'] denote the schedule in which the
allocations at [t1] and [t2] have been swapped. *)
Let sched' := swapped sched t1 t2.
- (* First, we note that the trivial case where t1 == t2 is not interesting
+ (** First, we note that the trivial case where t1 == t2 is not interesting
because then the two schedules are identical. *)
Lemma trivial_swap:
t1 = t2 ->
@@ -36,7 +36,7 @@ Section SwappedFacts.
by move /eqP ->.
Qed.
- (* In this trivial case, the amount of service received hence
+ (** In this trivial case, the amount of service received hence
is obviously always identical. *)
Lemma trivial_swap_service_invariant:
t1 = t2 ->
@@ -49,7 +49,7 @@ Section SwappedFacts.
by rewrite trivial_swap.
Qed.
- (* In any case, the two schedules do not differ at non-swapped times. *)
+ (** In any case, the two schedules do not differ at non-swapped times. *)
Lemma swap_other_times_invariant:
forall t,
t <> t1 ->
@@ -60,7 +60,7 @@ Section SwappedFacts.
by rewrite /sched' /swapped !rest_of_schedule_invariant //.
Qed.
- (* By definition, if a job is scheduled at t2 in the original
+ (** By definition, if a job is scheduled at t2 in the original
schedule, then it is found at t1 in the new schedule. *)
Lemma swap_job_scheduled_t1:
forall j,
@@ -74,7 +74,7 @@ Section SwappedFacts.
- by rewrite ifT.
Qed.
- (* Similarly, a job scheduled at t1 in the original schedule is
+ (** Similarly, a job scheduled at t1 in the original schedule is
scheduled at t2 after the swap. *)
Lemma swap_job_scheduled_t2:
forall j,
@@ -88,7 +88,7 @@ Section SwappedFacts.
- by rewrite ifT.
Qed.
- (* If a job is scheduled at any time not involved in the swap, then
+ (** If a job is scheduled at any time not involved in the swap, then
it remains scheduled at that time in the new schedule. *)
Lemma swap_job_scheduled_other_times:
forall j t,
@@ -102,7 +102,7 @@ Section SwappedFacts.
by rewrite swap_other_times_invariant //; apply: not_eq_sym.
Qed.
- (* To make case analysis more convenient, we summarize the preceding
+ (** To make case analysis more convenient, we summarize the preceding
three lemmas as a disjunction. *)
Corollary swap_job_scheduled_cases:
forall j t,
@@ -126,7 +126,7 @@ Section SwappedFacts.
by rewrite -swap_job_scheduled_other_times.
Qed.
- (* From this, we can easily conclude that no jobs have appeared out
+ (** From this, we can easily conclude that no jobs have appeared out
of thin air: if a job scheduled at some time in the new schedule,
then it was also scheduled at some time in the original
schedule. *)
@@ -144,7 +144,7 @@ Section SwappedFacts.
- by exists t1.
Qed.
- (* Mirroring swap_job_scheduled_cases above, we also state a
+ (** Mirroring swap_job_scheduled_cases above, we also state a
disjunction for case analysis under the premise that a job is
scheduled in the original schedule. *)
Lemma swap_job_scheduled_original_cases:
@@ -169,7 +169,7 @@ Section SwappedFacts.
by rewrite swap_job_scheduled_other_times.
Qed.
- (* Thus, we can conclude that no jobs are lost: if a job is
+ (** Thus, we can conclude that no jobs are lost: if a job is
scheduled at some point in the original schedule, then it is also
scheduled at some point in the new schedule. *)
Corollary swap_job_scheduled_original:
@@ -190,11 +190,11 @@ Section SwappedFacts.
statements about invariants about the cumulative amount of
service received. *)
- (* To avoid dealing with symmetric cases, assume in the following
+ (** To avoid dealing with symmetric cases, assume in the following
that t1 and t2 are ordered. *)
Hypothesis H_well_ordered: t1 <= t2.
- (* As another trivial invariant, we observe that nothing has changed
+ (** As another trivial invariant, we observe that nothing has changed
before time t1. *)
Lemma swap_before_invariant:
forall t,
@@ -207,7 +207,7 @@ Section SwappedFacts.
[move: t_lt_t1|move: t_lt_t2]; rewrite ltnn.
Qed.
- (* Similarly, nothing has changed after time t2. *)
+ (** Similarly, nothing has changed after time t2. *)
Lemma swap_after_invariant:
forall t,
t2 < t ->
@@ -219,7 +219,7 @@ Section SwappedFacts.
[move: t1_lt_t|move: t2_lt_t]; rewrite ltnn.
Qed.
- (* Thus, we observe that, before t1, the two schedules are identical with
+ (** Thus, we observe that, before t1, the two schedules are identical with
regard to the service received by any job because they are identical. *)
Corollary service_before_swap_invariant:
forall t,
@@ -234,7 +234,7 @@ Section SwappedFacts.
by apply ltnW.
Qed.
- (* Likewise, we observe that, *after* t2, the swapped schedule again does not
+ (** Likewise, we observe that, *after* t2, the swapped schedule again does not
differ with regard to the service received by any job. *)
Lemma service_after_swap_invariant:
forall t,
@@ -256,7 +256,7 @@ Section SwappedFacts.
[rewrite addnC|]; by apply leq_addr.
Qed.
- (* Finally, we note that, trivially, jobs that are not involved in
+ (** Finally, we note that, trivially, jobs that are not involved in
the swap receive invariant service. *)
Lemma service_of_others_invariant:
forall t j,
@@ -280,26 +280,26 @@ End SwappedFacts.
scheduled obtained by swapping the allocations at times [t1] and
[t2]. *)
Section SwappedScheduleProperties.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job} `{JobArrival Job}.
- (* ... any given type of processor states: *)
+ (** ... any given type of processor states: *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider any given reference schedule. *)
+ (** ...consider any given reference schedule. *)
Variable sched: schedule PState.
- (* Suppose we are given two specific times [t1] and [t2]... *)
+ (** Suppose we are given two specific times [t1] and [t2]... *)
Variable t1 t2: instant.
- (* ...such that [t1] is no later than [t2]. *)
+ (** ...such that [t1] is no later than [t2]. *)
Hypothesis H_order: t1 <= t2.
- (* We let [sched'] denote the schedule in which the allocations at
+ (** We let [sched'] denote the schedule in which the allocations at
[t1] and [t2] have been swapped. *)
Let sched' := swapped sched t1 t2.
- (* First, we observe that if jobs never accomulate more service than
+ (** First, we observe that if jobs never accomulate more service than
required, then that's still the case after the swap. *)
Lemma swapped_service_bound:
(forall j t, service sched j t <= job_cost j) ->
@@ -325,7 +325,7 @@ Section SwappedScheduleProperties.
}
Qed.
- (* From the above service bound, we conclude that, if if completed jobs don't
+ (** From the above service bound, we conclude that, if if completed jobs don't
execute in the original schedule, then that's still the case after the
swap, assuming an ideal unit-service model (i.e., scheduled jobs receive
exactly one unit of service). *)
@@ -341,11 +341,11 @@ Section SwappedScheduleProperties.
by move=> j; apply service_at_most_cost.
Qed.
- (* Suppose all jobs in the original schedule come from some arrival sequence... *)
+ (** Suppose all jobs in the original schedule come from some arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_from_arr_seq: jobs_come_from_arrival_sequence sched arr_seq.
- (* ...then that's still the case in the new schedule. *)
+ (** ...then that's still the case in the new schedule. *)
Lemma swapped_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched' arr_seq.
Proof.
@@ -362,29 +362,29 @@ End SwappedScheduleProperties.
not yet missed its deadline, which is the core transformation of
the classic EDF optimality proof. *)
Section EDFSwap.
- (* For any given type of jobs with costs and deadlines... *)
+ (** For any given type of jobs with costs and deadlines... *)
Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.
- (* ... any given type of processor states... *)
+ (** ... any given type of processor states... *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider a given reference schedule... *)
+ (** ...consider a given reference schedule... *)
Variable sched: schedule PState.
- (* ...in which complete jobs don't execute... *)
+ (** ...in which complete jobs don't execute... *)
Hypothesis H_completed_jobs:
completed_jobs_dont_execute sched.
- (* ...and scheduled jobs always receive service. *)
+ (** ...and scheduled jobs always receive service. *)
Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model.
- (* Suppose we are given two specific times [t1] and [t2]... *)
+ (** Suppose we are given two specific times [t1] and [t2]... *)
Variable t1 t2: instant.
- (* ...that are ordered. *)
+ (** ...that are ordered. *)
Hypothesis H_well_ordered: t1 <= t2.
- (* Further, assume that, if there are jobs scheduled at times t1 and t2, then
+ (** Further, assume that, if there are jobs scheduled at times t1 and t2, then
they either have the same deadline or violate EDF, ... *)
Hypothesis H_not_EDF:
forall j1 j2,
@@ -392,7 +392,7 @@ Section EDFSwap.
scheduled_at sched j2 t2 ->
job_deadline j1 >= job_deadline j2.
- (* ...and that we don't move idle times or deadline misses earlier,
+ (** ...and that we don't move idle times or deadline misses earlier,
i.e., if t1 is not an idle time, then neither is t2 and whatever
job is scheduled at time t2 has not yet missed its deadline. *)
Hypothesis H_no_idle_time_at_t2:
@@ -400,22 +400,22 @@ Section EDFSwap.
scheduled_at sched j1 t1 ->
exists j2, scheduled_at sched j2 t2 /\ job_deadline j2 > t2.
- (* Consider the schedule obtained from swapping the allocations at times t1 and t2. *)
+ (** Consider the schedule obtained from swapping the allocations at times t1 and t2. *)
Let sched' := swapped sched t1 t2.
- (* The key property of this transformation is that, for any job that
+ (** The key property of this transformation is that, for any job that
meets its deadline in the original schedule, we have not
introduced any deadline misses, which we establish by considering
a number of different cases. *)
Section NoNewDeadlineMissesCases.
- (* Consider any job... *)
+ (** Consider any job... *)
Variable j: Job.
- (* ... that meets its deadline in the original schedule. *)
+ (** ... that meets its deadline in the original schedule. *)
Hypothesis H_deadline_met: job_meets_deadline sched j.
- (* First we observe that jobs that are not involved in the swap
+ (** First we observe that jobs that are not involved in the swap
still meet their deadlines. *)
Lemma uninvolved_implies_deadline_met:
~~ scheduled_at sched j t1 ->
@@ -427,7 +427,7 @@ Section EDFSwap.
by apply: service_of_others_invariant.
Qed.
- (* Next, we observe that a swap is unproblematic for the job scheduled at
+ (** Next, we observe that a swap is unproblematic for the job scheduled at
time t2. *)
Lemma moved_earlier_implies_deadline_met:
scheduled_at sched j t2 ->
@@ -439,7 +439,7 @@ Section EDFSwap.
by apply scheduled_at_implies_later_deadline with (sched0 := sched) => //.
Qed.
- (* Finally, we observe is also unproblematic for the job that is
+ (** Finally, we observe is also unproblematic for the job that is
moved to a later allocation. *)
Lemma moved_later_implies_deadline_met:
scheduled_at sched j t1 ->
@@ -455,7 +455,7 @@ Section EDFSwap.
End NoNewDeadlineMissesCases.
- (* From the above case analysis, we conclude that no deadline misses
+ (** From the above case analysis, we conclude that no deadline misses
are introduced in the schedule obtained from swapping the
allocations at times t1 and t2. *)
Theorem edf_swap_no_deadline_misses_introduced:
diff --git a/restructuring/analysis/transform/prefix.v b/restructuring/analysis/transform/prefix.v
index d006258566f0edb297bac244366f4abf7693b96a..7c299e1a38faca427116303f349fb7c1717629f5 100644
--- a/restructuring/analysis/transform/prefix.v
+++ b/restructuring/analysis/transform/prefix.v
@@ -7,14 +7,14 @@ From rt.restructuring.analysis Require Import basic_facts.all.
instant up to a given horizon. *)
Section SchedulePrefixMap.
- (* For any type of jobs and... *)
+ (** For any type of jobs and... *)
Context {Job : JobType}.
- (* ... any given type of processor states ... *)
+ (** ... any given type of processor states ... *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ... we define a procedure that applies a given function to every
+ (** ... we define a procedure that applies a given function to every
point in a given finite prefix of the schedule.
The point-wise transformation f is given a schedule and the point
@@ -38,16 +38,16 @@ Section SchedulePrefixMap.
original schedule, then the prefix_map does so as well. *)
Section PropertyPreservation.
- (* Given any property of schedules... *)
+ (** Given any property of schedules... *)
Variable P: schedule PState -> Prop.
- (* ...and a point-wise transformation [f],... *)
+ (** ...and a point-wise transformation [f],... *)
Variable f: schedule PState -> instant -> schedule PState.
- (* ...if [f] maintains property [P],... *)
+ (** ...if [f] maintains property [P],... *)
Hypothesis H_f_maintains_P: forall sched t, P sched -> P (f sched t).
- (* ...then so does a prefix map of [f]. *)
+ (** ...then so does a prefix map of [f]. *)
Lemma prefix_map_property_invariance:
forall sched h, P sched -> P (prefix_map sched f h).
Proof.
@@ -63,28 +63,28 @@ Section SchedulePrefixMap.
establishes a new property step-by-step. *)
Section PointwiseProperty.
- (* Given any property of schedules [P],... *)
+ (** Given any property of schedules [P],... *)
Variable P: schedule PState -> Prop.
- (* ...any point-wise property [Q],... *)
+ (** ...any point-wise property [Q],... *)
Variable Q: schedule PState -> instant -> Prop.
- (* ...and a point-wise transformation [f],... *)
+ (** ...and a point-wise transformation [f],... *)
Variable f: schedule PState -> instant -> schedule PState.
- (* ...if [f] maintains [P]... *)
+ (** ...if [f] maintains [P]... *)
Hypothesis H_f_maintains_P:
forall sched t_ref,
P sched -> P (f sched t_ref).
- (* ...and establishes [Q] (provided that [P] holds)... *)
+ (** ...and establishes [Q] (provided that [P] holds)... *)
Hypothesis H_f_grows_Q:
forall sched t_ref,
P sched ->
(forall t', t' < t_ref -> Q sched t') ->
forall t', t' <= t_ref -> Q (f sched t_ref) t'.
- (* ...then the prefix-map operation will "grow" [Q] up to the horizon. *)
+ (** ...then the prefix-map operation will "grow" [Q] up to the horizon. *)
Lemma prefix_map_pointwise_property:
forall sched horizon,
P sched ->
diff --git a/restructuring/analysis/transform/swap.v b/restructuring/analysis/transform/swap.v
index f44a4055705f0572d16069001b00c5fdcfc902da..58aab0568ac5ac5a049f43576b2c978086be3f3c 100644
--- a/restructuring/analysis/transform/swap.v
+++ b/restructuring/analysis/transform/swap.v
@@ -7,22 +7,22 @@ From rt.restructuring.analysis.basic_facts Require Import all.
(** We begin by defining the notion of a schedule with a "tweaked" (i.e.,
overridden) allocation. *)
Section ReplaceAt.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType}.
- (* ... any given type of processor states, ... *)
+ (** ... any given type of processor states, ... *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider any given reference schedule. *)
+ (** ...consider any given reference schedule. *)
Variable original_sched: schedule PState.
- (* Suppose we are given a specific time [t'] ... *)
+ (** Suppose we are given a specific time [t'] ... *)
Variable t': instant.
- (* ...and a replacement state [new_state]. *)
+ (** ...and a replacement state [new_state]. *)
Variable new_state: PState.
- (* Then the schedule with replacement is simply one that returns the given
+ (** Then the schedule with replacement is simply one that returns the given
[new_state] at [t'], and the original allocation at all other times. *)
Definition replace_at (t : instant) :=
if t' == t then new_state else (original_sched t).
@@ -33,19 +33,19 @@ End ReplaceAt.
(** Based on [replace_at], we define the notion of a schedule with swapped
allocations. *)
Section Swapped.
- (* For any given type of jobs... *)
+ (** For any given type of jobs... *)
Context {Job : JobType}.
- (* ... any given type of processor states, ... *)
+ (** ... any given type of processor states, ... *)
Context {PState: eqType}.
Context `{ProcessorState Job PState}.
- (* ...consider any given reference schedule. *)
+ (** ...consider any given reference schedule. *)
Variable original_sched: schedule PState.
- (* Given two specific times [t1] and [t2]... *)
+ (** Given two specific times [t1] and [t2]... *)
Variable t1 t2: instant.
- (* ...we define the notion of a schedule in which the two allocations at [t1]
+ (** ...we define the notion of a schedule in which the two allocations at [t1]
and [t2] have been swapped. *)
Definition swapped : schedule PState :=
let s1 := original_sched t1 in
diff --git a/restructuring/analysis/workload.v b/restructuring/analysis/workload.v
index aab4291b21300dc3918cce285ba719766e90cf69..45da39da0d98d4739f1a17422d40e728de284f61 100644
--- a/restructuring/analysis/workload.v
+++ b/restructuring/analysis/workload.v
@@ -8,23 +8,23 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** In this file, we establish basic facts about the workload of sets of jobs. *)
Section WorkloadFacts.
- (* Consider any type of tasks ... *)
+ (** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
- (* ... and any type of jobs associated with these tasks. *)
+ (** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
- (* Consider any job arrival sequence. *)
+ (** Consider any job arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (* For simplicity, let's define a local name. *)
+ (** For simplicity, let's define a local name. *)
Let arrivals_between := arrivals_between arr_seq.
- (* We prove that workload can be split into two parts. *)
+ (** We prove that workload can be split into two parts. *)
Lemma workload_of_jobs_cat:
forall t t1 t2 P,
t1 <= t <= t2 ->