log in  |  register  |  feedback?  |  help  |  web accessibility
Logo
Program verification under weak memory consistency
Wednesday, January 27, 2016, 11:00 am-12:00 pm Calendar
  • You are subscribed to this talk through .
  • You are watching this talk through .
  • You are subscribed to this talk. (unsubscribe, watch)
  • You are watching this talk. (unwatch, subscribe)
  • You are not subscribed to this talk. (watch, subscribe)
Abstract

Weak memory models formalize the inconsistent behaviors that one can observe in multithreaded programs running on modern hardware. In so doing, they complicate the already-difficult task of reasoning about correctness of concurrent code. Worse, they render impotent most formal methods that have been developed to tame concurrency, which almost universally assume a strong (i.e., sequentially consistent) memory model. In response, we have developed a number of alternative reasoning techniques that are sound for programs running weak memory consistency. I will cover both program logics, such as relaxed separation logic, as well as theorems that allow reducing reasoning about well-structured weakly consistent implementations down to sequential consistency, and show how these can be applied to reason about a practical RCU implementation.

Bio

Viktor Vafeiadis is a tenure-track researcher at MPI-SWS. He got his BA (2004) and PhD (2008) from the University of Cambridge. Before joining MPI-SWS in October 2010, he was a postdoc at Microsoft Research and at the University of Cambridge.

He is broadly interested in programming languages and verification with a focus on program logics for weak memory (RSL, FSL, GPS, OGRA), program logics for interleaving concurrency (RGSep, deny-guarantee, CAP, CSL soundness), compiler verification (C11 compilation, CompCertTSO, Pilsner, SepCompCert), automated verification of concurrent programs (Cave), and interactive theorem proving (Paco, Mtac, adjustable references).

This talk is organized by Mike Hicks