Lost in Abstraction: Monotonicity in Multi-Threaded Programs

Monotonicity in concurrent systems stipulates that, in any global state, extant system actions remain executable when new processes are added to the state. This concept is not only natural and common in multi-threaded software, but also useful: if every thread's memory is finite, monotonicity often guarantees the decidability of safety property verification even when the number of running threads is unknown.

In this talk I show that the act of obtaining finite-data thread abstractions for model checking can be at odds with monotonicity: Predicate-abstracting certain classical monotone software results in non-monotone multi-threaded Boolean programs --- the monotonicity is "lost in the abstraction". As a result, well-established sound and complete safety checking algorithms for certain infinite-state systems become inapplicable. I demonstrate how the monotonicity in the abstract programs can be restored, without affecting safety properties of the non-monotone abstraction. This significantly improves earlier approaches of enforcing monotonicity via overapproximations.

We have applied our method successfully to numerous system-level concurrent programs and synchronization algorithms, whose predicate abstractions are, in many cases, fundamentally beyond existing tools.

Joint work with Alexander Kaiser and Daniel Kroening, Oxford University

Thomas Wahl joined the faculty of Northeastern University in 2011. He moved to Boston from Oxford/United Kingdom, where he was a Research Officer in the Computing Laboratory (now Department of Computer Science). Prior to the Oxford experience, Wahl held a postdoctoral position at the Swiss Federal Institute of Technology (ETH) in Zurich. He obtained a
PhD degree in Computer Science from the University of Texas at Austin in 2007.

Wahl's research concerns the reliability of complex and mission-critical computing systems. Two domains notorious for their fragility are concurrency and numerical computing. With colleagues, Wahl has developed leading algorithms and techniques that permit the automated analysis of concurrent software such as multi-threaded or data-parallel programs using rigorous formal techniques, which are able to track down deep, unintuitive and nearly untestable program bugs. He has also investigated how floating-point arithmetic can "hijack" a program's computation when run on non-standard architectures, such as heterogeneous and custom-made embedded platforms.