2 \providecommand\hyper@newdestlabel[2]{}
3 \providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
4 \HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
5 \global\let\oldcontentsline\contentsline
6 \gdef\contentsline#1#2#3#4{\oldcontentsline{#1}{#2}{#3}}
7 \global\let\oldnewlabel\newlabel
8 \gdef\newlabel#1#2{\newlabelxx{#1}#2}
9 \gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
10 \AtEndDocument{\ifx\hyper@anchor\@undefined
11 \let\contentsline\oldcontentsline
12 \let\newlabel\oldnewlabel
15 \global\let\hyper@last\relax
16 \gdef\HyperFirstAtBeginDocument#1{#1}
17 \providecommand\HyField@AuxAddToFields[1]{}
18 \providecommand\HyField@AuxAddToCoFields[2]{}
20 \citation{lockfreequeue}
21 \citation{javaConcurrentHashMap}
25 \citation{scmemorymodel}
29 \citation{linearizableref}
30 \@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{\thepage }{section.1}}
31 \newlabel{sec:introduction}{{1}{\thepage }{Introduction}{section.1}{}}
32 \@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Background on Specifying the Correctness of Concurrent Data Structures}{\thepage }{subsection.1.1}}
34 \citation{VechevMCLinear}
37 \citation{lockfreequeue}
40 \@writefile{toc}{\contentsline {subsection}{\numberline {1.2}New Challenges from the C/C++ Memory Model}{\thepage }{subsection.1.2}}
41 \newlabel{sec:introNewChallenges}{{1.2}{\thepage }{New Challenges from the C/C++ Memory Model}{subsection.1.2}{}}
42 \@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces \textsc {CDSSpec}\xspace system overview}}{\thepage }{figure.1}}
43 \newlabel{fig:specworkflow}{{1}{\thepage }{\TOOL system overview}{figure.1}{}}
44 \@writefile{toc}{\contentsline {subsection}{\numberline {1.3}Specification Language and Tool Support}{\thepage }{subsection.1.3}}
45 \@writefile{toc}{\contentsline {subsection}{\numberline {1.4}Contributions}{\thepage }{subsection.1.4}}
47 \bibdata{confstrs-long,paper}
48 \bibcite{cpp11spec}{1}
49 \@writefile{toc}{\contentsline {section}{\numberline {2}Formalization of Correctness Model}{\thepage }{section.2}}
50 \newlabel{sec:formalization}{{2}{\thepage }{Formalization of Correctness Model}{section.2}{}}
51 \@writefile{toc}{\contentsline {section}{\numberline {3}References}{\thepage }{section.3}}
54 \bibcite{boehmpldi}{4}
58 \bibcite{linearizableref}{8}
59 \bibcite{scmemorymodel}{9}
60 \bibcite{javaConcurrentHashMap}{10}
61 \bibcite{lockfreequeue}{11}
62 \bibcite{cdschecker}{12}
63 \bibcite{VechevMCLinear}{13}
65 \newlabel{line:startWithRelaxed}{{4}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
66 \newlabel{line:setOfCandidates}{{7}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
67 \newlabel{line:findSCViolation}{{11}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
68 \newlabel{line:callStrengthenParam}{{13}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
69 \newlabel{line:weakenOrderParams}{{15}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
70 \newlabel{line:tmpOutputAsInput}{{18}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
71 \newlabel{line:finalResults}{{20}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
72 \newlabel{line:strengthenParam}{{24}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
73 \newlabel{line:possibleFixes}{{25}{\thepage }{Formalization of Correctness Model}{Item.9}{}}
74 \@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces Algorithm for inferring order parameters}}{\thepage }{figure.2}}
75 \newlabel{fig:algorithmfence}{{2}{\thepage }{Algorithm for inferring order parameters}{figure.2}{}}