# Difference between revisions of "Maximal Causal Models for Multithreaded Systems"

From FSL

m |
m |
||

Line 24: | Line 24: | ||

== PLDI'09 Submission == | == PLDI'09 Submission == | ||

</private><pub id='serbanuta-chen-rosu-2009-pldi' template='PubDefaultWithAbstractAndNoLinkedTitle'></pub><private> | </private><pub id='serbanuta-chen-rosu-2009-pldi' template='PubDefaultWithAbstractAndNoLinkedTitle'></pub><private> | ||

− | </private>== Technical Report 2008 == | + | </private> |

+ | == Technical Report 2008 == | ||

<pub id="serbanuta-chen-rosu-2008-tr-a" draft template='PubDefaultWithAbstractAndNoLinkedTitle'></pub> | <pub id="serbanuta-chen-rosu-2008-tr-a" draft template='PubDefaultWithAbstractAndNoLinkedTitle'></pub> |

## Revision as of 12:49, 3 October 2012

## Contents |

## RV'12

**Maximal Causal Models for Sequentially Consistent Systems**- Traian Florin Serbanuta, Feng Chen and Grigore Rosu
, LNCS. 7687, pp 136-150. 2013**RV'12**

*Abstract.*This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value as it can be used to prove the soundness of non-maximal, and thus smaller, causal models.

## Technical Report 2011

**Maximal Causal Models for Sequentially Consistent Systems**- Traian Florin Serbanuta, Feng Chen and Grigore Rosu
http://hdl.handle.net/2142/27708, October 2011**Technical Report**

*Abstract.*This paper shows that it is possible to build a maximal and sound causal model for concurrent computations from a given execution trace. It is sound, in the sense that any program which can generate a trace can also generate all traces in its causal model. It is maximal (among sound models), in the sense that by extending the causal model of an observed trace with a new trace, the model becomes unsound: there exists a program generating the original trace which cannot generate the newly introduced trace. Thus, the maximal sound model has the property that it comprises all traces which all programs that can generate the original trace can also generate. The existence of such a model is of great theoretical value. First, it can be used to prove the soundness of non-maximal, and thus smaller, causal models. Second, since it is maximal, the proposed model allows for natural and causal-model-independent definitions of trace-based properties; this paper proposes maximal definitions for causal dataraces and causal atomicity. Finally, although deﬁned axiomatically, the set of traces comprised by the proposed model are shown to be effectively constructed from the original trace. Thus, maximal causal models are also amenable for developing practical analysis tools.

## Technical Report 2010

**Maximal Causal Models for Sequentially Consistent Multithreaded Systems**- Traian Florin Serbanuta, Feng Chen and Grigore Rosu
http://hdl.handle.net/2142/17336, September 2010**Technical Report**

*Abstract.*This paper shows that it is possible to build a theoretically maximal and sound causal model for concurrent computations from a given execution trace. For an observed execution, the proposed model comprises all consistent executions which can be derived from it using only knowledge about the execution machine. The existence of such a model is of great theoretical value. First, by comprising all feasible executions, it can be used to prove soundness of other causal models: indeed, several models underlying existing techniques are shown to be embedded into the maximal model, so all these models are sound. Second, since it is maximal, the proposed model allows for natural and causal-model-independent deﬁnitions of trace-based properties; this paper proposes maximal deﬁnitions for causal dataraces and causal atomicity. Finally, although deﬁned axiomatically, the set of traces comprised by the proposed model are shown to be eﬀectively constructed from an initial observed trace. Thus, maximal causal models are not only theoretically relevant, but they are also amenable for developing practical analysis tools.

## Technical Report 2008

**Maximal Causal Models for Multithreaded Systems**- Traian Florin Serbanuta, Feng Chen and Grigore Rosu
UIUCDCS-R-2008-3017, December 2008**Technical report**

*Abstract.*Extracting causal models from observed executions has proved to be an effective approach to analyze concurrent programs. Most existing causal models are based on happens-before partial orders and/or Mazurkiewicz traces. Unfortunately, these models are inherently limited in the context of multithreaded systems, since multithreaded executions are mainly determined by consistency among shared memory accesses rather than by partial orders or event independence. This paper deﬁnes a novel theoretical foundation for multithreaded executions and a novel causal model, based on memory consistency con- straints. The proposed model is sound and maximal: (1) all traces consistent with the causal model are feasible executions of the multithreaded program under analysis; and (2) assuming only the observed execution and no knowledge about the source code of the program, the proposed model captures more feasible executions than any other sound causal model. An algorithm to systematically generate all the feasible executions comprised by maximal causal models is also proposed, which can be used for testing or model checking of multithreaded system executions. Finally, a specialized submodel of the maximal one is presented, which gives an efficient and effective solution to on-the-ﬂy datarace detection. This datarace-focused model, still captures more feasible executions than the existing happens-before-based approaches.