Mon 15 Jun 2015 14:00 - 14:25 at PLDI Main BLUE (Portland 254-255) - Verification Chair(s): Zachary Tatlock

Efficient concurrent programs and data structures rarely employ coarse-grained synchronization mechanisms (i.e., locks); instead, they implement custom synchronization patterns via fine-grained primitives, such as compare-and-swap. Due to sophisticated interference scenarios between threads, reasoning about such programs is challenging and error-prone, and can benefit from mechanization.

In this paper, we present the first completely formalized framework for mechanized verification of full functional correctness of fine-grained concurrent programs. Our tool is based on the recently proposed program logic FCSL. It is implemented as an embedded DSL in the dependently-typed language of the Coq proof assistant, and is powerful enough to reason about programming features such as higher-order functions and local thread spawning. By incorporating a uniform concurrency model, based on state-transition systems and partial commutative monoids, FCSL makes it possible to build proofs about concurrent libraries in a thread-local, compositional way, thus facilitating scalability and reuse: libraries are verified just once, and their specifications are used ubiquitously in client-side reasoning. We illustrate the proof layout in FCSL by example, outline its infrastructure, and report on our experience of using FCSL to verify a number of concurrent algorithms and data structures.

PLDI 2015 Artifact Evaluated Badge

Mon 15 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:40
VerificationResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Zachary Tatlock University of Washington, Seattle
14:00
25m
Talk
Mechanized Verification of Fine-grained Concurrent Programs
Research Papers
Ilya Sergey IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute
Link to publication Media Attached
14:25
25m
Talk
Verification of Producer-Consumer Synchronization in GPU Programs
Research Papers
Rahul Sharma Stanford University, Michael Bauer NVIDIA Research, Alex Aiken Stanford University
Media Attached
14:50
25m
Talk
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Research Papers
Peter Gammie NICTA, Tony Hosking Australian National University, Data61, and Purdue University, Kai Engelhardt UNSW and NICTA
Link to publication Media Attached
15:15
25m
Talk
Verifying Read-Copy-Update in a Logic for Weak Memory
Research Papers
Joseph Tassarotti Carnegie Mellon University, Derek Dreyer MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany
Media Attached