State Effects

The effect system for tracking state modifications is inspired by the article JPure: a Modular Purity System for Java (Dr. David J. Pearce, Conference on Compiler Construction, 2011). The effect annotations have slightly different names though, see section Translating from JPure.

The annotations for this system are defined in package annotation.effects.state.

What is a locality?

Every object has its locality. The concept of locality is identical to what is described in the JPure article. Citing from section 3.2:

Definition 2 (Locality). The locality of an object includes every field defined by its class and, for those annotated @local, the locality of the referenced object.

[For every field of an object], the field itself is always in the locality, but the referenced object may or may not be (depending on whether the field is annotated @local or not). Our definition of locality is, in some ways, similar to the notion of ownership.

For an example, let's take a mutable list:

class ML[T] {
  var data: T
  @local var next: ML[T]

  def replace(a: T, b: T): Unit @mod(this) = {
    if (data == a) data = b
    if (!next.isEmpty) next.replace(a, b)
  }
}

The locality of an instance of ML consists of:

1. the fields data and next
2. the locality of the object referenced by field next

Therefore the method replace only modifies the locality of the receiver this.

Returned locality: @loc

Using an @loc annotation on the return type, a method definition can declare which is the locality of the returned value. For instance, a method that returns one of its arguments has the following signature:

def f(a: A, b: B): A @loc(a) = a

For every method there exist the following localities:

• one for each parameter
• the receiver this
• the special locations fresh (freshly created, un-aliased objects) and any (unknown locality)
• plus, for nested methods:
  • one for each parameter of an outer method
  • one for each local value / variable declared in an outer method

Methods that return a freshly created, un-aliased object are declared with the annotation @loc() (or @loc(fresh), the two are equivalent). Note that a method can only return an un-aliased object if it doesn't have any side-effects (see JPure article): if a method has side-effects, it can potentially create an alias to the freshly created object, but @loc() requires the returned object to be un-aliased. Therefore, the @loc() annotation implies purity, i.e. @mod().

The @loc annotation can not only declare freshness, but also the locality of the returned value (see example above). This is especially important for getters (and Scala creates lots of them). Let's change the mutable list example a little bit: instead of directly accessing the field next, we go through a getter:

class ML[T] {
  var data: T
  @local private var next: ML[T]
  def getNext: ML[T] @loc(this) = next

  def replace(a: T, b: T): Unit @mod(this) = {
    if (data == a) data = b
    if (!getNext.isEmpty) getNext.replace(a, b)
  }
}

The getNext method has locality @loc(this) because the field it returns is annotated @local. To analyze the side-effect of the application getNext.replace(a, b), we first look at the locality returned by getNext, which is @loc(this). From the signature of replace, we see that it modifies the locality of the receiver, therefore we obtain the effect @mod(this).

If getNext did not have a locality annotation, the returned locality would be @loc(any), and therefore the call to replace would have effect @mod(any).

Modification effects: @mod and @store

What JPure does: @mod

Before explaining the @store effects, we show how the simpler (and less general) @mod effects work. The latter are equivalent to JPure's @Local annotations, see the comparison table.

The effect of modifying a locality is declared with the @mod annotation, as shown by the examples in the previous section. Modifying a locality means:

• assigning any value to non-local fields in the locality (e.g. assigning to data in the mutable list example)
• assigning a fresh object to a local field in the locality

Purity is expressed by @mod(), which is equivalent to @mod(fresh): modifying freshly created objects in a method is not observable from outside that method, therefore these effects can be masked.

Note that assigning to local fields is only allowed if the stored value is freshly allocated. This rule makes sure that there are no aliases created between localities of different objects, which is required for soundness of the system (which, in turn, has yet to be shown). Example:

def badModification[T](a: ML[T], b: ML[T]): Unit @mod(a) = {
  a.next = b
}

This method is rejected by effect checking because it assigns the @local field a.next to a non-fresh value b.next. The following code shows why it is unsound to allow it:

val aList: ML[Int] = createList(1,2,3)
val bList: ML[Int] = createList(11,12,13)
badModification(aList, bList)  // effect: @mod(aList)
aList.next.data = 4            // (*)

The last line (*) modifies the bList, but the effect system only sees a modification to aList (the locality of aList.next is aList, and we just modify one of the fields).

Generalization to @store

Unfortunately, the relatively simple @mod effects are not expressive enough in practice for Scala. The main reason is that all field accesses (except for private[this] fields) happen through getters and setters. The @mod effects cannot express what a setter is doing:

class ML[T] {
  @local private var next: ML[T]
  def setNext(n: ML[T]) {
    next = n
  }
}

We cannot annotate the effect of setNext as @mod(this): this is only true if the value n is freshly allocated, otherwise setNext has the topmost effect @mod(any). To solve that problem we introduce @store.

An annotation of the form @store(in, from1, from2, ...) expresses that the locality in is modified, and that values of the localities from1, from2, ... are stored in in. The setter in the above example is annotated as follows:

[...]
  def setNext(n: ML[T]): Unit @store(this, n) = {
[...]

Now, the side-effect of invoking the setter depends on the locality of the argument:

aList.setNext(freshList)   // effect (1): @store(aList, fresh)
aList.setNext(globalList)  // effect (2): @store(aList, any)

There are certain relations between @store and @mod effects (see next section) which make that:

• effect (1) is @mod(aList)
• effect (2) is @mod(any)

Relations between @mod and @store

For simplicity of annotations, both @mod and @store exist. In practice, we expect that users will have to deal with @store annotations very rarely. Internally, there are only @store effects, which are strictly more expressive. The following list describes how the two relate.

• @store(a) is equivalent to @mod(a)
• @store(a, fresh) is equivalent to @mod(a). This relates to the condition mentioned previously that for @mod(x), local fields in x can only be assigned to fresh values.
• @store() is equivalent to @store(fresh) and also @store(fresh, fresh). All of these are equivalent to @mod() and also @mod(fresh).
• @store(any) is equivalent to @mod(any)
• @store(a, any) is equivalent to @mod(any) - such a store effect can create arbitrary aliases, so we assume the topmost effect.

Assignment effects: @assign

Because Scala has nested methods, we introduce another effect domain which describes assignments to variables. If a local variable defined in an outer method is re-assigned in the body of a nested method, the nested method is annotated with an @assign effect.

Assignment effects are expressed with annotations of the form @assign(var, loc1, loc2, ...), which expresses an assignment to var. The value(s) stored in the variable are (potentially) located in locations loc1, loc2, ... Example:

def outer(a1: A, a2: A): Unit @mod(a1, a2) = {
  var x = a1
  def inner(): Unit @assign(x, a2) = {
    x = a2
  }
  x.modify()  // effect: @mod(a1)
  inner()
  x.modify()  // effect: @mod(a1, a2)
}

Note the difference between assignment and store effects. An assignment effect does not modify any object in the heap, it just changes the localities that a local variable might point to. [This is tracked using a typing environment while effect-type-checking.] In the example above, the first invocation of x.modify() has effect @mod(a1). The second invocation has effect @mod(a1, a2), since x might now point to either of the two localities.

Also note that the system currently does not support strong assignments.

Assignment effects to variables defined inside a method can be masked, as they are not observable from the outside. This implies that top-level methods never have an assignment effect.

Purity in the assignment domain is expressed with @assign().

## Translating from JPure

Description	JPure	Scala
Defining ownership	@Local on fields	@local on fields
Purity	@Pure on the method	@mod() on the return type
Modification effects	@Local on the parameters that are modified (on the method if this is modified)	@mod(param, this) on the return type
Non-purity (allow any modifications)	No annotations	No annotations, or @mod(any)
Store effects (e.g. for setters)	-	@store(this, param)
Assignment effects (for nested methods)	-	@assign(variable, param)
Freshness (implies purity)	@Fresh on the method	@loc() on the return type
Locality of the returned value	-	@loc(param, this)