Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
P
PROSA  Formally Proven Schedulability Analysis
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Pierre Roux
PROSA  Formally Proven Schedulability Analysis
Compare Revisions
master...arrivalcurves
Source
arrivalcurves
Select Git revision
...
Target
master
Select Git revision
Compare
Commits (1)
Add preliminary version of arrival curves
· ce2cf22c
Felipe Cerqueira
authored
Jan 10, 2017
ce2cf22c
Expand all
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
191 additions
and
1 deletion
+191
1
Makefile
Makefile
+3
1
model/arrival/curves/bounds.v
model/arrival/curves/bounds.v
+67
0
model/arrival/curves/conversion.v
model/arrival/curves/conversion.v
+121
0
No files found.
Makefile
View file @
ce2cf22c
This diff is collapsed.
Click to expand it.
model/arrival/curves/bounds.v
0 → 100644
View file @
ce2cf22c
Require
Import
rt
.
util
.
all
.
Require
Import
rt
.
model
.
arrival
.
basic
.
arrival_sequence
rt
.
model
.
arrival
.
basic
.
task_arrival
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
div
.
(* In this section, we define the notion of arrival curves, which
can be used to reason about the frequency of job arrivals. *)
Module
ArrivalCurves
.
Import
ArrivalSequence
TaskArrival
.
Section
DefiningArrivalCurves
.
Context
{
Task
:
eqType
}.
Context
{
Job
:
eqType
}.
Variable
job_task
:
Job
>
Task
.
(* Consider any job arrival sequence... *)
Variable
arr_seq
:
arrival_sequence
Job
.
(* ...and let tsk be any task to be analyzed. *)
Variable
tsk
:
Task
.
(* Recall the job arrivals of tsk in a given interval [t1, t2). *)
Let
arrivals_of_tsk
:
=
arrivals_of_task_between
job_task
arr_seq
tsk
.
Let
num_arrivals_of_tsk
:
=
num_arrivals_of_task
job_task
arr_seq
tsk
.
(* First, we define what constitutes an arrival bound for task tsk. *)
Section
ArrivalBound
.
(* Let max_arrivals denote any function that takes an interval length and
returns the associated number of job arrivals of tsk.
(This corresponds to the eta+ function in the literature.) *)
Variable
max_arrivals
:
time
>
nat
.
(* Then, we say that num_arrivals is an arrival bound iff, for any interval [t1, t2),
(num_arrivals (t2  t1)) bounds the number of jobs of tsk that arrive in that interval. *)
Definition
is_arrival_bound
:
=
forall
t1
t2
,
t1
<=
t2
>
num_arrivals_of_tsk
t1
t2
<=
max_arrivals
(
t2

t1
).
End
ArrivalBound
.
(* Next, we define the notion of a separation bound for task tsk, i.e., the smallest
interval length in which a certain number of jobs of tsk can be spawned. *)
Section
SeparationBound
.
(* Let min_length denote any function that takes a number of jobs and
returns an associated interval length.
(This corresponds to the delta function in the literature.) *)
Variable
min_length
:
nat
>
time
.
(* Then, we say that min_length is a separation bound iff, for any number of jobs
of tsk, min_separation lowerbounds the minimum interval length in which that number
of jobs can be spawned. *)
Definition
is_separation_bound
:
=
forall
t1
t2
,
t1
<=
t2
>
min_length
(
num_arrivals_of_tsk
t1
t2
)
<=
t2

t1
.
End
SeparationBound
.
End
DefiningArrivalCurves
.
End
ArrivalCurves
.
\ No newline at end of file
model/arrival/curves/conversion.v
0 → 100644
View file @
ce2cf22c
Require
Import
Coq
.
Logic
.
ConstructiveEpsilon
.
Require
Import
rt
.
util
.
all
.
Require
Import
rt
.
model
.
arrival
.
basic
.
arrival_sequence
.
Require
Import
rt
.
model
.
arrival
.
curves
.
bounds
.
From
mathcomp
Require
Import
ssreflect
ssrbool
eqtype
ssrnat
seq
div
.
(* In this section, we show how to convert between arrival bounds and separation bounds. *)
Module
ArrivalConversion
.
Import
ArrivalSequence
ArrivalCurves
.
(* For simplicity, we redefine some names. *)
Definition
linear_search
:
=
constructive_indefinite_ground_description_nat
.
(* Next, we show how to perform the conversion. *)
Section
Conversion
.
Context
{
Task
:
eqType
}.
Context
{
Job
:
eqType
}.
Variable
job_arrival
:
Job
>
time
.
Variable
job_task
:
Job
>
Task
.
(* Consider any job arrival sequence ...*)
Variable
arr_seq
:
arrival_sequence
Job
.
(* ...and let tsk be any task to be analyzed. *)
Variable
tsk
:
Task
.
(* First, we convert an arrival bound into a separation bound. *)
Section
ArrivalToSeparation
.
(* Let max_arrivals be any arrival bound of tsk. *)
Variable
max_arrivals
:
time
>
nat
.
Hypothesis
H_is_arrival_bound
:
is_arrival_bound
job_task
arr_seq
tsk
max_arrivals
.
(* Assume that jobs of each task arrive infinitely often. *)
Hypothesis
H_jobs_arrive_infinitely_often
:
forall
j1
,
exists
j2
,
job_task
j1
=
job_task
j2
/\
job_arrival
j1
<=
job_arrival
j2
.
(* Next, given any number of job arrivals, we show how to compute the minimum interval
length that can contain all these arrivals.
The computation is done using a linear search for larger values. *)
Section
ComputingSeparationBound
.
(* Consider any number of job arrivals. *)
Variable
num_arrivals
:
time
.
(* Then, we define a predicate that checks whether an interval delta is a separation
bound for this number of arrivals, ... *)
Definition
contains_all_arrivals
(
delta
:
nat
)
:
=
max_arrivals
delta
>=
num_arrivals
.
(* ...which we prove to be decidable (since it is a boolean). *)
Lemma
contains_all_arrivals_decidable
:
forall
delta
,
{
contains_all_arrivals
delta
}
+
{~
contains_all_arrivals
delta
}.
Proof
.
by
intros
delta
;
apply
Bool
.
bool_dec
.
Qed
.
(* Next, using the fact that jobs arrive infinitely often, we show that there always
exist an interval delta that contains this number of arrivals, ...*)
Lemma
interval_exists
:
exists
delta
,
contains_all_arrivals
delta
.
Proof
.
Admitted
.
(* ...we run a linear search that looks for this delta. This returns
a value delta and a proof that delta contains all the arrivals. *)
Definition
find_delta
:
=
linear_search
contains_all_arrivals
contains_all_arrivals_decidable
interval_exists
.
(* Next, we prove that this linear serch finds the minimum element that
satisfies the property.
(TODO: This proof is optional, just for tightness.
Also, it might require dealing with ConstructiveEpsilon). *)
Lemma
find_delta_returns_min
:
true
.
Admitted
.
(* To conclude, we define the conversion from arrival bound to separation bound
as this number returned by the linear search. *)
Definition
convert_to_separation_bound
:
=
proj1_sig
find_delta
.
End
ComputingSeparationBound
.
(* Based on the computation above, we prove that any value that is returned is indeed
a separation bound. *)
Lemma
conversion_to_separation_bound_is_valid
:
is_separation_bound
job_task
arr_seq
tsk
convert_to_separation_bound
.
Proof
.
intros
t1
t2
LE
.
Admitted
.
End
ArrivalToSeparation
.
(* Next, we convert a separation bound into an arrival bound. *)
Section
SeparationToArrival
.
(* Let min_length be any separation bound of tsk. *)
Variable
min_length
:
nat
>
time
.
Hypothesis
H_is_separation_bound
:
is_separation_bound
job_task
arr_seq
tsk
min_length
.
(* Then, by computing xxxxxx, ...*)
Definition
convert_to_arrival_bound
(
k
:
time
)
:
=
0
.
(* TODO: FIX *)
(* ...we transform min_length to obtain an arrival bound. *)
Lemma
conversion_to_upper_curve_succeeds
:
is_arrival_bound
job_task
arr_seq
tsk
convert_to_arrival_bound
.
Proof
.
Admitted
.
End
SeparationToArrival
.
End
Conversion
.
End
ArrivalConversion
.
\ No newline at end of file