IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

Maximal Causal Models for Sequentially Consistent Systems

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/27708

Files in this item

File Description Format
PDF serbanuta-chen-rosu-2011-tr.pdf (590KB) main article PDF
Title: Maximal Causal Models for Sequentially Consistent Systems
Author(s): Șerbănuță, Traian Florin; Chen, Feng; Rosu, Grigore
Subject(s): causal properties and models multithreaded systems runtime verification sequential consistency
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 al l 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 defined 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.
Issue Date: 2011-10-14
Citation Info: @techreport{serbanuta-chen-rosu-2011-tr, title={Maximal Causal Models for Sequentially Consistent Systems}, author = {Traian Florin \Serbanuta{} and Feng Chen and Grigore \Rosu{}}, year={2011}, month={October}, institution={University of Illinois at Urbana-Champaign}, }
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/27708
Publication Status: unpublished
Peer Reviewed: not peer reviewed
Date Available in IDEALS: 2011-10-15
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 122
  • Downloads this Month: 2
  • Downloads Today: 0

Browse

My Account

Information

Access Key