From: Peizhao Ou Date: Sun, 12 Apr 2015 00:39:29 +0000 (-0700) Subject: changes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=7f557a3891c3ec8f7a8ffc5461299d50428be247;hp=-c changes --- 7f557a3891c3ec8f7a8ffc5461299d50428be247 diff --git a/correctness-model/note.txt b/correctness-model/note.txt index e69de29..2e7daa7 100644 --- a/correctness-model/note.txt +++ b/correctness-model/note.txt @@ -0,0 +1,3 @@ +2-phase: read (plan) write + +redesign of data structures for HTM diff --git a/correctness-model/writeup/paper.aux b/correctness-model/writeup/paper.aux deleted file mode 100644 index d3d63d5..0000000 --- a/correctness-model/writeup/paper.aux +++ /dev/null @@ -1,75 +0,0 @@ -\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} -\@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{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} -\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}{}} diff --git a/correctness-model/writeup/paper.bbl b/correctness-model/writeup/paper.bbl deleted file mode 100644 index e7f99db..0000000 --- a/correctness-model/writeup/paper.bbl +++ /dev/null @@ -1,84 +0,0 @@ -\begin{thebibliography}{10} - -\bibitem{cpp11spec} -{ISO/IEC 14882:2011}, {Information} technology -- programming languages -- - {C++}. - -\bibitem{c11spec} -{ISO/IEC 9899:2011}, {Information} technology -- programming languages -- {C}. - -\bibitem{c11popl} -M.~Batty, S.~Owens, S.~Sarkar, P.~Sewell, and T.~Weber. -\newblock Mathematizing {C++} concurrency. -\newblock In {\em Proceedings of the Symposium on Principles of Programming - Languages}, 2011. - -\bibitem{boehmpldi} -H.~J. Boehm and S.~V. Adve. -\newblock Foundations of the {C++} concurrency memory model. -\newblock In {\em Proceedings of the 2008 ACM SIGPLAN Conference on Programming - Language Design and Implementation}, 2008. - -\bibitem{lineup} -S.~Burckhardt, C.~Dern, M.~Musuvathi, and R.~Tan. -\newblock Line-up: A complete and automatic linearizability checker. -\newblock In {\em Proceedings of the 2010 ACM SIGPLAN Conference on Programming - Language Design and Implementation}, 2010. - -\bibitem{rcu} -M.~Desnoyers, P.~E. McKenney, A.~S. Stern, M.~R. Dagenais, and J.~Walpole. -\newblock User-level implementations of read-copy update. -\newblock {\em IEEE Transactions on Parallel and Distributed Systems}, 2011. - -\bibitem{vyrd} -T.~Elmas, S.~Tasiran, and S.~Qadeer. -\newblock {VYRD}: Verifying concurrent programs by runtime refinement-violation - detection. -\newblock In {\em Proceedings of the 2005 ACM SIGPLAN Conference on Programming - Language Design and Implementation}, 2005. - -\bibitem{linearizableref} -M.~Herlihy and J.~Wing. -\newblock Linearizability: a correctness condition for concurrent objects. -\newblock {\em ACM Transactions on Programming Languages and Systems}, - 12(3):463--492, July 1990. - -\bibitem{scmemorymodel} -L.~Lamport. -\newblock How to make a multiprocessor computer that correctly executes - multiprocess programs. -\newblock {\em IEEE Transactions on Computers}, 28(9):690--691, Sept. 1979. - -\bibitem{javaConcurrentHashMap} -D.~Lea. -\newblock util.concurrent.{ConcurrentHashMap} in java.util.concurrent the {Java - Concurrency Package}. -\newblock - \url{http://docs.oracle.com/javase/8/docs/api/java/util/concurrent/ConcurrentHashMap.html}. - -\bibitem{lockfreequeue} -M.~M. Michael and M.~L. Scott. -\newblock Simple, fast, and practical non-blocking and blocking concurrent - queue algorithms. -\newblock In {\em Proceedings of the Fifteenth Annual ACM Symposium on - Principles of Distributed Computing}, 1996. - -\bibitem{cdschecker} -B.~Norris and B.~Demsky. -\newblock {CDSChecker}: Checking concurrent data structures written with - {C/C++} atomics. -\newblock In {\em Proceeding of the 28th ACM SIGPLAN Conference on - Object-Oriented Programming, Systems, Languages, and Applications}, 2013. - -\bibitem{VechevMCLinear} -M.~Vechev, E.~Yahav, and G.~Yorsh. -\newblock Experience with model checking linearizability. -\newblock In {\em International SPIN Workshop on Model Checking Software}, - 2009. - -\bibitem{relacy} -D.~Vyukov. -\newblock Relacy race detector. -\newblock \url{http://relacy.sourceforge.net/}, 2011 Oct. - -\end{thebibliography} diff --git a/correctness-model/writeup/paper.blg b/correctness-model/writeup/paper.blg deleted file mode 100644 index 6a4c408..0000000 --- a/correctness-model/writeup/paper.blg +++ /dev/null @@ -1,50 +0,0 @@ -This is BibTeX, Version 0.99d (TeX Live 2013/Debian) -Capacity: max_strings=35307, hash_size=35307, hash_prime=30011 -The top-level auxiliary file: paper.aux -The style file: abbrv.bst -Database file #1: confstrs-long.bib -Database file #2: paper.bib -Warning--to sort, need author or key in cpp11spec -Warning--to sort, need author or key in c11spec -You've used 14 entries, - 2118 wiz_defined-function locations, - 816 strings with 16605 characters, -and the built_in function-call counts, 3810 in all, are: -= -- 331 -> -- 190 -< -- 0 -+ -- 76 -- -- 62 -* -- 224 -:= -- 631 -add.period$ -- 38 -call.type$ -- 14 -change.case$ -- 73 -chr.to.int$ -- 0 -cite$ -- 16 -duplicate$ -- 158 -empty$ -- 358 -format.name$ -- 62 -if$ -- 806 -int.to.chr$ -- 0 -int.to.str$ -- 14 -missing$ -- 10 -newline$ -- 69 -num.names$ -- 24 -pop$ -- 115 -preamble$ -- 1 -purify$ -- 59 -quote$ -- 0 -skip$ -- 108 -stack$ -- 0 -substring$ -- 116 -swap$ -- 21 -text.length$ -- 0 -text.prefix$ -- 0 -top$ -- 0 -type$ -- 56 -warning$ -- 2 -while$ -- 27 -width$ -- 16 -write$ -- 133 -(There were 2 warnings) diff --git a/correctness-model/writeup/paper.log b/correctness-model/writeup/paper.log deleted file mode 100644 index b7ef3f1..0000000 --- a/correctness-model/writeup/paper.log +++ /dev/null @@ -1,659 +0,0 @@ -This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013/Debian) (format=pdflatex 2014.3.31) 10 APR 2015 18:30 -entering extended mode - restricted \write18 enabled. - %&-line parsing enabled. -**paper.tex -(./paper.tex -LaTeX2e <2011/06/27> -Babel <3.9h> and hyphenation patterns for 78 languages loaded. -(./sig-alternate.cls -(/usr/share/texlive/texmf-dist/tex/latex/graphics/epsfig.sty -Package: epsfig 1999/02/16 v1.7a (e)psfig emulation (SPQR) - -(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty -Package: graphicx 1999/02/16 v1.0f Enhanced LaTeX Graphics (DPC,SPQR) - -(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty -Package: keyval 1999/03/16 v1.13 key=value parser (DPC) -\KV@toks@=\toks14 -) -(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty -Package: graphics 2009/02/05 v1.0o Standard LaTeX Graphics (DPC,SPQR) - -(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty -Package: trig 1999/03/16 v1.09 sin cos tan (DPC) -) -(/etc/texmf/tex/latex/config/graphics.cfg -File: graphics.cfg 2009/08/28 v1.8 graphics configuration of TeX Live -) -Package graphics Info: Driver file: pdftex.def on input line 91. - -(/usr/share/texlive/texmf-dist/tex/latex/pdftex-def/pdftex.def -File: pdftex.def 2011/05/27 v0.06d Graphics/color for pdfTeX - -(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/infwarerr.sty -Package: infwarerr 2010/04/08 v1.3 Providing info/warning/error messages (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/ltxcmds.sty -Package: ltxcmds 2011/11/09 v1.22 LaTeX kernel commands for general use (HO) -) -\Gread@gobject=\count79 -)) -\Gin@req@height=\dimen102 -\Gin@req@width=\dimen103 -) -\epsfxsize=\dimen104 -\epsfysize=\dimen105 -) -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty -Package: amssymb 2013/01/14 v3.01 AMS font symbols - -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty -Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support -\@emptytoks=\toks15 -\symAMSa=\mathgroup4 -\symAMSb=\mathgroup5 -LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' -(Font) U/euf/m/n --> U/euf/b/n on input line 106. -)) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty -Package: amsmath 2013/01/14 v2.14 AMS math features -\@mathmargin=\skip41 - -For additional information on amsmath, use the `?' option. -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty -Package: amstext 2000/06/29 v2.01 - -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty -File: amsgen.sty 1999/11/30 v2.0 -\@emptytoks=\toks16 -\ex@=\dimen106 -)) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty -Package: amsbsy 1999/11/29 v1.2d -\pmbraise@=\dimen107 -) -(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty -Package: amsopn 1999/12/14 v2.01 operator names -) -\inf@bad=\count80 -LaTeX Info: Redefining \frac on input line 210. -\uproot@=\count81 -\leftroot@=\count82 -LaTeX Info: Redefining \overline on input line 306. -\classnum@=\count83 -\DOTSCASE@=\count84 -LaTeX Info: Redefining \ldots on input line 378. -LaTeX Info: Redefining \dots on input line 381. -LaTeX Info: Redefining \cdots on input line 466. -\Mathstrutbox@=\box26 -\strutbox@=\box27 -\big@size=\dimen108 -LaTeX Font Info: Redeclaring font encoding OML on input line 566. -LaTeX Font Info: Redeclaring font encoding OMS on input line 567. -\macc@depth=\count85 -\c@MaxMatrixCols=\count86 -\dotsspace@=\muskip10 -\c@parentequation=\count87 -\dspbrk@lvl=\count88 -\tag@help=\toks17 -\row@=\count89 -\column@=\count90 -\maxfields@=\count91 -\andhelp@=\toks18 -\eqnshift@=\dimen109 -\alignsep@=\dimen110 -\tagshift@=\dimen111 -\tagwidth@=\dimen112 -\totwidth@=\dimen113 -\lineht@=\dimen114 -\@envbody=\toks19 -\multlinegap=\skip42 -\multlinetaggap=\skip43 -\mathdisplay@stack=\toks20 -LaTeX Info: Redefining \[ on input line 2665. -LaTeX Info: Redefining \] on input line 2666. -) -Document Class 'sig-alternate' <23rd. May '12>. Modified by G.K.M. Tobin/Gerry -Murray -Based in part upon document Style `acmconf' <22 May 89>. Hacked 4/91 by -shivers@cs.cmu.edu, 4/93 by theobald@cs.mcgill.ca -Excerpts were taken from (Journal Style) 'esub2acm.cls'. -****** Bugs/comments/suggestions/technicalities to Gerry Murray -- murray@hq.ac -m.org ****** -Questions on the style, SIGS policies, etc. to Adrienne Griscti griscti@acm.org - -\footheight=\dimen115 -\@maxsep=\dimen116 -\@dblmaxsep=\dimen117 -\aucount=\count92 -\originalaucount=\count93 -\auwidth=\dimen118 -\auskip=\dimen119 -\auskipcount=\count94 -\auskip=\dimen120 -\allauboxes=\dimen121 -\addauthors=\toks21 -\addauflag=\count95 -\subtitletext=\toks22 -\savesection=\count96 -\sectioncntr=\count97 -\c@figure=\count98 -\c@table=\count99 -\titleboxnotes=\toks23 -\titleboxnoteflag=\count100 -Document Class: sig-alternate 2012/05/23 - V2.5 - based on acmproc.cls V1.3 -(/usr/share/texlive/texmf-dist/tex/latex/base/latexsym.sty -Package: latexsym 1998/08/17 v2.2e Standard LaTeX package (lasy symbols) -\symlasy=\mathgroup6 -LaTeX Font Info: Overwriting symbol font `lasy' in version `bold' -(Font) U/lasy/m/n --> U/lasy/b/n on input line 47. -) -\@acmtitlebox=\box28 -\titlenotecount=\count101 -\tntoks=\toks24 -\tntokstwo=\toks25 -\tntoksthree=\toks26 -\tntoksfour=\toks27 -\tntoksfive=\toks28 -\catcount=\count102 -\copyrightnotice=\toks29 -\conf=\toks30 -\confinfo=\toks31 -\c@part=\count103 -\c@section=\count104 -\c@subsection=\count105 -\c@subsubsection=\count106 -\c@paragraph=\count107 - -Using 'Abbrev' bibliography style -LaTeX Info: Redefining \cite on input line 1211. -\bibindent=\dimen122 -\colcntr=\count108 -\saveb@x=\box29 -\copyrtyr=\toks32 -\acmcopyr=\toks33 -\boilerplate=\toks34 -\copyrightetc=\toks35 -(/usr/share/texlive/texmf-dist/tex/latex/base/fontenc.sty -Package: fontenc 2005/09/27 v1.99g Standard LaTeX package - -(/usr/share/texlive/texmf-dist/tex/latex/base/t1enc.def -File: t1enc.def 2005/09/27 v1.99g Standard LaTeX file -LaTeX Font Info: Redeclaring font encoding T1 on input line 43. -) -LaTeX Font Info: Try loading font information for T1+aer on input line 100. - -(/usr/share/texlive/texmf-dist/tex/latex/ae/t1aer.fd -File: t1aer.fd 1997/11/16 Font definitions for T1/aer. -))) -(/usr/share/texlive/texmf-dist/tex/latex/psnfss/times.sty -Package: times 2005/04/12 PSNFSS-v9.2a (SPQR) -) -(/usr/share/texlive/texmf-dist/tex/latex/psnfss/helvet.sty -Package: helvet 2005/04/12 PSNFSS-v9.2a (WaS) -) -(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty -\Urlmuskip=\muskip11 -Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc. -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/listings.sty -\lst@mode=\count109 -\lst@gtempboxa=\box30 -\lst@token=\toks36 -\lst@length=\count110 -\lst@currlwidth=\dimen123 -\lst@column=\count111 -\lst@pos=\count112 -\lst@lostspace=\dimen124 -\lst@width=\dimen125 -\lst@newlines=\count113 -\lst@lineno=\count114 -\abovecaptionskip=\skip44 -\belowcaptionskip=\skip45 -\lst@maxwidth=\dimen126 - -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2013/08/26 1.5b (Carsten Heinz) -\c@lstnumber=\count115 -\lst@skipnumbers=\count116 -\lst@framebox=\box31 -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/listings.cfg -File: listings.cfg 2013/08/26 1.5b listings configuration -)) -Package: listings 2013/08/26 1.5b (Carsten Heinz) - -(/usr/share/texlive/texmf-dist/tex/latex/enumitem/enumitem.sty -Package: enumitem 2011/09/28 v3.5.2 Customized lists -\labelindent=\skip46 -\enit@outerparindent=\dimen127 -\enit@toks=\toks37 -\enit@inbox=\box32 -\enitdp@description=\count117 -) -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty -Package: hyperref 2012/11/06 v6.83m Hypertext links for LaTeX - -(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-hyperref.sty -Package: hobsub-hyperref 2012/05/28 v1.13 Bundle oberdiek, subset hyperref (HO) - - -(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/hobsub-generic.sty -Package: hobsub-generic 2012/05/28 v1.13 Bundle oberdiek, subset generic (HO) -Package: hobsub 2012/05/28 v1.13 Construct package bundles (HO) -Package hobsub Info: Skipping package `infwarerr' (already loaded). -Package hobsub Info: Skipping package `ltxcmds' (already loaded). -Package: ifluatex 2010/03/01 v1.3 Provides the ifluatex switch (HO) -Package ifluatex Info: LuaTeX not detected. -Package: ifvtex 2010/03/01 v1.5 Detect VTeX and its facilities (HO) -Package ifvtex Info: VTeX not detected. -Package: intcalc 2007/09/27 v1.1 Expandable calculations with integers (HO) -Package: ifpdf 2011/01/30 v2.3 Provides the ifpdf switch (HO) -Package ifpdf Info: pdfTeX in PDF mode is detected. -Package: etexcmds 2011/02/16 v1.5 Avoid name clashes with e-TeX commands (HO) -Package etexcmds Info: Could not find \expanded. -(etexcmds) That can mean that you are not using pdfTeX 1.50 or -(etexcmds) that some package has redefined \expanded. -(etexcmds) In the latter case, load this package earlier. -Package: kvsetkeys 2012/04/25 v1.16 Key value parser (HO) -Package: kvdefinekeys 2011/04/07 v1.3 Define keys (HO) -Package: pdftexcmds 2011/11/29 v0.20 Utility functions of pdfTeX for LuaTeX (HO -) -Package pdftexcmds Info: LuaTeX not detected. -Package pdftexcmds Info: \pdf@primitive is available. -Package pdftexcmds Info: \pdf@ifprimitive is available. -Package pdftexcmds Info: \pdfdraftmode found. -Package: pdfescape 2011/11/25 v1.13 Implements pdfTeX's escape features (HO) -Package: bigintcalc 2012/04/08 v1.3 Expandable calculations on big integers (HO -) -Package: bitset 2011/01/30 v1.1 Handle bit-vector datatype (HO) -Package: uniquecounter 2011/01/30 v1.2 Provide unlimited unique counter (HO) -) -Package hobsub Info: Skipping package `hobsub' (already loaded). -Package: letltxmacro 2010/09/02 v1.4 Let assignment for LaTeX macros (HO) -Package: hopatch 2012/05/28 v1.2 Wrapper for package hooks (HO) -Package: xcolor-patch 2011/01/30 xcolor patch -Package: atveryend 2011/06/30 v1.8 Hooks at the very end of document (HO) -Package atveryend Info: \enddocument detected (standard20110627). -Package: atbegshi 2011/10/05 v1.16 At begin shipout hook (HO) -Package: refcount 2011/10/16 v3.4 Data extraction from label references (HO) -Package: hycolor 2011/01/30 v1.7 Color options for hyperref/bookmark (HO) -) -(/usr/share/texlive/texmf-dist/tex/generic/ifxetex/ifxetex.sty -Package: ifxetex 2010/09/12 v0.6 Provides ifxetex conditional -) -(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/auxhook.sty -Package: auxhook 2011/03/04 v1.3 Hooks for auxiliary files (HO) -) -(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/kvoptions.sty -Package: kvoptions 2011/06/30 v3.11 Key value format for package options (HO) -) -\@linkdim=\dimen128 -\Hy@linkcounter=\count118 -\Hy@pagecounter=\count119 - -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def -File: pd1enc.def 2012/11/06 v6.83m Hyperref: PDFDocEncoding definition (HO) -) -\Hy@SavedSpaceFactor=\count120 - -(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/hyperref.cfg -File: hyperref.cfg 2002/06/06 v1.2 hyperref configuration of TeXLive -) -Package hyperref Info: Option `colorlinks' set `true' on input line 4319. -Package hyperref Info: Option `breaklinks' set `true' on input line 4319. -Package hyperref Info: Option `draft' set `true' on input line 4319. -Package hyperref Info: Hyper figures OFF on input line 4443. -Package hyperref Info: Link nesting OFF on input line 4448. -Package hyperref Info: Hyper index ON on input line 4451. -Package hyperref Info: Plain pages OFF on input line 4458. -Package hyperref Info: Backreferencing OFF on input line 4463. -Package hyperref Info: Implicit mode ON; LaTeX internals redefined. -Package hyperref Info: Bookmarks ON on input line 4688. -\c@Hy@tempcnt=\count121 -LaTeX Info: Redefining \url on input line 5041. -\XeTeXLinkMargin=\dimen129 -\Fld@menulength=\count122 -\Field@Width=\dimen130 -\Fld@charsize=\dimen131 -Package hyperref Info: Hyper figures OFF on input line 6295. -Package hyperref Info: Link nesting OFF on input line 6300. -Package hyperref Info: Hyper index ON on input line 6303. -Package hyperref Info: backreferencing OFF on input line 6310. -Package hyperref Info: Link coloring ON on input line 6313. -Package hyperref Info: Link coloring with OCG OFF on input line 6320. -Package hyperref Info: PDF/A mode OFF on input line 6325. -LaTeX Info: Redefining \ref on input line 6365. -LaTeX Info: Redefining \pageref on input line 6369. - - -Package hyperref Warning: Option `pdfpagelabels' is turned off -(hyperref) because \thepage is undefined. - -\c@Item=\count123 -\c@Hfootnote=\count124 -) - -Package hyperref Message: Driver (autodetected): hpdftex. - -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def -File: hpdftex.def 2012/11/06 v6.83m Hyperref driver for pdfTeX -\Fld@listcount=\count125 -\c@bookmark@seq@number=\count126 - -(/usr/share/texlive/texmf-dist/tex/latex/oberdiek/rerunfilecheck.sty -Package: rerunfilecheck 2011/04/15 v1.7 Rerun checks for auxiliary files (HO) -Package uniquecounter Info: New unique counter `rerunfilecheck' on input line 2 -82. -) -\Hy@SectionHShift=\skip47 -) -(/usr/share/texlive/texmf-dist/tex/latex/rotating/rotating.sty -Package: rotating 2009/03/28 v2.16a rotated objects in LaTeX - -(/usr/share/texlive/texmf-dist/tex/latex/base/ifthen.sty -Package: ifthen 2001/05/26 v1.1c Standard LaTeX ifthen package (DPC) -) -\c@r@tfl@t=\count127 -\rotFPtop=\skip48 -\rotFPbot=\skip49 -\rot@float@box=\box33 -\rot@mess@toks=\toks38 -) -(/usr/share/texlive/texmf-dist/tex/latex/algorithms/algorithm.sty -Package: algorithm 2009/08/24 v0.1 Document Style `algorithm' - floating enviro -nment - -(/usr/share/texlive/texmf-dist/tex/latex/float/float.sty -Package: float 2001/11/08 v1.3d Float enhancements (AL) -\c@float@type=\count128 -\float@exts=\toks39 -\float@box=\box34 -\@float@everytoks=\toks40 -\@floatcapt=\box35 -) -\@float@every@algorithm=\toks41 -\c@algorithm=\count129 -) -(/usr/share/texlive/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty -Package: algpseudocode - -(/usr/share/texlive/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty -Package: algorithmicx 2005/04/27 v1.2 Algorithmicx - -Document Style algorithmicx 1.2 - a greatly improved `algorithmic' style -\c@ALG@line=\count130 -\c@ALG@rem=\count131 -\c@ALG@nested=\count132 -\ALG@tlm=\skip50 -\ALG@thistlm=\skip51 -\c@ALG@Lnr=\count133 -\c@ALG@blocknr=\count134 -\c@ALG@storecount=\count135 -\c@ALG@tmpcounter=\count136 -\ALG@tmplength=\skip52 -) -Document Style - pseudocode environments for use with the `algorithmicx' style -) (/usr/share/texlive/texmf-dist/tex/latex/tools/xspace.sty -Package: xspace 2009/10/20 v1.13 Space after command names (DPC,MH) -) -(/usr/share/texlive/texmf-dist/tex/latex/graphics/color.sty -Package: color 2005/11/14 v1.0j Standard LaTeX Color (DPC) - -(/etc/texmf/tex/latex/config/color.cfg -File: color.cfg 2007/01/18 v1.5 color configuration of teTeX/TeXLive -) -Package color Info: Driver file: pdftex.def on input line 130. -) -(/usr/share/texlive/texmf-dist/tex/latex/base/textcomp.sty -Package: textcomp 2005/09/27 v1.99g Standard LaTeX package -Package textcomp Info: Sub-encoding information: -(textcomp) 5 = only ISO-Adobe without \textcurrency -(textcomp) 4 = 5 + \texteuro -(textcomp) 3 = 4 + \textohm -(textcomp) 2 = 3 + \textestimated + \textcurrency -(textcomp) 1 = TS1 - \textcircled - \t -(textcomp) 0 = TS1 (full) -(textcomp) Font families with sub-encoding setting implement -(textcomp) only a restricted character set as indicated. -(textcomp) Family '?' is the default used for unknown fonts. -(textcomp) See the documentation for details. -Package textcomp Info: Setting ? sub-encoding to TS1/1 on input line 71. - -(/usr/share/texlive/texmf-dist/tex/latex/base/ts1enc.def -File: ts1enc.def 2001/06/05 v3.0e (jk/car/fm) Standard LaTeX file -) -LaTeX Info: Redefining \oldstylenums on input line 266. -Package textcomp Info: Setting cmr sub-encoding to TS1/0 on input line 281. -Package textcomp Info: Setting cmss sub-encoding to TS1/0 on input line 282. -Package textcomp Info: Setting cmtt sub-encoding to TS1/0 on input line 283. -Package textcomp Info: Setting cmvtt sub-encoding to TS1/0 on input line 284. -Package textcomp Info: Setting cmbr sub-encoding to TS1/0 on input line 285. -Package textcomp Info: Setting cmtl sub-encoding to TS1/0 on input line 286. -Package textcomp Info: Setting ccr sub-encoding to TS1/0 on input line 287. -Package textcomp Info: Setting ptm sub-encoding to TS1/4 on input line 288. -Package textcomp Info: Setting pcr sub-encoding to TS1/4 on input line 289. -Package textcomp Info: Setting phv sub-encoding to TS1/4 on input line 290. -Package textcomp Info: Setting ppl sub-encoding to TS1/3 on input line 291. -Package textcomp Info: Setting pag sub-encoding to TS1/4 on input line 292. -Package textcomp Info: Setting pbk sub-encoding to TS1/4 on input line 293. -Package textcomp Info: Setting pnc sub-encoding to TS1/4 on input line 294. -Package textcomp Info: Setting pzc sub-encoding to TS1/4 on input line 295. -Package textcomp Info: Setting bch sub-encoding to TS1/4 on input line 296. -Package textcomp Info: Setting put sub-encoding to TS1/5 on input line 297. -Package textcomp Info: Setting uag sub-encoding to TS1/5 on input line 298. -Package textcomp Info: Setting ugq sub-encoding to TS1/5 on input line 299. -Package textcomp Info: Setting ul8 sub-encoding to TS1/4 on input line 300. -Package textcomp Info: Setting ul9 sub-encoding to TS1/4 on input line 301. -Package textcomp Info: Setting augie sub-encoding to TS1/5 on input line 302. -Package textcomp Info: Setting dayrom sub-encoding to TS1/3 on input line 303. -Package textcomp Info: Setting dayroms sub-encoding to TS1/3 on input line 304. - -Package textcomp Info: Setting pxr sub-encoding to TS1/0 on input line 305. -Package textcomp Info: Setting pxss sub-encoding to TS1/0 on input line 306. -Package textcomp Info: Setting pxtt sub-encoding to TS1/0 on input line 307. -Package textcomp Info: Setting txr sub-encoding to TS1/0 on input line 308. -Package textcomp Info: Setting txss sub-encoding to TS1/0 on input line 309. -Package textcomp Info: Setting txtt sub-encoding to TS1/0 on input line 310. -Package textcomp Info: Setting lmr sub-encoding to TS1/0 on input line 311. -Package textcomp Info: Setting lmdh sub-encoding to TS1/0 on input line 312. -Package textcomp Info: Setting lmss sub-encoding to TS1/0 on input line 313. -Package textcomp Info: Setting lmssq sub-encoding to TS1/0 on input line 314. -Package textcomp Info: Setting lmvtt sub-encoding to TS1/0 on input line 315. -Package textcomp Info: Setting qhv sub-encoding to TS1/0 on input line 316. -Package textcomp Info: Setting qag sub-encoding to TS1/0 on input line 317. -Package textcomp Info: Setting qbk sub-encoding to TS1/0 on input line 318. -Package textcomp Info: Setting qcr sub-encoding to TS1/0 on input line 319. -Package textcomp Info: Setting qcs sub-encoding to TS1/0 on input line 320. -Package textcomp Info: Setting qpl sub-encoding to TS1/0 on input line 321. -Package textcomp Info: Setting qtm sub-encoding to TS1/0 on input line 322. -Package textcomp Info: Setting qzc sub-encoding to TS1/0 on input line 323. -Package textcomp Info: Setting qhvc sub-encoding to TS1/0 on input line 324. -Package textcomp Info: Setting futs sub-encoding to TS1/4 on input line 325. -Package textcomp Info: Setting futx sub-encoding to TS1/4 on input line 326. -Package textcomp Info: Setting futj sub-encoding to TS1/4 on input line 327. -Package textcomp Info: Setting hlh sub-encoding to TS1/3 on input line 328. -Package textcomp Info: Setting hls sub-encoding to TS1/3 on input line 329. -Package textcomp Info: Setting hlst sub-encoding to TS1/3 on input line 330. -Package textcomp Info: Setting hlct sub-encoding to TS1/5 on input line 331. -Package textcomp Info: Setting hlx sub-encoding to TS1/5 on input line 332. -Package textcomp Info: Setting hlce sub-encoding to TS1/5 on input line 333. -Package textcomp Info: Setting hlcn sub-encoding to TS1/5 on input line 334. -Package textcomp Info: Setting hlcw sub-encoding to TS1/5 on input line 335. -Package textcomp Info: Setting hlcf sub-encoding to TS1/5 on input line 336. -Package textcomp Info: Setting pplx sub-encoding to TS1/3 on input line 337. -Package textcomp Info: Setting pplj sub-encoding to TS1/3 on input line 338. -Package textcomp Info: Setting ptmx sub-encoding to TS1/4 on input line 339. -Package textcomp Info: Setting ptmj sub-encoding to TS1/4 on input line 340. -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2013/08/26 1.5b listings language file -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstlang1.sty -File: lstlang1.sty 2013/08/26 1.5b listings language file -) -(/usr/share/texlive/texmf-dist/tex/latex/listings/lstmisc.sty -File: lstmisc.sty 2013/08/26 1.5b (Carsten Heinz) -) - -LaTeX Warning: Unused global option(s): - [nocopyrightspace]. - -(./paper.aux) -\openout1 = `paper.aux'. - -LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for PD1/pdf/m/n on input line 150. -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 150. -LaTeX Font Info: Try loading font information for TS1+cmr on input line 150. - - (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmr.fd -File: ts1cmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: ... okay on input line 150. -LaTeX Font Info: Try loading font information for T1+ptm on input line 150. - -(/usr/share/texlive/texmf-dist/tex/latex/psnfss/t1ptm.fd -File: t1ptm.fd 2001/06/04 font definitions for T1/ptm. -) -(/usr/share/texlive/texmf-dist/tex/context/base/supp-pdf.mkii -[Loading MPS to PDF converter (version 2006.09.02).] -\scratchcounter=\count137 -\scratchdimen=\dimen132 -\scratchbox=\box36 -\nofMPsegments=\count138 -\nofMParguments=\count139 -\everyMPshowfont=\toks42 -\MPscratchCnt=\count140 -\MPscratchDim=\dimen133 -\MPnumerator=\count141 -\makeMPintoPDFobject=\count142 -\everyMPtoPDFconversion=\toks43 -) -\c@lstlisting=\count143 -\AtBeginShipoutBox=\box37 - - -Package hyperref Warning: Height of page (\paperheight) is invalid (0.0pt), -(hyperref) using 11in. - - -Package hyperref Warning: Draft mode on. - -Package hyperref Info: Link coloring ON on input line 150. -(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty -Package: nameref 2012/10/27 v2.43 Cross-referencing by name of section - -(/usr/share/texlive/texmf-dist/tex/generic/oberdiek/gettitlestring.sty -Package: gettitlestring 2010/12/03 v1.4 Cleanup title references (HO) -) -\c@section@level=\count144 -) -LaTeX Info: Redefining \ref on input line 150. -LaTeX Info: Redefining \pageref on input line 150. -LaTeX Info: Redefining \nameref on input line 150. -LaTeX Font Info: Try loading font information for U+msa on input line 162. - -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd -File: umsa.fd 2013/01/14 v3.01 AMS symbols A -) -LaTeX Font Info: Try loading font information for U+msb on input line 162. - -(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd -File: umsb.fd 2013/01/14 v3.01 AMS symbols B -) -LaTeX Font Info: Try loading font information for U+lasy on input line 162. - -(/usr/share/texlive/texmf-dist/tex/latex/base/ulasy.fd -File: ulasy.fd 1998/08/17 v2.2e LaTeX symbol font definitions -) (./abstract.tex) -(./introduction.tex -Underfull \hbox (badness 1622) in paragraph at lines 15--26 -[]\T1/ptm/m/n/9 The C/C++ stan-dard com-mit-tee ex-tended the C and C++ - [] - - -Underfull \hbox (badness 1062) in paragraph at lines 27--38 -[]\T1/ptm/m/n/9 Researchers have de-vel-oped tools for ex-plor-ing the be-hav- - [] - - -Underfull \vbox (badness 7116) has occurred while \output is active [] - - [1{/var/lib/texmf/fonts/map/pdftex/updmap/pdftex.map} - - -] -LaTeX Font Info: Font shape `T1/ptm/bx/n' in size <9> not available -(Font) Font shape `T1/ptm/b/n' tried instead on input line 76. -LaTeX Font Info: Try loading font information for T1+pcr on input line 119. - -(/usr/share/texlive/texmf-dist/tex/latex/psnfss/t1pcr.fd -File: t1pcr.fd 2001/06/04 font definitions for T1/pcr. -) -Underfull \hbox (badness 10000) in paragraph at lines 142--163 -[]\T1/ptm/b/n/9 Constraining Re-order-ings (Spec-i-fy-ing Syn-chro-niza-tion - [] - - -File: figures/specworkflow.pdf Graphic file (type pdf) - - -Package pdftex.def Info: figures/specworkflow.pdf used on input line 174. -(pdftex.def) Requested size: 149.31004pt x 113.82695pt. -LaTeX Font Info: Font shape `T1/ptm/bx/sc' in size <9> not available -(Font) Font shape `T1/ptm/b/sc' tried instead on input line 176. - [2 <./figures/specworkflow.pdf>]) -(./formalization.tex -Underfull \hbox (badness 1975) in paragraph at lines 115--125 -[]$\OMS/cmsy/m/n/9 8\OML/cmm/m/it/9 X; Y; X \OMS/cmsy/m/n/9 2 [] ^ \OML/cmm/m/i -t/9 Y \OMS/cmsy/m/n/9 2 [] ^ - [] - -) (./paper.bbl [3]) -Package atveryend Info: Empty hook `BeforeClearDocument' on input line 182. - [4] -Package atveryend Info: Empty hook `AfterLastShipout' on input line 182. - (./paper.aux) -Package atveryend Info: Empty hook `AtVeryEndDocument' on input line 182. -Package atveryend Info: Empty hook `AtEndAfterFileList' on input line 182. -Package atveryend Info: Empty hook `AtVeryVeryEnd' on input line 182. - ) -Here is how much of TeX's memory you used: - 9020 strings out of 493308 - 129583 string characters out of 6140092 - 257583 words of memory out of 5000000 - 12319 multiletter control sequences out of 15000+600000 - 67735 words of font info for 70 fonts, out of 8000000 for 9000 - 957 hyphenation exceptions out of 8191 - 41i,12n,58p,446b,414s stack positions out of 5000i,500n,10000p,200000b,80000s -{/usr/share/texlive/texmf-dist/fonts/enc/dvips/base/8r.enc} -Output written on paper.pdf (4 pages, 152256 bytes). -PDF statistics: - 64 PDF objects out of 1000 (max. 8388607) - 0 named destinations out of 1000 (max. 500000) - 6 words of extra memory for PDF output out of 10000 (max. 10000000) - diff --git a/correctness-model/writeup/paper.pdf b/correctness-model/writeup/paper.pdf deleted file mode 100644 index 2fc673b..0000000 Binary files a/correctness-model/writeup/paper.pdf and /dev/null differ