From: Peizhao Ou
Date: Sat, 11 Apr 2015 01:32:08 +0000 (0700)
Subject: changes
XGitUrl: http://plrg.eecs.uci.edu/git/?p=cdsspeccompiler.git;a=commitdiff_plain;h=e614e496496b9822e4d0f1f78c04cf66aa0aaee5
changes

diff git a/correctnessmodel/writeup/formalization.tex b/correctnessmodel/writeup/formalization.tex
index 5d10f43..2cc4564 100644
 a/correctnessmodel/writeup/formalization.tex
+++ b/correctnessmodel/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{happensbefore} 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 happensbefore 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 conuterintuitive 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 realworld data structures, store operations
+of ordering points are ordered by happensbefore 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/correctnessmodel/writeup/paper.aux b/correctnessmodel/writeup/paper.aux
index 8dd863b..d3d63d5 100644
 a/correctnessmodel/writeup/paper.aux
+++ b/correctnessmodel/writeup/paper.aux
@@ 46,15 +46,15 @@
\bibstyle{abbrv}
\bibdata{confstrslong,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/correctnessmodel/writeup/paper.log b/correctnessmodel/writeup/paper.log
index f101d8e..b7ef3f1 100644
 a/correctnessmodel/writeup/paper.log
+++ b/correctnessmodel/writeup/paper.log
@@ 1,4 +1,4 @@
This is pdfTeX, Version 3.14159262.51.40.14 (TeX Live 2013/Debian) (format=pdflatex 2014.3.31) 10 APR 2015 16:03
+This is pdfTeX, Version 3.14159262.51.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 9399
\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 115125
+[]$\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/correctnessmodel/writeup/paper.pdf b/correctnessmodel/writeup/paper.pdf
index a772843..2fc673b 100644
Binary files a/correctnessmodel/writeup/paper.pdf and b/correctnessmodel/writeup/paper.pdf differ