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

related work.

parent 7521322a
......@@ -137,3 +137,12 @@
pages={1881--1890},
year={2018}
}
@article{smith2019linearizability,
title={Linearizability on hardware weak memory models},
author={Smith, Graeme and Winter, Kirsten and Colvin, Robert J},
journal={Formal Aspects of Computing},
pages={1--32},
year={2019},
publisher={Springer}
}
......@@ -112,6 +112,7 @@ For now, we illustrate how a weaker specification can be easily deduced from thi
% ------------------------------------------------------------------------------
\subsubsection{A Persistent Specification}
\label{sec:queue:spec:sc:persistent}
If it were not for logical atomicity, and we still wanted to share the ownership
of the queue, we would have little choice left than renouncing to an exclusive
......
......@@ -27,56 +27,45 @@ In particular, for this reason, our queue implementation \emph{is not} a refinem
The refinement approach has also been used to prove correct some data structures used in a concurrent garbage collector~\cite{zakowski2018verified}.
In a weakly consistent setting,
% Vérification de bibliothèques en mémoire faible :
In a weakly consistent setting, new problems arise.
As discussed in \sref{sec:queue:spec:weak}, even the definition of linearizability needs special care.
\citet{smith2019linearizability} propose new definitions of linearizability for the case of weak memory models.
% Ce papier est le seul sur le sujet qui est vraiment publié ailleurs qu'arxiv. Vu que je n'ai pas lu les autres, je préfère ne pas les mentionner, de peur que ce soit n'importe quoi:
% On Library Correctness under Weak Memory Consistency
% https://www.soundandcomplete.org/papers/Libraries-POPL-2019.pdf
% Causal Linearizability, Doherty and Derrick 2016
% Linearizability in a weak-memory setting: Smith, Winter, Colvin 2018
% Des mêmes auteurs: https://arxiv.org/abs/1810.09612v1
% Preuve manuelle de queue basée sur un examen détaillé du modèle mémoire:
% Correct and Efficient Work-Stealing for Weak Memory Models le2013correctws
% Correct and efficient bounded FIFO queues le2013correctfifo
% Généralisation d'Owicki-Gries à release-acquire, application à RCU
% Owicki-Gries Reasoning for Weak Memory Models lahav2015owicki
% Strong Logic for Weak Memory:
% {GPS:} navigating weak memory with ghosts, protocols, and separation
% il y a plusieurs case studies où des structures concurrentes sont vérifiées.
% Ok. mais leur spec est une spec faible qui ne parle pas d'atomicité logique. Ils utilisent un prédicat que tous les éléments doivent vérifier
% Constantin Enea, "Verifying Visibility-Based Weak Consistency".
% Technique de preuve à base de simulations (ce n'est pas de la
% logique de séparation), avec mise en oeuvre basé sur des prouveurs
% automatiques.
\nocite{krishna-emmi-enea-jovanovic-20}
\nocite{emmi-enea-19}
\begin{comment}
% Extrait de mon journal, POPL 2019:
Constantin Enea. "Weak-Consistency Specification via Visibility Relaxation".
Objets concurrents (dans le JDK par exemple) ont des specs faibles. Par
exemple, la méthode size() sur une collection renvoie un résultat plus ou
moins fiable s'il y a des updates en parallèle. Il cherche une façon simple et
générique de spécifier ces comportements relâchés. Approche axiomatique:
parler de linéarisation, mais parler aussi de visibilité. Pour chaque
linéarisation des opérations précédentes, on se demande lesquelles sont
visibles. Je n'y comprends pas grand-chose. Il y a des relations po, hb, etc.
En gros, c'est un modèle mémoire faible axiomatique, mais pas pour la mémoire
primitive; pour un objet concurrent avec des opérations add, remove, size,
etc. Tout ça donne des version relâchées de la notion de linéarisabilité, je
suppose. Ensuite, il y a du test; il veut annoter des méthodes du JDK avec des
specs dans son langage, et détecter (par le test) si ces specs sont bien
respectées. Je ne suis pas. Jens Palsberg demande comment on peut vérifier un
client qui utilise plusieurs objets différents avec des specs différentes.
Réponse pas très claire.
\end{comment}
In contrast, other authors have developed new kinds of specifications which allow for weak behaviors of the library itself~\cite{krishna-emmi-enea-jovanovic-20,emmi-enea-19,raad-19}.
We found that our method of combining logically atomic triples with views is expressive and allow for concise specifications at the same time.
%% % Constantin Enea, "Verifying Visibility-Based Weak Consistency".
%% % Technique de preuve à base de simulations (ce n'est pas de la
%% % logique de séparation), avec mise en oeuvre basé sur des prouveurs
%% % automatiques.
%% \nocite{krishna-emmi-enea-jovanovic-20}
%% \nocite{emmi-enea-19}
%% \begin{comment}
%% % Extrait de mon journal, POPL 2019:
%% Constantin Enea. "Weak-Consistency Specification via Visibility Relaxation".
%% Objets concurrents (dans le JDK par exemple) ont des specs faibles. Par
%% exemple, la méthode size() sur une collection renvoie un résultat plus ou
%% moins fiable s'il y a des updates en parallèle. Il cherche une façon simple et
%% générique de spécifier ces comportements relâchés. Approche axiomatique:
%% parler de linéarisation, mais parler aussi de visibilité. Pour chaque
%% linéarisation des opérations précédentes, on se demande lesquelles sont
%% visibles. Je n'y comprends pas grand-chose. Il y a des relations po, hb, etc.
%% En gros, c'est un modèle mémoire faible axiomatique, mais pas pour la mémoire
%% primitive; pour un objet concurrent avec des opérations add, remove, size,
%% etc. Tout ça donne des version relâchées de la notion de linéarisabilité, je
%% suppose. Ensuite, il y a du test; il veut annoter des méthodes du JDK avec des
%% specs dans son langage, et détecter (par le test) si ces specs sont bien
%% respectées. Je ne suis pas. Jens Palsberg demande comment on peut vérifier un
%% client qui utilise plusieurs objets différents avec des specs différentes.
%% Réponse pas très claire.
%% \end{comment}
Previous works include the generalization of various methods to weak-consistency: \citet{le2013correctws,le2013correctfifo} used manual methods directly tied to the axiomatic memory model to prove the correctness of a queue and of a work-stealing algorithm, while \citet{lahav2015owicki} adapted the Owicki-Gries methodology to the release-acquire fragment of the C11 memory model and applied it to verify a read-copy-update library.
The idea of a separation logic for programs with a relaxed memory semantics has been first developed in the RSL logic~\cite{vafeiadis-narayan-13}, and further developed in subsequent work~\cite{turon-vafeiadis-dreyer-14,doko-vafeiadis-16,kaiser-17,dang-20,mevel-jourdan-pottier-20}.
None of these papers addressed the problem of the full functional correctness of a data structure.
In particular, the specification proposed for a circular buffer in GPS~\cite{turon-vafeiadis-dreyer-14} is a weak specification in the style of \sref{sec:queue:spec:sc:persistent}: in contrast to ours, it does not specify in which order the elements leave the queue.
% TODO pour plus tard:
......
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