Commit 0d860ddb authored by Glen Mével's avatar Glen Mével
Browse files

small cleanup

parent d4d9c914
......@@ -11,8 +11,3 @@ loop:
clean::
latexmk -c
rm -rf `cat .gitignore`
WWW=yquem.inria.fr:public_html/publis/mevel-jourdan-pottier-cosmo-2020.pdf
export: all
scp -p -B -C main.pdf $(WWW)
......@@ -6,7 +6,6 @@ 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'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 atomicity}, 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 adapt an unpublished, modern version of Iris's logically atomic triples~\cite{jung-slides-2019}, to the setting of \cosmo{}.
......
Markdown is supported
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