\relax 
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldcontentsline\contentsline
\gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\contentsline\oldcontentsline
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax 
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\citation{rcu}
\citation{lockfreequeue}
\citation{javaConcurrentHashMap}
\citation{cpp11spec}
\citation{c11spec}
\citation{boehmpldi}
\citation{scmemorymodel}
\citation{cdschecker}
\citation{c11popl}
\citation{relacy}
\citation{linearizableref}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{\thepage }{section.1}}
\newlabel{sec:introduction}{{1}{\thepage }{Introduction}{section.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Background on Specifying the Correctness of Concurrent Data Structures}{\thepage }{subsection.1.1}}
\citation{lineup}
\citation{VechevMCLinear}
\citation{vyrd}
\citation{rcu}
\citation{lockfreequeue}
\citation{cdschecker}
\citation{relacy}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}New Challenges from the C/C++ Memory Model}{\thepage }{subsection.1.2}}
\newlabel{sec:introNewChallenges}{{1.2}{\thepage }{New Challenges from the C/C++ Memory Model}{subsection.1.2}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces  \textsc  {CDSSpec}\xspace  system overview}}{\thepage }{figure.1}}
\newlabel{fig:specworkflow}{{1}{\thepage }{\TOOL system overview}{figure.1}{}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Specification Language and Tool Support}{\thepage }{subsection.1.3}}
\@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Contributions}{\thepage }{subsection.1.4}}
\bibstyle{abbrv}
\bibdata{confstrs-long,paper}
\bibcite{cpp11spec}{1}
\bibcite{c11spec}{2}
\bibcite{c11popl}{3}
\bibcite{boehmpldi}{4}
\bibcite{lineup}{5}
\bibcite{rcu}{6}
\bibcite{vyrd}{7}
\@writefile{toc}{\contentsline {section}{\numberline {2}Formalization of Correctness Model}{\thepage }{section.2}}
\newlabel{sec:formalization}{{2}{\thepage }{Formalization of Correctness Model}{section.2}{}}
\@writefile{toc}{\contentsline {section}{\numberline {3}References}{\thepage }{section.3}}
\bibcite{linearizableref}{8}
\bibcite{scmemorymodel}{9}
\bibcite{javaConcurrentHashMap}{10}
\bibcite{lockfreequeue}{11}
\bibcite{cdschecker}{12}
\bibcite{VechevMCLinear}{13}
\bibcite{relacy}{14}
\newlabel{line:startWithRelaxed}{{4}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:setOfCandidates}{{7}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:findSCViolation}{{11}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:callStrengthenParam}{{13}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:weakenOrderParams}{{15}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:tmpOutputAsInput}{{18}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:finalResults}{{20}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:strengthenParam}{{24}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\newlabel{line:possibleFixes}{{25}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Algorithm for inferring order parameters}}{\thepage }{figure.2}}
\newlabel{fig:algorithmfence}{{2}{\thepage }{Algorithm for inferring order parameters}{figure.2}{}}