SPLASH 2014
Mon 20 - Fri 24 October 2014 Portland, Oregon, United States
Fri 24 Oct 2014 11:15 - 11:37 at Salon E - Specification and Verification Chair(s): Gary Leavens

Weak memory models formalize the inconsistent behaviors that one can expect to observe in multithreaded programs running on modern hardware. In so doing, however, they complicate the already-difficult task of reasoning about correctness of concurrent code. Worse, they render impotent the sophisticated formal methods that have been developed to tame concurrency, which almost universally assume a strong (i.e. sequentially consistent) memory model.

This paper introduces GPS, the first program logic to provide a full-fledged suite of modern verification techniques—including ghost state, protocols, and separation logic—for high-level, structured reasoning about weak memory. We demonstrate the effectiveness of GPS by applying it to challenging examples drawn from the Linux kernel as well as lock-free data structures. We also define the semantics of GPS and prove in Coq that it is sound with respect to the axiomatic C11 weak memory model.

Fri 24 Oct

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Specification and VerificationOOPSLA at Salon E
Chair(s): Gary Leavens University of Central Florida
10:30
22m
Talk
Bounded Exhaustive Test Input Generation from Hybrid Invariants
OOPSLA
Nicolás Rosner Dept. of Computer Science FCEyN, University of Buenos Aires, Valeria Bengolea Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Pablo Ponzio Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Shadi Abdul Khalek Google, Nazareno Aguirre Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires, Sarfraz Khurshid University of Texas at Austin
Link to publication
10:52
22m
Talk
Compiler Verification Meets Cross-Language Linking via Data Abstraction
OOPSLA
Peng Wang MIT CSAIL, Santiago Cuellar Princeton, Adam Chlipala MIT
Link to publication
11:15
22m
Talk
GPS: Navigating Weak Memory with Ghosts, Protocols, and Separation
OOPSLA
Aaron Turon MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany, Derek Dreyer MPI-SWS
Link to publication
11:37
22m
Talk
Natural Proofs for Asynchronous Programs using Almost-Synchronous Invariants
OOPSLA
Ankush Desai University of California, Berkeley, Pranav Garg University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign
Link to publication