Types for progress in actor programs

Minas Charalambides, Karl Palmskog, Gul Agha

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Properties in the actor model can be described in terms of the message-passing behavior of actors. In this paper, we address the problem of using a type system to capture liveness properties of actor programs. Specifically, we define a simple actor language in which demands for certain types of messages may be generated during execution, in a manner specified by the programmer. For example, we may want to require that each request to an actor eventually results in a reply. The difficulty lies in that such requests can be generated dynamically, alongside the associated requirements for replies. Such replies might be sent in response to intermediate messages that never arrive, but the property may also not hold for more trivial reasons; for instance, when the code of potential senders of the reply omit the required sending command in some branches of a conditional statement. We show that, for a restricted class of actor programs, a system that tracks typestates can statically guarantee that such dynamically generated requirements will eventually be satisfied.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer-Verlag Berlin Heidelberg
Pages315-339
Number of pages25
DOIs
StatePublished - Jan 1 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11665 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Actors
  • Concurrency
  • Liveness
  • Typestate

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Types for progress in actor programs'. Together they form a unique fingerprint.

  • Cite this

    Charalambides, M., Palmskog, K., & Agha, G. (2019). Types for progress in actor programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 315-339). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11665 LNCS). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-030-21485-2_18