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

oopsla2014
10:30 - 12:00: OOPSLA - Specification and Verification at Salon E
Chair(s): Gary Leavens University of Central Florida
oopsla2014141413940000010:30 - 10:52
Talk
Nicolás RosnerDept. of Computer Science FCEyN, University of Buenos Aires, Valeria BengoleaDept. of Computer Science FCEFQyN, University of Rio Cuarto, Pablo PonzioDept. of Computer Science FCEFQyN, University of Rio Cuarto, Shadi Abdul KhalekGoogle, Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. of Software Engineering Instituto Tecnológico de Buenos Aires, Sarfraz KhurshidUniversity of Texas at Austin
Link to publication
oopsla2014141414075000010:52 - 11:15
Talk
Link to publication
oopsla2014141414210000011:15 - 11:37
Talk
Aaron TuronMPI-SWS, Viktor VafeiadisMPI-SWS, Germany, Derek DreyerMPI-SWS
Link to publication
oopsla2014141414345000011:37 - 12:00
Talk
Ankush DesaiUniversity of California, Berkeley, Pranav GargUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign
Link to publication