Actris: session-type based reasoning in separation logic

Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

Abstract

Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however,
it is often combined with other programming and concurrency paradigms, such as higher-order functions,
mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional
correctness of programs that use a combination of the aforementioned features. Actris combines the power
of modern concurrent separation logics with a first-class protocol mechanism—based on session types—for
reasoning about message passing in the presence of other concurrency paradigms. We show that Actris
provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a
distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using
relatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in the
Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs,
as well as all examples in the paper, in the Coq proof assistant
Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
EditorsPhilip Wadler
Number of pages30
Volume4
PublisherAssociation for Computing Machinery
Publication date2020
Pages6:1
Article number6
DOIs
Publication statusPublished - 2020

Keywords

  • message passing
  • concurrent programming
  • separation logics
  • session types
  • functional correctness

Fingerprint

Dive into the research topics of 'Actris: session-type based reasoning in separation logic'. Together they form a unique fingerprint.

Cite this