Types for progress in actor programs

Minas Charalambides, Karl Palmskog, Gul A 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
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

Fingerprint

Message passing
Liveness
Requirements
Message Passing
Type Systems
Actors
Trivial
Branch

Keywords

  • Actors
  • Concurrency
  • Liveness
  • Typestate

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Charalambides, M., Palmskog, K., & Agha, G. A. (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. https://doi.org/10.1007/978-3-030-21485-2_18

Types for progress in actor programs. / Charalambides, Minas; Palmskog, Karl; Agha, Gul A.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag, 2019. p. 315-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11665 LNCS).

Research output: Chapter in Book/Report/Conference proceedingChapter

Charalambides, M, Palmskog, K & Agha, GA 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). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11665 LNCS, Springer-Verlag, pp. 315-339. https://doi.org/10.1007/978-3-030-21485-2_18
Charalambides M, Palmskog K, Agha GA. Types for progress in actor programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag. 2019. p. 315-339. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-21485-2_18
Charalambides, Minas ; Palmskog, Karl ; Agha, Gul A. / Types for progress in actor programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag, 2019. pp. 315-339 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{f96a8e97440349409987122b76143f11,
title = "Types for progress in actor programs",
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.",
keywords = "Actors, Concurrency, Liveness, Typestate",
author = "Minas Charalambides and Karl Palmskog and Agha, {Gul A}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-21485-2_18",
language = "English (US)",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "315--339",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Types for progress in actor programs

AU - Charalambides, Minas

AU - Palmskog, Karl

AU - Agha, Gul A

PY - 2019/1/1

Y1 - 2019/1/1

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

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

KW - Actors

KW - Concurrency

KW - Liveness

KW - Typestate

UR - http://www.scopus.com/inward/record.url?scp=85068876528&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85068876528&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-21485-2_18

DO - 10.1007/978-3-030-21485-2_18

M3 - Chapter

AN - SCOPUS:85068876528

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 315

EP - 339

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer-Verlag

ER -