Commit b2eb7fa1 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Citations.

parent 2ad3246f
......@@ -17188,6 +17188,16 @@
year = "2010",
}
 
@InProceedings{vindum-birkedal-21,
author = "Simon Friis Vindum and Lars Birkedal",
title = "Contextual refinement of the {Michael-Scott} queue",
booktitle = cpp,
pages = "76--90",
month = jan,
year = "2021",
URL = "https://cs.au.dk/~birke/papers/2021-ms-queue-final.pdf",
}
@InCollection{viper,
author = "Peter M{\"{u}}ller and Malte Schwerhoff and Alexander
J. Summers",
......
......@@ -86,11 +86,12 @@ and a proof of its client (perhaps a concurrent application,
or another concurrent data structure)
can be modularly combined.
In this paper, we present a specification of a concurrent queue, in a weak-memory setting,
and we formally that a particular concurrent queue implementation satisfies this specification.
While other such formalizations already exist% TODO : citations, e.g. la queue Michael-Scott de Vindum
, we consider a more realistic setting where memory does not obey sequential consistency but is rather described by a more subtle weak memory model.
Such a formalization is innovative and challenging in several aspects:
In this paper, we present a specification of a concurrent queue,
and we formally verify that a particular concurrent queue implementation satisfies this specification.
While other such formalizations already exist in a sequentially-consistent
setting~\cite{vindum-birkedal-21,vindum-frumin-birkedal-21}, % TODO : more citations
we consider a weak-memory setting.
Such a formalization effort is innovative and challenging in several aspects:
\begin{itemize}
\item Weak memory models are infamously known for the subtlety of the reasoning they impose. We choose to use \cosmo~\cite{mevel-jourdan-pottier-20}, a recently developed concurrent separation logic based on Iris supporting the weak memory model of \mocaml{}~\cite{mocaml,dolan-18}.
We believe it is a good balance between the ease of reasoning in the logic and the flexibility and performance of the underlying memory model.
......
......@@ -45,3 +45,12 @@
year={2014},
organization={Springer}
}
@Unpublished{vindum-frumin-birkedal-21,
author = {Simon Friis Vindum and Dan Frumin and Lars Birkedal},
title={Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook's Folly Library},
note = {Submitted for publication},
month = mar,
year = 2021,
note = {\url{https://cs.au.dk/~birke/papers/mpmc-queue.pdf}},
}
\section{Related Work and conclusion}
\label{sec:related}
% Linearizability in a weak-memory setting: Smith, Winter, Colvin
\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?
% 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
......
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