Differences

This shows you the differences between two versions of the page.

Link to this comparison view

— 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.