related.tex 4.21 KB
Newer Older
Jacques-Henri Jourdan's avatar
Intro    
Jacques-Henri Jourdan committed
1
\section{Related Work and conclusion}
2
3
\label{sec:related}

POTTIER Francois's avatar
POTTIER Francois committed
4
5
6
7
8
9
10
11
12
13
14
15
% 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

POTTIER Francois's avatar
POTTIER Francois committed
16
17
18
19
% Approche semi-automatisée sans mémoire faible:
% Automated Verification of CountDownLatch
% https://arxiv.org/abs/1908.09758
% Approche semi-automatisée avec mémoire faible (FSL automatisée dans Viper):
POTTIER Francois's avatar
POTTIER Francois committed
20
21
22
23
24
25
26
27
28
29
30
31
32
% 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

POTTIER Francois's avatar
POTTIER Francois committed
33
34
% Causal Linearizability, Doherty and Derrick 2016
% Linearizability in a weak-memory setting: Smith, Winter, Colvin 2018
POTTIER Francois's avatar
POTTIER Francois committed
35
36
37
38
39
40
41
42
43
44
% 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
POTTIER Francois's avatar
POTTIER Francois committed
45

POTTIER Francois's avatar
POTTIER Francois committed
46
47
48
49
% Cet article est probablement à connaître et à citer:
% ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
% https://arxiv.org/abs/2006.13635

POTTIER Francois's avatar
POTTIER Francois committed
50
51
52
53
54
55
56
\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?

57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
% 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}
POTTIER Francois's avatar
POTTIER Francois committed
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

% 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