Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Maxime Lesourd
rt-proofs
Commits
5a6db6de
Commit
5a6db6de
authored
Aug 20, 2019
by
jonathan julou
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
encore du readme
parent
c2399f4e
Pipeline
#19187
passed with stages
in 3 minutes and 32 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
43 additions
and
2 deletions
+43
-2
restructuring/README_jonathan.md
restructuring/README_jonathan.md
+43
-2
No files found.
restructuring/README_jonathan.md
View file @
5a6db6de
...
...
@@ -108,13 +108,43 @@ and further development suggestions</h1>
there is no proof of the equivalence between the 2 hypothesis model for all t and
the infinite model. However that model is the one used later.
<h3>
/restructuring/analysis/latency.v
</h3>
It contains the proof (main_lemma) that for a chain of tasks forming a path,
the sum of the WCRT of each task is an upper bound on the propagation time
of a job through the path.
<h3>
/restructuring/analysis/schedulability.v
</h3>
It contains the definitions of WCRT and BCRT as bound on response time for all jobs
and what it means to be schedulable (unused by me as of now).
<h3>
/restructuring/analysis/periodic_jitter_same_law.v
</h3>
The whole point of this file is the lemma periodic_jitter_same_law.
It states that if two tasks are dependent and the first one follows the
periodic with jitter arrival model, then the second one too, and it will
have the same period, but a jitter equal to the original jitter plus the
difference of WCRT and BCRT.
<h3>
/restructuring/analysis/analysis_up_to_t/schedulability_up_to_t.v
</h3>
It defines what it means to be a upper or lower response time bound until t,
and then shows the equivalence between being a bound up ot t for all t and
being a general time bound.
<h3>
/restructuring/analysis/analysis_up_to_t/cpa_temporal_step.v
</h3>
It defines what it means to be a upper or lower response time bound until t,
and then shows the equivalence between being a bound up ot t for all t and
being a general time bound.
<h2>
III) Suggestions
</h2>
<h3>
/restructuring/model/arrival/periodic_jitter.v
</h3>
Since the third hypothesis is totally useless for our further uses,
Since the third hypothesis
(surjectivity)
is totally useless for our further uses,
it would have to be removed to tie everything together with actual proofs.
For now, there is a hole in the logical reasonment in coq, since for the infinite
...
...
@@ -122,7 +152,18 @@ and further development suggestions</h1>
it was removed, we don't have a direct equivalence between the two right now.
What has to be done is to remove the 3rd hypothesis, and then rerun the proofs in
periodic_jitter_propagation.v removing all that is linked to that third hypothesis.
periodic_jitter_propagation.v removing all things surjectivity.
<h3>
/restructuring/analysis/latency.v
</h3>
All the mess with the reparticularization of the main_lemma and the local/general
hypothesis should 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.
<h3>
/restructuring/analysis/analysis_up_to_t/cpa_temporal_step
</h3>
...
...
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