Systematic Concurrency Testing with Maximal Causality

Luo, Qingzhou; Huang, Jeff; Rosu, Grigore

Permalink

https://hdl.handle.net/2142/77745 Copy

Description

Title

Systematic Concurrency Testing with Maximal Causality

Author(s)

• Luo, Qingzhou
• Huang, Jeff
• Rosu, Grigore

Issue Date

2015

Keyword(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.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/77745

Sponsor(s)/Grant Number(s)

• NSF CCF-1218605
• NSA grant H98230-10-C-0294
• Rockwell Collins contract 4504813093
• DARPA HACMS program as SRI subcontract 19-000222

Owning Collections