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

ICFP21 paper : Add stuff from ACM

parent f301a20b
......@@ -2612,6 +2612,99 @@ MACRO {nov} {"Nov."}
MACRO {dec} {"Dec."}
%%% ACM journal names
MACRO {cie} {"ACM Computers in Entertainment"}
MACRO {csur} {"ACM Computing Surveys"}
MACRO {dgov} {"Digital Government: Research and Practice"}
MACRO {dtrap} {"Digital Threats: Research and Practice"}
MACRO {health} {"ACM Transactions on Computing for Healthcare"}
MACRO {imwut} {"PACM on Interactive, Mobile, Wearable and Ubiquitous Technologies"}
MACRO {jacm} {"Journal of the ACM"}
MACRO {jdiq} {"ACM Journal of Data and Information Quality"}
MACRO {jea} {"ACM Journal of Experimental Algorithmics"}
MACRO {jeric} {"ACM Journal of Educational Resources in Computing"}
MACRO {jetc} {"ACM Journal on Emerging Technologies in Computing Systems"}
MACRO {jocch} {"ACM Journal on Computing and Cultural Heritage"}
MACRO {pacmcgit} {"Proceedings of the ACM on Computer Graphics and Interactive Techniques"}
MACRO {pacmhci} {"PACM on Human-Computer Interaction"}
MACRO {pacmpl} {"PACM on Programming Languages"}
MACRO {pomacs} {"PACM on Measurement and Analysis of Computing Systems"}
MACRO {taas} {"ACM Transactions on Autonomous and Adaptive Systems"}
MACRO {taccess} {"ACM Transactions on Accessible Computing"}
MACRO {taco} {"ACM Transactions on Architecture and Code Optimization"}
MACRO {talg} {"ACM Transactions on Algorithms"}
MACRO {tallip} {"ACM Transactions on Asian and Low-Resource Language Information Processing"}
MACRO {tap} {"ACM Transactions on Applied Perception"}
MACRO {tcps} {"ACM Transactions on Cyber-Physical Systems"}
MACRO {tds} {"ACM/IMS Transactions on Data Science"}
MACRO {teac} {"ACM Transactions on Economics and Computation"}
MACRO {tecs} {"ACM Transactions on Embedded Computing Systems"}
MACRO {telo} {"ACM Transactions on Evolutionary Learning"}
MACRO {thri} {"ACM Transactions on Human-Robot Interaction"}
MACRO {tiis} {"ACM Transactions on Interactive Intelligent Systems"}
MACRO {tiot} {"ACM Transactions on Internet of Things"}
MACRO {tissec} {"ACM Transactions on Information and System Security"}
MACRO {tist} {"ACM Transactions on Intelligent Systems and Technology"}
MACRO {tkdd} {"ACM Transactions on Knowledge Discovery from Data"}
MACRO {tmis} {"ACM Transactions on Management Information Systems"}
MACRO {toce} {"ACM Transactions on Computing Education"}
MACRO {tochi} {"ACM Transactions on Computer-Human Interaction"}
MACRO {tocl} {"ACM Transactions on Computational Logic"}
MACRO {tocs} {"ACM Transactions on Computer Systems"}
MACRO {toct} {"ACM Transactions on Computation Theory"}
MACRO {todaes} {"ACM Transactions on Design Automation of Electronic Systems"}
MACRO {tods} {"ACM Transactions on Database Systems"}
MACRO {tog} {"ACM Transactions on Graphics"}
MACRO {tois} {"ACM Transactions on Information Systems"}
MACRO {toit} {"ACM Transactions on Internet Technology"}
MACRO {tomacs} {"ACM Transactions on Modeling and Computer Simulation"}
MACRO {tomm} {"ACM Transactions on Multimedia Computing, Communications and Applications"}
MACRO {tompecs} {"ACM Transactions on Modeling and Performance Evaluation of Computing Systems"}
MACRO {toms} {"ACM Transactions on Mathematical Software"}
MACRO {topc} {"ACM Transactions on Parallel Computing"}
MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}
MACRO {tops} {"ACM Transactions on Privacy and Security"}
MACRO {tos} {"ACM Transactions on Storage"}
MACRO {tosem} {"ACM Transactions on Software Engineering and Methodology"}
MACRO {tosn} {"ACM Transactions on Sensor Networks"}
MACRO {tqc} {"ACM Transactions on Quantum Computing"}
MACRO {trets} {"ACM Transactions on Reconfigurable Technology and Systems"}
MACRO {tsas} {"ACM Transactions on Spatial Algorithms and Systems"}
MACRO {tsc} {"ACM Transactions on Social Computing"}
MACRO {tslp} {"ACM Transactions on Speech and Language Processing"}
MACRO {tweb} {"ACM Transactions on the Web"}
%%% Some traditional macros
MACRO {acmcs} {"ACM Computing Surveys"}
MACRO {acta} {"Acta Informatica"}
MACRO {cacm} {"Communications of the ACM"}
MACRO {ibmjrd} {"IBM Journal of Research and Development"}
MACRO {ibmsj} {"IBM Systems Journal"}
MACRO {ieeese} {"IEEE Transactions on Software Engineering"}
MACRO {ieeetc} {"IEEE Transactions on Computers"}
MACRO {ieeetcad}
{"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}
MACRO {ipl} {"Information Processing Letters"}
MACRO {jcss} {"Journal of Computer and System Sciences"}
MACRO {scp} {"Science of Computer Programming"}
MACRO {sicomp} {"SIAM Journal on Computing"}
MACRO {toois} {"ACM Transactions on Office Information Systems"}
MACRO {tcs} {"Theoretical Computer Science"}
READ
......
We use Cosmo, a modern concurrent separation logic, to formally specify and verify
an implementation of a multiple-producer multiple-consumer concurrent queue in the
setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in
which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of
logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and
the weak memory model.
We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model.
We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures.
In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.
......@@ -37,7 +37,7 @@
%% Right brace \} Tilde \~}
\NeedsTeXFormat{LaTeX2e}
\ProvidesClass{acmart}
[2020/11/15 v1.75 Typesetting articles for the Association for Computing Machinery]
[2021/04/16 v1.77 Typesetting articles for the Association for Computing Machinery]
\def\@classname{acmart}
\InputIfFileExists{acmart-preload-hook.tex}{%
\ClassWarning{\@classname}{%
......@@ -120,6 +120,10 @@
\PackageError{\@classname}{The option balance can be either true or
false}}
\ExecuteOptionsX{balance}
\define@boolkey+{acmart.cls}[@ACM@]{pbalance}[true]{}{%
\PackageError{\@classname}{The option pbalance can be either true or
false}}
\ExecuteOptionsX{pbalance=false}
\define@boolkey+{acmart.cls}[@ACM@]{natbib}[true]{%
\if@ACM@natbib
\PackageInfo{\@classname}{Explicitly selecting natbib mode}%
......@@ -487,6 +491,7 @@
\rule\z@\footnotesep\ignorespaces#1\@finalstrut\strutbox}%
\color@endgroup}}
\def\@makefnmark{\hbox{\@textsuperscript{\normalfont\@thefnmark}}}
\RequirePackage{hyperxmp}
\let\@footnotemark@nolink\@footnotemark
\let\@footnotetext@nolink\@footnotetext
\RequirePackage[bookmarksnumbered,unicode]{hyperref}
......@@ -526,7 +531,6 @@
\fi
\hypersetup{pdflang={en},
pdfdisplaydoctitle}}
\RequirePackage{hyperxmp}
\if@ACM@natbib
\let\citeN\cite
\let\cite\citep
......@@ -1268,9 +1272,12 @@
DC, USA}%
\fi
\def\acmBooktitle#1{\gdef\@acmBooktitle{#1}}
\acmBooktitle{}
\ifx\acmConference@name\@undefined\else
\acmBooktitle{Proceedings of \acmConference@name
\ifx\acmConference@name\acmConference@shortname\else
\ (\acmConference@shortname)\fi}
\ (\acmConference@shortname)\fi}
\fi
\def\@editorsAbbrev{(Ed.)}
\def\@acmEditors{}
\def\editor#1{\ifx\@acmEditors\@empty
......@@ -1302,12 +1309,16 @@
\@acmSubmissionID\fi}}%
\gdef\authors{Anonymous Author(s)}%
\else
\gdef\addresses{\@author{#2}}%
\expandafter\gdef\expandafter\addresses\expandafter{%
\expandafter\@author\expandafter{%
\csname typeset@author\the\num@authors\endcsname{#2}}}%
\gdef\authors{#2}%
\fi
\else
\if@ACM@anonymous\else
\g@addto@macro\addresses{\and\@author{#2}}%
\expandafter\g@addto@macro\expandafter\addresses\expandafter{%
\expandafter\and\expandafter\@author\expandafter{%
\csname typeset@author\the\num@authors\endcsname{#2}}}%
\g@addto@macro\authors{\and#2}%
\fi
\fi
......@@ -1358,7 +1369,14 @@
\if@ACM@anonymous\else
\g@addto@macro\addresses{\email{#1}{#2}}%
\fi}
\def\orcid#1{\unskip\ignorespaces}
\def\orcid#1{\unskip\ignorespaces%
\IfBeginWith{#1}{http}{%
\expandafter\gdef\csname
typeset@author\the\num@authors\endcsname##1{%
\href{#1}{##1}}}{%
\expandafter\gdef\csname
typeset@author\the\num@authors\endcsname##1{%
\href{https://orcid.org/#1}{##1}}}}
\def\authorsaddresses#1{\def\@authorsaddresses{#1}}
\authorsaddresses{\@mkauthorsaddresses}
\def\@titlenotes{}
......@@ -1887,7 +1905,7 @@
\else
\@specialsection{Keywords}%
\fi
\noindent\@keywords}\par\egroup
\noindent\@keywords\par}\egroup
\fi
\let\metadata@authors=\authors
\nxandlist{, }{, }{, }\metadata@authors
......@@ -2366,12 +2384,13 @@
\def\streetaddress##1{\unskip, ##1}%
\def\postcode##1{\unskip, ##1}%
\def\position##1{\unskip\ignorespaces}%
\def\institution##1{\unskip, ##1}%
\gdef\@ACM@institution@separator{, }%
\def\institution##1{\unskip\@ACM@institution@separator ##1\gdef\@ACM@institution@separator{ and }}%
\def\city##1{\unskip, ##1}%
\def\state##1{\unskip, ##1}%
\renewcommand\department[2][0]{\unskip\@addpunct, ##2}%
\def\country##1{\unskip, ##1}%
\def\and{\unskip; }%
\def\and{\unskip; \gdef\@ACM@institution@separator{, }}%
\def\@author##1{##1}%
\def\email##1##2{\unskip, \nolinkurl{##2}}%
\addresses
......@@ -2587,7 +2606,10 @@
\fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
\fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}%
\if@ACM@nonacm\else%
\if@ACM@nonacm
\fancyhead[LE]{\ACM@linecountL}%
\fancyhead[RO]{\ACM@linecountR}%
\else%
\fancyhead[LE]{\ACM@linecountL\@headfootfont\footnotesize
\acmConference@shortname,
\acmConference@date, \acmConference@venue}%
......@@ -2600,7 +2622,10 @@
\fancyfoot[C]{\if@ACM@printfolios\footnotesize\thepage\fi}%
\fancyhead[LO]{\ACM@linecountL\@headfootfont\shorttitle}%
\fancyhead[RE]{\@headfootfont\@shortauthors\ACM@linecountR}%
\if@ACM@nonacm\else%
\if@ACM@nonacm
\fancyhead[LE]{\ACM@linecountL}%
\fancyhead[RO]{\ACM@linecountR}%
\else%
\fancyhead[LE]{\ACM@linecountL\@headfootfont
\acmConference@shortname,
\acmConference@date, \acmConference@venue}%
......@@ -2931,6 +2956,25 @@
\popQED\endtrivlist\@endpefalse
}
\AtEndPreamble{%
\if@ACM@pbalance
\global\@ACM@balancefalse
\ifcase\ACM@format@nr
\relax % manuscript
\or % acmsmall
\or % acmlarge
\or % acmtog
\RequirePackage{pbalance}%
\or % sigconf
\RequirePackage{pbalance}%
\or % siggraph
\RequirePackage{pbalance}%
\or % sigplan
\RequirePackage{pbalance}%
\or % sigchi
\RequirePackage{pbalance}%
\or % sigchi-a
\fi
\fi
\if@ACM@balance
\ifcase\ACM@format@nr
\relax % manuscript
......@@ -2988,8 +3032,15 @@
\def\@tempa{#1}%
\ifx\@tempa\@empty\def\@tempa{arxiv}\fi
\def\@tempb{arxiv}%
\ifx\@tempa\@tempb
arXiv:\href{https://arxiv.org/abs/#2}{#2}\else arXiv:#2%
\ifx\@tempa\@tempb\relax
arXiv:\href{https://arxiv.org/abs/#2}{#2}%
\else
\def\@tempb{arXiv}%
\ifx\@tempa\@tempb\relax
arXiv:\href{https://arxiv.org/abs/#2}{#2}%
\else
arXiv:#2%
\fi
\fi}
\let\@vspace@orig=\@vspace
\let\@vspacer@orig=\@vspacer
......
......@@ -136,7 +136,8 @@
journal = pacmpl,
volume = "5",
number = "ICFP",
year={2021}
year={2021},
doi={10.1145/3473586}
}
@inproceedings{zakowski2018verified,
......
......@@ -28,23 +28,22 @@
% Journal information (used by PACMPL format).
% Supplied to authors by publisher for camera-ready submission.
%%% The following is specific to ICFP '21 and the paper
%%% 'Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model'
%%% by Glen Mével and Jacques-Henri Jourdan.
%%%
\setcopyright{rightsretained}
\acmPrice{}
\acmDOI{10.1145/3473571}
\acmYear{2021}
\copyrightyear{2021}
\acmSubmissionID{icfp21main-p23-p}
\acmJournal{PACMPL}
\acmVolume{5}
\acmNumber{ICFP}
\acmArticle{n}
\acmYear{2021}
\acmArticle{66}
\acmMonth{8}
\acmDOI{10.1145/nnnnnnn.nnnnnnn}
\startPage{1}
% Copyright information.
% Supplied to authors (based on authors' rights management selection;
% see authors.acm.org) by publisher for camera-ready submission.
\setcopyright{none} % For review submission
% \setcopyright{acmcopyright}
% \setcopyright{acmlicensed}
% \setcopyright{rightsretained}
% \copyrightyear{2021} % If different from \acmYear
% Bibliography style.
\bibliographystyle{ACM-Reference-Format}
......@@ -94,7 +93,7 @@
\keywords{separation logic, program verification, concurrency, weak memory, concurrent queue}
% Insert CCSXML here.
\begin{CCSXML}
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003752.10003790.10011742</concept_id>
......@@ -106,11 +105,17 @@
<concept_desc>Theory of computation~Program verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10010124.10010138.10010140</concept_id>
<concept_desc>Theory of computation~Program specifications</concept_desc>
<concept_significance>500</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}
\ccsdesc[500]{Theory of computation~Separation logic}
\ccsdesc[500]{Theory of computation~Program verification}
\ccsdesc[500]{Theory of computation~Program specifications}
\maketitle
......
......@@ -12,7 +12,7 @@ and giving intuitions about its mode of operation~(\sref{sec:queue:impl:invarian
\input{lang}
\subsection{Overview of the data stucture}
\subsection{Overview of the Data Structure}
\label{sec:queue:impl:presentation}
\input{figure-queue-impl}
......@@ -78,7 +78,7 @@ property of the queue is:
0 \leq \tail \leq \head \leq \tail+\capacity
\]
\subsection{Explanation of the code}
\subsection{Explanation of the Code}
\label{sec:queue:impl:code}
The function~\enqueue repeatedly calls \tryenqueue until it succeeds;
......@@ -127,7 +127,7 @@ and can fail either because the buffer is empty or because of a competing dequeu
\footref{fn:distinguishfail}
\subsection{Monotonicity of the internal state of the queue}
\subsection{Monotonicity of the Internal State of the Queue}
\label{sec:queue:impl:invariants}
Once the queue has been created, the reference~\refhead is only accessed from
......@@ -154,7 +154,7 @@ still $2\head$ when we overwrite it with $2\head+1$.
Symmetrically, the status is still $2\tail+1$ when a dequeuer overwrites it with
$2(\tail+\capacity)$.
\subsection{Notes on contention in the queue}
\subsection{Notes on Contention in the Queue}
\label{sec:queue:impl:contention}
A noteworthy feature of this implementation is that
......
......@@ -54,7 +54,7 @@ We detail these definitions in the following sections.
\label{fig:queue:axioms}
\end{figure}
\subsection{Public state}
\subsection{Public State}
%\input{figure-queue-ghost-isqueue}
......@@ -80,7 +80,7 @@ We do not explain the construction in more detail; the interested reader may ref
It is worth remarking that this construction makes the representation predicate exclusive: it is absurd to own simultaneously two assertions of the form $\isQueue - - -$.
\subsection{Internal invariant}
\subsection{Internal Invariant}
Along with the exclusive representation predicate $\isQueue\tview\hview\elemViewList$,
we provide the user with a persistent assertion $\queueInv$ defined in~\fref{fig:queue:inv:inv}. It contains the
......@@ -119,7 +119,7 @@ The authority of $\gqueue$ is simple: it simply ties internal values to the
public state of the queue, as explained earlier.
We now explain the other two pieces of ghost state.
\subsection{Monotonicity of statuses}
\subsection{Monotonicity of Statuses}
%\input{figure-queue-ghost-witness}
%\input{figure-queue-cmra-statlat}
......@@ -181,7 +181,7 @@ composition of the CMRA\@~\cite{timany2021monotonicity}.
In this case, we equip the product set \(\Z \times \typeView\) with
the join-semilattice structure whose definition appears in~\fref{fig:queue:cmra:statlat}.
\subsection{Available and occupied slots}
\subsection{Available and Occupied Slots}
In~\fref{fig:queue:inv:inv}, the last two lines of the invariant describe the state of each slot.
For clarity, we introduce two abbreviations:
......@@ -292,7 +292,7 @@ ownership of its item field, so that it can write to it. Hence the invariant
does not have the corresponding pointsto assertion. The thread must give it back
when updating the status.
\subsection{Slot tokens}
\subsection{Slot Tokens}
%\input{figure-queue-ghost-token}
......@@ -404,7 +404,7 @@ and verified. However, they are not needed to
prove that the code satisfies its specification. For example, the fact that \reftail and \refhead are
strictly monotonic, and the fact that statuses are non-negative, are not explicitly used.
\subsection{Logical atomicity}
\subsection{Logical Atomicity}
\label{sec:queue:proof:la}
The specification that we wish to prove is a logically atomic Hoare triple.
......
\subsection{Specification under sequential consistency}
\subsection{Specification Under Sequential Consistency}
\label{sec:queue:spec:sc}
\input{figure-queue-spec-sc}
......@@ -125,7 +125,7 @@ For now, we illustrate how a weaker specification can be easily deduced from thi
% ------------------------------------------------------------------------------
\subsubsection{A Persistent Specification}
\subsubsection{A persistent specification}
\label{sec:queue:spec:sc:persistent}
If it were not for logical atomicity, and we still wanted to share the ownership
......
\subsection{Specification in a sequential setting}
\subsection{Specification in a Sequential Setting}
\label{sec:queue:spec:seq}
\input{figure-queue-spec-seq}
......
\subsection{Specification under weak memory}
\subsection{Specification Under Weak Memory}
\label{sec:queue:spec:weak}
\begin{figure}
......
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