Region-based Local State

Since Sys­tem C fea­tures ef­fect han­dlers and mul­ti­ple re­sump­tions, mu­ta­ble state needs to be used with care. Take the fol­low­ing stan­dard han­dler for am­bi­gu­ity that runs ex­plores all pos­si­ble choices.

interface Amb { def flip(): Boolean }

def allChoices { prog : {Amb} => Unit }: Unit {
  try { prog {amb} } with amb: Amb {
    def flip() { resume(true); resume(false) }
  }
}

If we de­clare the mu­ta­ble vari­able out­side of the han­dler for am­bi­gu­ity, changes should be per­sisted across dif­fer­ent ex­plored al­ter­na­tives:

def stateExample1() {
  var x = 1;
  allChoices { {amb: Amb} =>
    if (amb.flip()) { x = 2 } else { () };
    println(x)
  }
}
stateExample1()

whereas, if we de­clare the mu­ta­ble vari­able within the han­dler for am­bi­gu­ity, it should per­form back­track­ing:

def stateExample2() {
  allChoices { {amb: Amb} =>
    var x = 1;
    if (amb.flip()) { x = 2 } else { () };
    println(x)
  }
}
stateExample2()

In order to achieve this cor­rect back­track­ing be­hav­iour, state is al­lo­cated on the stack, cap­tured to­gether with the con­tin­u­a­tion and re­stored on re­sump­tion.

Re­gions

In fact, all local mu­ta­ble vari­ables are al­lo­cated in cor­re­spond­ing re­gions. The re­gions be­come vis­i­ble, when try­ing to close over the ref­er­ences:

def stateExample1b() {
  var x = 1;
  val closure = box { () => x };
  ()
}

The in­ferred ca­pa­bil­ity set for closure is {stateExample1b}. This il­lus­trates that x is al­lo­cated in a re­gion as­so­ci­ated with the cur­rent func­tion de­f­i­n­i­tion. We could also make this more ex­plicit as:

def stateExample1c() {
  region r {
    var x in r = 1;
    val closure = box { () => x };
    ()
  }
}

Now, the in­ferred ca­pa­bil­ity set at closure is {r}. Re­gions are sec­ond-class and can be passed to func­tions:

def newCounter {pool: Region} {
  var state in pool = 0;
  return box { () => println(state); state = state + 1 }
}

Hov­er­ing over newCounter, we can see that the in­ferred re­turn type is () => Unit at {pool}. That is, we re­turn a func­tion that closes over the re­gion that we passed to it.

Let us al­lo­cate a fresh re­gion and use the above de­fined func­tion:

def stateExample3() {
  region pool {
    val c1 = newCounter {pool};
    val c2 = newCounter {pool};

    c1();
    c1();
    c2();
    c1();
    c2()
  }
}
stateExample3()

Back­track­able Re­gions

Of course the two con­cepts can be com­bined and re­gions show the cor­rect back­track­ing be­hav­ior.

def exampleProgram {amb:Amb} {reg:Region} {
  var x in reg = 1;
  if (amb.flip()) { x = 2 } else { () };
  println(x)
}

def stateExample4() {
  region pool {
    allChoices { {amb: Amb} =>
      exampleProgram {amb} {pool}
    }
  }
}
stateExample4()

and nested the other way around:

def stateExample5() {
  allChoices { {amb: Amb} =>
    region pool {
      exampleProgram {amb} {pool}
    }
  }
}
stateExample5()