changes

[cdsspec-compiler.git] / correctness-model / writeup / paper.tex

diff --git a/correctness-model/writeup/paper.tex b/correctness-model/writeup/paper.tex
new file mode 100644 (file)
index 0000000..d65f512
--- /dev/null
+++ b/correctness-model/writeup/paper.tex
@@ -0,0 +1,182 @@
+%-----------------------------------------------------------------------------
+%
+%               Template for sigplanconf LaTeX Class
+%
+% Name:         sigplanconf-template.tex
+%
+% Purpose:      A template for sigplanconf.cls, which is a LaTeX 2e class
+%               file for SIGPLAN conference proceedings.
+%
+% Guide:        Refer to "Author's Guide to the ACM SIGPLAN Class,"
+%               sigplanconf-guide.pdf
+%
+% Author:       Paul C. Anagnostopoulos
+%               Windfall Software
+%               978 371-2316
+%               paul@windfall.com
+%
+% Created:      15 February 2005
+%
+%-----------------------------------------------------------------------------
+
+
+\documentclass[nocopyrightspace]{sig-alternate}
+
+% The following \documentclass options may be useful:
+%
+% 10pt          To set in 10-point type instead of 9-point.
+% 11pt          To set in 11-point type instead of 9-point.
+% authoryear    To obtain author/year citation style instead of numeric.
+\usepackage{times}
+\usepackage[scaled]{helvet} % see www.ctan.org/get/macros/latex/required/psnfss/psnfss2e.pdf
+\usepackage{url}                  % format URLs
+\usepackage{listings}          % format code
+\usepackage{enumitem}      % adjust spacing in enums
+\sloppy
+\usepackage[colorlinks=true,allcolors=blue,breaklinks,draft]{hyperref}
+\newcommand{\doi}[1]{doi:~\href{http://dx.doi.org/#1}{\Hurl{#1}}}   % print a hyperlinked DOI
+
+\usepackage{rotating}
+\usepackage{algorithm}% http://ctan.org/pkg/algorithms
+\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
+%\usepackage{syntax}
+%\usepackage{times}
+
+\usepackage{amsmath}
+\usepackage{graphicx}
+\usepackage{xspace}
+\usepackage{amssymb}
+
+\usepackage{listings}
+\usepackage{color}
+\usepackage{textcomp}
+\definecolor{listinggray}{gray}{0.9}
+\definecolor{lbcolor}{rgb}{0.9,0.9,0.9}
+\lstset{
+       % backgroundcolor=\color{lbcolor},
+       % rulecolor=,
+       % aboveskip={1.5\baselineskip},
+       % extendedchars=true,
+       tabsize=3,
+       language=C++,
+       basicstyle=\ttfamily\scriptsize,
+       upquote=true,
+       columns=fixed,
+       showstringspaces=false,
+       breaklines=true,
+       prebreak = \raisebox{0ex}[0ex][0ex]{\ensuremath{\hookleftarrow}},
+       % frame=single,
+       showtabs=false,
+       showspaces=false,
+       showstringspaces=false,
+       identifierstyle=\ttfamily,
+       keywordstyle=\color[rgb]{0,0,1},
+       commentstyle=\color[rgb]{0.133,0.545,0.133},
+       stringstyle=\color[rgb]{0.627,0.126,0.941},
+       numbers=left,
+       numberstyle=\tiny,
+       numbersep=8pt,
+       escapeinside={/*@}{@*/}
+}
+
+\usepackage{algpseudocode}
+
+%% Not used yet
+% \usepackage{times}
+% \usepackage{latexsym}
+% \usepackage{amsfonts}
+% \usepackage{amsthm}
+% \usepackage{txfonts}
+% \usepackage{url}
+% \usepackage{subfigure}
+
+% \usepackage{bbm}
+% \usepackage{stfloats}
+
+\newcommand{\squishlist}{
+  \begin{list}{$\bullet$}
+    { 
+      \setlength{\itemsep}{1pt}      
+      \setlength{\parsep}{1pt}
+      \setlength{\topsep}{1pt}       
+      \setlength{\partopsep}{1pt}
+      \setlength{\leftmargin}{1em} 
+      \setlength{\labelwidth}{0.5em}
+      \setlength{\labelsep}{0.5em} 
+    }
+}
+
+\newcommand{\squishend}{
+  \end{list}
+}
+
+\newcommand{\squishcount}{
+%  \begin{enumerate}
+%}
+   \begin{list}{\bf \arabic{enumi}.}
+    { \usecounter{enumi}
+      \setlength{\itemsep}{1pt}      \setlength{\parsep}{0pt}
+      \setlength{\topsep}{0pt}       \setlength{\partopsep}{0pt}
+      \setlength{\leftmargin}{1em} \setlength{\labelwidth}{0.5em}
+      \setlength{\labelsep}{0.5em} } }
+
+\newcommand{\countend}{
+%  \end{enumerate}
+%}
+\end{list}}
+
+
+\newcommand{\code}[1]{\text{\tt #1}}
+\newcommand{\mypara}[1]{\noindent {#1}}
+\newcommand{\etal}{\textit{et al}.\xspace}
+\newcommand{\cdschecker}[0]{\textsc{CDSChecker}\xspace}
+\newcommand{\TOOL}[0]{\textsc{CDSSpec}\xspace}
+
+\newcommand{\TODO}[0]{\textbf{TODO}\xspace}
+\newcommand{\todo}[1]{{\bf [[#1]]}}
+%\newcommand{\todo}[1]{}
+\newcommand{\comment}[1]{}
+\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
+\newcommand{\rf}{\reltext{rf}}
+\newcommand{\relation}[1]{\xrightarrow{\textit{#1}}}
+\newcommand{\reltext}[1]{\textit{#1}}
+
+%\newcommand{\mysection}[1]{\vspace{-.15cm}\section{#1}\vspace{-.15cm}}
+\newcommand{\mysection}[1]{\section{#1}}
+%\newcommand{\mysubsection}[1]{\vspace{-.15cm}\subsection{#1}\vspace{-.1cm}}
+\newcommand{\mysubsection}[1]{\subsection{#1}}
+%\newcommand{\mysubsubsection}[1]{\vspace{-.15cm}\subsubsection{#1}\vspace{-.1cm}}
+\newcommand{\mysubsubsection}[1]{\subsubsection{#1}}
+\begin{document}
+
+
+\sloppy
+
+\title{CDSSpec: Testing Concurrent Data Structures Under the C/C++11 Memory Model}
+
+\author{Peizhao Ou and Brian Demsky}
+
+
+
+\maketitle
+
+\begin{abstract}
+\input{abstract}
+\end{abstract}
+
+\input{introduction}
+%\input{memorymodel}
+%\input{example}
+\input{formalization}
+%\input{specification}
+%\input{implementation}
+%\input{evaluation}
+%\input{related}
+%\input{conclusion}
+
+
+% We recommend abbrvnat bibliography style.
+\bibliographystyle{abbrv}
+\bibliography{confstrs-long,paper}
+
+\end{document}