Withdraw
Loading…
Maximal Causal Models for Multithreaded Systems
Serbanuta, Traian Florin; Chen, Feng; Rosu, Grigore
Loading…
Permalink
https://hdl.handle.net/2142/10863
Description
- Title
- Maximal Causal Models for Multithreaded Systems
- Author(s)
- Serbanuta, Traian Florin
- Chen, Feng
- Rosu, Grigore
- Issue Date
- 2008-12
- Keyword(s)
- Computer Science
- 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 defines a novel theoretical foundation for multithreaded executions and a novel causal model, based on memory consistency constraints. 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-fly datarace detection. This datarace-focused model, still captures more feasible executions than the existing happens-before-based approaches.
- Type of Resource
- text
- Permalink
- http://hdl.handle.net/2142/10863
Owning Collections
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…