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.2017.25
URN: urn:nbn:de:0030-drops-72541
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7254/
Go to the corresponding LIPIcs Volume Portal

Stiévenart, Quentin ; Nicolay, Jens ; De Meuter, Wolfgang ; De Roover, Coen

Mailbox Abstractions for Static Analysis of Actor Programs

pdf-format:
LIPIcs-ECOOP-2017-25.pdf (0.7 MB)

Abstract

Properties such as the absence of errors or bounds on mailbox sizes are hard to deduce statically for actor-based programs.
This is because actor-based programs exhibit several sources of unboundedness, in addition to the non-determinism that is inherent to the concurrent execution of actors.
We developed a static technique based on abstract interpretation to soundly reason in a finite amount of time about the possible executions of an actor-based program.
We use our technique to statically verify the absence of errors in actor-based programs, and to compute upper bounds on the actors' mailboxes.
Sound abstraction of these mailboxes is crucial to the precision of any such technique.
We provide several mailbox abstractions and categorize them according to the extent to which they preserve message ordering and multiplicity of messages in a mailbox.
We formally prove the soundness of each mailbox abstraction, and empirically evaluate their precision and performance trade-offs on a corpus of benchmark programs.
The results show that our technique can statically verify the absence of errors for more benchmark programs than the state-of-the-art analysis.

BibTeX - Entry

@InProceedings{stivenart_et_al:LIPIcs:2017:7254,
  author =	{Quentin Sti{\'e}venart and Jens Nicolay and Wolfgang De Meuter and Coen De Roover},
  title =	{{Mailbox Abstractions for Static Analysis of Actor Programs}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{25:1--25:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{Peter M{\"u}ller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7254},
  URN =		{urn:nbn:de:0030-drops-72541},
  doi =		{10.4230/LIPIcs.ECOOP.2017.25},
  annote =	{Keywords: static analysis, abstraction, abstract interpretation, actors, mailbox}
}

Keywords: static analysis, abstraction, abstract interpretation, actors, mailbox
Collection: 31st European Conference on Object-Oriented Programming (ECOOP 2017)
Issue Date: 2017
Date of publication: 16.06.2017

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