Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/spec-checker-compiler
[cdsspec-compiler.git] / 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
94 \newcommand{\pushcode}[1][1]{\hskip\dimexpr#1\algorithmicindent\relax}
95
96 %% Not used yet
97 % \usepackage{times}
98 % \usepackage{latexsym}
99 % \usepackage{amsfonts}
100 % \usepackage{amsthm}
101 % \usepackage{txfonts}
102 % \usepackage{url}
103 % \usepackage{subfigure}
104
105 % \usepackage{bbm}
106 % \usepackage{stfloats}
107
108 \newcommand{\squishlist}{
109   \begin{list}{$\bullet$}
110     { 
111       \setlength{\itemsep}{1pt}      
112       \setlength{\parsep}{1pt}
113       \setlength{\topsep}{1pt}       
114       \setlength{\partopsep}{1pt}
115       \setlength{\leftmargin}{1em} 
116       \setlength{\labelwidth}{0.5em}
117       \setlength{\labelsep}{0.5em} 
118     }
119 }
120
121 \newcommand{\squishend}{
122   \end{list}
123 }
124
125 \newcommand{\squishcount}{
126 %  \begin{enumerate}
127 %}
128    \begin{list}{\bf \arabic{enumi}.}
129     { \usecounter{enumi}
130       \setlength{\itemsep}{1pt}      \setlength{\parsep}{0pt}
131       \setlength{\topsep}{0pt}       \setlength{\partopsep}{0pt}
132       \setlength{\leftmargin}{1em} \setlength{\labelwidth}{0.5em}
133       \setlength{\labelsep}{0.5em} } }
134
135 \newcommand{\countend}{
136 %  \end{enumerate}
137 %}
138 \end{list}}
139
140
141 \newcommand{\code}[1]{\text{\tt #1}}
142 \newcommand{\mypara}[1]{\noindent {#1}}
143 \newcommand{\etal}{\textit{et al}.\xspace}
144 \newcommand{\cdschecker}[0]{\textsc{CDSChecker}\xspace}
145 \newcommand{\TOOL}[0]{\textsc{CDSSpec}\xspace}
146
147 \newcommand{\TODO}[0]{\textbf{TODO}\xspace}
148 \newcommand{\todo}[1]{{\bf [[#1]]}}
149 %\newcommand{\todo}[1]{}
150 \newcommand{\comment}[1]{}
151 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
152 \newcommand{\rf}{\reltext{rf}}
153 \newcommand{\relation}[1]{\xrightarrow{\textit{#1}}}
154 \newcommand{\reltext}[1]{\textit{#1}}
155
156 %\newcommand{\mysection}[1]{\vspace{-.15cm}\section{#1}\vspace{-.15cm}}
157 \newcommand{\mysection}[1]{\section{#1}}
158 %\newcommand{\mysubsection}[1]{\vspace{-.15cm}\subsection{#1}\vspace{-.1cm}}
159 \newcommand{\mysubsection}[1]{\subsection{#1}}
160 %\newcommand{\mysubsubsection}[1]{\vspace{-.15cm}\subsubsection{#1}\vspace{-.1cm}}
161 \newcommand{\mysubsubsection}[1]{\subsubsection{#1}}
162 \begin{document}
163
164
165 \sloppy
166
167 \title{CDSSpec: Testing Concurrent Data Structures Under the C/C++11 Memory Model}
168
169 \author{Peizhao Ou and Brian Demsky}
170
171
172
173 \maketitle
174
175 \begin{abstract}
176 \input{abstract}
177 \end{abstract}
178
179 \input{introduction}
180 %\input{memorymodel}
181 %\input{example}
182 \input{formalization}
183 %\input{specification}
184 %\input{implementation}
185 %\input{evaluation}
186 %\input{related}
187 %\input{conclusion}
188
189
190 % We recommend abbrvnat bibliography style.
191 \bibliographystyle{abbrv}
192 \bibliography{confstrs-long,paper}
193
194 \end{document}