Tracked regions

Tracked regions

A simple class

class Cell {
  var data: int

  method Increment()
    modifies this
  {
    data := data + 1;
  }
}

A composite class

class Machine {
  var motor: Motor
  var screen: Monitor

  method Operate()
    modifies this, motor, screen
  {
    motor.Turn();
    screen.Update();
  }
}

Abstraction

class Machine {
  ghost var Repr: set<object>
  ...
  var motor: Motor
  var screen: Monitor

  method Operate()
    ...
    modifies Repr
  {
    motor.Turn();
    screen.Update();
  }
}

A datatype

datatype Machine =
  | Machine(motor: Motor, screen: Monitor)
{
  method OperateImmutable() returns (this': Machine)
  {
    var motor' := motor.TurnImmutable();
    var screen' := screen.UpdateImmutable();
    this' := Machine(motor', screen');
  }
}

End goal: confined mutations

datatype Machine =
  | Machine(r: region, motor: Motor, screen: Monitor)
{
  method OperateImmutable() returns (this': Machine)
  {
    var Machine(r, motor, screen) := this;
    motor.Turn();
    screen.Update();
    this' := Machine(r, motor, screen);
  }
}

The immutable datatype uses a region that it modifies, and the client never needs to know!

Regions

Global heap

class Cell {
  var data: int
}

method Inc(c: Cell)
  modifies c
{
  c.data := c.data + 1;
}

Heap as parameter

method Inc(: Heap, c: Cell) returns (: Heap)
  modifies c
{
  c.data := c.data + 1;
}

Heap as in-out parameter

method Inc`(c: Cell)
  modifies c
{
  c.data := c.data + 1;
}

Multiple regions

method Inc```(c: Cell`, d: Cell`, e: Cell`)
  modifies c`
{
  c`.data := c`.data + d`.data + e`.data;
}

Inferring region “mode” of types

method Inc```(c: Cell`, d: Cell`, e: Cell`)
  modifies c
{
  c.data := c.data + d.data + e.data;
}

If regions are distinct and are parts of types, then

• regions can be inferred in operations
• regions can be modeled as separate variables

Local regions

method Inc2``(c: Cell`, e: Cell`)
  modifies c
{
  var : region;
  var d := new Cell`;
  d.data := 1;
  Inc```(c, d, e);
}

The region names in this method body can probably be inferred.

Lexically scoped regions

{
  var outer: Cell;
  {
    var : region;
    var inner := new Cell`;
    // the following assignment is ill-typed,
    // because the type of `outer` cannot mention 
    outer := inner;
  }
}

The lexical regions are similar to what the programming language Euclid provided

Dynamically scoped regions

• To place regions into data structures, we need to go beyond lexical regions
• The useful property that lexical scoping gives us is that
  • regions are distinct and never duplicated
• To get that useful property beyond lexical scoping, we need to track provenance

Provenance

provenance

noun

the place of origin or earliest known history of something

• the beginning of something's existence; something's origin
• a record of ownership of a work of art or an antique, used as a guide to authenticity of quality

Linear, affine, unique, monadic, tracked

There are many names:

• Uniqueness types track what has been
• Affine types restrict what is to come
• Linear types restrict what is to come and ensures something happens
• Monadic types give a way to thread unique in-out parameters

I will use the term tracked types

A little language

Method ::= method M(x*) returns (x*) BlockStmt
BlockStmt ::= { Stmt* }
Stmt ::=
  | var x
  | x := Expr             // simple assignment
  | x* := M(Expr*)        // method call
  | var Ctor(x*) := Expr  // datatype destructor
  | if Expr BlockStmt else BlockStmt
  | BlockStmt
Expr ::=
  | x                     // variable
  | F(Expr*)              // constants, operators, functions
  | Ctor(Expr*)           // datatype constructor

A language like this is typical when defining linear types.

Tracking rules

The judgment

U;V  S  U';V'

says that if

• unrestrcted variables U and
• tracked variables V

are available when statement S is started, then

• unrestrcted variables U' and
• tracked variables V'

are available after statement S.

U;V  E : m

says that, if U;V are available, then expression E evaluates to a value of mode m (un/tr).

Variable introduction

If x requires manual initialization:

U;V  var x  U;V

If x is auto-initialized:

x : un
----------------------
U;V  var x  U,x;V

x : tr
----------------------
U;V  var x  U;V,x

​

If type of x requires manual initialization:

U;V  var x  U;V

If x is auto-initialized:

U;V  var x  U;V +x

Simple assignment

x : m'
U;V  E : m
m'  m
-------------------------------
U;V,V  x := E  U;V +x

If

U;V  E : _
U;V  S  U;V
U;V  T  U;V
U' = U  U
V' = V  V
---------------------------------
U;V,V  if E S else T  U';V'

Block statement

  U;V  { S }  U;V
------------------------------------
U;V  { S S ... S }  U;V

Method call

M : (m) returns (m)
U;V  E : m
x : m'
m'  m
------------------------------------
U;V,V  x := M(E)  U;V +x

Datatype destruction

datatype m, Ctor : m
U;V  E : m
x : m'
m'  m
-------------------------------------------
U;V,V  var Ctor(x) := E  U;V +x

Note that dereliction is built into the rules, but that's okay, because of the ... E : m requirement above and the x : m' in the rule for simple assignment

Rules for expressions

x : m
x  U  V
------------
U;V  x : m

F : m  m
U;V  E : m
----------------
U;V  F(E) : m

datatype m, Ctor : m
U;V  E : m
---------------------
U;V  Ctor(E) : m

Adding classes to the little language

Stmt ::= ...
  | x := new Type`      // object allocation
  | Expr`.f := Expr     // object field update
Expr ::= ...
  | Expr`.f             // object field selection

Allocation

  V
---------------------------------
U;V  x := new Type`  U;V +x

Object field read/write

class m, f : m'
U;,V  E : m
U;,V  E : m'
--------------------------------------
U;,V,V,V  E`.f := E  U;,V

class m, f : m'
U;V  E : m
  V
-----------------
U;V  E`.f : m'

Are we done?

(At least) three things are missing/wrong:

• The strictness of tracked types is unnatural for objects
• Reading from an object consumes the object
• We need to be able to use tracked values in a function without consuming them

Tracked objects

tracked class QueryEngine {
  var : region
  var cache: Cache`
  ...

  method Operate()
  {
    var , cache := this; // "unpack this"
    cache`.Lookup();
    ...
    this := new QueryEngine{ , cache }; // "pack this"
  }
}

Reading from a region

tracked datatype Counter =
  | Counter(: region, cell: Cell`)
{
  method Inc() returns (this': Counter)
  {
    var Counter(, cell) := this;
    var x := cell`.data + 1; // RHS consumes cell
    cell`.data := x;         // LHS consumes cell
    this' := Counter(, cell);
  }
}

Using tracked values in a function

tracked datatype Machine =
  | Machine(: region, motor: Motor`, screen: Monitor`)
{
  predicate Valid() {
    var Machine(, motor, screen) := this;
    screen`.vsize == screen`.hsize
  }
}

This is a complication in Chalice / Viper

Shared/borrowed values

• Change U;V environment to U;B;V where B has the shared values

Other questions

• Is a method always implicitly allowed to extend a given region?

    method UndeclaredAllocations`() {
      var cell := new Cell`;
      cell.data := 12;
    }

• Can you do local storage with this region mechanism? (Then, is there a distinction between regions that can or cannot be extended?)

    method LocalStorage() {
      var : region;
      var cell := new Cell`;
      cell`.DoSomething();
      AnotherMethod`();
    }

• Can these regions be used as a programming device? (Then, do all regions need to be present at run time?)

    method EfficientDeallocation() {
      var : region;
      ...
      SomeMethod`(...);
      ...
      //  is automatically freed here
    }

Comparisons

• In separation logic, regions are not explicit in the program text
• In Linear Dafny, regions are handled by the verifier, not the type system