Wed 28 Oct 2015 11:37 - 12:00 at Grand Station 1 - 1. Model Checking Chair(s): Julian Dolby

Modern event-driven applications, such as, web pages and mobile apps, rely on asynchrony to ensure smooth end-user experience. Unfortunately, even though these applications are executed by a single event-loop thread, they can still exhibit nondeterministic behaviors depending on the execution order of interfering asynchronous events. As in classic shared-memory concurrency, this nondeterminism makes it challenging to discover errors that manifest only in specific schedules of events. In this work we propose the first stateless model checker for event-driven applications, called R4. Our algorithm systematically explores the nondeterminism in the application and concisely exposes its overall effect, which is useful for bug discovery. The algorithm builds on a combination of three key insights: (i) a dynamic partial order reduction (DPOR) technique for reducing the search space, tailored to the domain of event-driven applications, (ii) conflict-reversal bounding based on a hypothesis that most errors occur with a small number of event reorderings, and (iii) approximate replay of event sequences, which is critical for separating harmless from harmful nondeterminism. We instantiate R4 for the domain of client-side web applications and use it to analyze event interference in a number of real-world programs. The experimental results indicate that the precision and overall exploration capabilities of our system significantly exceed that of existing techniques.

Wed 28 Oct

oopsla2015
10:30 - 12:00: OOPSLA - 1. Model Checking at Grand Station 1
Chair(s): Julian DolbyIBM Research
oopsla201510:30 - 10:52
Talk
Anthony Widjaja LinYale-NUS College, Singapore, Matthew HagueRoyal Holloway University of London, UK, C.-H. Luke OngUniversity of Oxford, UK
Link to publication
oopsla201510:52 - 11:15
Talk
Brian DemskyUniversity of California at Irvine, USA, Patrick LamUniversity of Waterloo, Canada
Link to publication
oopsla201511:15 - 11:37
Talk
Ivan KurajMassachusetts Institute of Technology, USA, Viktor KunčakEPFL, Switzerland, Daniel JacksonMassachusetts Institute of Technology, USA
DOI
oopsla201511:37 - 12:00
Talk
Casper Svenning JensenAarhus University, Denmark, Anders MøllerAarhus University, Veselin RaychevETH Zurich, Switzerland, Dimitar DimitrovETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
DOI