diff --git a/papers/icfp2021/local.bib b/papers/icfp2021/local.bib
index 9980ff2c7662ad6d8d72c4ff5a51f291aa3b2a58..b0b0a05dc1c6523dee227eb1cd27f928ebb69d4b 100644
--- a/papers/icfp2021/local.bib
+++ b/papers/icfp2021/local.bib
@@ -128,4 +128,12 @@
author={Anonymous},
year={2021},
note={Under submission at ICFP'21}
-}
\ No newline at end of file
+}
+
+@inproceedings{zakowski2018verified,
+ title={Verified compilation of linearizable data structures: mechanizing rely guarantee for semantic refinement},
+ author={Zakowski, Yannick and Cachera, David and Demange, Delphine and Pichardie, David},
+ booktitle={Proceedings of the 33rd Annual ACM Symposium on Applied Computing},
+ pages={1881--1890},
+ year={2018}
+}
diff --git a/papers/icfp2021/related.tex b/papers/icfp2021/related.tex
index ad7aa0525ebaaa4ec69372545ccfe506092fdbcc..a9e6ffc374a8e1aec2ac65f30cbe024e997db5cd 100644
--- a/papers/icfp2021/related.tex
+++ b/papers/icfp2021/related.tex
@@ -6,73 +6,25 @@ Several approaches were tried, targeting various verification frameworks, variou
The notion of \emph{linearizability} is central for specifying such libraries.
\citet{dongol2015verifying} gave a survey of the different techniques used for linearizability of concurrent libraries at that time.
-%TODO : corriger l'netrée biblio de l'article d'Armaël
-Of particular interest in the context of separation logic is the technique of \emph{logical tomicity}, which has been recently proved to be equivalent to linearizability~\cite{gueneau2021theorems}.
-This concept has been developped through several iterations
-
-
-
-In order to state a weak form o linearizability, the specification we used is based on the concept of logical atomicity.
-We discovered
-
-
-
-
-
-% Survey (2015) sur linearizability:
-% https://bura.brunel.ac.uk/bitstream/2438/11530/1/Fulltext.pdf
-% dongol2015verifying
-
-% Pour l'atomicité logique en SL:
-% Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning
-% TaDA: A Logic for Time and Data Abstraction
-% Expressive modular fine-grained concurrency specification
-% Modular Reasoning about Separation of Concurrent Data Structures
-% The Future is Ours: Prophecy Variables in Separation Logic
-
-
-
-% Vérification de structures concurrentes en SL :
-
-% Cet article est probablement à connaître et à citer:
-% ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
-% ReLoC: A mechanised relational logic for fine-grained concurrency
-% https://arxiv.org/abs/2006.13635
-
-% Preuve d'une structure de queue en Iris :
-% Contextual Refinement of the Michael-Scott Queue
-% => Utilise Reloc pour faire une preuve par rafinement d'une queue coarse-grained
-\cite{vindum-birkedal-21}
-\cite{vindum-frumin-birkedal-21}
-% glen dit que c'est quasiment la même implémentation que nous
-% mais la spec est différente, ils utilisent ReLoC
-% donc une logique relationnelle?
-
-
-% dans le style raffinement, il y a aussi les articles de Turon
-
-% POPL 2007, Modular verification of a non-blocking stack. parkinson-bornat-ohearn-07
+%TODO : corriger l'entrée biblio de l'article d'Armaël pour la version finale
+Of particular interest in the context of separation logic is the technique of \emph{logical tomicity}, which has been recently proved to be equivalent to linearizability~\cite{gueneau2021theorems} in the context of a sequentially consistent model.
+This concept has been developed through several iterations over the last decade~\cite{da2014tada,iris-15,jacobs2011expressive,svendsen-birkedal-parkinson-hocap-13,jung-prophecies-20}.
+In the present work, we adapted an unpublished, modern version of Iris' logically atomic triples~\cite{jung-slides-2019}, and adapted it to the logic \cosmo{}.
+This is, to the best of our knowledge, the first use of logical atomicity in a weakly consistent setting.
+% TODO : je ne sais pas quoi dire de ça. Dans la mesure où ce n'est qu'un preprint arxiv, je propose de ne pas en parler pour l'instant.
% Concurrent Data Structures Linked in Time
% Delbianco et al.
% https://germand.github.io/pubs/relink-ECOOP17.pdf
% c'est de la logique de séparation, avec preuve de linéarisabilité,
-% et état fantôme
-
-
-
+% et état fantôme pour l'historique
-
-% Vérification de structures concurrentes hors SL :
-
-% Dodds et al. (2015)
-% A Scalable, Correct Time-Stamped Stack
-% pas de logique de séparation je crois, mais une preuve (manuelle?) de linéarisabilité
-% pas de mémoire faible (utilisation d'atomiques SC de C11)
-
-% Zakowski, preuve à base de raffinement:
-% Verified Compilation of Linearizable Data Structures
-% https://hal.archives-ouvertes.fr/hal-01653620/document
+Another popular approach for proving the correctness of concurrent libraries is the use of refinement with respect to a simpler implementation.
+This is the track chosen by ReLoc~\cite{frumin2018reloc}, which has recently been combined with logical atomicity~\cite{frumin2018reloc}.
+Interestingly, Reloc has been recently used for proving the correctness of a concurrent queue implementation, which is very close to ours~\cite{vindum-birkedal-21,vindum-frumin-birkedal-21}.
+However, this proof does not handle relaxed memory behaviors, so that it did not have to provide a solution to the problem of specifying the lack of happens-before relationship between some data structure accesses, which we discussed in \sref{sec:queue:spec:weak}.
+In particular, for this reason, our queue implementation \emph{is not} a refinement of a naive implementation which would use a lock for guarding a sequential implementation, so a refinement-based approach would be useful for proving our library correct.
+The refinement approach has also been used to prove correct some data structures used in a concurrent garbage collector~\cite{zakowski2018verified}.
@@ -127,6 +79,9 @@ Réponse pas très claire.
\end{comment}
+% TODO pour plus tard:
+
+
% Approche semi-automatisée sans mémoire faible:
% Automated Verification of CountDownLatch
@@ -136,7 +91,6 @@ Réponse pas très claire.
% => Dans les deux cas : pas pertinent pour ce papier. cela ne parle pas de véification de structure de données, ni d'atomicité logique
-% TODO pour plus tard:
% model-checking
% https://www.cis.upenn.edu/~alur/Pldi07.pdf
@@ -155,10 +109,15 @@ Réponse pas très claire.
% https://arxiv.org/pdf/2010.00911.pdf
+% Dodds et al. (2015)
+% A Scalable, Correct Time-Stamped Stack
+% pas de logique de séparation je crois, mais une preuve (manuelle?) de linéarisabilité
+% pas de mémoire faible (utilisation d'atomiques SC de C11)
+% => Ça me semble pas intéressant pour nous. En plus, le focus est surtout sur l'algorithme lui-même plutôt que sur sa preuve.
+% TODO : dans le style raffinement, il y a aussi les articles de Turon
-
-
-
-
-
+% POPL 2007, Modular verification of a non-blocking stack. parkinson-bornat-ohearn-07
+% Il semblerait que la spec est très faible : la stack n'est en fait, je crois, qu'un bag de pointeurs.
+% quand on fait push, il faut donner l'ownership du pointer qu'on y met, quand on fait pop, on récupère un pointeur, mais on ne sait rien dessus (pas de spécification fonctionnelle)
+% TODO : quoi dire là-dessus. Pour l'instant, j'en parle pas, ça a l'aire vraiment trop éloigné de ce qu'on fait.