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

We report on a machine-checked verification of safety for a state-of-the-art, on-the-fly, concurrent, mark-sweep garbage collector that is designed for multi-core architectures with weak memory consistency. The proof explicitly incorporates the relaxed memory semantics of x86 multiprocessors. To our knowledge, this is the first fully machine-checked proof of safety for such a garbage collector. We couch the proof in a framework that system implementers will find appealing, with the fundamental components of the system specified in a simple and intuitive programming language. The abstract model is detailed enough for its correspondence with an assembly language implementation to be straightforward.

PLDI 2015 Artifact Evaluated Badge

Mon 15 Jun
Times are displayed in time zone: Tijuana, Baja California change

14:00 - 15:40: VerificationResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Zachary TatlockUniversity of Washington, Seattle
14:00 - 14:25
Talk
Mechanized Verification of Fine-grained Concurrent Programs
Research Papers
Ilya SergeyIMDEA Software Institute, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
14:25 - 14:50
Talk
Verification of Producer-Consumer Synchronization in GPU Programs
Research Papers
Rahul SharmaStanford University, Michael BauerNVIDIA Research, Alex AikenStanford University
Media Attached
14:50 - 15:15
Talk
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
Research Papers
Peter GammieNICTA, Tony HoskingAustralian National University, Data61, and Purdue University, Kai EngelhardtUNSW and NICTA
Link to publication Media Attached
15:15 - 15:40
Talk
Verifying Read-Copy-Update in a Logic for Weak Memory
Research Papers
Joseph TassarottiCarnegie Mellon University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached