Mon 15 Jun 2015 14:50 - 15:15 at PLDI Main RED (Portland 256) - Correctness Chair(s): Jens Palsberg

Reproducing concurrency bugs is a prominent challenge. Existing techniques either rely on recording very fine grained execution information and hence have high runtime overhead, or strive to log as little information as possible but provide no guarantee in reproducing a bug. We present Light, a technique that features much lower overhead compared to techniques based on fine grained recording, and that guarantees to reproduce concurrent bugs. We leverage and formally prove that recording flow dependencies is the necessary and sufficient condition to reproduce a concurrent bug. The flow dependencies, together with the thread local orders that can be automatically inferred (and hence not logged), are encoded as scheduling constraints. An SMT solver is used to derive a replay schedule, which is guaranteed to exist even though it may be different from the original schedule. Our experiments show that Light has only 44% logging overhead, almost one order of magnitude lower than the state of the art techniques relying on logging memory accesses. Its space overhead is only 10% of those techniques. Light can also reproduce all the bugs we have collected whereas existing techniques miss some of them.

Mon 15 Jun

pldi2015-papers
14:00 - 15:40: Research Papers - Correctness at PLDI Main RED (Portland 256)
Chair(s): Jens PalsbergUniversity of California, Los Angeles
pldi2015-papers14:00 - 14:25
Talk
Maarten FaddegonUniversity of Kent, UK, Olaf ChitilUniversity of Kent, UK
Media Attached
pldi2015-papers14:25 - 14:50
Talk
Media Attached
pldi2015-papers14:50 - 15:15
Talk
Peng LiuPurdue University, Xiangyu ZhangPurdue University, Omer TrippIBM Thomas J. Watson Research Center, Yunhui ZhengIBM T.J. Watson Research Center
Media Attached
pldi2015-papers15:15 - 15:40
Talk
Nathan ChongUniversity College London, Alastair DonaldsonImperial College London, Andrei LascuImperial College London, Christopher LidburyImperial College London
Media Attached