From 6929caa19560a4057d12c4c52ecf19a3be08502b Mon Sep 17 00:00:00 2001
From: Vedant Chavda
Date: Fri, 24 Jul 2020 18:02:09 +0530
Subject: [PATCH] polish comments
---
analysis/facts/model/offset.v | 2 +-
analysis/facts/model/task_arrivals.v | 5 ++--
analysis/facts/periodic/arrival_separation.v | 10 ++++----
analysis/facts/periodic/sporadic.v | 9 ++++++--
analysis/facts/sporadic.v | 24 +++++++++++---------
model/task/arrival/task_max_inter_arrival.v | 13 ++++++-----
util/list.v | 4 ++--
7 files changed, 38 insertions(+), 29 deletions(-)
diff --git a/analysis/facts/model/offset.v b/analysis/facts/model/offset.v
index ae7398b..f64c274 100644
--- a/analysis/facts/model/offset.v
+++ b/analysis/facts/model/offset.v
@@ -13,7 +13,7 @@ Section OffsetLemmas.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
- (** Consider any unique arrival sequence with consistent arrivals, ... *)
+ (** Consider any arrival sequence with consistent and non-duplicate arrivals, ... *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.
diff --git a/analysis/facts/model/task_arrivals.v b/analysis/facts/model/task_arrivals.v
index 9d49f8c..ef4207e 100644
--- a/analysis/facts/model/task_arrivals.v
+++ b/analysis/facts/model/task_arrivals.v
@@ -103,7 +103,7 @@ Section TaskArrivals.
now rewrite -filter_cat -arrivals_between_cat.
Qed.
- (** We observe that for any job [j], task arrivals up to [job_arrival j] can be split
+ (** We observe that for any job [j], task arrivals up to [job_arrival j] can be split
into task arrivals before [job_arrival j] and task arrivals at [job_arrival j]. *)
Lemma task_arrivals_up_to_cat:
forall j,
@@ -133,7 +133,8 @@ Section TaskArrivals.
now apply arrived_between_implies_in_arrivals.
Qed.
- (** Unique arrival sequence leads to unique task arrivals. *)
+ (** An arrival sequence with non-duplicate arrivals implies that the
+ task arrivals also contain non-duplicate arrivals. *)
Lemma uniq_task_arrivals :
forall j,
arrives_in arr_seq j ->
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 857cea6..c2c1f60 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -41,9 +41,9 @@ Section JobArrivalSeparation.
Hypothesis H_j2_of_task : job_task j2 = tsk.
Hypothesis H_consecutive_jobs : job_index arr_seq j2 = job_index arr_seq j1 + 1.
- (** We show that if [j2] is the next job to arrive after [j1]
- (i.e., [job_index j2] is one greater than [job_index j1]) then
- [j2] arrives one [task_period] after [j1]. *)
+ (** We show that if job [j1] and [j2] are consecutive jobs with [j2]
+ arriving after [j1], then their arrival times are separated by
+ their task's period. *)
Lemma consecutive_job_separation :
job_arrival j2 = job_arrival j1 + task_period tsk.
Proof.
@@ -60,7 +60,7 @@ Section JobArrivalSeparation.
(** In this section we show that for two unequal jobs of a task,
there exists a non-zero multiple of their task's period which separates
their arrival times. *)
- Section ArrivalSeparationOfJobs.
+ Section ArrivalSeparationWithGivenIndexDifference.
(** Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
@@ -117,7 +117,7 @@ Section JobArrivalSeparation.
}
Qed.
- End ArrivalSeparationOfJobs.
+ End ArrivalSeparationWithGivenIndexDifference.
(** Consider any two _distinct_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 19741cd..2a33e69 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -16,8 +16,8 @@ Section PeriodicTasksAsSporadicTasks.
(** Any type of periodic tasks ... *)
Context {Task : TaskType} `{PeriodicModel Task}.
- (** ... and their corresponding jobs from a consistent
- and unique arrival sequence ... *)
+ (** ... and their corresponding jobs from a consistent arrival sequence with
+ non-duplicate arrivals ... *)
Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
Variable arr_seq : arrival_sequence Job.
@@ -62,10 +62,15 @@ Section PeriodicTasksAsSporadicTasks.
(** For convenience, we state these obvious correspondences also at the level
of entire task sets. *)
+
+ (** First, we show that all tasks in a task set with valid periods
+ also have valid min inter-arrival times. *)
Remark valid_periods_are_valid_inter_arrival_times:
forall ts, valid_periods ts -> valid_taskset_inter_arrival_times ts.
Proof. trivial. Qed.
+ (** Second, we show that each task in a periodic task set respects
+ the sporadic task model. *)
Remark periodic_task_sets_respect_sporadic_task_model:
forall ts,
valid_periods ts ->
diff --git a/analysis/facts/sporadic.v b/analysis/facts/sporadic.v
index 5abd731..f35a8e2 100644
--- a/analysis/facts/sporadic.v
+++ b/analysis/facts/sporadic.v
@@ -137,8 +137,8 @@ Section SporadicArrivals.
Hypothesis H_j1_task : job_task j1 = tsk.
Hypothesis H_j2_task : job_task j2 = tsk.
- (** We show that a sporadic task with valid [task_min_inter_arrival_time] cannot
- have more than one job arriving at any time. *)
+ (** We show that a sporadic task with valid min inter-arrival time cannot
+ have more than one job arriving at any time. *)
Lemma size_task_arrivals_at_leq_one :
(exists j,
size (task_arrivals_at_job_arrival arr_seq j) > 1 /\
@@ -159,8 +159,9 @@ Section SporadicArrivals.
now ssromega.
Qed.
- (** No job of task [tsk] arrives at [job_arrival j1] other
- than [j1] itself. *)
+ (** We show that no jobs of the task [tsk] other than [j1] arrive at
+ the same time as [j1], and thus the task arrivals at [job arrival j1]
+ consists only of job [j1]. *)
Lemma only_j_in_task_arrivals_at_j :
task_arrivals_at_job_arrival arr_seq j1 = [::j1].
Proof.
@@ -180,9 +181,9 @@ Section SporadicArrivals.
now repeat split => //; try rewrite H_j1_task.
Qed.
- (** Index of any job [j] in the sequence
- [task_arrivals_at arr_seq (job_task j) (job_arrival j)]
- is zero.*)
+ (** We show that a job [j1] is the first job that arrives
+ in task arrivals at [job_arrival j1] by showing that the
+ index of job [j1] in [task_arrivals_at_job_arrival arr_seq j1] is 0. *)
Lemma index_j_in_task_arrivals_at:
index j1 (task_arrivals_at_job_arrival arr_seq j1) = 0.
Proof.
@@ -207,8 +208,8 @@ Section SporadicArrivals.
now ssromega.
Qed.
- (** We show that [task_arrivals_at_job_arrival arr_seq j1] can be
- written in terms of [task_arrivals_between]. *)
+ (** We show that task arrivals at [job_arrival j1] can be written as
+ task arrivals between [job_arrival j1] and [job_arrival j1 + 1]. *)
Lemma task_arrivals_at_as_task_arrivals_between :
task_arrivals_at_job_arrival arr_seq j1 = task_arrivals_between arr_seq tsk (job_arrival j1) (job_arrival j1).+1.
Proof.
@@ -216,8 +217,9 @@ Section SporadicArrivals.
now rewrite big_nat1 H_j1_task.
Qed.
- (** The sequence [task_arrivals_up_to_job_arrival arr_seq j] can be written as a concatenation
- of [task_arrivals_up_to_job_arrival arr_seq (prev_job j)] and [::j]. *)
+ (** We show that the task arrivals up to the previous job [j1] concatenated with
+ the sequence [::j1] (the sequence containing only the job [j1]) is same as
+ task arrivals up to [job_arrival j1]. *)
Lemma prev_job_cat :
job_index arr_seq j1 > 0 ->
task_arrivals_up_to_job_arrival arr_seq (prev_job arr_seq j1) ++ [::j1] = task_arrivals_up_to_job_arrival arr_seq j1.
diff --git a/model/task/arrival/task_max_inter_arrival.v b/model/task/arrival/task_max_inter_arrival.v
index 65f20c1..da231f5 100644
--- a/model/task/arrival/task_max_inter_arrival.v
+++ b/model/task/arrival/task_max_inter_arrival.v
@@ -1,7 +1,7 @@
Require Export prosa.model.task.concept.
Require Export prosa.model.task.arrivals.
-(** * Task Max Inter Arrival *)
+(** * Task Max Inter-Arrival *)
(** We define a task-model parameter [task_max_inter_arrival_time] as
the maximum time difference between the arrivals of consecutive jobs. *)
@@ -9,7 +9,7 @@ Class TaskMaxInterArrival (Task : TaskType) :=
task_max_inter_arrival_time : Task -> duration.
(** In the following section, we define two properties that a task must satisfy
-for its max inter-arrival time to be valid. *)
+for its maximum inter-arrival time to be valid. *)
Section ValidTaskMaxInterArrival.
(** Consider any type of tasks, ... *)
@@ -24,13 +24,14 @@ Section ValidTaskMaxInterArrival.
(** ... and any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
- (** Firstly, the task max inter-arrival time for a task is positive. *)
+ (** Firstly, the task maximum inter-arrival time for a task is positive. *)
Definition positive_task_max_inter_arrival_time (tsk : Task) :=
task_max_inter_arrival_time tsk > 0.
- (** Secondly, for any job [j] of a task [tsk] except the first one, there exists
- a job [j'] of task [tsk] that arrives before [j] with the arrival
- separation between [j] and [j'] being at most [task_max_inter_arrival_time tsk]. *)
+ (** Secondly, for any job [j] (with a positive [job_index]) of a task [tsk],
+ there exists a job [j'] of task [tsk] that arrives before [j]
+ with [j] not arriving any later than the task maximum inter-arrival
+ time of [tsk] after [j']. *)
Definition arr_sep_task_max_inter_arrival (tsk : Task) :=
forall (j : Job),
arrives_in arr_seq j ->
diff --git a/util/list.v b/util/list.v
index bf407c8..3879b76 100644
--- a/util/list.v
+++ b/util/list.v
@@ -426,8 +426,8 @@ Section AdditionalLemmas.
now rewrite -EQ_a -EQ_b EQ.
Qed.
- (** We prove that the element given by [nth d xs n] in a sequence [xs] either
- lies in [xs] or is equal to [d]. *)
+ (** We show that the nth element in a sequence lies in the
+ sequence or is the default element. *)
Lemma default_or_in :
forall (T : eqType) (n : nat) (d : T) (xs : seq T),
nth d xs n = d \/ nth d xs n \in xs.
--
GitLab