Mainstream programming is migrating to concurrent architectures to improve performance and facilitate more complex computation. The state of the art static analysis tools for detecting concurrency errors are imprecise, generate a large number of false error warnings, and require manual verification of each warning. In this paper we present a meta heuristic to help reduce the manual effort required in the verification of warnings generated by static analysis tools. We manually generate a small sequence of program locations that represent points of interest in checking the feasibility of a particular static analysis warning; then we use a meta heuristic to automatically control scheduling decisions in a model checker to guide the program along the input sequence to test the feasibility of the warning. The meta heuristic guides a greedy depth-first search based on a two-tier ranking system where the first tier considers the number of program locations already observed from the input sequence, and the second tier considers the perceived closeness to the next location in the input sequence. The error traces generated by this technique are real and require no further manual verification. We show the effectiveness of our approach by detecting feasible concurrency errors in benchmarked concurrent programs and the JDK 1.4 concurrent libraries based on warnings generated by the Jlint static analysis tool.

Pdf version

Conference Slides

N. Rungta and E. G. Mercer. “A meta heuristic for effectively detecting concurrency errors,” Haifa Verification Conference, Haifa, Israel, November 2008.

@inproceedings{rungta:hvc08,
author = {N. Rungta and E. G. Mercer},
title= {A meta heuristic for effectively detecting concurrency errors},
booktitle= {Haifa Verification Conference},
year = {2008},
address={Haifa, Israel},}