Towards an Empirical Study of Affine Types for Isolated Actors in Scala

TL;DR

This paper explores integrating LaCasa's affine type system with Scala's Akka actors to ensure actor isolation, aiming to improve security and data-race freedom, supported by an empirical study on real-world systems.

Contribution

It introduces a novel integration of LaCasa's type system with Akka actors and provides empirical evidence of its practical effort in existing applications.

Findings

LaCasa integration can be applied to real-world Akka systems.

Using LaCasa requires manageable effort for developers.

The approach enhances actor isolation and security.

Abstract

LaCasa is a type system and programming model to enforce the object capability discipline in Scala, and to provide affine types. One important application of LaCasa's type system is software isolation of concurrent processes. Isolation is important for several reasons including security and data-race freedom. Moreover, LaCasa's affine references enable efficient, by-reference message passing while guaranteeing a "deep-copy" semantics. This deep-copy semantics enables programmers to seamlessly port concurrent programs running on a single machine to distributed programs running on large-scale clusters of machines. This paper presents an integration of LaCasa with actors in Scala, specifically, the Akka actor-based middleware, one of the most widely-used actor systems in industry. The goal of this integration is to statically ensure the isolation of Akka actors. Importantly, we present the results of an empirical study investigating the effort required to use LaCasa's type system in existing open-source Akka-based systems and applications.

Tables

Table 1. Table 1: Results of the empirical study.

Program	LOC (Scala/Akka)	LOC (LaCasa/Akka)	Changes	Changes (%)
ThreadRing	130	153	27 add./10 del.	28.5%
Chameneos	143	165	26 add./7 del.	23.1%
Banking	118	135	27 add./12 del.	33.1%
Average	130	151		28.2%

Full text

This paper presents an integration of LaCasa with actors in Scala, specifically, the Akka actor-based middleware, one of the most widely-used actor systems in industry. The goal of this integration is to statically ensure the isolation of Akka actors. Importantly, we present the results of an empirical study investigating the effort required to use LaCasa’s type system in existing open-source Akka-based systems and applications.

1 Introduction

The desire for languages to catch more errors at compile time seems to have increased in the last couple of years. Recent languages, like Rust [16], show that a language does not have to sacrifice a lot, if any, convenience to gain access to safer workable environments. Entire classes of memory-related bugs can be eliminated, statically, through the use of affine types. In the context of this paper it is important that affine types can also enforce isolation of concurrent processes.

LaCasa [6] shows that affine types do not necessarily need to be constrained to new languages: it introduces affine types for Scala, an existing, widely-used language. LaCasa is implemented as a compiler plugin for Scala 2.11.111See https://github.com/phaller/lacasa However, so far it has been unclear how big the effort is to apply LaCasa in practice. This paper is a first step to investigate this question empirically on open-source Scala programs using the Akka actor framework [9].

Contributions

This paper presents an integration of LaCasa and Akka. Thus, our integration enforces isolation for an existing actor library. Furthermore, we present the results of an empirical study evaluating the effort to use isolation types in real applications. To our knowledge it is the first empirical study evaluating isolation types for actors in a widely-used language.

Selected Related Work

Active ownership [4] is a minimal variant of ownership types providing race freedom for active objects while enabling by-reference data transfer between active objects. The system is realized as an extended subset of Java. Kilim [15] combines static analysis and type checking to provide isolated actors in Java. For neither of the two above systems, active ownership and Kilim, have the authors reported any empirical results on the syntactic overhead of the respective systems, unlike the present paper. SOTER [13] is a static analysis tool which infers if the content of a message is compatible with an ownership transfer semantics. This approach is complementary to a type system which enables developers to require ownership transfer semantics. Pony [5] and Rust [16] are new language designs with type systems to ensure data-race freedom in the presence of zero-copy transfer between actors/concurrent processes. It is unclear how to obtain empirical results on the syntactic overhead of the type systems of Pony or Rust. In contrast, LaCasa extends an existing, widely-used language, enabling empirical studies.

2 Background

In this paper we study affine types as provided by LaCasa [6], an extension of the Scala programming language. LaCasa is implemented as a combination of a compiler plugin for the Scala 2.11.x compiler and a small runtime library. LaCasa provides affine references which may be consumed at most once. In LaCasa an affine reference to a value of type T has type Box[T]. The name of type constructor Box indicates that access to an affine reference is restricted. Accessing the wrapped value of type T requires the use of a special open construct:

⬇

1 val box: Box[T] = ...

2 box open { x => / use ‘x‘ / }

open is implemented as a method which takes the closure { x => /* use ‘x‘ */ } as an argument. The closure body then provides access to the object x wrapped by the box of type Box[T]. However, LaCasa restricts the environment (*i.e., *the captured variables) of the argument closure in order to ensure affinity: mutable variables may not be captured. Without this restriction it would be simple to duplicate the wrapped value, violating affinity:

⬇

1 val box: Box[T] = ...

2 var leaked: Option[T] = None

3 box open { x =>

4 leaked = Some(x) // illegal

5 }

6 val copy: T = leaked.get

LaCasa also protects against leaking wrapped values to global state:

⬇

1 object Global { var cnt: LeakyCounter = null }

2 class LeakyCounter {

3 var state: Int = 0

4 def increment(): Unit = { state += 1 }

5 def leak(): Unit = { Global.cnt = this }

6 ...

7 }

8 val box: Box[LeakyCounter] = ... // illegal

9 box open { cnt =>

10 cnt.leak()

11 }

12 val copy: LeakyCounter = Global.cnt

The above LeakyCounter class is illegal to be wrapped in a box. The reason is that even without capturing a mutable variable within open, it is possible to create a copy of the counter, because the leak method leaks a reference to the counter to global mutable state (the Global singleton object). To prevent this kind of affinity violation, LaCasa restricts the creation of boxes of type Box[A] to types A which conform to the object capability discipline [12]. According to the object capability discipline, a method m may only use object references that have been passed explicitly to m, or this. Concretely, accessing Global on line 5 is illegal, since Global was not passed explicitly to method leak.

In previous work [6] we have formalized the object capability discipline as a type system and we have shown that in combination with LaCasa’s type system, affinity of box-typed references is ensured.

Affine references, *i.e., *references of type Box[T], may be consumed, causing them to become unaccessible. Consumption is expressed using permissions which control access to box-typed references. Consuming an affine reference consumes its corresponding permission.

Ensuring at-most-once consumption of affine references thus requires each permission to be linked to a specific box, and this link must be checked statically. In LaCasa permissions are linked to boxes using path-dependent types [3]. For example, Figure 1 shows a method m which has two formal parameters: a box b and a permission p (its implicit modifier may be ignored for now). The type CanAccess of permissions has a type member C which is used to establish a static link to box b by requiring the equality type C = b.C to hold. The type b.C is a path-dependent type with the property that there is only a single runtime object, namely b, whose type member C is equal to type b.C. In order to prevent forging permissions, permissions are only created when creating boxes; it is impossible to create permissions for existing boxes.

Since permissions may be consumed (as shown below), it is important that opening a box requires its permission to be available. Figure 2 shows how this is ensured using an implicit parameter [14] of the open method (line 5). Note that the shown type signature is simplified; the actual signature uses a spore type [11] instead of a function type on line 4 to ensure that the types of captured variables are immutable.

Consuming Permissions

Permissions in LaCasa are just Scala implicit values. This means their availability is flow-insensitive. Therefore, changing the set of available permissions requires changing scope. In LaCasa, calling a permission-consuming method requires passing an explicit continuation closure. The LaCasa type checker enforces that the consumed permission is then no longer available in the scope of this continuation closure. Figure 3 shows an example. LaCasa enforces that such continuation-passing methods do not return (see [6]), indicated by Scala’s bottom type, Nothing.

2.1 Akka

Akka [9] is an implementation of the actor model [7, 2] for Scala. Actors are concurrent processes communicating via asynchronous messages. Each actor buffers received messages in a local “mailbox” – a queue of incoming messages. An Akka actor processes at most one incoming message at a time. Figure 4 shows the definition of an actor’s behavior in Akka. The behavior of each actor is defined by a subclass of a predefined Actor trait. The ExampleActor subclass implements the receive method which is abstract in trait Actor. The receive method returns a message handler defined as a block of pattern-matching cases. This message handler is used to process each message in the actor’s mailbox. The Actor subclass is then used to create a new actor as follows:

⬇

1 val ref: ActorRef = system.actorOf(Props[ExampleActor], "example-actor")

2 ref ! msg

The result of creating a new actor is a reference object (ref) of type ActorRef. An ActorRef is a handle that can be used to send asynchronous messages to the actor using the ! operator (line 2).

3 Integrating LaCasa and Akka

The Adapter

The LaCasa-Akka adapter222See https://github.com/fsommar/lacasa/tree/akka is an extension on top of Akka. During its design, an important constraint was to keep it separate from Akka’s internals – primarily to limit the effect of internal changes as Akka evolves.

The adapter consists of two parts: SafeActor[T] and SafeActorRef[T], both with the same responsibilities as their counterparts in the Akka API. However, note that in contrast to the latter, they are generic over the message type. Akka instead relies on pattern matching to discern the types of received messages (see Section 2.1). For the LaCasa-Akka adapter, however, it is necessary to know the types of messages at compile time, to prevent the exchange of unsafe message types.

SafeActor

A subclass of Akka’s Actor, SafeActor provides a different receive method signature, which is the primary difference between the two. Instead of receiving an untyped message, of type Any, SafeActor[T] receives a boxed message of type T, and an access permission for the contents of the box (see Figure 5).

SafeActorRef

The API for SafeActorRef is a wrapper of Akka’s ActorRef, and contains a subset of the latter’s methods and functionality. It uses the same method names, but method signatures are different, to include necessary safety measures. For every method accepting a box, there is a dual method accepting a box and a continuation closure. Recall that it is the only way to enforce that boxes are consumed (see Section 2). The dual methods use the AndThen suffix to indicate that they accept a continuation closure.

For message types that are immutable, the API can be significantly simplified, resembling that of a regular Akka ActorRef. Meanwhile, internally, the message is still boxed up and forwarded for handling by the SafeActor. Importantly, though, the box does not have to be consumed, enabling the method to return and continue execution – removing the need for the AndThen family of methods.

4 Empirical Study

We converted several Scala/Akka programs to use the LaCasa-Akka adapter described in Section 3. The goal of this conversion is to evaluate the effort required to use LaCasa’s type system in practice. The converted programs are part of the Savina actor benchmark suite [8]. Concretely, we converted the following programs: (1) In ThreadRing, an integer token message is passed around a ring of N connected actors. This benchmark is adopted from Theron [10]; (2) Chameneos is a micro-benchmark measuring the effects of contention on shared resources while processing messages; (3) Banking is a bank transaction micro-benchmark measuring synchronous request-response with interfering transactions.

Table 1 shows the results. On average 28.2% of the lines of code of each program needed to be changed (we exclude changes to imports). It is important to note that we expect this number to be significantly lower for larger applications where sequential, non-actor-based code dominates the code base. The most important reasons for code changes are (a) the declaration of safe message classes and (b) the insertion and removal of messages into/from boxes. For example, in ThreadRing 33.3% of added lines are due to declaring message classes as safe.

5 Conclusion

LaCasa extends Scala’s type system with affine types, with applications to race-free concurrent programming and safe off-heap memory management. This paper shows how LaCasa can ensure the isolation of actors in Akka, a widely-used actor framework for Scala, while providing safe and efficient ownership transfer of asynchronous messages. According to our empirical study, adjusting existing Akka-based Scala programs requires changing 28.2% of the lines of code on average. However, this initial result represents a worst-case scenario, since the study only considered micro-benchmarks where actor-related code dominates, unlike larger real-world applications. An empirical study extending our results to medium-to-large open-source code bases is ongoing.