“Data-race free” programs

In section 6.3 of the paper Causal memory: definitions, implementations, and programming, the authors define "data-race free" as follows:

Program $\Pi$ is data-race free if, for all histories $H$ of $\Pi$ and all causality orders $\leadsto$ of $H$, if $H$ has a serialization that respects $\leadsto$ (note that this implies that $H$ is sequentially consistent), then $H$ is data-race free with respect to $\leadsto$.

The one-sentence definition is too complicated for me to follow. It involves various notions and their relations. Specifically, a program is a set of its histories. Given a history, there may be more than one causality order for it, because there may be multiple writes of a value to a variable and thus more than one writes-into order. Let $H$ be a history with causality order $\leadsto$. We have to consider whether it is sequentially consistent and data-race free with respect to $\leadsto$.

The following image enumerates all the possible classes of executions which I can think of produced by any program. The red crosses in the image indicate non-existence. For instance, the "path" $\Pi - H_1 - \leadsto_{12} - S_{12} - DRF_{12}$ means that $S_{12}$ is a serialization (thus sequentially consistent) of history $H_1$ that respects $\leadsto_{12}$ but is not data-race free with respect to $\leadsto_{12}$. EDIT: Here are some explanations of this image. For any program, there are five possible classes of executions. $H_0$ indicates the class of executions which have no causality orders at all (i.e., it causality orders are cyclic). The executions like $H_1$ have more than one causality orders, such as $\leadsto_{11}, \leadsto_{12},$ and $\leadsto_{13}$. However, $H_1$ (as a representative of its class) is not sequentially consistent respecting $\leadsto_{11}$ (denoted by the red cross over $S_{11}$); $H_1$ is sequentially consistent respecting $\leadsto_{12}$ but is not data-race free with respect to $\leadsto_{12}$ (denoted by the red cross over $DRF_{12}$); and $H_1$ is sequentially consistent respecting $\leadsto_{13}$ and is data-race free with respect to $\leadsto_{13}$. The cases for $H_2$, $H_3$, and $H_4$ are similar.

Here comes my first problem:

(1). What are the classes of executions excluded by "data-race free"? (and does the image miss some classes of executions?)

In my opinion, only the executions like $H_1$ are excluded. The reason is that the "path" $\Pi - H_1 - \leadsto_{12} - S_{12} - DRF_{12}$ violates the definition of "data-race free".

Immediately following the definition of data-race free, the authors show that data-race free programs produce only sequential consistent executions when run on causal memory:

Theorem 5. If $\Pi$ is data-race free, then all histories of $\Pi$ with causal memory are sequentially consistent.

In the first paragraph of its proof, it says that "Let $H$ be a finite (infinite) causal history and let $\leadsto$ be a causality order that proves that $H$ is causal. We will prove that $H$ is data-race free with respect to $\leadsto$ and has a serialization that respects $\leadsto$".

Here come my other two problems:

(2). Back to the image above, does the theorem mean that when run on causal memory data-race free programs produce only the executions like $H_3$ which are both sequentially consistent and data-race free with respect to each of its causality orders?

(3). If so, is it right to conclude that the executions produced by data-race free programs when run on causal memory actually satisfy some stronger consistency model (though not formally defined) than sequentially consistent model?

Besides the answers to my problems, any personal (or even subjective) comments worthy of note on the definition "data-race free" are appreciated.

• I can't understand your figure. Regarding your first question, after the proof of Theorem 5 there is an example of an execution which is not data-race free. Regarding question 1, the causal memory doesn't necessarily realize all causality orders. For each causality order it does realize, by definition the execution is data-race free, and the theorem shows that it is sequentially consistent. Regarding question 2, the stronger consistency model is data-race freeness. – Yuval Filmus Mar 2 '14 at 2:34
• @YuvalFilmus Thanks. I have added some explanations of the figure. I am trying to figure out the classes of executions which are excluded by "data-race free" by first enumerating all possible classes of them and then examining them one by one. Note that I have changed the problem numbers to refer to. For question (2), what do mean by the causal memory doesn't necessarily realize all causality orders. Whose causality orders are you referring to? For question (3), I am seeking for an approval and a disapproval. Are there some theoretical treatments about the data-race freeness model? – hengxin Mar 2 '14 at 6:24
• @vzn think the basic idea here is that this is a tree of execution orders, where each node is a different sequence that could be "chosen" by the parallelizing thread logic. It seems that you are making comments on the figure. Sorry for its vagueness. I have added some explanations of it. Hope it is clearer now. (Maybe this post should (can) be moved to tcs.se as you suggested). – hengxin Mar 2 '14 at 6:37