From: Peizhao Ou Date: Sat, 11 Apr 2015 01:32:08 +0000 (-0700) Subject: changes X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=e614e496496b9822e4d0f1f78c04cf66aa0aaee5;ds=sidebyside changes --- diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex index 5d10f43..2cc4564 100644 --- a/correctness-model/writeup/formalization.tex +++ b/correctness-model/writeup/formalization.tex @@ -32,7 +32,9 @@ operations to generate a consistent sequential history. Intuitively however, we can weaken some constraints, e.g. the \textit{happens-before} edges in some cases, to generate a reordering of ordering points such that they yield a sequential history that is consistent -with the specification. We formalize our approach as follow. +with the specification. We formalize our approach as follow. The goal is to come +up with a correctness model that is weaker than linearizability and SC and yet +is composable. First of all, we represent a trace as an \textit{execution graph}, where each node represents each API method call with a set of ordering points, and edges @@ -86,17 +88,43 @@ y = 1; x = 2; r2 = x; r4 = y; \end{verbatim} } - -We define an action \textit{tranform} that can be performed on the graph as +We encounter a challenge for the execution where the following holds: +\path{r1 == 2 && r2 == 1 && r3 == 1 && r4 == 2}. For any total order that is +consistent with the happens-before relation, that total order will be +inconsistent with the modification order in either variable \code{x} or +\code{y}. For example, if \code{y = 1} is ordered before \code{y = 2}, then +\code{x = 1} is ordered before \code{x = 2} while \code{r1 = x} is ordered +before \code{r2 = x}. As a result, we cannot possibly move up the second load +operation \code{r2 = x} across \code{r1 = x} to generate a consistent sequential +history. To solve this, one option is that allow loads to move up any operation +including load and store operation on the same location. However, it is +extremely conuter-intuitive for a later load operation to read an older value. +By analysis, the problem here is that the store operations with different values +to the same memory location are not ordered. This is actually a really rare case +because it could be possible that only one store operation takes effect and all +other store operations are useless. We believe that such case of blind stores +from different threads is not the general pattern for concurrent data +structures, and we believe that store operations are ordered. In terms of +ordering points, we believe that in real-world data structures, store operations +of ordering points are ordered by happens-before relation. +\todo{argue why ordered stores are reasonable to concurrent data structures} + +We next define an action called \textit{tranform} that can be performed on the graph as follow: -\mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in -\textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge +$ \forall X, Y, X \in \textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge address(X)\not=address(Y) \wedge -X \relation{hb} Y \wedge Y \in \textit{LoadOps}\xspace -\Rightarrow \forall Z, Z +X \relation{hb} Y \wedge +Y \in \textit{LoadOps}\xspace +\Rightarrow +\forall Z, +Z \in \textit{orderingPoints}\xspace \wedge +Z \relation{hb} X, +Z \relation{hb} Y \wedge \neg X \relation{hb} Y $. +Under these analysis and assumptions, we clearly define our correctness model as +follow: \begin{figure}[!htbp] \begin{algorithmic}[1] @@ -133,15 +161,4 @@ $. \caption{\label{fig:algorithmfence}Algorithm for inferring order parameters} \end{figure} - - -\mypara{\bf Generating the Reordering:} -The \TOOL checker first builds an execution graph where the nodes are -method calls and the edges represent the -$\reltext{opo}$ ordering of the ordering points of the methods that -correspond to the source and destination nodes. Assuming the absence -of cycles in the execution graph, -the $\reltext{opo}$ ordering is used to generate the sequential history. -The \TOOL checker -topologically sorts the graph to generate the equivalent sequential -execution. +\todo{prove that our correctness model is composable} diff --git a/correctness-model/writeup/paper.aux b/correctness-model/writeup/paper.aux index 8dd863b..d3d63d5 100644 --- a/correctness-model/writeup/paper.aux +++ b/correctness-model/writeup/paper.aux @@ -46,15 +46,15 @@ \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} -\@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} diff --git a/correctness-model/writeup/paper.log b/correctness-model/writeup/paper.log index f101d8e..b7ef3f1 100644 --- a/correctness-model/writeup/paper.log +++ b/correctness-model/writeup/paper.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013/Debian) (format=pdflatex 2014.3.31) 10 APR 2015 16:03 +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. @@ -619,16 +619,14 @@ 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 4981) in paragraph at lines 93--99 -\T1/ptm/b/n/9 Hoisting loads: $\OMS/cmsy/m/n/9 8\OML/cmm/m/it/9 X; Y; X \OMS/cm -sy/m/n/9 2 [] ^ \OML/cmm/m/it/9 Y \OMS/cmsy/m/n/9 2 +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 - -] + [4] Package atveryend Info: Empty hook `AfterLastShipout' on input line 182. (./paper.aux) Package atveryend Info: Empty hook `AtVeryEndDocument' on input line 182. @@ -638,7 +636,7 @@ 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 - 256583 words of memory out of 5000000 + 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 @@ -653,7 +651,7 @@ courier/ucrr8a.pfb> -Output written on paper.pdf (4 pages, 151101 bytes). +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) diff --git a/correctness-model/writeup/paper.pdf b/correctness-model/writeup/paper.pdf index a772843..2fc673b 100644 Binary files a/correctness-model/writeup/paper.pdf and b/correctness-model/writeup/paper.pdf differ