Differences
This shows you the differences between two versions of the page.
seminars:seminar_3_1_16 [2017/09/21 02:02] |
seminars:seminar_3_1_16 [2017/09/21 02:02] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Stateless model checking with data-race preemption points ====== | ||
+ | |||
+ | Tuesday March 1, 2016\\ | ||
+ | Location: CIC Panther Hollow Room\\ | ||
+ | Time: 4:30PM\\ | ||
+ | |||
+ | |||
+ | {{:seminars:benb.jpg?256|}}\\ | ||
+ | |||
+ | **[[http://www.pdl.cmu.edu/People/blum.shtml|Ben Blum (Carnegie Mellon University)]]**\\ | ||
+ | |||
+ | |||
+ | |||
+ | ===== 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. Several reduction techniques can | ||
+ | mitigate this explosion, but even after pruning equivalent | ||
+ | interleavings, the state space size is often intractable. Most prior | ||
+ | tools are limited to preempting only on synchronization APIs, which | ||
+ | reduces the space further, but can miss unsynchronized thread | ||
+ | communication bugs. 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 is prone to | ||
+ | false positives: spurious reports of access pairs that cannot be | ||
+ | reordered to produce a bug. | ||
+ | |||
+ | In this talk I will discuss Quicksand, a new technique and tool I have | ||
+ | built to manage the exploration of many state spaces using different | ||
+ | preemption points. It uses state space estimation to prioritize jobs | ||
+ | most likely to complete in a fixed CPU budget, and it incorporates | ||
+ | data-race analysis to add new preemption points on the fly. Preempting | ||
+ | threads during a data race's instructions can automatically classify the | ||
+ | race as buggy or benign, and uncovers new bugs not reachable by prior | ||
+ | model checkers. In our evaluation, Quicksand found 1.8x as many bugs | ||
+ | compared to stateless model checking without data-race preemption | ||
+ | points. | ||
+ | |||
+ | I am planning to submit this research for OOPSLA's March 25th deadline, | ||
+ | so any feedback from people experienced in either the research topic or | ||
+ | the conference would be much appreciated. | ||
+ | |||
+ | ===== Bio ===== | ||
+ | Ben Blum is a 5th year Ph.D. student in the Parallel Data Lab under the advisorship of Garth Gibson. | ||