A Type System for Scala Actors to Enforce Race Safety Without Sacrificing Performance

Posted by Sadek Drobi on Jul 20, 2009

Community

Architecture,

Java

Topics

Language Design ,

Programming ,

Compilers

Tags

Actors ,

JVM ,

Scala ,

Concurrency

Philipp Haller and Martin Odersky submitted a paper that introduces a new approach for enabling safe massage transfer in Scala actors model implementation. Whereas message-based concurrency is instrumental for building scalable architectures that support concurrent processes, it implies important trade-offs in terms of performance and power (flexibility) on the one hand and race safety on the other hand.

Ideally, a sent message should get “moved from the memory region of the sender to the (possibly disjoint) memory region of the receiver.” However, given performance requirements in “critical code that deals with large messages, such as image processing pipelines or network protocol stacks”, messages have to be passed “between processes running on the same shared-memory computer by reference.” To avoid data races in this context, constraints should be imposed on messages shape: they have to be immutable or alias-free. This can, nevertheless, have negative consequences on performance since “data stored in an object graph that does not satisfy the shape constraints must first be serialized into a permitted form before it can be sent within a message”.

In Scala actors – unlike in Erlang’s – messages can be of any kind: immutable or mutable and their state is not copied “when sending messages between actors operating on the same computer”. This allows gains in performance and flexibility but makes it challenging to ensure race safety for shared messaged. Until now, race safety was not enforced by the language of its libraries but was rather a matter of programming conventions that were restricting capabilities of message passing mechanism.

To reduce these constraints, Haller and Odersky suggest a type system based on capability checking (i.e. access permissions for objects) and external uniqueness that “is used to control aliasing of transferred objects” and to guarantee reference uniqueness. They argue indeed that the notion of reference uniqueness is central for enforcing race safety in the presence of mutation in message-based concurrency. They give an example where an actor “receives a reference to a linked list” and another list, that “may have been built locally or may have been received from elsewhere”, is appended to the first list before it is passed on”:

actor {
	receive {
		case rlist: LinkedList =>
			val other: LinkedList = ...
			rlist.append(other)
			next.send(rlist)
	}
}
 
class Node {
	var el: Object
	var prev, next: Node
}
class LinkedList {
	var head: Node
	def append(other: LinkedList) {
		if (head == null)
			head = other.head
		else if (other.head != null) {
			var h = head
			while (h.next != null) h = h.next
			h.next = other.head
			h.next.prev = h
		}
	}
}

To be able to send on the extended list it is necessary to check that “mutation did not introduce any [external] aliasing that could violate race safety”, in other words that “a unique reference to a list, such as rlist, should remain unique after invoking append on it”.

The authors name their system that allows to do that “Object Capability Types” (OCT) and they formalize it as an extension of the EPFL Scala compiler. To implement it, Haller and Odersky introduce a series of annotations that allow adding information necessary for type checking in a simple and concise way that works for all methods of common collection classes in Scala’s standard library without changing their implementation. The three annotations - @unique, @transient, and @exposed – can be carried by local variables, method parameters, and method results:

class Node {
	var el: Object
	var prev, next: Node
}
class LinkedList {
	var head: Node
	@transient
	def append(other: LinkedList @unique) {
		expose (this) { xl =>
			val ol = localize(other, xl)
			if (xl.head == null)
				xl.head = ol.head
			else if (ol.head != null) {
				var h = xl.head
				while (h.next != null) h = h.next
				h.next = ol.head
				h.next.prev = h
			}
		}
	}
}

The @transient annotation […] applies to the receiver, i.e., this. It requires this to be unique; moreover, calling the method will not consume this reference, that is, after the call the reference is still available (and unique). This corresponds to our requirement that ownership transfer should be safe after calling append. The @unique annotation at the argument type requires the argument to be unique. Moreover, it grants the method the right to consume the argument, which means that it is invalid to access the argument after the call returns.

[…]

To prevent aliases that could destroy its uniqueness, a unique object must be exposed before its fields can be accessed.

To address the issue of transferring objects containing sub-objects that are often aliased in complex ways, the authors introduce the notion of cluster. Even though, clusters are not declared explicitly the “type system checks the cluster property according to the way an object is constructed and operated on subsequently”:

In our system, the fact that it is safe to transfer an object depends on the objects reachable from it. An object O1 is reachable from another object O2 if and only if a field of O2 refers to O1 or an object reachable from O2 refers to O1. Our system guarantees safe transfer for object graphs characterized as clusters. […] 

[It] guarantees statically that a cluster of objects is externally unique when it is transferred, which implies type safety.

OCT system is meant to remove significant limitations on message shape imposed by existing approaches, still enforcing race safety without sacrificing performance in applications with large message sizes. Even though it is already implemented as a light weight extension to Scala, to further facilitate the use of this approach, Philipp Haller and Martin Odersky intend to introduce type inference that would spare developers some work. 

1. Back to top

   Scala Actors to Enforce Race Safety

   Jul 20, 2009 10:28 AM by Sebastian Kübeck

   I fixed the problem by copying objects if they are mutable. For objects that should not be copied, method calls are synchronized.
   
   
   see: Object Oriented Concurrency Meets Actors#, I fixed the problem by copying objects. For objects that should not be copied, method calls are synchronized.
   
   
   See: Object Oriented Concurrency Meets Actors

   Reply

2. Back to top

   Re: Scala Actors to Enforce Race Safety

   Jul 20, 2009 10:32 AM by Sadek Drobi

   You don't eliminate race conditions by having method calls synchronized when shared mutable state is involved.

   Reply

3. Back to top

   Re: Scala Actors to Enforce Race Safety

   Jul 20, 2009 11:03 AM by Sebastian Kübeck

   Obviously, however, I am talking about a different model so you are right in this context. Nice article!

   Reply

• Older >