From: Peizhao Ou Date: Fri, 10 Apr 2015 23:05:57 +0000 (-0700) Subject: changes X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e8942c527bf582229e12d9a922a099dd168375d6;p=cdsspec-compiler.git changes --- diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex index aecb783..5d10f43 100644 --- a/correctness-model/writeup/formalization.tex +++ b/correctness-model/writeup/formalization.tex @@ -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 diff --git a/correctness-model/writeup/paper.aux b/correctness-model/writeup/paper.aux index 605a7ee..8dd863b 100644 --- a/correctness-model/writeup/paper.aux +++ b/correctness-model/writeup/paper.aux @@ -52,11 +52,16 @@ \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} diff --git a/correctness-model/writeup/paper.log b/correctness-model/writeup/paper.log index 7b65903..f101d8e 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 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} -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) diff --git a/correctness-model/writeup/paper.pdf b/correctness-model/writeup/paper.pdf index e32ddb8..a772843 100644 Binary files a/correctness-model/writeup/paper.pdf and b/correctness-model/writeup/paper.pdf differ