Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Environments
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Vedant Chavda
PROSA  Formally Proven Schedulability Analysis
Commits
6929caa1
Commit
6929caa1
authored
Jul 24, 2020
by
Vedant Chavda
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
polish comments
parent
265a36d8
Pipeline
#31947
passed with stages
in 16 minutes and 1 second
Changes
7
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
Showing
7 changed files
with
38 additions
and
29 deletions
+38
29
analysis/facts/model/offset.v
analysis/facts/model/offset.v
+1
1
analysis/facts/model/task_arrivals.v
analysis/facts/model/task_arrivals.v
+3
2
analysis/facts/periodic/arrival_separation.v
analysis/facts/periodic/arrival_separation.v
+5
5
analysis/facts/periodic/sporadic.v
analysis/facts/periodic/sporadic.v
+7
2
analysis/facts/sporadic.v
analysis/facts/sporadic.v
+13
11
model/task/arrival/task_max_inter_arrival.v
model/task/arrival/task_max_inter_arrival.v
+7
6
util/list.v
util/list.v
+2
2
No files found.
analysis/facts/model/offset.v
View file @
6929caa1
...
@@ 13,7 +13,7 @@ Section OffsetLemmas.
...
@@ 13,7 +13,7 @@ Section OffsetLemmas.
Context
`
{
JobTask
Job
Task
}.
Context
`
{
JobTask
Job
Task
}.
Context
`
{
JobArrival
Job
}.
Context
`
{
JobArrival
Job
}.
(** Consider any
unique arrival sequence with consistent
arrivals, ... *)
(** Consider any
arrival sequence with consistent and nonduplicate
arrivals, ... *)
Variable
arr_seq
:
arrival_sequence
Job
.
Variable
arr_seq
:
arrival_sequence
Job
.
Hypothesis
H_consistent_arrivals
:
consistent_arrival_times
arr_seq
.
Hypothesis
H_consistent_arrivals
:
consistent_arrival_times
arr_seq
.
Hypothesis
H_uniq_arr_seq
:
arrival_sequence_uniq
arr_seq
.
Hypothesis
H_uniq_arr_seq
:
arrival_sequence_uniq
arr_seq
.
...
...
analysis/facts/model/task_arrivals.v
View file @
6929caa1
...
@@ 103,7 +103,7 @@ Section TaskArrivals.
...
@@ 103,7 +103,7 @@ Section TaskArrivals.
now
rewrite

filter_cat

arrivals_between_cat
.
now
rewrite

filter_cat

arrivals_between_cat
.
Qed
.
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]. *)
into task arrivals before [job_arrival j] and task arrivals at [job_arrival j]. *)
Lemma
task_arrivals_up_to_cat
:
Lemma
task_arrivals_up_to_cat
:
forall
j
,
forall
j
,
...
@@ 133,7 +133,8 @@ Section TaskArrivals.
...
@@ 133,7 +133,8 @@ Section TaskArrivals.
now
apply
arrived_between_implies_in_arrivals
.
now
apply
arrived_between_implies_in_arrivals
.
Qed
.
Qed
.
(** Unique arrival sequence leads to unique task arrivals. *)
(** An arrival sequence with nonduplicate arrivals implies that the
task arrivals also contain nonduplicate arrivals. *)
Lemma
uniq_task_arrivals
:
Lemma
uniq_task_arrivals
:
forall
j
,
forall
j
,
arrives_in
arr_seq
j
>
arrives_in
arr_seq
j
>
...
...
analysis/facts/periodic/arrival_separation.v
View file @
6929caa1
...
@@ 41,9 +41,9 @@ Section JobArrivalSeparation.
...
@@ 41,9 +41,9 @@ Section JobArrivalSeparation.
Hypothesis
H_j2_of_task
:
job_task
j2
=
tsk
.
Hypothesis
H_j2_of_task
:
job_task
j2
=
tsk
.
Hypothesis
H_consecutive_jobs
:
job_index
arr_seq
j2
=
job_index
arr_seq
j1
+
1
.
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]
(** We show that if
job [j1] and [j2] are consecutive jobs with [j2]
(i.e., [job_index j2] is one greater than [job_index j1]) then
arriving after [j1], then their arrival times are separated by
[j2] arrives one [task_period] after [j1]
. *)
their task's period
. *)
Lemma
consecutive_job_separation
:
Lemma
consecutive_job_separation
:
job_arrival
j2
=
job_arrival
j1
+
task_period
tsk
.
job_arrival
j2
=
job_arrival
j1
+
task_period
tsk
.
Proof
.
Proof
.
...
@@ 60,7 +60,7 @@ Section JobArrivalSeparation.
...
@@ 60,7 +60,7 @@ Section JobArrivalSeparation.
(** In this section we show that for two unequal jobs of a task,
(** In this section we show that for two unequal jobs of a task,
there exists a nonzero multiple of their task's period which separates
there exists a nonzero multiple of their task's period which separates
their arrival times. *)
their arrival times. *)
Section
ArrivalSeparation
OfJobs
.
Section
ArrivalSeparation
WithGivenIndexDifference
.
(** Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]
(** Consider any two _consecutive_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
that stem from the arrival sequence. *)
...
@@ 117,7 +117,7 @@ Section JobArrivalSeparation.
...
@@ 117,7 +117,7 @@ Section JobArrivalSeparation.
}
}
Qed
.
Qed
.
End
ArrivalSeparation
OfJobs
.
End
ArrivalSeparation
WithGivenIndexDifference
.
(** Consider any two _distinct_ jobs [j1] and [j2] of task [tsk]
(** Consider any two _distinct_ jobs [j1] and [j2] of task [tsk]
that stem from the arrival sequence. *)
that stem from the arrival sequence. *)
...
...
analysis/facts/periodic/sporadic.v
View file @
6929caa1
...
@@ 16,8 +16,8 @@ Section PeriodicTasksAsSporadicTasks.
...
@@ 16,8 +16,8 @@ Section PeriodicTasksAsSporadicTasks.
(** Any type of periodic tasks ... *)
(** Any type of periodic tasks ... *)
Context
{
Task
:
TaskType
}
`
{
PeriodicModel
Task
}.
Context
{
Task
:
TaskType
}
`
{
PeriodicModel
Task
}.
(** ... and their corresponding jobs from a consistent
(** ... and their corresponding jobs from a consistent
arrival sequence with
and unique arrival sequence
... *)
nonduplicate arrivals
... *)
Context
{
Job
:
JobType
}
`
{
JobTask
Job
Task
}
`
{
JobArrival
Job
}.
Context
{
Job
:
JobType
}
`
{
JobTask
Job
Task
}
`
{
JobArrival
Job
}.
Variable
arr_seq
:
arrival_sequence
Job
.
Variable
arr_seq
:
arrival_sequence
Job
.
...
@@ 62,10 +62,15 @@ Section PeriodicTasksAsSporadicTasks.
...
@@ 62,10 +62,15 @@ Section PeriodicTasksAsSporadicTasks.
(** For convenience, we state these obvious correspondences also at the level
(** For convenience, we state these obvious correspondences also at the level
of entire task sets. *)
of entire task sets. *)
(** First, we show that all tasks in a task set with valid periods
also have valid min interarrival times. *)
Remark
valid_periods_are_valid_inter_arrival_times
:
Remark
valid_periods_are_valid_inter_arrival_times
:
forall
ts
,
valid_periods
ts
>
valid_taskset_inter_arrival_times
ts
.
forall
ts
,
valid_periods
ts
>
valid_taskset_inter_arrival_times
ts
.
Proof
.
trivial
.
Qed
.
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
:
Remark
periodic_task_sets_respect_sporadic_task_model
:
forall
ts
,
forall
ts
,
valid_periods
ts
>
valid_periods
ts
>
...
...
analysis/facts/sporadic.v
View file @
6929caa1
...
@@ 137,8 +137,8 @@ Section SporadicArrivals.
...
@@ 137,8 +137,8 @@ Section SporadicArrivals.
Hypothesis
H_j1_task
:
job_task
j1
=
tsk
.
Hypothesis
H_j1_task
:
job_task
j1
=
tsk
.
Hypothesis
H_j2_task
:
job_task
j2
=
tsk
.
Hypothesis
H_j2_task
:
job_task
j2
=
tsk
.
(** We show that a sporadic task with valid
[task_min_inter_arrival_time]
cannot
(** We show that a sporadic task with valid
min interarrival time
cannot
have more than one job arriving at any time. *)
have more than one job arriving at any time. *)
Lemma
size_task_arrivals_at_leq_one
:
Lemma
size_task_arrivals_at_leq_one
:
(
exists
j
,
(
exists
j
,
size
(
task_arrivals_at_job_arrival
arr_seq
j
)
>
1
/\
size
(
task_arrivals_at_job_arrival
arr_seq
j
)
>
1
/\
...
@@ 159,8 +159,9 @@ Section SporadicArrivals.
...
@@ 159,8 +159,9 @@ Section SporadicArrivals.
now
ssromega
.
now
ssromega
.
Qed
.
Qed
.
(** No job of task [tsk] arrives at [job_arrival j1] other
(** We show that no jobs of the task [tsk] other than [j1] arrive at
than [j1] itself. *)
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
:
Lemma
only_j_in_task_arrivals_at_j
:
task_arrivals_at_job_arrival
arr_seq
j1
=
[
::
j1
].
task_arrivals_at_job_arrival
arr_seq
j1
=
[
::
j1
].
Proof
.
Proof
.
...
@@ 180,9 +181,9 @@ Section SporadicArrivals.
...
@@ 180,9 +181,9 @@ Section SporadicArrivals.
now
repeat
split
=>
//
;
try
rewrite
H_j1_task
.
now
repeat
split
=>
//
;
try
rewrite
H_j1_task
.
Qed
.
Qed
.
(**
Index of any job [j] in the sequence
(**
We show that a job [j1] is the first job that arrives
[task_arrivals_at arr_seq (job_task j) (job_arrival j)]
in task arrivals at [job_arrival j1] by showing that the
i
s zero.
*)
i
ndex of job [j1] in [task_arrivals_at_job_arrival arr_seq j1] is 0.
*)
Lemma
index_j_in_task_arrivals_at
:
Lemma
index_j_in_task_arrivals_at
:
index
j1
(
task_arrivals_at_job_arrival
arr_seq
j1
)
=
0
.
index
j1
(
task_arrivals_at_job_arrival
arr_seq
j1
)
=
0
.
Proof
.
Proof
.
...
@@ 207,8 +208,8 @@ Section SporadicArrivals.
...
@@ 207,8 +208,8 @@ Section SporadicArrivals.
now
ssromega
.
now
ssromega
.
Qed
.
Qed
.
(** We show that
[task_arrivals_at_job_arrival arr_seq j1] can be
(** We show that
task arrivals at [job_arrival j1] can be written as
written in terms of [task_arrivals_between
]. *)
task arrivals between [job_arrival j1] and [job_arrival j1 + 1
]. *)
Lemma
task_arrivals_at_as_task_arrivals_between
:
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
.
task_arrivals_at_job_arrival
arr_seq
j1
=
task_arrivals_between
arr_seq
tsk
(
job_arrival
j1
)
(
job_arrival
j1
).+
1
.
Proof
.
Proof
.
...
@@ 216,8 +217,9 @@ Section SporadicArrivals.
...
@@ 216,8 +217,9 @@ Section SporadicArrivals.
now
rewrite
big_nat1
H_j1_task
.
now
rewrite
big_nat1
H_j1_task
.
Qed
.
Qed
.
(** The sequence [task_arrivals_up_to_job_arrival arr_seq j] can be written as a concatenation
(** We show that the task arrivals up to the previous job [j1] concatenated with
of [task_arrivals_up_to_job_arrival arr_seq (prev_job j)] and [::j]. *)
the sequence [::j1] (the sequence containing only the job [j1]) is same as
task arrivals up to [job_arrival j1]. *)
Lemma
prev_job_cat
:
Lemma
prev_job_cat
:
job_index
arr_seq
j1
>
0
>
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
.
task_arrivals_up_to_job_arrival
arr_seq
(
prev_job
arr_seq
j1
)
++
[
::
j1
]
=
task_arrivals_up_to_job_arrival
arr_seq
j1
.
...
...
model/task/arrival/task_max_inter_arrival.v
View file @
6929caa1
Require
Export
prosa
.
model
.
task
.
concept
.
Require
Export
prosa
.
model
.
task
.
concept
.
Require
Export
prosa
.
model
.
task
.
arrivals
.
Require
Export
prosa
.
model
.
task
.
arrivals
.
(** * Task Max Inter
Arrival *)
(** * Task Max Inter

Arrival *)
(** We define a taskmodel parameter [task_max_inter_arrival_time] as
(** We define a taskmodel parameter [task_max_inter_arrival_time] as
the maximum time difference between the arrivals of consecutive jobs. *)
the maximum time difference between the arrivals of consecutive jobs. *)
...
@@ 9,7 +9,7 @@ Class TaskMaxInterArrival (Task : TaskType) :=
...
@@ 9,7 +9,7 @@ Class TaskMaxInterArrival (Task : TaskType) :=
task_max_inter_arrival_time
:
Task
>
duration
.
task_max_inter_arrival_time
:
Task
>
duration
.
(** In the following section, we define two properties that a task must satisfy
(** In the following section, we define two properties that a task must satisfy
for its max interarrival time to be valid. *)
for its max
imum
interarrival time to be valid. *)
Section
ValidTaskMaxInterArrival
.
Section
ValidTaskMaxInterArrival
.
(** Consider any type of tasks, ... *)
(** Consider any type of tasks, ... *)
...
@@ 24,13 +24,14 @@ Section ValidTaskMaxInterArrival.
...
@@ 24,13 +24,14 @@ Section ValidTaskMaxInterArrival.
(** ... and any arrival sequence. *)
(** ... and any arrival sequence. *)
Variable
arr_seq
:
arrival_sequence
Job
.
Variable
arr_seq
:
arrival_sequence
Job
.
(** Firstly, the task max interarrival time for a task is positive. *)
(** Firstly, the task max
imum
interarrival time for a task is positive. *)
Definition
positive_task_max_inter_arrival_time
(
tsk
:
Task
)
:
=
Definition
positive_task_max_inter_arrival_time
(
tsk
:
Task
)
:
=
task_max_inter_arrival_time
tsk
>
0
.
task_max_inter_arrival_time
tsk
>
0
.
(** Secondly, for any job [j] of a task [tsk] except the first one, there exists
(** Secondly, for any job [j] (with a positive [job_index]) of a task [tsk],
a job [j'] of task [tsk] that arrives before [j] with the arrival
there exists a job [j'] of task [tsk] that arrives before [j]
separation between [j] and [j'] being at most [task_max_inter_arrival_time tsk]. *)
with [j] not arriving any later than the task maximum interarrival
time of [tsk] after [j']. *)
Definition
arr_sep_task_max_inter_arrival
(
tsk
:
Task
)
:
=
Definition
arr_sep_task_max_inter_arrival
(
tsk
:
Task
)
:
=
forall
(
j
:
Job
),
forall
(
j
:
Job
),
arrives_in
arr_seq
j
>
arrives_in
arr_seq
j
>
...
...
util/list.v
View file @
6929caa1
...
@@ 426,8 +426,8 @@ Section AdditionalLemmas.
...
@@ 426,8 +426,8 @@ Section AdditionalLemmas.
now
rewrite

EQ_a

EQ_b
EQ
.
now
rewrite

EQ_a

EQ_b
EQ
.
Qed
.
Qed
.
(** We
prove that the element given by [nth d xs n] in a sequence [xs] either
(** We
show that the nth element in a sequence lies in the
lies in [xs] or is equal to [d]
. *)
sequence or is the default element
. *)
Lemma
default_or_in
:
Lemma
default_or_in
:
forall
(
T
:
eqType
)
(
n
:
nat
)
(
d
:
T
)
(
xs
:
seq
T
),
forall
(
T
:
eqType
)
(
n
:
nat
)
(
d
:
T
)
(
xs
:
seq
T
),
nth
d
xs
n
=
d
\/
nth
d
xs
n
\
in
xs
.
nth
d
xs
n
=
d
\/
nth
d
xs
n
\
in
xs
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment