Stateless Model Checking with Data-Race Preemption Points (Systems Seminar by Ben Blum, CMU)
Event details
| Date | 07.11.2016 |
| Hour | 14:15 › 15:00 |
| Speaker | Ben Blum, CMU |
| Location | |
| Category | Conferences - Seminars |
Abstract: Stateless model checking is a powerful technique for testing concurrent programs, but suffers from exponential state space explosion when the test input parameters are too large. Data race detection, another concurrency testing approach, focuses on suspicious memory access pairs during a single test execution. It avoids concerns of state space size, but may report races that do not lead to observable failures, which jeopardizes a user’s willingness to use the analysis.
Quicksand is a new stateless model checking framework which manages the exploration of many state spaces using different preemption points. It uses state space estimation to prioritize jobs dynamically, and incorporates data-race analysis to add new preemption points on the fly. Preempting during racy instructions can automatically classify the race as buggy or benign, and also enables full verification of all possible schedules when completion is possible within the CPU budget. In our evaluation, Quicksand found 1.25x as many bugs and verified 4.3x as many tests compared to prior model checking approaches.
Bio: Ben Blum is a graduate student in the Computer Science Department at Carnegie Mellon (CMU), advised by Garth Gibson. Before starting his PhD, he worked on Landslide, a tool to systematically test software under all possible thread interleavings.
Coffee will be available 15 minutes before the talk.
Quicksand is a new stateless model checking framework which manages the exploration of many state spaces using different preemption points. It uses state space estimation to prioritize jobs dynamically, and incorporates data-race analysis to add new preemption points on the fly. Preempting during racy instructions can automatically classify the race as buggy or benign, and also enables full verification of all possible schedules when completion is possible within the CPU budget. In our evaluation, Quicksand found 1.25x as many bugs and verified 4.3x as many tests compared to prior model checking approaches.
Bio: Ben Blum is a graduate student in the Computer Science Department at Carnegie Mellon (CMU), advised by Garth Gibson. Before starting his PhD, he worked on Landslide, a tool to systematically test software under all possible thread interleavings.
Coffee will be available 15 minutes before the talk.
Practical information
- Informed public
- Free
Contact
- Jonas Wagner