[Pl-seminar] 1/14 Seminar: Viktor Vafeiadis, Program verification under weak memory consistency

[William J. Bowman]

NUPRL Seminar presents

Viktor Vafeiadis
Max Planck Institute for Software Systems

13:30--15:00
Thursday, Jan. 14, 2016
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
Host: Amal Ahmed


Program verification under weak memory consistency

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 received 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 interested in programming languages and verification with a
focus program logics for weak memory, program logics for concurrency,
compiler verifications, automated verification of concurrent programs,
and interactive theorem proving.

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20160108/c776a1a3/attachment.pgp>