Files in this item



application/pdfluo-huang-rosu-2015-uiuc-tr.pdf (740kB)
updated report pdfPDF


Title:Systematic Concurrency Testing with Maximal Causality
Author(s):Luo, Qingzhou; Huang, Jeff; Rosu, Grigore
Subject(s):concurrency, systematic exploration, testing, maximal causal model
Abstract:We propose the first systematic concurrent program testing approach that is able to cover the entire scheduling space with a provably minimal number of test runs. Each run corresponds to a distinct maximal causal model extracted from a given execution trace, which captures the largest possible set of causally equivalent legal executions. The maximal causal models can be represented using first-order logic constraints, and testing all the executions comprised by a maximal causal model reduces to offline constraint solving. Based on the same constraint model, we also develop a schedule generation algorithm that iteratively generates new casually different schedules. The core idea is to systematically force previous read operations to read different values, thus enumerating all the causal models. We have implemented our approach in an explicit stateless model checker, and our eval- uation showed that our technique is able to 1) find concurrency bugs faster; 2) finish state space exploration with much fewer schedules than previous techniques.
Issue Date:2015
Genre:Technical Report
Sponsor:NSF CCF-1218605
NSA grant H98230-10-C-0294
Rockwell Collins contract 4504813093
DARPA HACMS program as SRI subcontract 19-000222
Date Available in IDEALS:2015-05-22

This item appears in the following Collection(s)

Item Statistics