Commit 7e715113 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Notes on related work.

parent a97b594c
\section{Related Work and conclusion}
\label{sec:related}
% Un travail assez ancien sur une structure concurrente vérifiée en SL:
% POPL 2007,
% Modular verification of a non-blocking stack.
% Preuve manuelle basée sur un examen détaillé du modèle mémoire:
% Correct and Efficient Work-Stealing for Weak Memory Models
% https://fzn.fr/readings/ppopp13.pdf
% Un peu ancien, (2015)
% Ori Lahav, Viktor Vafeiadis:
% Owicki-Gries Reasoning for Weak Memory Models
% Approche semi-automatisée (FSL automatisée dans Viper):
% https://www.cs.ubc.ca/~alexsumm/papers/SummersMueller18.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é
% Strong Logic for Weak Memory:
% il y a plusieurs case studies où des structures concurrentes sont vérifiées.
% Survey (2015) sur linearizability:
% https://bura.brunel.ac.uk/bitstream/2438/11530/1/Fulltext.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
% 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
% On Library Correctness under Weak Memory Consistency
% https://www.soundandcomplete.org/papers/Libraries-POPL-2019.pdf
\cite{vindum-birkedal-21}
......@@ -37,3 +73,26 @@ 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}
% Zakowski, preuve à base de raffinement:
% Verified Compilation of Linearizable Data Structures
% https://hal.archives-ouvertes.fr/hal-01653620/document
% dans le style raffinement, il y a aussi les articles de Turon
% TODO pour plus tard:
% model-checking
% https://www.cis.upenn.edu/~alur/Pldi07.pdf
% Checking Concurrent Data Structures Under the C/C++11 Memory Model
% https://dl.acm.org/doi/10.1145/3155284.3018749
% Verifying linearizability with hindsight
% O'Hearn et al.
% plus tard, cf. Guerraoui et al.
% et plus tard,
% Order out of Chaos: Proving Linearizability Using Local Views
% https://arxiv.org/pdf/1805.03992.pdf
% et encore plus tard,
% Proving Highly-Concurrent Traversals Correct
% https://arxiv.org/pdf/2010.00911.pdf
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