ECOOP 2015
Sun 5 - Fri 10 July 2015 Prague, Czech Republic
Thu 9 Jul 2015 14:30 - 15:00 at Bohemia - Type Systems Chair(s): Peter Müller

We present a refinement type system for reasoning about asynchronous programs manipulating shared mutable state. Our type system guarantees the absence of races and the preservation of user- specified invariants using a combination of two ideas: refinement types and concurrent separation logic. Our type system allows precise, but automatic, reasoning about programs using two ingredients. First, our types are indexed by sets of resource names and the type system tracks the effect of program execution on individual heap locations and task handles. In particular, it allows making strong updates to the types of heap locations. Second, our types track ownership of shared state across concurrently posted tasks and allow reasoning about ownership trans- fer between tasks using permissions. We demonstrate through several examples that these two ingredients, on top of the framework of liquid types, are powerful enough to reason about correct behavior of practical, complex, asynchronous systems manipulating shared heap resources. We have implemented type inference for our type system and have used it to prove complex invariants of asynchronous OCaml programs. We also show how the type system detects subtle concurrency bugs in a file system implementation.

Thu 9 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

13:30 - 15:00
Type SystemsResearch Track at Bohemia
Chair(s): Peter Müller ETH Zurich
13:30
30m
Talk
Intensional Effect Polymorphism
Research Track
Yuheng Long Iowa State University, Yu David Liu State University of New York (SUNY) Binghamton, Hridesh Rajan Iowa State University
14:00
30m
Talk
Type Inference for Place-Oblivious Objects
Research Track
Riyaz Haque University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles
14:30
30m
Talk
Asynchronous Liquid Separation Types
Research Track
Johannes Kloos MPI-SWS, Rupak Majumdar MPI-SWS, Viktor Vafeiadis MPI-SWS, Germany