Commit e47e261e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

TODOs...

parent ef716952
......@@ -4,22 +4,23 @@ REM: nouvelle limite = 27 pages sans la biblio
À FAIRE SELON RÉPONSE AUX RAPPORTEURS:
- utiliser \begin{theorem}\end{theorem} ailleurs dans l’article
(p.ex. dans la section Pipeline)
- S 4.6: réécrire cette section sans écrire la preuve du début à la fin, mais
- S 4.7: réécrire cette section sans écrire la preuve du début à la fin, mais
un focus sur quelques instants importants de la preuve. « tel moment de la
preuve est important parce que XXX. à ce moment, on dispose de YYY et il
faut prouver ZZZ. ça marche parce que ΩΩΩ »
- étoffer section pipeline
- remarque: dans le pipeline on n’utilise que la synchro écrivain → lecteur
- utiliser \begin{theorem}\end{theorem} ailleurs dans l’article
(p.ex. dans la section Pipeline)
RELATED WORK:
- une demande sans réponse d’un rapporteur pour davantage de related work:
> C "The general approach to specifying weak-memory data structures
> probably needs further evaluation and comparison with other approaches"
RELATED WORK:
+ reprendre et alléger le related work de Cosmo pour la partie mémoire faible / Cosmo
+ à approfondir: preuve de struct. de données concurrentes
-> papier: Lars Birkedal et Simon Friis ont fait une preuve de queue (pas mémoire faible)
......@@ -43,37 +44,3 @@ RELATED WORK:
--> récursif, regarder son related work
+ nous = 1er papier à présenter une struct de données concurrente en mémoire
faible avec de la SL ??
répondre à la question «la structure est-elle linéarisable»
le mot est-il bien défini dans la littérature
une définition ici ?
"A sound and complete definition of linearizability on weak memory models"
"Linearizability on hardware weak memory models"
proposition de JH:
linéarisable = explicable par un historique totalement ordonné
séquentiellement consistante = les accès sont ordonnés par hb
AUTRE:
- related: écrire la comparaison détaillée avec Folly
- contenu: dans l’intro on insiste que l’atomicité logique en mémoire faible
c’est nouveau, mais dans l’article on ne dit rien de particulier à ce sujet,
on se contente de prendre la même définition qu’en SC et de dire que ça
marche
MINEUR:
- terminologie? échanger “tail” et “head” (vie courante: on ajoute en queue)
(relevé par 1 des 3 rapporteurs)
- biblio: citer Shavit dans l’intro de la section Queue
+ la synchro lecteur k → l’écrivain k+C (S 3.3) a-t-elle un rapport
avec la “quiescent consistency” décrite par Shavit ?
- remarque: la queue en mémoire faible est comparable aux refs atomiques, en ce
qu’elle sert de conteneur pour une valeur ET de structure de synchro
- remarque: dans le pipeline on n’utilise que la synchro écrivain → lecteur
- remarque? les triplets dans Iris ont de l’infrastructure pour les assertions
“laterable” (séparable en une assertion persistante et une assertion timeless)
sans que l’utilisateur ait à manier 2 assertions, et sans ▷
- forme: ajouter de l’espace vertical à l’intérieur des pré/post des triplets
verticaux car les grands crochets/accolades sont collés aux traits du triplet;
(cf p.ex Fig 5 "spec mémoire faible", ou Fig 7 "triplets de M-OCaml")
......@@ -69,7 +69,8 @@
\nthpointstoAT \loc \idx {\mkval{\val_0}\view}
}
{\ArrayCAS \loc \idx {\val_1} {\val_2}}
{\Lam \val'. \isepV{%
{\Lam \val'. \parbox[center][4.3em]{0pt}{}
\isepV{%
\val' = \False \cr
\nthpointstoAT \loc \idx {\mkval{\val_0}\view} \cr
\seen \view
......@@ -83,7 +84,8 @@
\seen \view'
}
{\ArrayCAS \loc \idx {\val_1} {\val_2}}
{\Lam \val'. \isepV{%
{\Lam \val'. \parbox[center][4.3em]{0pt}{}
\isepV{%
\val' = \True \cr
\nthpointstoAT \loc \idx {\mkval{\val_2}{\view \viewjoin \view'}} \cr
\seen \view
......
......@@ -65,6 +65,7 @@
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
{\parbox[center][3em]{0pt}{}}
\matchwithnobinder{\boolval}
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
......@@ -84,6 +85,7 @@
\end{array}}
{\trydequeue~\queue}
{\Lam \elemopt.
{\parbox[center][3em]{0pt}{}}
\matchwithnobinder{\elemopt}
{\None }{%
\isQueue {\hphantom(\tview\hphantom{{}\viewjoin\view)}} \hview \elemViewList
......
......@@ -54,7 +54,7 @@ needs a demonstration that they allow the modular verification of realistic mult
In particular, they must enable their users to precisely specify and verify concurrent data structure implementations.
A concurrent queue is an archetypal example of such a data structure:
it is widely used in practice, for example
to manage a sequence of tasks that are generated and handled by different threads. % TODO : citations
to manage a sequence of tasks that are generated and handled by different threads.
While a coarse-grained implementation---that is, a sequential implementation
protected by a lock---%
would certainly be correct,
......@@ -66,11 +66,9 @@ often rely on subtle properties of the memory model.
An informal correctness argument is difficult, likely unreliable, hence unconvincing.
Thus, concurrent data structures are prime candidates for formal
verification. In fact, many machine-checked proofs of concurrent
data structures have appeared in the literature already, % TODO citations
% Bornat et O'Hearn, pour remonter un peu loin
% citer un survey serait bien...
data structures have appeared in the literature already~\cite{parkinson-bornat-ohearn-07,frumin2018reloc,frumin2020reloc,zakowski2018verified},
but relatively few verification efforts take place
in a weak-memory setting, % TODO citations
in a weak-memory setting~\cite{le2013correctws,le2013correctfifo},
and fewer still rely on a modular methodology,
where a proof of a concurrent data structure
and a proof of its client (perhaps a concurrent application,
......
% ------------------------------------------------------------------------------
»% ------------------------------------------------------------------------------
% Proof of the bounded queue.
......@@ -408,10 +408,11 @@ strictly monotonic, and the fact that statuses are non-negative, are not explici
\label{sec:queue:proof:la}
The specification that we wish to prove is a logically atomic Hoare triple.
The definition of such triples is given by~\citet[\S7]{iris-15} and
further refined by~\citet{jung-slides-2019}. We do not attempt to replicate
their explanation and full definition. An approximate definition that suffices to
capture the essence of logical atomicity, and to understand our proof, is:
The definition of such triples for Iris is given by~\citet[\S7]{iris-15} and further refined by~\citet{jung-slides-2019}.
It turns out that this definition can be ported as is using the connectives of \hlog.
As we will see in \sref{sec:queue:proof:tryenqueue} and \sref{sec:pipeline:proof}, the logically atomic triples so defined can be proved and are sufficient for interesting clients.
We do not attempt to replicate in this paper the full definition.
An approximate definition that suffices to capture the essence of logical atomicity, and to understand our proof, is:
%
\[\begin{array}{rcl}%
\lahoare<x>{P}{e}{\pred}
......@@ -479,6 +480,7 @@ the definition of $\queueInv$, we ought to prove the following assertion:
\end{array}}
{\tryenqueue~\queue~\elem}
{\Lam \boolval.
\parbox[center][3em]{0pt}{}
\matchwithnobinder{\boolval}
{\False}{\isQueue \tview {\hphantom(\hview\hphantom{{}\viewjoin\view)}} \elemViewList}
{\True }{%
......
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