correctness-model/writeup/paper.tex

   1 %-----------------------------------------------------------------------------
   2 %
   3 %               Template for sigplanconf LaTeX Class
   4 %
   5 % Name:         sigplanconf-template.tex
   6 %
   7 % Purpose:      A template for sigplanconf.cls, which is a LaTeX 2e class
   8 %               file for SIGPLAN conference proceedings.
   9 %
  10 % Guide:        Refer to "Author's Guide to the ACM SIGPLAN Class,"
  11 %               sigplanconf-guide.pdf
  12 %
  13 % Author:       Paul C. Anagnostopoulos
  14 %               Windfall Software
  15 %               978 371-2316
  16 %               paul@windfall.com
  17 %
  18 % Created:      15 February 2005
  19 %
  20 %-----------------------------------------------------------------------------
  21
  22
  23 \documentclass[nocopyrightspace]{sig-alternate}
  24
  25 % The following \documentclass options may be useful:
  26 %
  27 % 10pt          To set in 10-point type instead of 9-point.
  28 % 11pt          To set in 11-point type instead of 9-point.
  29 % authoryear    To obtain author/year citation style instead of numeric.
  30 \usepackage{times}
  31 \usepackage[scaled]{helvet} % see www.ctan.org/get/macros/latex/required/psnfss/psnfss2e.pdf
  32 \usepackage{url}                  % format URLs
  33 \usepackage{listings}          % format code
  34 \usepackage{enumitem}      % adjust spacing in enums
  35 \sloppy
  36 \usepackage[colorlinks=true,allcolors=blue,breaklinks,draft]{hyperref}
  37 \newcommand{\doi}[1]{doi:~\href{http://dx.doi.org/#1}{\Hurl{#1}}}   % print a hyperlinked DOI
  38
  39 \usepackage{rotating}
  40 \usepackage{algorithm}% http://ctan.org/pkg/algorithms
  41 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
  42 %\usepackage{syntax}
  43 %\usepackage{times}
  44
  45 \usepackage{amsmath}
  46 \usepackage{graphicx}
  47 \usepackage{xspace}
  48 \usepackage{amssymb}
  49
  50 \usepackage{listings}
  51 \usepackage{color}
  52 \usepackage{textcomp}
  53 \definecolor{listinggray}{gray}{0.9}
  54 \definecolor{lbcolor}{rgb}{0.9,0.9,0.9}
  55 \lstset{
  56         % backgroundcolor=\color{lbcolor},
  57         % rulecolor=,
  58         % aboveskip={1.5\baselineskip},
  59         % extendedchars=true,
  60         tabsize=3,
  61         language=C++,
  62         basicstyle=\ttfamily\scriptsize,
  63         upquote=true,
  64         columns=fixed,
  65         showstringspaces=false,
  66         breaklines=true,
  67         prebreak = \raisebox{0ex}[0ex][0ex]{\ensuremath{\hookleftarrow}},
  68         % frame=single,
  69         showtabs=false,
  70         showspaces=false,
  71         showstringspaces=false,
  72         identifierstyle=\ttfamily,
  73         keywordstyle=\color[rgb]{0,0,1},
  74         commentstyle=\color[rgb]{0.133,0.545,0.133},
  75         stringstyle=\color[rgb]{0.627,0.126,0.941},
  76         numbers=left,
  77         numberstyle=\tiny,
  78         numbersep=8pt,
  79         escapeinside={/*@}{@*/}
  80 }
  81
  82 \usepackage{algpseudocode}
  83
  84 \usepackage[utf8]{inputenc}
  85 \usepackage[english]{babel}
  86
  87 \newtheorem{theorem}{Theorem}
  88 \newtheorem{corollary}{Corollary}[theorem]
  89 \newtheorem{lemma}[theorem]{Lemma}
  90
  91 \newcommand{\hb}[0]{\textit{hb}\xspace}
  92 \newcommand{\mo}[0]{\textit{mo}\xspace}
  93 \newcommand{\moc}[0]{\textit{moc}\xspace}
  94
  95 \newcommand{\address}[0]{\texttt{address}\xspace}
  96 \newcommand{\StoreOp}[0]{\textit{StoreOps}\xspace}
  97 \newcommand{\LoadOp}[0]{\textit{LoadOps}\xspace}
  98 \newcommand{\Ops}[0]{\textit{Ops}\xspace}
  99 \newcommand{\Address}[0]{\textit{Address}\xspace}
 100 \newcommand{\Value}[0]{\textit{Value}\xspace}
 101 \newcommand{\movable}[0]{\textit{movable}\xspace}
 102
 103 \newcommand{\pushcode}[1][1]{\hskip\dimexpr#1\algorithmicindent\relax}
 104
 105 %% Not used yet
 106 % \usepackage{times}
 107 % \usepackage{latexsym}
 108 % \usepackage{amsfonts}
 109 % \usepackage{amsthm}
 110 % \usepackage{txfonts}
 111 % \usepackage{url}
 112 % \usepackage{subfigure}
 113
 114 % \usepackage{bbm}
 115 % \usepackage{stfloats}
 116
 117 \newcommand{\squishlist}{
 118   \begin{list}{$\bullet$}
 119     {
 120       \setlength{\itemsep}{1pt}
 121       \setlength{\parsep}{1pt}
 122       \setlength{\topsep}{1pt}
 123       \setlength{\partopsep}{1pt}
 124       \setlength{\leftmargin}{1em}
 125       \setlength{\labelwidth}{0.5em}
 126       \setlength{\labelsep}{0.5em}
 127     }
 128 }
 129
 130 \newcommand{\squishend}{
 131   \end{list}
 132 }
 133
 134 \newcommand{\squishcount}{
 135 %  \begin{enumerate}
 136 %}
 137    \begin{list}{\bf \arabic{enumi}.}
 138     { \usecounter{enumi}
 139       \setlength{\itemsep}{1pt}      \setlength{\parsep}{0pt}
 140       \setlength{\topsep}{0pt}       \setlength{\partopsep}{0pt}
 141       \setlength{\leftmargin}{1em} \setlength{\labelwidth}{0.5em}
 142       \setlength{\labelsep}{0.5em} } }
 143
 144 \newcommand{\countend}{
 145 %  \end{enumerate}
 146 %}
 147 \end{list}}
 148
 149
 150 \newcommand{\code}[1]{\text{\tt #1}}
 151 \newcommand{\mypara}[1]{\noindent {#1}}
 152 \newcommand{\etal}{\textit{et al}.\xspace}
 153 \newcommand{\cdschecker}[0]{\textsc{CDSChecker}\xspace}
 154 \newcommand{\TOOL}[0]{\textsc{CDSSpec}\xspace}
 155
 156 \newcommand{\TODO}[0]{\textbf{TODO}\xspace}
 157 \newcommand{\todo}[1]{{\bf [[#1]]}}
 158 %\newcommand{\todo}[1]{}
 159 \newcommand{\comment}[1]{}
 160 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
 161 \newcommand{\rf}{\reltext{rf}}
 162 \newcommand{\relation}[1]{\xrightarrow{\textit{#1}}}
 163 \newcommand{\reltext}[1]{\textit{#1}}
 164
 165 %\newcommand{\mysection}[1]{\vspace{-.15cm}\section{#1}\vspace{-.15cm}}
 166 \newcommand{\mysection}[1]{\section{#1}}
 167 %\newcommand{\mysubsection}[1]{\vspace{-.15cm}\subsection{#1}\vspace{-.1cm}}
 168 \newcommand{\mysubsection}[1]{\subsection{#1}}
 169 %\newcommand{\mysubsubsection}[1]{\vspace{-.15cm}\subsubsection{#1}\vspace{-.1cm}}
 170 \newcommand{\mysubsubsection}[1]{\subsubsection{#1}}
 171 \begin{document}
 172
 173
 174 \sloppy
 175
 176 \title{CDSSpec: Testing Concurrent Data Structures Under the C/C++11 Memory Model}
 177
 178 \author{Peizhao Ou and Brian Demsky}
 179
 180
 181
 182 \maketitle
 183
 184 \begin{abstract}
 185 \input{abstract}
 186 \end{abstract}
 187
 188 \input{introduction}
 189 %\input{memorymodel}
 190 %\input{example}
 191 \input{formalization}
 192 %\input{specification}
 193 %\input{implementation}
 194 %\input{evaluation}
 195 %\input{related}
 196 %\input{conclusion}
 197
 198
 199 % We recommend abbrvnat bibliography style.
 200 \bibliographystyle{abbrv}
 201 \bibliography{confstrs-long,paper}
 202
 203 \end{document}