.gitlab-ci.yml

@@ -155,7 +155,7 @@ spell-check:
   extends:  
     - .not_in_wip_branches  
   stage: build
-  image: bbbrandenburg/aspell-ci
+  image: bbbrandenburg/hunspell:2022-08
   script:
     - scripts/flag-typos-in-comments.sh `find .  -iname '*.v' ! -path './classic/*'`
 

analysis/abstract/abstract_rta.v

@@ -123,7 +123,7 @@ Section Abstract_RTA.
     Variable t1 t2: instant.
     Hypothesis H_busy_interval: busy_interval j t1 t2.
     
-    (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+    (** Let's define [A] as a relative arrival time of job [j] (with respect to time [t1]). *)
     Let A := job_arrival j - t1.
 
     (** In order to prove that R is a response-time bound of job j, we use hypothesis H_R_is_maximum. 
@@ -164,7 +164,7 @@ Section Abstract_RTA.
        interval remains completed. *)
     Section FixpointOutsideBusyInterval.
 
-      (** By assumption, suppose that t2 is less than or equal to [t1 + A_sp + F_sp]. *)
+      (** By assumption, suppose that [t2] is less than or equal to [t1 + A_sp + F_sp]. *)
       Hypothesis H_big_fixpoint_solution : t2 <= t1 + (A_sp + F_sp).
 
       (** Then we prove that [job_arrival j + R] is no less than [t2]. *)
@@ -198,7 +198,7 @@ Section Abstract_RTA.
        [t1 + A_sp + F_sp] lies inside the busy interval. *)
     Section FixpointInsideBusyInterval.
 
-      (** So, assume that [t1 + A_sp + F_sp] is less than t2. *) 
+      (** So, assume that [t1 + A_sp + F_sp] is less than [t2]. *) 
       Hypothesis H_small_fixpoint_solution : t1 + (A_sp + F_sp) < t2.
 
       (** Next, let's consider two other cases: *)
@@ -221,7 +221,7 @@ Section Abstract_RTA.
           Variable F : duration.
           (** (a) the sum of [A_sp] and [F_sp] is equal to the sum of [A] and [F]... *)
           Hypothesis H_Asp_Fsp_eq_A_F : A_sp + F_sp = A + F.
-          (** (b) [F] is at mo1st [F_sp]... *)
+          (** (b) [F] is at most [F_sp]... *)
           Hypothesis H_F_le_Fsp : F <= F_sp.
           (** (c) and [A + F] is a solution for the response-time recurrence for [A]. *)
           Hypothesis H_A_F_fixpoint:

analysis/abstract/abstract_seq_rta.v

@@ -220,7 +220,7 @@ Section Sequential_Abstract_RTA.
       Hypothesis H_j2_from_tsk: job_of_task tsk j2.
       Hypothesis H_j1_cost_positive: job_cost_positive j1.
 
-      (** Consider the busy interval <<[t1, t2)>> of job j1. *)
+      (** Consider the busy interval <<[t1, t2)>> of job [j1]. *)
       Variable t1 t2 : instant.
       Hypothesis H_busy_interval : busy_interval j1 t1 t2.
 
@@ -241,7 +241,7 @@ Section Sequential_Abstract_RTA.
       Qed.
 
       (** Next we prove that if a job is pending after the beginning
-         of the busy interval <<[t1, t2)>> then it arrives after t1. *)
+         of the busy interval <<[t1, t2)>> then it arrives after [t1]. *)
       Lemma arrives_after_beginning_of_busy_interval:
         forall t,
           t1 <= t ->
@@ -280,14 +280,14 @@ Section Sequential_Abstract_RTA.
       Variable t1 t2 : instant.
       Hypothesis H_busy_interval : busy_interval j t1 t2.
 
-      (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+      (** Let's define [A] as a relative arrival time of job [j] (with respect to time [t1]). *)
       Let A : duration := job_arrival j - t1.
 
       (** Consider an arbitrary time x ... *)
       Variable x : duration.
-      (** ... such that (t1 + x) is inside the busy interval... *)
+      (** ... such that [(t1 + x)] is inside the busy interval... *)
       Hypothesis H_inside_busy_interval : t1 + x < t2.
-      (** ... and job j is not completed by time (t1 + x). *)
+      (** ... and job [j] is not completed by time [(t1 + x)]. *)
       Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + x).
 
       (** In this section, we show that the cumulative interference of job j in the interval <<[t1, t1 + x)>>
@@ -549,8 +549,8 @@ Section Sequential_Abstract_RTA.
         Qed.
 
         (** Finally, we show that the cumulative interference of job j in the interval <<[t1, t1 + x)>>
-           is bounded by the sum of the task workload in the interval [t1, t1 + A + ε) and
-           the cumulative interference of [j]'s task in the interval [t1, t1 + x). *)
+           is bounded by the sum of the task workload in the interval <<[t1, t1 + A + ε)>> and
+           the cumulative interference of [j]'s task in the interval <<[t1, t1 + x)>>. *)
         Lemma cumulative_job_interference_le_task_interference_bound:
           cumul_interference j t1 (t1 + x)
           <= (task_workload_between t1 (t1 + A + ε) - job_cost j)

analysis/abstract/definitions.v

@@ -96,7 +96,7 @@ Section AbstractRTADefinitions.
         (forall t, t1 < t < t2 -> ~ quiet_time j t). 
 
       (** Next, we say that an interval <<[t1, t2)>> is a busy interval iff
-         [t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
+          <<[t1, t2)>> is a busy-interval prefix and [t2] is a quiet time. *)
       Definition busy_interval (j : Job) (t1 t2 : instant) :=
         busy_interval_prefix j t1 t2 /\
         quiet_time j t2.

analysis/abstract/run_to_completion.v

@@ -57,9 +57,9 @@ Section AbstractRTARunToCompletionThreshold.
   Hypothesis H_busy_interval : busy_interval j t1 t2.
 
   (** First, we prove that job [j] completes by the end of the busy interval.
-     Note that the busy interval contains the execution of job j, in addition
-     time instant t2 is a quiet time. Thus by the definition of a quiet time
-     the job should be completed before time t2. *)
+      Note that the busy interval contains the execution of job j, in addition
+      time instant [t2] is a quiet time. Thus by the definition of a quiet time
+      the job should be completed before time [t2]. *)
   Lemma job_completes_within_busy_interval:
     completed_by sched j t2.
   Proof.
@@ -74,7 +74,7 @@ Section AbstractRTARunToCompletionThreshold.
      the total time where job [j] is scheduled inside the busy interval. *)
   Section InterferenceIsComplement.
 
-    (** Consider any sub-interval <<[t, t + delta)>> inside the busy interval [t1, t2). *)
+    (** Consider any sub-interval <<[t, t + delta)>> inside the busy interval <<[t1, t2)>>. *)
     Variables (t : instant) (delta : duration).
     Hypothesis H_greater_than_or_equal : t1 <= t.
     Hypothesis H_less_or_equal: t + delta <= t2.

analysis/facts/behavior/arrivals.v

@@ -275,7 +275,7 @@ Section ArrivalSequencePrefix.
     Qed.
 
     (** Next, we prove that if a job belongs to the prefix
-        (jobs_arrived_before t), then it arrives in the arrival
+        [(jobs_arrived_before t)], then it arrives in the arrival
         sequence. *)
     Lemma in_arrivals_implies_arrived:
       forall j t1 t2,
@@ -291,16 +291,16 @@ Section ArrivalSequencePrefix.
     Proof. by move=> t ? ?; exists t. Qed.
 
     (** Next, we prove that if a job belongs to the prefix
-         (jobs_arrived_between t1 t2), then it indeed arrives between t1 and
-         t2. *)
+         [(jobs_arrived_between t1 t2)], then it indeed arrives between [t1] and
+         [t2]. *)
     Lemma in_arrivals_implies_arrived_between:
       forall j t1 t2,
         j \in arrivals_between arr_seq t1 t2 ->
         arrived_between j t1 t2.
     Proof. by move=> ? ? ? /mem_bigcat_nat_exists[t0 [/job_arrival_at <-]]. Qed.
 
-    (** Similarly, if a job belongs to the prefix (jobs_arrived_before t),
-           then it indeed arrives before time t. *)
+    (** Similarly, if a job belongs to the prefix [(jobs_arrived_before t)],
+         then it indeed arrives before time [t]. *)
     Lemma in_arrivals_implies_arrived_before:
       forall j t,
         j \in arrivals_before arr_seq t ->
@@ -308,7 +308,7 @@ Section ArrivalSequencePrefix.
     Proof. by move=> ? ? /in_arrivals_implies_arrived_between. Qed.
 
     (** Similarly, we prove that if a job from the arrival sequence arrives
-        before t, then it belongs to the sequence (jobs_arrived_before t). *)
+        before t, then it belongs to the sequence [(jobs_arrived_before t)]. *)
     Lemma arrived_between_implies_in_arrivals:
       forall j t1 t2,
         arrives_in arr_seq j ->

analysis/facts/behavior/service.v

@@ -94,7 +94,7 @@ Section Composition.
   Proof. move=> ?; exact: service_during_last_plus_before. Qed.
 
   (** Finally, we deconstruct the service received during an interval <<[t1, t3)>>
-     into the service at a midpoint t2 and the service in the intervals before
+     into the service at a midpoint [t2] and the service in the intervals before
      and after. *)
   Lemma service_split_at_point:
     forall t1 t2 t3,

analysis/facts/model/rbf.v

@@ -242,7 +242,7 @@ Section RequestBoundFunctions.
 
   (** Let [max_arrivals] be a family of valid arrival curves, i.e., for any task [tsk] in [ts]
      [max_arrival tsk] is (1) an arrival bound of [tsk], and (2) it is a monotonic function
-     that equals 0 for the empty interval Δ = 0. *)
+     that equals 0 for the empty interval [Δ = 0]. *)
   Context `{MaxArrivals Task}.
   Hypothesis H_valid_arrival_curve : valid_arrival_curve (max_arrivals tsk).
   Hypothesis H_is_arrival_curve : respects_max_arrivals arr_seq tsk (max_arrivals tsk).
@@ -388,10 +388,10 @@ Section TotalRBFMonotonic.
 
 End TotalRBFMonotonic.
 
-(** ** RBFs Equal to Zero for Duration ε *)
+(** ** RBFs Equal to Zero for Duration [ε] *)
 
 (** In the following section, we derive simple properties that follow in
-    the pathological case of an RBF that yields zero for duration ε. *)
+    the pathological case of an RBF that yields zero for duration [ε]. *)
 Section DegenerateTotalRBFs.
 
   (** Consider a set of tasks characterized by WCETs and arrival curves ... *)

analysis/facts/preemption/job/preemptive.v

@@ -45,7 +45,7 @@ Section FullyPreemptiveModel.
       by rewrite H1; compute.
   Qed.
 
-  (** ... or ε when [job_cost j > 0]. *)  
+  (** ... or [ε] when [job_cost j > 0]. *)  
   Lemma job_max_nps_is_ε:
     forall j,
       job_cost j > 0 -> 

analysis/facts/preemption/rtc_threshold/nonpreemptive.v

@@ -47,7 +47,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
       by rewrite H3; compute.
   Qed.
   
-  (** ... and ε otherwise. *)
+  (** ... and [ε] otherwise. *)
   Fact job_rtc_threshold_is_ε:
     forall j,
       job_cost j > 0 ->

analysis/facts/transform/edf_opt.v

@@ -97,7 +97,7 @@ Section FindSwapCandidateFacts.
   (** Since we are considering a uniprocessor model, only one job is
      scheduled at a time. Hence once we know that a job is scheduled
      at the time that [find_swap_candidate] returns, we can conclude
-     that it arrives not later than at time t1. *)
+     that it arrives not later than at time [t1]. *)
   Corollary fsc_found_job_arrival:
     forall j2,
       scheduled_at sched j2 (find_swap_candidate sched t1 j1) ->

analysis/facts/transform/edf_wc.v

@@ -219,7 +219,7 @@ Section FSCWorkConservationLemmas.
     - by apply (non_idle_swap_maintains_work_conservation_t1 arr_seq _ _ _ j2).
     - case: (boolP(t == t2)) => [/eqP EQ'| /eqP NEQ'].
       + by apply (non_idle_swap_maintains_work_conservation_t2 arr_seq _ _ _ j1).
-      + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET]. (* t <> t2 *)
+      + case: (boolP((t <= t1) || (t2 < t))) => [NOT_BET | BET].
         * move: NOT_BET; move/orP => [] => NOT_BET.
           { by apply (non_idle_swap_maintains_work_conservation_LEQ_t1 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j).  }
           { by apply (non_idle_swap_maintains_work_conservation_GT_t2 arr_seq _ _ _ H_range _ _ H_not_idle t2_not_idle j). }

analysis/facts/transform/swaps.v

@@ -18,11 +18,11 @@ Section SwappedFacts.
   Variable t1 t2: instant.
 
   (** In the following, let [sched'] denote the schedule in which the
-     allocations at [t1] and [t2] have been swapped. *)
+      allocations at [t1] and [t2] have been swapped. *)
   Let sched' := swapped sched t1 t2.
   
-  (** First, we note that the trivial case where t1 == t2 is not interesting
-     because then the two schedules are identical. *)
+  (** First, we note that the trivial case where [t1 == t2] is not interesting
+      because then the two schedules are identical. *)
   Lemma trivial_swap:
     t1 = t2 ->
     forall t,
@@ -58,8 +58,8 @@ Section SwappedFacts.
     by rewrite /sched' /swapped !rest_of_schedule_invariant //.
   Qed.
 
-  (** By definition, if a job is scheduled at t2 in the original
-     schedule, then it is found at t1 in the new schedule. *)
+  (** By definition, if a job is scheduled at [t2] in the original
+     schedule, then it is found at [t1] in the new schedule. *)
   Lemma swap_job_scheduled_t1:
     forall j,
       scheduled_at sched' j t1 =
@@ -72,8 +72,8 @@ Section SwappedFacts.
     - by rewrite ifT.
   Qed.
 
-  (** Similarly, a job scheduled at t1 in the original schedule is
-     scheduled at t2 after the swap. *)
+  (** Similarly, a job scheduled at [t1] in the original schedule is
+     scheduled at [t2] after the swap. *)
   Lemma swap_job_scheduled_t2:
     forall j,
       scheduled_at sched' j t2 =
@@ -189,11 +189,11 @@ Section SwappedFacts.
       service received. *)
   
   (** To avoid dealing with symmetric cases, assume in the following
-     that t1 and t2 are ordered. *)
+     that [t1] and [t2] are ordered. *)
   Hypothesis H_well_ordered: t1 <= t2.
 
   (** As another trivial invariant, we observe that nothing has changed
-     before time t1. *)
+     before time [t1]. *)
   Lemma swap_before_invariant:
     forall t,
       t < t1 ->
@@ -205,7 +205,7 @@ Section SwappedFacts.
        [move: t_lt_t1|move: t_lt_t2]; rewrite ltnn.
   Qed.
 
-  (** Similarly, nothing has changed after time t2. *)
+  (** Similarly, nothing has changed after time [t2]. *)
   Lemma swap_after_invariant:
     forall t,
       t2 < t ->
@@ -217,7 +217,7 @@ Section SwappedFacts.
        [move: t1_lt_t|move: t2_lt_t]; rewrite ltnn.
   Qed.
 
-  (** Thus, we observe that, before t1, the two schedules are identical with
+  (** Thus, we observe that, before [t1], the two schedules are identical with
      regard to the service received by any job because they are identical. *)
   Corollary service_before_swap_invariant:
     forall t,
@@ -232,7 +232,7 @@ Section SwappedFacts.
       by apply ltnW.
   Qed.
 
-  (** Likewise, we observe that, *after* t2, the swapped schedule again does not
+  (** Likewise, we observe that, *after* [t2], the swapped schedule again does not
      differ with regard to the service received by any job. *)
   Lemma service_after_swap_invariant:
     forall t,
@@ -379,8 +379,8 @@ Section EDFSwap.
   (** ...that are ordered. *)
   Hypothesis H_well_ordered: t1 <= t2.
 
-  (** Further, assume that, if there are jobs scheduled at times t1 and t2, then
-     they either have the same deadline or violate EDF, ... *)
+  (** Further, assume that, if there are jobs scheduled at times [t1] and [t2], then
+      they either have the same deadline or violate EDF, ... *)
   Hypothesis H_not_EDF:
     forall j1 j2,
       scheduled_at sched j1 t1 ->
@@ -388,14 +388,14 @@ Section EDFSwap.
       job_deadline j1 >=  job_deadline j2.
 
   (** ...and that we don't move idle times or deadline misses earlier,
-     i.e., if t1 is not an idle time, then neither is t2 and whatever
-     job is scheduled at time t2 has not yet missed its deadline. *)
+     i.e., if [t1] is not an idle time, then neither is [t2] and whatever
+     job is scheduled at time [t2] has not yet missed its deadline. *)
   Hypothesis H_no_idle_time_at_t2:
     forall j1,
       scheduled_at sched j1 t1 ->
       exists j2, scheduled_at sched j2 t2 /\ job_deadline j2 > t2.
 
-  (** Consider the schedule obtained from swapping the allocations at times t1 and t2. *)
+  (** Consider the schedule obtained from swapping the allocations at times [t1] and [t2]. *)
   Let sched' := swapped sched t1 t2.
 
   (** The key property of this transformation is that, for any job that
@@ -423,7 +423,7 @@ Section EDFSwap.
     Qed.
 
     (** Next, we observe that a swap is unproblematic for the job scheduled at
-       time t2. *)
+       time [t2]. *)
     Lemma moved_earlier_implies_deadline_met:
       scheduled_at sched j t2 ->
       job_meets_deadline sched' j.
@@ -453,7 +453,7 @@ Section EDFSwap.
 
   (** From the above case analysis, we conclude that no deadline misses
      are introduced in the schedule obtained from swapping the
-     allocations at times t1 and t2. *)
+     allocations at times [t1] and [t2]. *)
   Theorem edf_swap_no_deadline_misses_introduced:
     forall j, job_meets_deadline sched j -> job_meets_deadline sched' j.
   Proof.

behavior/arrival_sequence.v

@@ -81,16 +81,16 @@ Section ArrivalTimeProperties.
   (** Let j be any job. *)
   Variable j: Job.
 
-  (** We say that job j has arrived at time t iff it arrives at some time t_0
-     with t_0 <= t. *)
+  (** We say that job j has arrived at time [t] iff it arrives at some time [t_0]
+      with [t_0 <= t]. *)
   Definition has_arrived (t : instant) := job_arrival j <= t.
 
   (** Next, we say that job j arrived before t iff it arrives at some time t_0
-     with t_0 < t. *)
+      with t_0 < t. *)
   Definition arrived_before (t : instant) := job_arrival j < t.
 
-  (** Finally, we say that job j arrives between t1 and t2 iff it arrives at
-     some time t with t1 <= t < t2. *)
+  (** Finally, we say that job j arrives between [t1] and [t2] iff it arrives at
+      some time [t] with [t1 <= t < t2]. *)
   Definition arrived_between (t1 t2 : instant) := t1 <= job_arrival j < t2.
 
 End ArrivalTimeProperties.

implementation/refinements/arrival_curve.v

@@ -15,7 +15,7 @@ Definition get_horizon_of_task (tsk : Task) : duration :=
 Definition get_time_steps_of_task (tsk : Task) : seq duration :=
   time_steps_of (get_arrival_curve_prefix tsk).
 
-(** ... a function that yields the same time steps, offset by δ, ...**)
+(** ... a function that yields the same time steps, offset by [δ], ...**)
 Definition time_steps_with_offset tsk δ := [seq t + δ | t <- get_time_steps_of_task tsk].
 
 (** ... and a generalization of the previous function that repeats the time

implementation/refinements/task.v

@@ -84,7 +84,7 @@ Section Definitions.
   Definition get_time_steps_of_task_T (tsk : task_T) : seq T :=
     time_steps_of_T (get_extrapolated_arrival_curve_T tsk).
 
-  (** ... a function that yields the same time steps, offset by δ, ... *)
+  (** ... a function that yields the same time steps, offset by [δ], ... *)
   Definition time_steps_with_offset_T tsk δ :=
     [seq t + δ | t <- get_time_steps_of_task_T tsk]%C.
 

model/schedule/edf.v

@@ -7,8 +7,8 @@ Require Export prosa.behavior.all.
     "EDF schedule".
 
     Note that the "proper" way to define an EDF schedule in Prosa is to use the
-    EDF priority policy defined in model.priority.edf and the notion of
-    priority-compliant schedules defined in model.schedule.priority_driven, as
+    EDF priority policy defined in [model.priority.edf] and the notion of
+    priority-compliant schedules defined in [model.schedule.priority_driven], as
     well as the general notion of work-conservation provided in
     model.schedule.work_conserving, which will have the benefit of taking into
     account issues such as various readiness models (e.g., jitter) and diverse

model/task/preemption/fully_nonpreemptive.v

@@ -30,7 +30,7 @@ Section TaskRTCThresholdFullyNonPreemptive.
   (** In the fully non-preemptive model, no job can be preempted prior to its
       completion. In other words, once a job starts running, it is guaranteed
       to finish. Thus, we can set the task-level run-to-completion threshold
-      to ε. *)
+      to [ε]. *)
   Definition fully_nonpreemptive_rtc_threshold : TaskRunToCompletionThreshold Task :=
     fun tsk : Task => ε.
 

model/task/preemption/fully_preemptive.v

@@ -11,7 +11,7 @@ Section FullyPreemptiveModel.
   Context {Task : TaskType}.
 
   (** In the fully preemptive model, any job can be preempted at any
-      time. Thus, the maximal non-preemptive segment has length at most ε
+      time. Thus, the maximal non-preemptive segment has length at most [ε]
       (i.e., one time unit such as a processor cycle). *)
   Definition fully_preemptive_task_model : TaskMaxNonpreemptiveSegment Task :=
     fun tsk : Task => ε.

results/edf/rta/bounded_pi.v

@@ -231,17 +231,17 @@ Section AbstractRTAforEDFwithArrivalCurves.
         Hypothesis H_busy_interval :
           definitions.busy_interval sched interference interfering_workload j t1 t2.
 
-        (** Let's define A as a relative arrival time of job j (with respect to time t1). *)
+        (** Let's define A as a relative arrival time of job j (with respect to time [t1]). *)
         Let A := job_arrival j - t1.
 
-        (** Consider an arbitrary shift Δ inside the busy interval ...  *)
+        (** Consider an arbitrary offset [Δ] inside the busy interval ...  *)
         Variable Δ : duration.
         Hypothesis H_Δ_in_busy : t1 + Δ < t2.
 
         (** ... and the set of all arrivals between [t1] and [t1 + Δ]. *)
         Let jobs := arrivals_between arr_seq t1 (t1 + Δ).
 
-        (** We define a predicate [EDF_from tsk].Predicate [EDF_from tsk]
+        (** We define a predicate [EDF_from tsk]. The predicate [EDF_from tsk]
             holds true for any job [jo] of task [tsk] such that
             [job_deadline jo <= job_deadline j]. *)
         Let EDF_from (tsk : Task) := fun (jo : Job) => EDF jo j && (job_task jo == tsk).
@@ -355,7 +355,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
 
       (** Given any job j of task [tsk] that arrives exactly A units after the beginning of
          the busy interval, the bound of the total interference incurred by j within an
-         interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
+         interval of length [Δ] is equal to [task_rbf (A + ε) - task_cost tsk + IBF_other(A, Δ)]. *)
       Let total_interference_bound tsk (A Δ : duration) :=
             task_rbf (A + ε) - task_cost tsk + IBF_other A Δ.