quark.tex

%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
%\documentclass[sigplan,review]{acmart}
\documentclass[sigplan,screen]{acmart}
%\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For final camera-ready submission, w/ required CCS and ACM Reference
%\documentclass[acmsmall]{acmart}\settopmatter{}

%\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{caption}
\usepackage{subcaption}
\usepackage{xspace}
\usepackage{mathtools}
\usepackage{mathpartir}
\usepackage{ifpdf}
\usepackage{graphicx}
%\usepackage[usenames,dvipsnames]{color}
\usepackage{stmaryrd}
%\usepackage[numbers]{natbib}
\usepackage{amsthm}
\usepackage{listings}          % format code
\usepackage{wrapfig}
\usepackage{textcomp}
\usepackage{tabularx}
\usepackage{color}
\usepackage{url}
\usepackage{tikz}
\usepackage{multirow,array}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{microtype}
\usepackage{balance} % To balance columns on last page

\input{mydefs.tex}

%%% The following is specific to PLDI '22 and the paper
%%% 'RunTime-Assisted Convergence in Replicated Data Types'
%%% by Gowtham Kaki, Prasanth Prahladan, and Nicholas V. Lewchenko.
%%%
\setcopyright{rightsretained}
\acmPrice{}
\acmDOI{10.1145/3519939.3523724}
\acmYear{2022}
\copyrightyear{2022}
\acmSubmissionID{pldi22main-p536-p}
\acmISBN{978-1-4503-9265-5/22/06}
\acmConference[PLDI '22]{Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation}{June 13--17, 2022}{San Diego, CA, USA}
\acmBooktitle{Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI '22), June 13--17, 2022, San Diego, CA, USA}

%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
%% Citation style
%% Note: author/year citations are required for papers published as an
%% issue of PACMPL.
\citestyle{acmnumeric}   %% For author/year citations


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format must update the '\documentclass' and
%% topmatter commands above; see 'acmart-sigplanproc-template.tex'.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\begin{document}

%% Title information
\title[RunTime-Assisted Convergence in Replicated Data Types]{RunTime-Assisted Convergence \\ in Replicated Data Types}
%% [Short Title] is optional;
                                        %% when present, will be used in
                                        %% header instead of Full Title.
%\titlenote{with title note}             %% \titlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'
%\subtitle{Subtitle}                     %% \subtitle is optional
%\subtitlenote{with subtitle note}       %% \subtitlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'


%% Author information
%% Contents and number of authors suppressed with 'anonymous'.
%% Each author should be introduced by \author, followed by
%% \authornote (optional), \orcid (optional), \affiliation, and
%% \email.
%% An author may have multiple affiliations and/or emails; repeat the
%% appropriate command.
%% Many elements are not rendered, but should be provided for metadata
%% extraction tools.

%% Author with single affiliation.
\author{Gowtham Kaki}
%\authornote{with author1 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
\orcid{0000-0002-4189-3189}             %% \orcid is optional
\affiliation{
%  \position{Position1}
%  \department{Department1}              %% \department is recommended
  \institution{University of Colorado Boulder}            %% \institution is required
%  \streetaddress{Street1 Address1}
  \city{Boulder}
%  \state{State1}
%  \postcode{Post-Code1}
  \country{USA}                    %% \country is recommended
}
\email{gowtham.kaki@colorado.edu}          %% \email is recommended

%% Second Author
\author{Prasanth Prahladan}
%\authornote{with author2 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
%\orcid{nnnn-nnnn-nnnn-nnnn}             %% \orcid is optional
\affiliation{
%  \position{Position2a}
%  \department{Department2a}             %% \department is recommended
  \institution{University of Colorado Boulder}           %% \institution is required
%  \streetaddress{Street2a Address2a}
  \city{Boulder}
%  \state{State2a}
%  \postcode{Post-Code2a}
  \country{USA}                   %% \country is recommended
}
\email{prasanth.prahladan@colorado.edu}         %% \email is recommended

%% Third Author
\author{Nicholas V. Lewchenko}
%\authornote{with author2 note}          %% \authornote is optional;
                                        %% can be repeated if necessary
%\orcid{nnnn-nnnn-nnnn-nnnn}             %% \orcid is optional
\affiliation{
%  \position{Position2a}
%  \department{Department2a}             %% \department is recommended
  \institution{University of Colorado Boulder}           %% \institution is required
%  \streetaddress{Street2a Address2a}
  \city{Boulder}
%  \state{State2a}
%  \postcode{Post-Code2a}
  \country{USA}                   %% \country is recommended
}
\email{nile1033@colorado.edu}         %% \email is recommended
%

%% Abstract
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\begin{abstract}
  We propose a runtime-assisted approach to enforce convergence in
  distributed executions of replicated data types. The key
  distinguishing aspect of our approach is that it guarantees
  convergence \emph{unconditionally} -- without requiring data type
  operations to satisfy algebraic laws such as commutativity and
  idempotence. Consequently, programmers are no longer obligated to
  prove convergence on a per-type basis. Moreover, our approach lets
  sequential data types be reused in a distributed setting by
  extending their implementations rather than refactoring them.  The
  novel component of our approach is a distributed runtime that
  orchestrates \emph{well-formed } executions that are guaranteed to
  converge. Despite the utilization of a runtime, our approach comes
  at no additional cost of latency and availability. Instead, we
  introduce a novel tradeoff against a metric called \emph{staleness},
  which roughly corresponds to the time taken for replicas to
  converge. We implement our approach in a system called \quark and
  conduct a thorough evaluation of its tradeoffs. 
%%We also briefly discuss the utility of our approach in
%%realizing causal coherency semantics in shared-memory concurrent
%%systems,
\end{abstract}


%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
\begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10010147.10010919.10010177</concept_id>
<concept_desc>Computing methodologies~Distributed programming languages</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10010520.10010575.10010578</concept_id>
<concept_desc>Computer systems organization~Availability</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011074.10011099.10011692</concept_id>
<concept_desc>Software and its engineering~Formal software verification</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Computing methodologies~Distributed programming languages}
\ccsdesc[500]{Computer systems organization~Availability}
\ccsdesc[300]{Software and its engineering~Formal software verification}
%% End of generated code


%% Keywords
%% comma separated list
\keywords{Replication, MRDT, CRDT, Runtime, Convergence, Concurrent
Revisions, Causal Consistency, Decentralized Systems}  %% \keywords are mandatory in final camera-ready submission


%% \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.
\maketitle


\input{introduction}

\input{motivation}

\input{abstract-semantics}

\input{concrete-semantics}

\input{implementation}

\input{evaluation}

\input{related}

%% Acknowledgments
\begin{acks}                            %% acks environment is optional
  We thank the anonymous reviewers and our shepherd Doug Lea for their
  thoughtful comments. First author has benefited from discussions
  with Anmol Sahoo and Suresh Jagannathan. Anmol has also developed
  and maintained the OCaml-Scylla library, which is a key piece of
  infrastructure underlying \quark.
\end{acks}

%% Bibliography
\bibliography{all}

\end{document}