Finding concurrency bugs under imprecise harnesses
One way of scaling verification technology to real software is to reduce the code size under analysis. Instead of applying verification to the entire system, one can pick a single component and apply verification to it. While this can dramatically help reduce analysis time, it can lead to false alarms when, for instance, the test harness does not set up the initial state properly before calling into the component.
In this work, we explore the possibility of automatically filtering away (or prioritizing) warnings that result from imprecision in the harness. We limit our attention to the scenario when one is interested in finding bugs due to concurrency. We define a warning to be an interleaved bug when it manifests on an input for which no sequential interleaving produces a warning. We argue that limiting a static analysis to only consider interleaved bugs greatly reduces false positives during static concurrency analysis in the presence of an imprecise harness.
Akash Lal is a researcher at Microsoft Research, Bangalore. His interests are in the area of programming languages and program analysis, with a focus on building bug-finding tools for concurrent programs. He joined Microsoft in 2009 after completing his PhD from University of Wisconsin-Madison under the supervision of Prof. Thomas Reps. For his thesis, he received the Outstanding Graduate Researcher Award, given by the Computer Sciences Department of UW-Madison, and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He completed his Bachelor's degree from IIT-Delhi in 2003