License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2017.16
URN: urn:nbn:de:0030-drops-72523
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7252/
Go to the corresponding LIPIcs Volume Portal

Huang, Shiyou ; Huang, Jeff

Speeding Up Maximal Causality Reduction with Static Dependency Analysis

pdf-format:
LIPIcs-ECOOP-2017-16.pdf (0.8 MB)

Abstract

Stateless Model Checking (SMC) offers a powerful approach to verifying multithreaded programs but suffers from the state-space explosion problem caused by the huge thread interleaving space. The pioneering reduction technique Partial Order Reduction (POR) mitigates this problem by pruning equivalent interleavings from the state space. However, limited by the happens-before relation, POR still explores redundant executions. The recent advance, Maximal Causality Reduction (MCR), shows a promising performance improvement over the existing reduction techniques, but it has to construct complicated constraints to ensure the feasibility of the derived execution due to the lack of dependency information. In this work, we present a new technique, which extends MCR with static analysis to reduce the size of the constraints, thus speeding up the exploration of the state space. We also address the redundancy problem caused by the use of static analysis. We capture the dependency between a read and a later event e in the trace from the system dependency graph and identify those reads that e is not control dependent on. Our approach then ignores the constraints over such reads to reduce the complexity of the constraints. The experimental results show that compared to MCR, the number of the constraints and the solving time by our approach are averagely reduced by 31.6% and 27.8%, respectively.

BibTeX - Entry

@InProceedings{huang_et_al:LIPIcs:2017:7252,
  author =	{Shiyou Huang and Jeff Huang},
  title =	{{Speeding Up Maximal Causality Reduction with Static Dependency Analysis}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{16:1--16:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7252},
  URN =		{urn:nbn:de:0030-drops-72523},
  doi =		{10.4230/LIPIcs.ECOOP.2017.16},
  annote =	{Keywords: Model Checking, Dynamic Analysis, Program Dependency Analysis}
}

Keywords: Model Checking, Dynamic Analysis, Program Dependency Analysis
Collection: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 16.06.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI