Commit c2399f4e authored by jonathan julou's avatar jonathan julou

ajout readme

parent bff26f1c
Pipeline #19185 passed with stages
in 6 minutes and 38 seconds
<h1>Modifications made during the internship on CPA
and further development suggestions</h1>
<h2>I) Modifications </h2>
<h3>Outside of restructuring</h3>
<h4>util</h4>
Creation of the file jonathan.v.
It contains functions that should eventually be put somewhere else.
The 2 main properties are those on sums.
It is possible that the easier lemmas already exist somewhere else.
In the files where jonathan.v is imported, if the latter was to be deleted,
it would be necessary to replace the "jonathan.blabla" everywhere, where blabla is the name of the function.
However it should be pretty quick using the search and replace tool.
<h4>/!\ the python script proofloc.py was also modified for testing. /!\</h4>
This change shouldn't be merged with prosa
<h3>Inside restructuring</h3>
<h4>model</h4>
dependency.v : the navigational functions next_task, prev_task
and some lemmas associated with them were added.
simple_abstracted.v : a definition of an abstract arrival model
was added in the folder arrival.
periodic_jitter.v : defines a periodic with jitter
arrival model.
periodic_jitter_up_to_t.v : defines a periodic with jitter
arrival model that is verified
until some instant t.
<h4>analysis</h4>
The folder analysis_up_to_t and all the files it contains were added.
Their purpose is to set up the basics in order to develop a proof
of the correctness of the result given by the CPA algorithm.
Aside from schedulability.v, all files were modified to proove the propagation
of the periodic-jitter model between linearly dependent tasks, and to proove
the correctness of the naive latency as sum of the WCRTs.
<h2>II) Detailed purpose of each file</h2>
<h3>/util/jonathan.v</h3>
It contains some utilitary lemmas used in multiple files in restructuring/analysis.
The essential lemmas are the "sum_to_args_leq" and "sum_to_args_lt", which allow
to deduce a superiority relation on the upper bounds of the arguments of two sums
starting at zero from a strict relation between the two sums.
The other lemmas are properties on booleans or natural numbers which are often
trivial and are there only because they were used multiple times.
<h3>/restructuring/model/arrival/simple_abstracted.v</h3>
It defines a general arrival model abstraction for a task as a property on
said task and the arrival sequence of jobs.
There is also the definition of a finite arrival model which also takes into account
an instant to give the property. It is used in the analysis_up_to_t folder to
describe an arrival model that is valid if verified by the arrival sequence until an
instant t.
<h3>/restructuring/model/arrival/periodic_jitter.v</h3>
It defines the periodic with jitter arrival model.
Each Task is given 3 parameters, a period, a jitter, and an offset, whiwh can be unknown.
The jitter is not well defined.
It requires an annotation of the trace that gives for all job its job_jitter.
There is also a definition of the theoretical arrival of a job, as the difference of
the job_arrival and the job_jitter.
the model itself requires 3 properties to be verified.
The first one, which I like to call the correction, requires that for all job in the
task, its theoretical arrival happens after the offset, so that the first arrival
doesn't violate the offset. Furthermore, the difference of the theoretical arrival
and the offset must be a multiple of the period. And finally the job_jitter is to be
less than the task jitter.
The second one, which I like to call the injectivity, requires that for all pair of
distinct jobs, they can't have the same theoretical arrival.
The third one, which I like to call the surjectivity, requires that for each temporal
slot associated to a period shifted by the offset,
there is a job that has its theoretical arrival in it.
<h3>/restructuring/model/arrival/periodic_jitter_up_to_t.v</h3>
It converts the definition of a periodic with jitter arrival model to
a model that verifies the periodic jitter properties until an instant t.
There are two until_t-models : one with 3 hypothesis, another with 2.
there is the proof of the equivalence between the 3 hypothesis model for all t and
the infinite model. However that model is unused later.
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.
<h2>III) Suggestions</h2>
<h3>/restructuring/model/arrival/periodic_jitter.v</h3>
Since the third hypothesis 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
model everything was proved with the third hypothesis and for the finite model
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.
<h3>/restructuring/analysis/analysis_up_to_t/cpa_temporal_step</h3>
For now, the induction for the final result uses an analysis on WCRT at each step.
It is easier for periodic with jitter since it allows us to reuse the propagation
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.
......@@ -99,11 +99,9 @@ Section CPA_temp_step.
a system with correct arrival models to certify that
the BCRTs and WCRTs are correct up to that instant.*)
Hypothesis response_time_analysis :
forall t tsk, tsk \in ts ->
forall t tsk, tsk \in ts ->
all_task_models_correct_until_t 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 ).
task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk.
(*at all time, for every task, it is possible to perform an analysis of
a system with correct arrival models to certify that
......@@ -152,11 +150,10 @@ Section CPA_temp_step.
Lemma induction_first_step : forall tsk, tsk \in ts ->
task_response_time_upper_bound_until_t sched arr_seq 0 (task_WCRT tsk) tsk /\
task_response_time_lower_bound_until_t sched arr_seq 0 (task_BCRT tsk) tsk /\
all_task_models_correct_until_t 0.
Proof.
intros tsk belong.
split. 2:split.
split.
- unfold task_response_time_upper_bound_until_t.
intros j P1 P2. split.
intro Q. apply completed_implies_scheduled_before in Q.
......@@ -168,11 +165,6 @@ Section CPA_temp_step.
* ssromega.
+ ssromega.
- unfold task_response_time_lower_bound_until_t.
intros j P1 P2.
intro Q. apply completed_implies_scheduled_before in Q.
destruct Q as [t' Q]. destruct Q as [Q1 Q2]. ssromega. apply H_positive_cost.
apply H_jobs_must_arrive.
- unfold all_task_models_correct_until_t.
intros tsssk Q. apply models_correct_on_init. exact Q.
Qed.
......@@ -191,7 +183,6 @@ Section CPA_temp_step.
assert (P:
(forall t : instant, task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk
/\ task_response_time_lower_bound_until_t sched arr_seq t (task_BCRT tsk) tsk
/\ all_task_models_correct_until_t t)
->
(forall t : instant, task_response_time_upper_bound_until_t sched arr_seq t (task_WCRT tsk) tsk )).
......@@ -203,24 +194,18 @@ Section CPA_temp_step.
apply induction_first_step. exact belong.
}
{ (*HEREDITY*)
destruct IHt as [W IHt].
destruct IHt as [B CC].
destruct IHt as [W CC].
assert (next_CC: all_task_models_correct_until_t t.+1).
{ apply time_step. exact CC. }
assert (next_RTA_destructable:
task_response_time_lower_bound_until_t sched arr_seq t.+1
(task_BCRT tsk) tsk
/\
assert (next_RTA:
task_response_time_upper_bound_until_t sched arr_seq t.+1
(task_WCRT tsk) tsk).
{ apply response_time_analysis. exact belong. exact next_CC. }
destruct next_RTA_destructable as [G D].
split. 2:split.
exact D. exact G. exact next_CC.
split.
exact next_RTA. exact next_CC.
}
Qed.
......
......@@ -788,7 +788,7 @@ Section Propagatability.
task_response_time_upper_bound arr_seq sched tsk (task_WCRT tsk).
Proof.
intros tsk P.
apply final_result with H0 ts task_BCRT task_input_PJM periodic_jitter_schedule_property.
apply final_result with H0 ts task_input_PJM periodic_jitter_schedule_property.
- intros t t1 t2 B W. unfold cpa_temporal_step.task_model_correct_until_t.
apply all_models_propagatable_PJM. exact B.
......
HORS DE RESTRUCTURING
UTIL
ajout d'un fourre-tout jonathan.v. Il faudrait eventuellement ranger les fonctions qu'il contient. Les principales sont les 2 propriétés sur les sommes, il est possible que les propriétés plus simples sur les propriétés existent déjà.
Dans les fichiers qui l'importent, il faudra remplacer les jonathan.blabla dans les fonctions, mais avec l'outil de recherche ca devrait etre assez rapide.
/!\ le script python proofloc.py est aussi modifié, ne pas le merge avec prosa /!\
DANS RESTRUCTURING
MODEL
dependency.v : ajout des fonctions de navigation next_task, prev_task
et lemmes associés
simple_abstracted.v : dans le dossier arrival, ajout des definitions de modèle
d'arrivée abstrait et idem jusqu'a t
periodic_jitter_model_up_to_t : copie de verify_up_to_t renommée et placée au bon
endroit
ANALYSIS
ajout du dossier analysis_up_to_t et de tous les fichiers qu'il contient
modification de tous les autres fichiers sauf schedulability
et latency_backup (squelette fait par Maxime qui ne devrait plus servir)
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment