Files in this item



application/pdfmain.pdf (297kB)
The article PDF.PDF


Title:Types for Progress in Actor Programs
Author(s):Charalambides, Minas; Palmskog, Karl; Agha, Gul
Subject(s):actors, concurrency, types, progress, liveness
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.
Issue Date:2017-09-18
Citation Info:Minas Charalambides, Karl Palmskog and Gul Agha: Types for Progress in Actor Programs. Workshop on Actors and Active Objects, IFM 2017 satellite event, September 18th, 2017, TORINO, ITALY.
Rights Information:Copyright 2017 Minas Charalambides, Karl Palmskog, Gul Agha
Creative Commons Attribution ShareAlike 4.0 International license (CC BY-SA 4.0)
Date Available in IDEALS:2019-05-09

This item appears in the following Collection(s)

Item Statistics