Danger of shared mutability

Data races may occur if there are >2 concurrent accesses to the same memory location with:

1. at least one being a write,
2. at least one being non-atomic

• undefined behavior in sequential programs; e.g., iterator invalidation if simultaneously:

  • iterating over a data structure

  • mutating the data structure

    val nats = scala.collection.mutable.MutableList(1)
    for (nat <- nats) {
        println(nat)
        if (nat < 10) nats += nat + 1
    }  // prints 1 and 2 (not 1 only, not 1 through 10)

Solutions to mutability problems

Pragmatic approaches:

• disallow mutability
  • purely functional (e.g., Haskell)
• unalias to-be-mutated data
  • copy on write (e.g., R)

Related work:

• ownership type systems (theoretical)
• LaCasa & P. Haller's PhD thesis on actors & unique ownership (Scala)
• borrow checker (Rust, practical)

Static prevention of mutability (Rust)

Rust's borrow checker enforces that a resource is referred to by either:

• one or more immutable references (&T); or
• at most one live mutable reference (&mut T)

Notes:

• A live reference can be (safely) dereferenced
• A (reachable) mutable reference can be reborrowed for a shorter lifetime:
  • through a function call
  • it is not live at the call site until the function returns

State of the art (Rust)

Example:

  let mut x = 5;
  let y = &mut x;
  *y += 1;
  println!("{}", x);

fails to compile:

error: cannot borrow 'x' as immutable because it is
       also borrowed as mutable
            println!("{}", x);

• hard to reason about; the line at fault is

   let y = &mut x;

State of the art (Rust)

Example (desugared):

let mut x = 5;
{ let y = &mut x;
  *y += 1;
  println!("{}", x);
}

Explanation of compilation error:

|
|         let y = &mut x;
|                      - mutable borrow occurs here
|         *y += 1;
|         println!("{}", x);
|                        ^ immutable borrow occurs here
|     }
|     - mutable borrow ends here

Motivation and Goals

• Model borrowing and alias control from Rust in Scala
  • desirable because of ScalaNative (explicit memory management)
• Avoid direct translation of Rust's typing rules
  • keep the language simple

 
Non-goals:

• hide monadic or continuation passing style (CPS) from the user
  • doable via a compiler plug-in and macros
• fully model (transfer of) ownership

Key idea

• Remove the dependence on flow sensitivity
  • an expression may have different types depending on control flow
  • introduce an auxiliary scope whenever flow-dependent information changes

E.g., translate Rust code (flow-sensitive):

let y = &mut x;
...

to Scala code (flow-insensitive):

bindMut(x) { y => ... }

Type-checking

bindImm(1) { imm =>
  bindImm(imm) { immAlias => ... }  // ok
  bindMut(imm) { mutAlias => ... }  // error (2a)
  imm.value = 0  // error (3)
}
bindMut(42) { mut =>
  bindImm(mut) { imm => ... }  // error (2b)
  bindMut(mut) { mutAlias => ... }  // error (2)
  val mutAlias = mut  // error (2)
  mut.value = 0  // ok
  mut  // error (1)
} mut.value = 1  // error (1)

Rules:

1. no escaped variables (lexical scoping)
2. no creation of mutable variables out of other variables (and vice versa)
3. no assignments on immutable variables

Overall design

• library level - enforces the previous rules
  • enforce the CPS-style let bindings to make variable bindings explicit
• meta level - enforces that unsafe workarounds are prohibited
  • use Scala Macros
    • disallow certain syntactic patterns when binding to variables
  • override the behavior of assignments using Scala-Virtualized
    • restricts aliasing to occur only via library-provided facilities

Library-level design

Variable wrapper

class Mut[T]
class Imm[T]
class Var[T,A](private var v: T) {  // A <: Mut[T]/Imm[T]
  def value = v
  def value_=(v2: T)(implicit ev: A =:= Mut[T]) = v = v2
}

Note: the setter that allows assignment is enabled only if access (A) is mutable.

Implicit conversions (bridge methods)

class LowPrioMut
object LowPrioMut {
  implicit def valToMut[T](v: T): Var[T,Mut[T]] =
          new Var[T,Mut[T]](v)
}

object Var extends LowPrioMut {
  implicit def valToImm[T](v: T): Var[T,Imm[T]] =
          new Var[T,Imm[T]](v)
}

Note: conversion to a mutable wrapper takes precedence (higher priority).

Bind functions (lexical scoping)

Idea: exploit 2nd-class values, annotated with @local

Properties:

1. Cannot be stored in mutable variables (vars) or fields
2. Cannot be returned from (member) functions
3. Cannot be accessed by 1st-class functions through free variables
4. (Cannot be coerced to 1st-class; 1st-class can be treated as 2nd-class.)

 
Intuition: 2nd-class Var[T,A] bindings cannot escape the declaring scope.

See also: our OOPSLA'16 paper on Affordable 2nd-Class Values for Fun and Profit

Preventing shared mutable aliases (Mut[T])

def bindMut[T, U](r: Var[T,Mut[T]])(
  @local f: (@local Var[T,Mut[T]]) => U) = f(r)

How does it work?

bindMut(42) { outer =>  // outer is inferred as 2nd-class
  ...
  bindMut(outer) { inner =>  // error: r must be 1st-class
      ...
      outer  // ok: f may refer to 2nd-class free variables
  }
  ...
}

Allowing shared immutable aliases (Imm[T])

def bindImm[T, U](@local r: Var[T,Imm[T]])(
  @local f: (@local Var[T,Imm[T]]) => U) = f(new Var[T,Imm[T]](r.value))

How does it work?

bindImm(42) { outer =>  // outer is inferred as 2nd-class
  ...
  bindImm(outer) { inner => ... } // ok
  ...
}

Meta-level design

Preventing a ref.value passed to bindMut/bindImm via Macros

Concern: ref.value may be implicitly converted to bind* parameter type

bindMut(123) { ref =>
  bindImm(ref.value) { imm => ... /* ouch */  }
}
bindImm("foo") { ref =>
  bindImm(ref) { ref2 =>
    bindMut(ref.value) { mut => ... /* ouch */ }
  }
}

• statically enforce that the argument to bindMut/bindImm are either:
  • an r-value (e.g. 123, "foo")
  • another Variable (e.g., Var[Int,Imm[Int]])
• done via a syntactic inspection in the wrapper macros letMut/let

Preventing escaping of a ref.value through a non-wrapper

Concern: a ref.value may escape through a non-wrapper (val/var)

letMut(123) { mut =>
  letMut(ref.value) { mut => ... }  // error (Var.value as arg.)
  var indirect = mut.value  // error (Var.value in assignment)
  let(indirect) { imm => ... }  // error (not an r-value/Var)
}

• using Scala-Virtualized, override
  • __newVar to disallow syntactic forms like var x = ref.value
  • __assign to disallow syntactic forms such as x = ref.value

Borrowing

Definition: permit temporary aliasing

• during a method call
• in an inner scope

Idea: let function parameter (or a local variable) be 2nd-class

def doWithBorrowed[T](@local ref: Var[T,Mut[T]]) = ...

Example:

bindMut(new MutableObject()) { mut =>
  ...
  doWithBorrowed(mut)
  ...
  {
    @local val borrowed = mut  // requires @local to type-check
    ...
  }
}

Gradual introduction of borrowing

• avoid changing parameter types in all functions to use Var wrappers
  • especially important for (3rd-party) functions

Wrappers:

def call[T, R](f: (@local T) => R)(@local ref: Var[T,_])
def call[T1,T2, R](f: (@local T1, @local T2) => R)(
  @local ref1: Var[T1,_])(@local ref2: Var[T2,_])
...

Note: Adding @local annotations to function parameters is highly automatable

• see our OOPSLA'16 paper

Borrowing Example

def storeMut(@local sb: StringBuilder,
             @local store: Store): String = {
  store.field = sb  // error (cannot store 2nd-class/borrowed)
  sb.toString
}
  
bindMut(new Store()) { storeThatLeaksMutable =>
  bindMut(new StringBuilder()) { sb =>
    val s = call(storeMut)(sb)(storeThatLeaksMutable)
    sb.value.append("brakes encapsulation")
    assert(s == storeThatLeaksMutable.field.toString)  // would fail
  }
}

Note: the StringBuilder could not be stored during the borrow.

Conclusion

We have shown how to:

1. Use 2nd-class values in Scala to model key ingredients of borrowing as in Rust
2. Use macros and virtualized overloads to disallow escape hatches
3. Stay context-insensitive

Key challenges & solutions:

1. flow sensitivity solved by monadic style
2. lifetime of borrowed references solved by 2nd-class values