Commit e063582d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Changements pour la version finale finale ICFP.

parent ff0a1245
......@@ -2964,7 +2964,7 @@
publisher = springer,
series = lncs,
volume = "3170",
URL = "http://dx.doi.org/10.1007/978-3-540-28644-8_2",
doi = "10.1007/978-3-540-28644-8_2",
}
 
@Article{brookes-07,
......@@ -5778,7 +5778,7 @@
number = "{POPL}",
pages = "60:1--60:28",
year = "2019",
URL = "https://doi.org/10.1145/3290373",
doi = "10.1145/3290373",
}
 
@TechReport{emms-leiss-96,
......
......@@ -50,7 +50,8 @@
booktitle={European Conference on Object-Oriented Programming},
pages={207--231},
year={2014},
organization={Springer}
organization={Springer},
doi={10.1007/978-3-662-44202-9_9}
}
@Unpublished{vindum-frumin-birkedal-21,
......@@ -75,7 +76,8 @@
author={Frumin, Dan and Krebbers, Robbert and Birkedal, Lars},
booktitle={Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
pages={442--451},
year={2018}
year={2018},
doi={10.1145/3209108.3209174}
}
@article{frumin2020reloc,
......@@ -90,7 +92,8 @@
author={Jacobs, Bart and Piessens, Frank},
booktitle={Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
pages={271--282},
year={2011}
year={2011},
doi={10.1145/1926385.1926417}
}
@inproceedings{le2013correctws,
......@@ -116,7 +119,8 @@
booktitle={International Colloquium on Automata, Languages, and Programming},
pages={311--323},
year={2015},
organization={Springer}
organization={Springer},
doi={10.1007/978-3-662-47666-6_25}
}
@article{dongol2015verifying,
......@@ -127,7 +131,8 @@
number={2},
pages={1--43},
year={2015},
publisher={ACM}
publisher={ACM},
doi={10.1145/2796550}
}
@article{gueneau2021theorems,
......@@ -171,5 +176,6 @@
title={Practical lock-freedom},
author={Fraser, Keir},
year={2004},
institution={University of Cambridge, Computer Laboratory}
institution={University of Cambridge, Computer Laboratory},
doi={}
}
\subsection{Specification Under Sequential Consistency}
\subsection{Specification under Sequential Consistency}
\label{sec:queue:spec:sc}
\input{figure-queue-spec-sc}
......@@ -125,8 +125,7 @@ For now, we illustrate how a weaker specification can be easily deduced from thi
% ------------------------------------------------------------------------------
\subsubsection{A persistent specification}
\label{sec:queue:spec:sc:persistent}
\paragraph{A persistent specification}
If it were not for logical atomicity, and we still wanted to share the ownership
of the queue, we would have little choice left than renouncing to an exclusive
......
\subsection{Specification Under Weak Memory}
\subsection{Specification under Weak Memory}
\label{sec:queue:spec:weak}
\begin{figure}
......
......@@ -64,7 +64,7 @@ We found that our method of combining logically atomic triples with views is exp
Previous works include the generalization of various methods to weak consistency: \citet{le2013correctws,le2013correctfifo} used manual methods directly tied to the axiomatic memory model to prove the correctness of a queue and of a work-stealing algorithm, while \citet{lahav2015owicki} adapted the Owicki-Gries methodology to the release-acquire fragment of the C11 memory model and applied it to verify a read-copy-update library.
The idea of a separation logic for programs with a relaxed memory semantics has been first developed in the RSL logic~\cite{vafeiadis-narayan-13}, and further developed in subsequent work~\cite{turon-vafeiadis-dreyer-14,doko-vafeiadis-16,kaiser-17,dang-20,mevel-jourdan-pottier-20}.
None of these papers addressed the problem of the full functional correctness of a data structure.
In particular, the specification proposed for a circular buffer in GPS~\cite{turon-vafeiadis-dreyer-14} is a weak specification in the style of \sref{sec:queue:spec:sc:persistent}: in contrast to ours, it does not specify in which order the elements leave the queue.
In particular, the specification proposed for a circular buffer in GPS~\cite{turon-vafeiadis-dreyer-14} is a weak specification in the style of the persistent specification given at the end of \sref{sec:queue:spec:sc}: in contrast to ours, it does not specify in which order the elements leave the queue.
% TODO pour plus tard:
......
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