Academic Commons

Theses Doctoral

Sound and Precise Analysis of Multithreaded Programs through Schedule Specialization and Execution Filters

Wu, Jingyue

Multithreaded programs are known to be difficult to analyze. A key reason is that they typically have an enormous number of execution interleavings, or schedules. Static analysis with respect to all schedules requires over-approximation, resulting in poor precision; dynamic analysis rarely covers more than a tiny fraction of all schedules, so its result may not hold for schedules not covered.
To address this challenge, we propose a novel approach called schedule specialization that restricts the schedules of a program to make it easier to analyze. Schedule specialization combines static and dynamic analysis. It first statically analyzes a multithreaded program with respect to a small set of schedules for precision, and then enforces these schedules at runtime for soundness of the static analysis results.
To demonstrate that this approach works, we build three systems. The first system is a specialization framework that specializes a program into a simpler program based on a schedule for precision. It allows stock analyses to automatically gain precision with only little modification.
The second system is Peregrine, a deterministic multithreading system that collects and enforces schedules on future inputs. Peregrine reuses a small set of schedules on many inputs, ensuring our static analysis results to be sound for a wide range of inputs. It also enforces these schedules efficiently, making schedule specialization suitable for production usage.
Although schedule specialization can make static concurrency error detection more precise, some concurrency errors such as races may still slip detection and enter production systems. To mitigate this limitation, we build Loom, a live-workaround system that protects a live multithreaded program from races that slip detection. It allows developers to easily write execution filters to safely and efficiently work around deployed races in live multithreaded programs without restarting them.

Subjects

Files

  • thumnail for Wu_columbia_0054D_12350.pdf Wu_columbia_0054D_12350.pdf binary/octet-stream 1 MB Download File

More About This Work

Academic Units
Computer Science
Thesis Advisors
Yang, Junfeng
Degree
Ph.D., Columbia University
Published Here
October 7, 2014
Academic Commons provides global access to research and scholarship produced at Columbia University, Barnard College, Teachers College, Union Theological Seminary and Jewish Theological Seminary. Academic Commons is managed by the Columbia University Libraries.