From fa2f1873b7e7fb591751a7e0ce2dc4eafde728a5 Mon Sep 17 00:00:00 2001
From: mmaida <mmaida@mpi-sws.org>
Date: Wed, 1 Apr 2020 19:07:37 +0200
Subject: [PATCH] Fixed broken intervals
---
analysis/abstract/abstract_rta.v | 4 ++--
analysis/abstract/abstract_seq_rta.v | 16 ++++++++--------
analysis/abstract/definitions.v | 6 +++---
analysis/abstract/ideal_jlfp_rta.v | 4 ++--
analysis/abstract/run_to_completion.v | 6 +++---
analysis/abstract/search_space.v | 2 +-
analysis/definitions/busy_interval.v | 4 ++--
analysis/definitions/priority_inversion.v | 2 +-
analysis/definitions/task_schedule.v | 4 ++--
analysis/facts/behavior/service.v | 6 +++---
analysis/facts/busy_interval/busy_interval.v | 18 +++++++++---------
analysis/facts/busy_interval/carry_in.v | 10 +++++-----
.../facts/busy_interval/priority_inversion.v | 10 +++++-----
analysis/facts/model/ideal_schedule.v | 4 ++--
analysis/facts/model/service_of_jobs.v | 10 +++++-----
behavior/arrival_sequence.v | 2 +-
model/aggregate/service_of_jobs.v | 6 +++---
model/task/arrival/curves.v | 2 +-
model/task/arrivals.v | 2 +-
results/edf/rta/bounded_pi.v | 2 +-
20 files changed, 60 insertions(+), 60 deletions(-)
diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index b785de44d..f8e8764a9 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -120,7 +120,7 @@ Section Abstract_RTA.
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.
@@ -303,7 +303,7 @@ Section Abstract_RTA.
(** 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] incurs interference at any time instant t ∈ [t1, t1 + A).
+ follows that job [j] incurs interference at any time instant t ∈ <<[t1, t1 + A)>>.
Therefore [interference_bound_function(tsk, A, A + F)] is at least [A]. *)
Lemma relative_arrival_le_interference_bound:
A <= interference_bound_function tsk A (A + F).
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index 0a69ff1dd..01365ebda 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -221,7 +221,7 @@ 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.
@@ -242,7 +242,7 @@ Section Sequential_Abstract_RTA.
Qed.
(** Next we prove that if a job is pending after the beginning
- of the busy interval [t1, t2) then it arrives after t1. *)
+ of the busy interval <<[t1, t2)>> then it arrives after t1. *)
Lemma arrives_after_beginning_of_busy_interval:
forall t,
t1 <= t ->
@@ -277,7 +277,7 @@ Section Sequential_Abstract_RTA.
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.
@@ -291,7 +291,7 @@ Section Sequential_Abstract_RTA.
(** ... 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 tasks, jobs of
@@ -299,14 +299,14 @@ Section Sequential_Abstract_RTA.
Section TaskInterferenceBoundsInterference.
(** 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
+ 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. *)
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.
@@ -476,7 +476,7 @@ Section Sequential_Abstract_RTA.
End Case4.
(** 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]
+ 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]. *)
Lemma interference_plus_sched_le_serv_of_task_plus_task_interference:
@@ -547,7 +547,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:
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 3a0b51466..461e4ef68 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -98,7 +98,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. *)
@@ -107,7 +107,7 @@ 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 /\
@@ -205,7 +205,7 @@ Section AbstractRTADefinitions.
(** 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
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index 53b778c38..8a1a04db7 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -271,7 +271,7 @@ Section JLFPInstantiation.
conventional workload, i.e., the one defined with concrete schedule parameters. *)
Section InstantiatedWorkloadEquivalence.
- (** Let [t1,t2) be any time interval. *)
+ (** Let <<[t1,t2)>> be any time interval. *)
Variables t1 t2 : instant.
(** Consider any job j of [tsk]. *)
@@ -330,7 +330,7 @@ Section JLFPInstantiation.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
- (** We consider an arbitrary time interval [t1, t) that starts with a quiet time. *)
+ (** We consider an arbitrary time interval <<[t1, t)>> that starts with a quiet time. *)
Variable t1 t : instant.
Hypothesis H_quiet_time : quiet_time_cl j t1.
diff --git a/analysis/abstract/run_to_completion.v b/analysis/abstract/run_to_completion.v
index 95d8d5687..d5089707e 100644
--- a/analysis/abstract/run_to_completion.v
+++ b/analysis/abstract/run_to_completion.v
@@ -65,7 +65,7 @@ Section AbstractRTARunToCompletionThreshold.
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.
@@ -87,13 +87,13 @@ Section AbstractRTARunToCompletionThreshold.
the total time where job [j] is scheduled inside the busy interval. *)
Section InterferenceIsComplement.
- (** Consider any sub-interval [t, t + delta) inside the busy interval [t1, t2). *)
+ (** Consider any sub-interval <<[t, t + delta)>> inside the busy interval [t1, t2). *)
Variables (t : instant) (delta : duration).
Hypothesis H_greater_than_or_equal : t1 <= t.
Hypothesis H_less_or_equal: t + delta <= t2.
(** We prove that sum of cumulative service and cumulative interference
- in the interval [t, t + delta) is equal to delta. *)
+ 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.
Proof.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index 71342597f..65ae681a2 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -58,7 +58,7 @@ Section AbstractRTAReduction.
(** Recall the definition of [ε], which defines the neighborhood of a point in the timeline.
Note that [ε = 1] under discrete time. *)
(** To ensure that the search converges more quickly, we only check values of [A] in the interval
- [[0, B)] for which the interference bound function changes, i.e., every point [x] in which
+ <<[0, B)>> for which the interference bound function changes, i.e., every point [x] in which
[interference_bound_function (A - ε, x)] is not equal to [interference_bound_function (A, x)]. *)
Definition is_in_search_space A :=
A = 0 \/
diff --git a/analysis/definitions/busy_interval.v b/analysis/definitions/busy_interval.v
index 87c413a2b..137ac75a4 100644
--- a/analysis/definitions/busy_interval.v
+++ b/analysis/definitions/busy_interval.v
@@ -40,7 +40,7 @@ Section BusyIntervalJLFP.
completed_by sched j_hp t.
(** Based on the definition of quiet time, we say that interval
- [t1, t_busy) is a (potentially unbounded) busy-interval prefix
+ <<[t1, t_busy)>> is a (potentially unbounded) busy-interval prefix
iff the interval starts with a quiet time where a higher or equal
priority job is released and remains non-quiet. We also require
job j to be released in the interval. *)
@@ -50,7 +50,7 @@ Section BusyIntervalJLFP.
(forall t, t1 < t < t_busy -> ~ quiet_time t) /\
t1 <= job_arrival j < t_busy.
- (** 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 (t1 t2 : instant) :=
busy_interval_prefix t1 t2 /\
diff --git a/analysis/definitions/priority_inversion.v b/analysis/definitions/priority_inversion.v
index 073333a9d..a0363b490 100644
--- a/analysis/definitions/priority_inversion.v
+++ b/analysis/definitions/priority_inversion.v
@@ -46,7 +46,7 @@ Section CumulativePriorityInversion.
else false.
(** Then we compute the cumulative priority inversion incurred by
- a job within some time interval [t1, t2). *)
+ a job within some time interval <<[t1, t2)>>. *)
Definition cumulative_priority_inversion (t1 t2 : instant) :=
\sum_(t1 <= t < t2) is_priority_inversion t.
diff --git a/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
index f69f2ca2d..e8f65b867 100644
--- a/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ -36,12 +36,12 @@ Section ScheduleOfTask.
Definition task_service_at (t : instant) := task_scheduled_at t.
(** Based on the notion of instantaneous service, we define the
- cumulative service received by [tsk] during any interval [t1, t2)... *)
+ cumulative service received by [tsk] during any interval <<[t1, t2)>>... *)
Definition task_service_during (t1 t2 : instant) :=
\sum_(t1 <= t < t2) task_service_at t.
(** ...and the cumulative service received by [tsk] up to time t2,
- i.e., in the interval [0, t2). *)
+ i.e., in the interval <<[0, t2)>>. *)
Definition task_service (t2 : instant) := task_service_during 0 t2.
End ScheduleOfTask.
diff --git a/analysis/facts/behavior/service.v b/analysis/facts/behavior/service.v
index c320cbec6..451869ca5 100644
--- a/analysis/facts/behavior/service.v
+++ b/analysis/facts/behavior/service.v
@@ -53,7 +53,7 @@ Section Composition.
Qed.
(** 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)
+ 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.) *)
Lemma service_during_cat:
@@ -114,7 +114,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:
@@ -518,7 +518,7 @@ Section RelationToScheduled.
Hypothesis H_same_service: service sched j t1 = service sched j t2.
(** First, we observe that this means that the job receives no service
- during [t1, t2)... *)
+ during <<[t1, t2)>>... *)
Lemma constant_service_implies_no_service_during:
service_during sched j t1 t2 = 0.
Proof.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index f00b5b9f4..8f0607e8c 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -68,7 +68,7 @@ Section ExistsBusyIntervalJLFP.
(** Assume that the priority relation is reflexive. *)
Hypothesis H_priority_is_reflexive : reflexive_priorities.
- (** Consider any busy interval [t1, t2) of job [j]. *)
+ (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval : busy_interval t1 t2.
@@ -137,7 +137,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_priority_is_reflexive : reflexive_priorities.
Hypothesis H_priority_is_transitive : transitive_priorities.
- (** Consider any busy interval prefix [t1, t2). *)
+ (** Consider any busy interval prefix <<[t1, t2)>>. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix t1 t2.
@@ -216,7 +216,7 @@ Section ExistsBusyIntervalJLFP.
by exists jhp; apply SE1; rewrite in_cons; apply/orP; left.
Qed.
- (** We prove that at any time instant [t] within [t1, t2) the processor is not idle. *)
+ (** We prove that at any time instant [t] within <<[t1, t2)>> the processor is not idle. *)
Lemma not_quiet_implies_not_idle:
forall t,
t1 <= t < t2 ->
@@ -254,7 +254,7 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_no_quiet_time : forall t, t1 < t <= t1 + Δ -> ~ quiet_time t.
(** For clarity, we introduce a notion of the total service of jobs released in
- time interval [t_beg, t_end) during the time interval [t1, t1 + Δ). *)
+ time interval <<[t_beg, t_end)>> during the time interval [t1, t1 + Δ). *)
Let service_received_by_hep_jobs_released_during t_beg t_end :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t_beg t_end) j t1 (t1 + Δ).
@@ -289,7 +289,7 @@ Section ExistsBusyIntervalJLFP.
Qed.
(** Next we prove that the total service within a "non-quiet"
- time interval [t1, t1 + Δ) is exactly Δ. *)
+ time interval <<[t1, t1 + Δ)>> is exactly Δ. *)
Lemma no_idle_time_within_non_quiet_time_interval:
service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
Proof.
@@ -353,12 +353,12 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_priority_is_transitive: transitive_priorities.
(** Next, we recall the notion of workload of all jobs released in a given interval
- [t1, t2) that have higher-or-equal priority w.r.t the job j being analyzed. *)
+ <<[t1, t2)>> that have higher-or-equal priority w.r.t the job j being analyzed. *)
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs j (arrivals_between t1 t2).
(** With regard to the jobs with higher-or-equal priority that are released
- in a given interval [t1, t2), we also recall the service received by these
+ in a given interval <<[t1, t2)>>, we also recall the service received by these
jobs in the same interval [t1, t2). *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
@@ -457,7 +457,7 @@ Section ExistsBusyIntervalJLFP.
(** Since the interval is always non-quiet, the processor is always busy
with tasks of higher-or-equal priority or some lower priority job which was scheduled,
- i.e., the sum of service done by jobs with actual arrival time in [t1, t1 + delta)
+ i.e., the sum of service done by jobs with actual arrival time in <<[t1, t1 + delta)>>
and priority inversion equals delta. *)
Lemma busy_interval_has_uninterrupted_service:
delta <= priority_inversion_bound + hp_service t1 (t1 + delta).
@@ -628,7 +628,7 @@ Section ExistsBusyIntervalJLFP.
infer that there is a time in which j is pending. *)
Hypothesis H_positive_cost: job_cost j > 0.
- (** Therefore there must exists a busy interval [t1, t2) that
+ (** Therefore there must exists a busy interval <<[t1, t2)>> that
contains the arrival time of j. *)
Corollary exists_busy_interval:
exists t1 t2,
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index ba87af2fd..cbebcf2f9 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -112,11 +112,11 @@ Section ExistsNoCarryIn.
(** Let the priority relation be reflexive. *)
Hypothesis H_priority_is_reflexive: reflexive_priorities.
- (** Recall the notion of workload of all jobs released in a given interval [t1, t2)... *)
+ (** Recall the notion of workload of all jobs released in a given interval <<[t1, t2)>>... *)
Let total_workload t1 t2 :=
workload_of_jobs predT (arrivals_between t1 t2).
- (** ... and total service of jobs within some time interval [t1, t2). *)
+ (** ... and total service of jobs within some time interval <<[t1, t2)>>. *)
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between 0 t2) t1 t2.
@@ -155,7 +155,7 @@ Section ExistsNoCarryIn.
Hypothesis H_no_carry_in: no_carry_in t.
(** First, recall that the total service is bounded by the total workload. Therefore
- the total service of jobs in the interval [t, t + Δ) is bounded by Δ. *)
+ the total service of jobs in the interval <<[t, t + Δ)>> is bounded by Δ. *)
Lemma total_service_is_bounded_by_Δ :
total_service t (t + Δ) <= Δ.
Proof.
@@ -198,7 +198,7 @@ Section ExistsNoCarryIn.
by apply idle_instant_implies_no_carry_in_at_t.
Qed.
- (** In the second case, the total service within the time interval [t, t + Δ) is equal to Δ.
+ (** In the second case, the total service within the time interval <<[t, t + Δ)>> is equal to Δ.
On the other hand, we know that the total workload is lower-bounded by the total service
and upper-bounded by Δ. Therefore, the total workload is equal to total service this
implies completion of all jobs by time [t + Δ] and hence no carry-in at time [t + Δ]. *)
@@ -267,7 +267,7 @@ Section ExistsNoCarryIn.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
- (** We show that there must exist a busy interval [t1, t2) that
+ (** We show that there must exist a busy interval <<[t1, t2)>> that
contains the arrival time of j. *)
Corollary exists_busy_interval_from_total_workload_bound :
exists t1 t2,
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 1e57c0fa7..173658b44 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -167,7 +167,7 @@ Section PriorityInversionIsBounded.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
- (** Consider any busy interval prefix [t1, t2) of job j. *)
+ (** Consider any busy interval prefix <<[t1, t2)>> of job j. *)
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix:
busy_interval_prefix arr_seq sched j t1 t2.
@@ -182,7 +182,7 @@ Section PriorityInversionIsBounded.
busy scheduling a job with higher or equal priority. *)
Section ProcessorBusyWithHEPJobAtPreemptionPoints.
- (** Consider an arbitrary preemption time t ∈ [t1,t2). *)
+ (** Consider an arbitrary preemption time t ∈ <<[t1,t2)>>. *)
Variable t : instant.
Hypothesis H_t_in_busy_interval : t1 <= t < t2.
Hypothesis H_t_preemption_time : preemption_time sched t.
@@ -497,7 +497,7 @@ Section PriorityInversionIsBounded.
Qed.
(** Also, we show that lower-priority jobs that are scheduled inside the
- busy-interval prefix [t1,t2) must arrive before that interval. *)
+ busy-interval prefix <<[t1,t2)>> must arrive before that interval. *)
Lemma low_priority_job_arrives_before_busy_interval_prefix:
forall jlp t,
t1 <= t < t2 ->
@@ -523,7 +523,7 @@ Section PriorityInversionIsBounded.
Qed.
(** Moreover, we show that lower-priority jobs that are scheduled
- inside the busy-interval prefix [t1,t2) must be scheduled
+ inside the busy-interval prefix <<[t1,t2)>> must be scheduled
before that interval. *)
Lemma low_priority_job_scheduled_before_busy_interval_prefix:
forall jlp t,
@@ -662,7 +662,7 @@ Section PriorityInversionIsBounded.
Qed.
(** Thanks to the fact that the scheduler respects the notion of preemption points
- we show that [jlp] is continuously scheduled in time interval [[t1, t1 + fpt)]. *)
+ we show that [jlp] is continuously scheduled in time interval <<[t1, t1 + fpt)>>. *)
Lemma continuously_scheduled_between_preemption_points:
forall t',
t1 <= t' < t1 + fpt ->
diff --git a/analysis/facts/model/ideal_schedule.v b/analysis/facts/model/ideal_schedule.v
index 3f6178e6b..f2c7ed3f6 100644
--- a/analysis/facts/model/ideal_schedule.v
+++ b/analysis/facts/model/ideal_schedule.v
@@ -103,7 +103,7 @@ Section IncrementalService.
Variable sched : schedule (ideal.processor_state Job).
(** As a base case, we prove that if a job j receives service in
- some time interval [t1,t2), then there exists a time instant t
+ some time interval <<[t1,t2)>>, then there exists a time instant t
∈ [t1,t2) such that j is scheduled at time t and t is the first
instant where j receives service. *)
Lemma positive_service_during:
@@ -141,7 +141,7 @@ Section IncrementalService.
}
Qed.
- (** Next, we prove that if in some time interval [t1,t2) a job j
+ (** Next, we prove that if in some time interval <<[t1,t2)>> a job j
receives k units of service, then there exists a time instant t ∈
[t1,t2) such that j is scheduled at time t and service of job j
within interval [t1,t) is equal to k. *)
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 0cc9bc935..596b58d7e 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -70,7 +70,7 @@ Section GenericModelLemmas.
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)
@@ -100,7 +100,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). *)
@@ -154,7 +154,7 @@ Section IdealModelLemmas.
Let arrivals_between := arrivals_between arr_seq.
Let completed_by := completed_by sched.
- (** We prove that if the total service within some time interval [[t1,t2)]
+ (** We prove that if the total service within some time interval <<[t1,t2)>>
is smaller than [t2-t1], then there is an idle time instant t ∈ [[t1,t2)]. *)
Lemma low_service_implies_existence_of_idle_time :
forall t1 t2,
@@ -272,10 +272,10 @@ Section IdealModelLemmas.
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]. *)
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index f186f8015..6cda84bf7 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -109,7 +109,7 @@ Section ArrivalSequencePrefix.
Variable arr_seq: arrival_sequence Job.
(** By concatenation, we construct the list of jobs that arrived in the
- interval [t1, t2). *)
+ interval <<[t1, t2)>>. *)
Definition arrivals_between (t1 t2 : instant) :=
\cat_(t1 <= t < t2) arrivals_at arr_seq t.
diff --git a/model/aggregate/service_of_jobs.v b/model/aggregate/service_of_jobs.v
index 58ce7d540..0771d2ce7 100644
--- a/model/aggregate/service_of_jobs.v
+++ b/model/aggregate/service_of_jobs.v
@@ -39,7 +39,7 @@ Section ServiceOfJobs.
\sum_(j <- jobs | P j) service_at sched j t.
(** ... and the cumulative service received during the interval
- [[t1, t2)] by jobs that satisfy predicate [P]. *)
+ <<[t1, t2)>> by jobs that satisfy predicate [P]. *)
Definition service_of_jobs (t1 t2 : instant) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
@@ -61,7 +61,7 @@ Section ServiceOfJobs.
(** Based on the definition of jobs of higher or equal priority, ... *)
Let of_higher_or_equal_priority j_hp := hep_job j_hp j.
- (** ...we define the service received during [[t1, t2)] by jobs of higher or equal priority. *)
+ (** ...we define the service received during <<[t1, t2)>> by jobs of higher or equal priority. *)
Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
@@ -78,7 +78,7 @@ Section ServiceOfJobs.
Variable jobs : seq Job.
(** We define the cumulative task service received by the jobs of
- task [tsk] within time interval [[t1, t2)]. *)
+ task [tsk] within time interval <<[t1, t2)>>. *)
Definition task_service_of_jobs_in t1 t2 :=
service_of_jobs (job_of_task tsk) jobs t1 t2.
diff --git a/model/task/arrival/curves.v b/model/task/arrival/curves.v
index 555230832..b8138bf22 100644
--- a/model/task/arrival/curves.v
+++ b/model/task/arrival/curves.v
@@ -65,7 +65,7 @@ Section ArrivalCurves.
monotone num_arrivals leq.
(** We say that [max_arrivals] is an upper arrival bound for task [tsk]
- iff, for any interval [[t1, t2)], [max_arrivals (t2 - t1)] bounds the
+ iff, for any interval <<[t1, t2)>>, [max_arrivals (t2 - t1)] bounds the
number of jobs of [tsk] that arrive in that interval. *)
Definition respects_max_arrivals (tsk : Task) (max_arrivals : duration -> nat) :=
forall (t1 t2 : instant),
diff --git a/model/task/arrivals.v b/model/task/arrivals.v
index 68d26224c..e3365e5a9 100644
--- a/model/task/arrivals.v
+++ b/model/task/arrivals.v
@@ -17,7 +17,7 @@ Section TaskArrivals.
Variable tsk : Task.
(** First, we construct the list of jobs of task [tsk] that arrive
- in a given half-open interval [[t1, t2)]. *)
+ in a given half-open interval <<[t1, t2)>>. *)
Definition task_arrivals_between (t1 t2 : instant) :=
[seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index b79368c00..bb9c97270 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -305,7 +305,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
Hypothesis H_job_of_tsk : job_task j = tsk.
Hypothesis H_job_cost_positive: job_cost_positive j.
- (** Consider any busy interval [t1, t2) of job [j]. *)
+ (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
Variable t1 t2 : duration.
Hypothesis H_busy_interval :
definitions.busy_interval sched interference interfering_workload j t1 t2.
--
GitLab