Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
R
rtproofs
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
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
Maxime Lesourd
rtproofs
Commits
0362e46e
Commit
0362e46e
authored
Aug 21, 2019
by
jonathan julou
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
ajout version experimentale
parent
37d0476e
Pipeline
#19210
passed with stages
in 5 minutes and 57 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Sidebyside
Showing
3 changed files
with
225 additions
and
5 deletions
+225
5
restructuring/README_jonathan.md
restructuring/README_jonathan.md
+18
4
restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v
restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v
+1
1
restructuring/analysis/analysis_up_to_t/cpa_temporal_step_experimental.v
...nalysis/analysis_up_to_t/cpa_temporal_step_experimental.v
+206
0
No files found.
restructuring/README_jonathan.md
View file @
0362e46e
...
...
@@ 145,6 +145,17 @@ and further development suggestions</h1>
This uses 2 hypothesis meant to provide analysis on a propagationnal property of the schedule, and an analysis on WCRT.
They have yet to be proved in the exemple of the periodic_jitter_model.
<h3>
/restructuring/analysis/analysis_up_to_t/cpa_temporal_step_experimental.v
</h3>
provides the same result as cpa_temporal_step, but by using a different analysis
of WCRT. This time I tried to make the analysis only at the end, which is easier
to understand intuitively.
However, it seems this approach won't work since for the last WCRT we don't have
the output model. The other approach had the advantage that we could propagate
the correction of that last WCRT from the correction at the start where there was
no job at the end of the chain.
<h3>
/restructuring/analysis/analysis_up_to_t/periodic_jitter_propagation_up_to_t.v
</h3>
There are two sections here.
...
...
@@ 182,13 +193,16 @@ and further development suggestions</h1>
<h3>
/restructuring/analysis/latency.v
</h3>
All the mess with the reparticularization of the main_lemma and the local/general
hypothesis
sh
ould be cleaned up.
hypothesis
c
ould be cleaned up.
It was necessary to have the particular view to understand how the path worked and
a general point of view was mandatory in order to actually do the induction,
however both ended up staying in the finished file.
The particularisation is absolutely useless.
The only potential problem is that it would become necessary to read
the dirty general lemmas rather than have the things spread out in the context.
<h3>
/restructuring/analysis/analysis_up_to_t/cpa_temporal_step
</h3>
...
...
@@ 197,7 +211,7 @@ and further development suggestions</h1>
property.
However it should be possible to just verify that at the end.
Therefore, it would require to change the result of the final lemma to
"forall t, all_task_models_correct_until_t t", which would give us that
all models are correct to infinity, and then use a static WCRT analysis on them
.
I tried to modify the proof in cpa_temporal_step_experimental.v to account for that,
nevertheless, it appears the new response_time_analysis would be impossible
because we don't have an output model at the end to verify the WCRT
.
restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v
View file @
0362e46e
...
...
@@ 209,4 +209,4 @@ Section CPA_temp_step.
}
Qed
.
End
CPA_temp_step
.
\ No newline at end of file
End
CPA_temp_step
.
restructuring/analysis/analysis_up_to_t/cpa_temporal_step_experimental.v
0 → 100644
View file @
0362e46e
From
rt
.
restructuring
.
model
Require
Export
dependency
.
From
rt
.
restructuring
.
model
Require
Export
simple_abstracted
.
From
mathcomp
Require
Export
bigop
path
.
From
rt
.
util
Require
Export
list
.
From
rt
.
util
Require
Import
ssromega
.
From
rt
.
util
Require
Import
bigcat
.
From
rt
.
restructuring
.
analysis
.
analysis_up_to_t
Require
Export
schedulability_up_to_t
.
Set
Bullet
Behavior
"Strict Subproofs"
.
Section
CPA_temp_step
.
(*========================================================================*)
(*  I  CONTEXT AND VARIABLES  I  *)
(*========================================================================*)
Context
{
PState
:
Type
}.
Context
(
sched
:
schedule
PState
).
Context
{
Job
:
JobType
}
{
Task
:
TaskType
}.
Context
`
{
JobDependency
Job
}
`
{
TaskDependency
Task
}.
Context
`
{
ProcessorState
Job
PState
}.
Context
`
{
JobCost
Job
}
`
{
JobArrival
Job
}
`
{
JobTask
Job
Task
}.
Context
(
arr_seq
:
arrival_sequence
Job
).
(*the set of all the tasks in the system*)
Variable
ts
:
{
set
Task
}.
(* for each task we get its BCRT et WCRT, as given by the CPA,
but without any bounding properties until the analysis gives them*)
Variable
task_WCRT
:
Task
>
duration
.
Variable
task_BCRT
:
Task
>
duration
.
(*========================================================================*)
(*  II  ARRIVAL MODEL PROPERTIES  II  *)
(*========================================================================*)
Let
FiniteModel
:
=
@
ArrivalModelUpTo
Job
Task
.
Let
Model
:
=
@
ArrivalModel
Job
Task
.
(*for all task, we get a hold of the input model calculated by CPA*)
Variable
task_arrival_model
:
Task
>
Model
.
Variable
task_arrival_finite_model
:
Task
>
FiniteModel
.
Variable
schedule_property
:
(
schedule
PState
)
>
(
arrival_sequence
Job
)
>
FiniteModel
>
Task
>
instant
>
Prop
.
(*what it means for a task to always respect its arrival model*)
Definition
task_model_correct
(
tsk
:
Task
)
:
=
(
task_arrival_model
tsk
)
arr_seq
tsk
.
(*what it means for a task to respect its arrival model until t*)
Definition
task_model_correct_until_t
(
tsk
:
Task
)
(
t
:
instant
)
:
=
(
task_arrival_finite_model
tsk
)
arr_seq
tsk
t
.
Definition
task_model_correct_eq
(
tsk
:
Task
)
:
=
task_model_correct
tsk
<>
forall
t
,
task_model_correct_until_t
tsk
t
.
Definition
propagatable_until_t
tsk1
tsk2
t
:
=
task_dependency
tsk1
tsk2
>
(
schedule_property
sched
arr_seq
(
task_arrival_finite_model
tsk1
))
tsk1
t
>
task_model_correct_until_t
tsk1
t
>
task_model_correct_until_t
tsk2
(
t
.+
1
).
(*example schedule property for the periodic with jitter model : *)
Definition
periodic_jitter_schedule_property
tsk
t
:
=
task_response_time_lower_bound_until_t
sched
arr_seq
t
(
task_BCRT
tsk
)
tsk
>
task_response_time_upper_bound_until_t
sched
arr_seq
t
(
task_WCRT
tsk
)
tsk
.
Definition
all_task_models_correct
:
=
forall
tsk
,
tsk
\
in
ts
>
task_model_correct
tsk
.
Definition
all_task_models_correct_until_t
t
:
=
forall
tsk
,
tsk
\
in
ts
>
task_model_correct_until_t
tsk
t
.
(*========================================================================*)
(*  III  HYPOTHESIS  III  *)
(*========================================================================*)
(*for all task, it is possible to go from the model up to t for all t
to the infinite model, and viceversa.*)
Hypothesis
H_all_models_eq
:
forall
tsk
,
task_model_correct_eq
tsk
.
(*for all tasks, it is possible to infer that the next task respect its model
from the correction of the previous model and of the WCRT and BCRT of said
task*)
Hypothesis
H_all_models_always_propagatable
:
forall
(
t
:
instant
)
(
tsk1
tsk2
:
Task
),
tsk1
\
in
ts
>
tsk2
\
in
ts
>
propagatable_until_t
tsk1
tsk2
t
.
(*we know that the arrival model for tasks without predecessors
(the 'inputs' of the task chain), the model is correct, since we have
a trace for it.*)
Hypothesis
H_input_model_known
:
forall
tsk
,
tsk
\
in
ts
>
prev_task
tsk
ts
=
None
>
(
forall
t
,
task_model_correct_until_t
tsk
t
).
(*jobs can't cost no service to complete*)
Hypothesis
H_positive_cost
:
forall
j
,
job_cost
j
>
0
.
(*jobs have to arrive before they begin to receive service.*)
Hypothesis
H_jobs_must_arrive
:
jobs_must_arrive_to_execute
sched
.
(*at all time, for every task, it is possible to perform an analysis of
a system with correct arrival models to certify that
the BCRTs and WCRTs are correct up to that instant.*)
Hypothesis
response_time_analysis
:
forall
tsk
,
tsk
\
in
ts
>
all_task_models_correct
>
task_response_time_upper_bound
arr_seq
sched
tsk
(
task_WCRT
tsk
).
(*at all time, for every task, it is possible to perform an analysis of
a system with correct arrival models to certify that
the schedule property is correct up to that instant.*)
Hypothesis
schedule_property_analysis
:
forall
t
tsk
,
tsk
\
in
ts
>
all_task_models_correct_until_t
t
>
schedule_property
sched
arr_seq
(
task_arrival_finite_model
tsk
)
tsk
t
.
(*necessary for the base case of the induction in the final lemma*)
(*should be easy to verify from an actual trace, since only the first task
can have a job at t=0. For the other tasks, it is sufficient to verify
that their model allows them to not have a job at t=0.*)
Hypothesis
models_correct_on_init
:
all_task_models_correct_until_t
0
.
Hypothesis
H_WCRT_positive
:
forall
tsk
,
task_WCRT
tsk
>
0
.
(*========================================================================*)
(*  IV  MAIN LEMMAS  VI  *)
(*========================================================================*)
(*at an instant t, if the arrival models, WCRT and BCRT
were correct until t, then the models are correct until t+1*)
Lemma
time_step
:
forall
t
,
all_task_models_correct_until_t
t
>
all_task_models_correct_until_t
(
t
.+
1
).
Proof
.
intros
t
CC
.
unfold
all_task_models_correct_until_t
.
intros
tsk
belong
.
destruct
(
prev_task
tsk
ts
)
eqn
:
E
.

assert
(
P
:
task_model_correct_until_t
s
t
).
{
unfold
all_task_models_correct_until_t
in
CC
.
apply
CC
.
apply
prev_task_in_task_set
with
tsk
.
exact
E
.
}
apply
H_all_models_always_propagatable
with
s
.
apply
prev_task_in_task_set
with
tsk
.
exact
E
.
exact
belong
.
apply
prev_task_dependency
with
ts
.
exact
belong
.
exact
E
.
apply
schedule_property_analysis
.
apply
prev_task_in_task_set
with
tsk
.
exact
E
.
exact
CC
.
exact
P
.

apply
H_input_model_known
.
exact
belong
.
exact
E
.
Qed
.
Lemma
all_arrival_finite_models_correct
:
forall
t
,
all_task_models_correct_until_t
t
.
Proof
.
induction
t
as
[
t
IHt
].
{
(*INITIALISATION*)
intros
tsssk
Q
.
apply
models_correct_on_init
.
exact
Q
.
}
{
(*HEREDITY*)
apply
time_step
.
exact
IHt
.
}
Qed
.
Lemma
all_arrival_models_correct
:
all_task_models_correct
.
Proof
.
unfold
all_task_models_correct
.
intros
tsk
belong
.
apply
H_all_models_eq
.
intro
t
.
assert
(
AAFMC
:
forall
t
,
all_task_models_correct_until_t
t
)
by
apply
all_arrival_finite_models_correct
.
unfold
all_task_models_correct_until_t
in
AAFMC
.
apply
AAFMC
.
exact
belong
.
Qed
.
(*final lemma: all WCRT correct for infinite traces.
It should be unnecessary to verify BCRTs at this step,
but should be easy by extracting it alongside the WCRT
in the assertion P.*)
Lemma
final_result
:
forall
tsk
,
tsk
\
in
ts
>
task_response_time_upper_bound
arr_seq
sched
tsk
(
task_WCRT
tsk
).
Proof
.
intros
tsk
belong
.
apply
response_time_analysis
.
exact
belong
.
apply
all_arrival_models_correct
.
Qed
.
End
CPA_temp_step
.
\ No newline at end of file
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