[Back]

N. Razavi, A. Farzan, A. Holzer:
"Bounded-Interference Sequentialization for Testing Concurrent Programs";
Talk: International Symposium on Leveraging Applications of Formal Methods (ISoLA), Heraklion, Kreta, Griechenland; 2012-10-15 - 2012-10-18; in: "Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change", Lecture Notes in Computer Science. Springer Verlag., 7609 (2012), ISBN: 978-3-642-34025-3; 372 - 387.

Testing concurrent programs is a challenging problem: (1) the tester has to come up with a set of input values that may trigger a bug, and (2) even with a bug-triggering input value, there may be a large number of interleavings that need to be explored. This paper proposes an approach for testing concurrent programs that explores both input and interleaving spaces in a systematic way. It is based on a program transformation technique that takes a concurrent program P as an input and generates a sequential program that simulates a subset of behaviours of P. It is then possible to use an available sequential testing tool to test the resulting sequential program. We introduce a new interleaving selection technique, called bounded-interference, which is based on the idea of limiting the degree of interference from other threads. The transformation is sound in the sense that any bug discovered by a sequential testing tool in the sequential program is a bug in the original concurrent program. We have implemented our approach into a prototype tool that tests concurrent C# programs. Our experiments show that our approach is effective in finding both previously known and new bugs.

http://dx.doi.org/10.1007/978-3-642-34026-0_28