Commit 8f047ba8 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Create related.tex and suggest two citations.

parent 0d8afb76
......@@ -105,6 +105,7 @@
\input{lang}
\input{queue}
\input{pipeline}
\input{related}
% ------------------------------------------------------------------------------
% Bibliography.
......
\section{Related Work}
\label{sec:related}
% 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}
Supports Markdown
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