changes
authorPeizhao Ou <peizhaoo@uci.edu>
Fri, 10 Apr 2015 23:05:57 +0000 (16:05 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Fri, 10 Apr 2015 23:05:57 +0000 (16:05 -0700)
correctness-model/writeup/formalization.tex
correctness-model/writeup/paper.aux
correctness-model/writeup/paper.log
correctness-model/writeup/paper.pdf

index aecb783..5d10f43 100644 (file)
@@ -1,21 +1,46 @@
 \mysection{Formalization of Correctness Model}\label{sec:formalization}
 
-Unlike the SC memory model, applying linearizability can be complicated under
-C/C++ by the fact that the C/C++ memory model allows atomic loads to read from
-atomic stores that appear later in the trace and that it is in general
-impossible to produce a sequential history that preserves program order for the
-C/C++ memory model. Intuitively however, we can weaken some constraints, e.g.
+Unlike the SC memory model, finding an appropriate correctness model for
+concurrent data structures under the C/C++11 memory model is challenging. For
+example, linearizability no longer fits C/C++ by the fact that the C/C++ memory
+model allows atomic loads to read from atomic stores that appear later in the
+trace and that it is in general impossible to produce a sequential history that
+preserves program order for the C/C++ memory model.
+
+Consider the following example:
+
+{
+\footnotesize
+\begin{verbatim}
+Thrd 1:              Thrd 2:
+x = 1;               y = 1;
+r1 = y;              r2 = x;
+\end{verbatim}
+}
+
+Suppose each operation in this example is the only operation of each method
+call, and shared variables \code{x} and \code{y} are both initilly \code{0}.
+Each store operation has \code{release} semantics and each load operation has
+\code{acquire} semantics. For the execution where both \code{r1} and \code{r2}
+obtain the old value \code{0}, we encounter a challenge of generating a
+sequential history. Since neither load operation reads
+from the corresponding store, they should be ordered before their corresponding
+store operation. On the other hand, both stores happen before the other load
+(intra-thread ordering), making it impossible to topologically sort the
+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.
 
-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 between nodes are
-derived from the \textit{happens-before} edges and the \textit{modification
-order} edges between ordering points. We define \textit{opo} as the
-\textit{ordering point order} relation between ordering point.  Given two
-operations $X$ and $Y$ that are both ordering points, the \textit{modification
-order} edges are as follow:
+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
+between nodes are derived from the \textit{happens-before} edges and the
+\textit{modification order} edges between ordering points. We define
+\textit{opo} as the \textit{ordering point order} relation between ordering
+point.  Given two operations $X$ and $Y$ that are both ordering points, the
+\textit{modification order} edges are as follow:
 
 \squishcount
 
@@ -30,10 +55,40 @@ order} edges are as follow:
 
 \vspace{0.3cm}
 
-Intuitively, if method $A$ 
-
-In order to relax the contraints on the original execution graph, we define an
-action \textit{tranform} that can be performed on the graph as follow:
+Intuitively, if method $A$ has an information flow to method $B$, we want method
+$B$ to see the effects before method $A$. In C/C++11, on the other hand, we want
+method $A$ to have \code{release} semantics while method $B$ to have
+\code{acquire} semantics so that they establish the happens-before relationship.
+For example, for a concurrent queue, we want a dequeuer synchronizes with the
+corresponding enqueuer so that when the dequeuer obtains a reference to an
+object, it can read the fully initialized value of that object. To some degree
+this can also avoid data races. When it comes to C/C++11 data structures, the
+ordering points of method calls should have release/acquire semantics on stores
+and loads.
+
+In order to relax the contraints on the original execution graph, we will have
+to disregard some happens-before edges. To make our model intuitive, we want to
+keep the happens-before edges from stores to stores and from load operations to
+store operations because that can ensure information is only flowing from
+earlier store operations. Besides, we also want to keep the happens-before edges
+between operations on the same memory location since otherwise the generated
+history will become very counter-intuitive. However, such a model does not work
+in C/C++ in general.  Consider the following example:
+
+Consider the following example:
+
+{
+\footnotesize
+\begin{verbatim}
+Thrd 1:     Thrd 2:     Thrd 3:     Thrd 4:
+x = 1;      y = 2;      r1 = x;     r3 = y;
+y = 1;      x = 2;      r2 = x;     r4 = y;
+\end{verbatim}
+}
+
+
+We define an action \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
index 605a7ee..8dd863b 100644 (file)
 \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}
-\@writefile{toc}{\contentsline {section}{\numberline {2}Formalization of Correctness Model}{\thepage }{section.2}}
-\newlabel{sec:formalization}{{2}{\thepage }{Formalization of Correctness Model}{section.2}{}}
+\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}{}}
@@ -68,8 +73,3 @@
 \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}
index 7b65903..f101d8e 100644 (file)
@@ -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 10:40
+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
 entering extended mode
  restricted \write18 enabled.
  %&-line parsing enabled.
@@ -619,7 +619,7 @@ 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 34--40
+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
  []
@@ -638,11 +638,11 @@ 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
- 252583 words of memory out of 5000000
+ 256583 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,418s stack positions out of 5000i,500n,10000p,200000b,80000s
+ 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}</usr/share/texliv
 e/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></usr/share/texlive/texmf
 -dist/fonts/type1/public/amsfonts/cm/cmmi9.pfb></usr/share/texlive/texmf-dist/f
@@ -653,7 +653,7 @@ courier/ucrr8a.pfb></usr/share/texlive/texmf-dist/fonts/type1/urw/helvetic/uhvb
 /share/texlive/texmf-dist/fonts/type1/urw/times/utmb8a.pfb></usr/share/texlive/
 texmf-dist/fonts/type1/urw/times/utmr8a.pfb></usr/share/texlive/texmf-dist/font
 s/type1/urw/times/utmri8a.pfb>
-Output written on paper.pdf (4 pages, 147616 bytes).
+Output written on paper.pdf (4 pages, 151101 bytes).
 PDF statistics:
  64 PDF objects out of 1000 (max. 8388607)
  0 named destinations out of 1000 (max. 500000)
index e32ddb8..a772843 100644 (file)
Binary files a/correctness-model/writeup/paper.pdf and b/correctness-model/writeup/paper.pdf differ