ready-without-appndix.tex

\documentclass[a4paper,UKenglish]{lipics-v2016}

%\newtheorem{theorem}{Theorem}[section]
%\newtheorem{conjecture}[theorem]{Conjecture}
%\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{proposition}[theorem]{Proposition}
%\newtheorem{lemma}[theorem]{Lemma}
%\newdef{definition}[theorem]{Definition}
%\newdef{remark}[theorem]{Remark}
%\newdef{example}[theorem]{Example}



\usepackage{epsfig}
\usepackage{amsmath}
\usepackage{color}
\usepackage{amsfonts,amssymb}
%\usepackage{txfonts}
%\usepackage{pxfonts}
%\usepackage{mathabx}
%\usepackage{makeidx}  % allows for indexgeneration
\usepackage{verbatim}
%\usepackage{url}
%\usepackage{hyperref}
\usepackage{times}
\usepackage{ulem}    %(\emph{....} in the texfile) is underlined instead of italic
\normalem
\usepackage{enumerate}
%\usepackage[square, comma, sort&compress, numbers]{natbib}

%added by Yi Lv%
%\usepackage[linesnumbered,ruled,procnumbered,noend]{algorithm2e}
%\usepackage[linesnumbered,ruled,procnumbered,vlined]{algorithm2e}
\usepackage[linesnumbered,ruled,procnumbered,noend]{algorithm2e}
\usepackage{stmaryrd}
%\usepackage{hyperref}
%added by Wang Chao%
%\usepackage{mathrsfs}
%\usepackage{extarrows}
\usepackage{thmtools}
\usepackage{thm-restate}

%add for TIkz
\usepackage[version=0.96]{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,shapes,snakes,automata,backgrounds,petri}
%\usepackage[latin1]{inputenc}
%\usepackage{placeins}
%\usepackage[bookmarks=false]{hyperref}

%\declaretheorem[name=Claim]{clm}
%\declaretheorem[name=Lemma]{lem}
%\declaretheorem[name=Theorem]{thm}


\DeclareSymbolFont{largesymbolsA}{U}{txexa}{m}{n}
\SetSymbolFont{largesymbolsA}{bold}{U}{txexa}{bx}{n}
\DeclareFontSubstitution{U}{txexa}{m}{n}
\DeclareMathSymbol{\bigsqcupplus}{\mathop}{largesymbolsA}{"02}

% "Import" \bigsqcupplus from txfonts without loading txfonts (since
% it changes the default font and replaces many symbols)

% Commands by Catuscia

%\DeclareMathOperator*{\minarg}{{\rm minarg}}

%Previous notation for the probabilistic choice
%\newcommand{\probsum}{\bigoplus}
%\newcommand{\smallprobsum}[1]{\mkern4mu{\textstyle\circ\mkern-15.5mu\sum_{#1}\:}}
%\newcommand{\bigprobsum}[1]{{\;\displaystyle\odot\mkern-21mu\sum_{#1}}}
%\newcommand{\probsum}[1]{\mathchoice{\bigprobsum{#1}}{\smallprobsum{#1}}{\smallprobsum{#1}}{\smallprobsum{#1}}}
%For the uniform distribution
%\newcommand{\usmallprobsum}[1]{\mkern4mu{\textstyle\circ\mkern-15.5mu\sum^\mathcal{U}_{#1}\:}}
%\newcommand{\ubigprobsum}[1]{{\;\displaystyle\odot\mkern-21mu\sum^\mathcal{U}_{#1}}}
%\newcommand{\uprobsum}[1]{\mathchoice{\ubigprobsum{#1}}{\usmallprobsum{#1}}{\usmallprobsum{#1}}{\usmallprobsum{#1}}}

%\newcommand{\nondsum}{\bigbox}
\newcommand{\nondsum}{\bigsqcupplus}
\newcommand{\probplus}[1]{\oplus_{#1}}
%\newcommand{\nondplus}{\square}
\newcommand{\bang}{!\,}
\newcommand{\nondplus}{{\textstyle\bigsqcupplus}}
\newcommand{\partmap}{\rightharpoonup}
\newcommand{\map}{\rightarrow}
%\newcommand{\exc}{\phi}
\newcommand{\exc}{\alpha}
\newcommand{\exec}{\mathit{exec}}
\newcommand{\execp}{\mathit{execp}}
\newcommand{\Act}{\mathit{Act}}
\newcommand{\Sec}{\mathit{Sec}}
\newcommand{\Obs}{\mathit{Obs}}
\newcommand{\etree}{\mathit{etree}}
\newcommand{\lstate}{\mathit{lst}}
\newcommand{\fstate}{\mathit{fst}}
%\newcommand{\STATE}{\mathcal{P}r}  $ original marked
%\newcommand{\STATE}{\mathcal{P}}   $ marked by me
%\newcommand{\st}{P}
\newcommand{\trans}{\mathcal{T}}
\newcommand{\Aut}{\mathcal{M}}
\newcommand{\init}{\mathit{init}}
\newcommand{\perr}{\mathcal{P}}

\newcommand{\calo}{\mathcal{O}}
\newcommand{\cals}{\mathcal{S}}
\newcommand{\sseq}{\vec s}
\newcommand{\oseq}{\vec o}
\newcommand{\ccsp}{CCS$_p$}

\newcommand{\bigfrac}[2]{\frac{\raisebox{1ex}{$#1$}}{\raisebox{-1.5ex}{$#2$}}}
\newcommand{\nondarr}[1]{\overset{#1}{\longrightarrow}}
\newcommand{\Nondarr}[1]{\overset{#1}{\Longrightarrow}}
\newcommand{\vectorArrow}[1]{\stackrel{\longrightarrow}{\mbox{#1}}}
\newcommand{\probarr}[1]{\overset{#1}{\dashrightarrow}}
\newcommand{\paral}{\,|\,}
\newcommand{\outp}[1]{\overline{#1}}
\renewcommand{\Pr}{{\rm Pr}}

%Commands by Chao Wang

%memory models%
\newcommand{\TSO}{\textrm{TSO}}
\newcommand{\PSO}{\textrm{PSO}}

%correctness conditions%
\newcommand{\lin}{\textrm{linearizability}}
\newcommand{\slin}{\textrm{static linearizability}}
\newcommand{\qlin}{\textrm{quasi linearizability}}
\newcommand{\TTlin}{\textrm{TSO-to-TSO linearizability}}

\newcommand{\pair}[2]{\langle #1 , #2 \rangle}% pairs
\newcommand{\setof}[2]{\{ \, #1 \mid #2 \, \}}% Sets
\newcommand{\set}[1]{\{ {#1}  \}  }
%\newcommand{\map}[3]{{#1} \colon {#2} \longmapsto {#3}} %functions
\newcommand{\den}[1]{[\![#1]\!]}% Denotation of
\newcommand{\mean}[1]{|\!|#1|\!|}
\newcommand{\forget}[1]{}

%%%%%%%%%%%%%GENERAL%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\itbox}[1]{{\it #1\/}}
\newcommand{\un}[1]{\uline{#1}}%\underline{#1}}
\newcommand{\ov}[1]{\overline{#1}}
\newcommand{\smallspace}{\vspace{10mm}}
\newcommand{\is}{\mbox{$\Longleftarrow\ $}}
\newcommand{\pright}[1]{\hfill{#1}}
\newcommand{\bnfor}{\;\;\mid\;\;}

\newcommand{\ar}[1]{\stackrel{\scriptstyle #1}{\longrightarrow}}

%%%%%%%%%italics in math mode
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\newcommand{\true}{{\it true}}
%\newcommand{\false}{{\it false}}
\newcommand{\calB}{{\cal B}}
\newcommand{\calF}{{\cal F}}
\newcommand{\calP}{{\cal P}}
\newcommand{\order}{{\cal O}}
\newcommand{\size}[1]{|#1|}

%other notations%
\newcommand{\LTS}{\textit{LTS}}
\newcommand{\bedt}[1]{{\color{blue}#1}}
\newcommand{\redt}[1]{{\color{red}#1}}

%\pagestyle{empty}
%\pagestyle{plain}


%\def\lastname{Xu,Palamidessi}

\title{Checking Linearizability of Concurrent Priority Queues}




\author[1]{Ahmed Bouajjani}
%\author[2]{Michael Emmi}
\author[1]{Constantin Enea}
\author[1]{Chao Wang}
\affil[1]{Institut de Recherche en Informatique Fondamentale, \\ \texttt{\{abou,cenea,wangch\}@irif.fr}}
%\affil[2]{Nokia Bell Labs, \\ \texttt{michael.emmi@nokia.com}}



\begin{document}

\maketitle

\input{abstract}

\input{introduction}

\input{priority-queues}

\input{checking-executions}

%\input{recur-process-concurrent}


%\input{preliminaries-EPQ}

%\input{rules-EPQ}

%\input{data-independence-EPQ}

%\input{ss-lin-EPQ}


\input{co-regular-EPQ}

\input{related}

%\input{relate-PQ-with-Queue-Stack-MultiSet-EPQ}




%\FloatBarrier
  \bibliography{violin}
\bibliographystyle{plainurl}
%\bibliography{biblio_cat.bib}


%\begin{thebibliography}{50}
%
%\bibitem{Bouajjani:2015}
%Bouajjani, A., Emmi, M., Enea, C., Hamza, J.:
%\newblock On reducing linearizability to state reachability.
%\newblock In: Halld{\'{o}}rsson, M.M. et al. (eds.) ICALP 2015, Part II, pp. 95--107. Springer (2015)
%
%\bibitem{Bouajjani:2015POPL}
%Bouajjani, A., Emmi, M., Enea, C., Hamza, J.:
%\newblock Tractable Refinement Checking for Concurrent Objects.
%\newblock In: {\em POPL'15}. pp.651--662. (2015)
%
%\bibitem{Wolper:1986}
%Wolper, P.:
%\newblock Expressing interesting properties of programs in propositional
%  temporal logic.
%\newblock In {\em POPL'86}. pp.184--193. (1986)
%
%\bibitem{Henzinger:2013}
%Henzinger A. T., Sezgin A., Vafeiadis, V.:
%\newblock Aspect-Oriented Linearizability Proofs.
%\newblock In {\em CONCUR'13}. pp.242--256. (2013)
%
%
%\bibitem{Herlihy:1990}
%Herlihy, M., Wing, M, J. A.:
%\newblock Linearizability: {A} Correctness Condition for Concurrent Objects.
%\newblock In {\em {ACM} Trans. Program. Lang. Syst.}. pp.463--492. (1990)
%
%
%\bibitem{Abdulla:2013}
%Abdulla, P. A., Haziza, F., Holšªk, L., Jonsson, B., Rezine, A.:
%\newblock An integrated specification and verification technique for highly concurrent data
%structures.
%\newblock In {\em TACAS'13}. pp.324--338. (2013)
%
%
%
%\end{thebibliography}
\newpage

\appendix

%\input{appendix-EPQ}






\end{document}