Maximal Causal Models for Multithreaded Systems

From FSL
Revision as of 07:10, 16 August 2012 by Tserban2 (Talk | contribs)

Jump to: navigation, search


Maximal Causal Models for Sequentially Consistent Systems
Traian Florin Serbanuta, Feng Chen and Grigore Rosu
RV'12, LNCS. 7687, pp 136-150. 2013
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.
PDF, Slides(PDF), BIB

Technical Report 2011

Technical Report 2010

Personal tools