Document Open Access Logo

Asynchronous Liquid Separation Types

Authors Johannes Kloos, Rupak Majumdar, Viktor Vafeiadis

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2015.396.pdf
  • Filesize: 0.64 MB
  • 25 pages

Document Identifiers

Author Details

Johannes Kloos
Rupak Majumdar
Viktor Vafeiadis

Cite As Get BibTex

Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous Liquid Separation Types. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 396-420, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.ECOOP.2015.396

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.

Subject Classification

Keywords
  • Liquid Types
  • Asynchronous Parallelism
  • Separation Logic
  • Type Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Lennart Augustsson. Cayenne - a language with dependent types. In Advanced Functional Programming, pages 240-267. Springer, 1999. Google Scholar
  2. Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, pages 115-137, 2005. Google Scholar
  3. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26, 2011. Google Scholar
  4. Karl Crary, David Walker, and J. Gregory Morrisett. Typed memory management in a calculus of capabilities. In POPL 1999, pages 262-275, 1999. Google Scholar
  5. Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In TACAS 2006, pages 287-302, 2006. Google Scholar
  6. Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. In ESOP 2009, pages 363-377, 2009. Google Scholar
  7. Tim Freeman and Frank Pfenning. Refinement types for ML. In PLDI 1991, pages 268-277, 1991. Google Scholar
  8. The Go programming language. URL: http://golang.org/.
  9. Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In APLAS 2007, pages 19-37, 2007. Google Scholar
  10. Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. In ESOP 2008, pages 353-367, 2008. Google Scholar
  11. Bart Jacobs, Jan Smans, and Frank Piessens. A quick tour of the VeriFast program verifier. In APLAS 2010, pages 304-311, 2010. Google Scholar
  12. R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL, pages 339-350, 2007. Google Scholar
  13. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV 2010, 2010. Google Scholar
  14. Johannes Kloos, Rupak Majumdar, and Viktor Vafeiadis. Asynchronous liquid separation types. http://plv.mpi-sws.org/ALStypes/. Full version.
  15. Barbara Liskov and Liuba Shrira. Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. In PLDI 1988, pages 260-267, 1988. Google Scholar
  16. Anil Madhavapeddy and David J. Scott. Unikernels: the rise of the virtual library operating system. Commun. ACM, 57(1):61-69, 2014. Google Scholar
  17. Y. Mandelbaum, D. Walker, and R. Harper. An effective theory of type refinements. In ICFP 2003, pages 213-225, 2003. Google Scholar
  18. Nick Mathewson. Fast portable non-blocking network programming with Libevent. URL: http://www.wangafu.net/~nickm/libevent-book/.
  19. The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2012. Version 8.4. Google Scholar
  20. Yaron Minsky, Anil Madhavapeddy, and Hickey Jason. Real-World OCaml. O'Reilly Media, 2013. Google Scholar
  21. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  22. Peter W. O'Hearn. Resources, concurrency, and local reasoning. Theor. Comput. Sci., 375(1-3):271-307, 2007. Google Scholar
  23. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  24. François Pottier and Jonathan Protzenko. Programming with permissions in Mezzo. In ICFP 2013, pages 173-184. ACM, 2013. Google Scholar
  25. Jonathan Protzenko. Introduction to Mezzo. Series of two blog posts, starting at http://gallium.inria.fr/blog/introduction-to-mezzo, Jan 2013.
  26. Veselin Raychev, Martin T. Vechev, and Manu Sridharan. Effective race detection for event-driven programs. In OOPSLA 2013, pages 151-166, 2013. Google Scholar
  27. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS 2002, pages 55-74, 2002. Google Scholar
  28. Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. Liquid types. In PLDI 2008, 2008. Google Scholar
  29. P.M. Rondon, M. Kawaguchi, and R. Jhala. Low-level liquid types. In POPL 2010, 2010. Google Scholar
  30. The Rust programming language. URL: http://www.rust-lang.org/.
  31. Koushik Sen and Mahesh Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV, LNCS 4144, pages 300-314. Springer, 2006. Google Scholar
  32. Frederick Smith, David Walker, and J. Gregory Morrisett. Alias types. In ESOP 2000, pages 366-381, 2000. Google Scholar
  33. Jérôme Vouillon. Lwt: a cooperative thread library. In ML 2008, pages 3-12, 2008. Google Scholar
  34. SatX10: A scalable plug & play parallel solver. URL: http://x10-lang.org/component/content/article/37-community/applications/207-satx10.html.
  35. H. Xi. Imperative programming with dependent types. In LICS 2000, 2000. Google Scholar
  36. H. Xi. Dependent ML: An approach to practical programming with dependent types. J. Funct. Program., 17(2):215-286, 2007. Google Scholar
  37. H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In PLDI 1998, pages 249-257, 1998. Google Scholar
  38. H. Xi and F. Pfenning. Dependent types in practical programming. In POPL 1999, 1999. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact