License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2015.396
URN: urn:nbn:de:0030-drops-52233
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5223/
Go to the corresponding LIPIcs Volume Portal

Kloos, Johannes ; Majumdar, Rupak ; Vafeiadis, Viktor

Asynchronous Liquid Separation Types

pdf-format:
13.pdf (0.6 MB)

Abstract

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 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 transfer 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.

BibTeX - Entry

@InProceedings{kloos_et_al:LIPIcs:2015:5223,
  author =	{Johannes Kloos and Rupak Majumdar and Viktor Vafeiadis},
  title =	{{Asynchronous Liquid Separation Types}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{396--420},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{John Tang Boyland},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5223},
  URN =		{urn:nbn:de:0030-drops-52233},
  doi =		{10.4230/LIPIcs.ECOOP.2015.396},
  annote =	{Keywords: Liquid Types, Asynchronous Parallelism, Separation Logic, Type Systems}
}

Keywords: Liquid Types, Asynchronous Parallelism, Separation Logic, Type Systems
Collection: 29th European Conference on Object-Oriented Programming (ECOOP 2015)
Issue Date: 2015
Date of publication: 29.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI