Write a Blog >>
Tue 20 Jun 2017 15:15 - 15:40 at Actes, Civil Engineering - Parallelization and Concurrency Chair(s): Milind Kulkarni

Verifying invariants of fine-grained concurrent data structures is challenging because interference from other threads may occur at any time. We propose a new way of proving invariants of fine-grained concurrent data structures: applying rely-guarantee reasoning to references in the concurrent setting. Rely-guarantee applied to references can verify bounds on thread interference, without requiring a whole program to be verified. This paper provides three new results. First, it provides a new approach to preserving invariants and restricting usage of concurrent data structures. Our approach targets a space between simple type systems and modern concurrent program logics, offering an intermediate point between unverified code and full verification. Furthermore, it avoids sealing concurrent data structure implementations, and can interact safely with unverified imperative code. Second, we demonstrate the approach’s broad applicability through a series of case studies, using two implementations: an axiomatic COQ DSL and a library for Liquid Haskell. Third, these two implementations allow us to compare and contrast verifications by interactive proof (COQ) and a weaker form that can be expressed using SMT-discharged dependent refinement types (Liquid Haskell).

Tue 20 Jun
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:40: Parallelization and ConcurrencyPLDI Research Papers at Actes, Civil Engineering
Chair(s): Milind KulkarniPurdue University
14:00 - 14:25
Talk
Synthesis of Divide and Conquer Parallelism for Loops
PLDI Research Papers
Azadeh FarzanUniversity of Toronto, Victor NicoletUniversity of Toronto
Media Attached
14:25 - 14:50
Talk
Futhark: Purely Functional GPU-programming with Nested Parallelism and In-place Array Updates
PLDI Research Papers
Troels HenriksenDIKU, University of Copenhagen, Niels G. W. SerupDIKU, University of Copenhagen, Martin ElsmanDepartment of Computer Science, University of Copenhagen, Fritz HengleinDIKU, Denmark, Cosmin OanceaDIKU, University of Copenhagen
Media Attached
14:50 - 15:15
Talk
Gradual Synthesis for Static Parallelization
PLDI Research Papers
Grigory FedyukovichUW CSE, Maaz Bin Safeer AhmadUW / CSE, Rastislav BodikUniversity of Washington
Pre-print Media Attached
15:15 - 15:40
Talk
Verifying invariants of lock-free data structures with rely-guarantee and refinement type
PLDI Research Papers
Colin GordonDrexel University, Michael D. ErnstUniversity of Washington, USA, Dan GrossmanUniversity of Washington, Matthew ParkinsonMicrosoft Research, UK
Pre-print Media Attached