changes

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

diff --git a/correctness-model/writeup/paper.aux b/correctness-model/writeup/paper.aux
new file mode 100644 (file)
index 0000000..605a7ee
--- /dev/null
+++ b/correctness-model/writeup/paper.aux
@@ -0,0 +1,75 @@
+\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}
+\bibcite{linearizableref}{8}
+\bibcite{scmemorymodel}{9}
+\bibcite{javaConcurrentHashMap}{10}
+\@writefile{toc}{\contentsline {section}{\numberline {2}Formalization of Correctness Model}{\thepage }{section.2}}
+\newlabel{sec:formalization}{{2}{\thepage }{Formalization of Correctness Model}{section.2}{}}
+\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}{}}
+\@writefile{toc}{\contentsline {section}{\numberline {3}References}{\thepage }{section.3}}
+\bibcite{lockfreequeue}{11}
+\bibcite{cdschecker}{12}
+\bibcite{VechevMCLinear}{13}
+\bibcite{relacy}{14}