4.4. References🔗

References are dynamically allocated through the ref(_) construct. Given a value, ref(_) finds a fresh location on the heap and stores the value there. The location is then returned.

def alloc : Exp := hl(
  let l1 := ref(#0);
  let l2 := ref(#0);
  (l1, l2))

After allocation, we can read and update the value at the returned location l with !l and l ← v, respectively. (The Rocq port spells the store as l <- v; iris-lean uses the left-arrow ←.)

def load : Exp := hl(
  let l := ref(#5);
  !l)

def store : Exp := hl(
  let l := ref(#5);
  l ← #6;
  !l)

To allow for synchronisation between threads, HeapLang provides a single primitive called compare-and-exchange, written cmpXchg(l, v1, v2). This instruction atomically reads the contents of location l, checks if it is equal to v1, and, in case of equality, updates l to contain v2. The instruction returns a pair (v, b), with v being the original value stored at l, and b a boolean indicating whether the location was updated.

def cmpxchg_fail : Exp := hl(
  let l := ref(#5);
  cmpXchg(l, #6, #7))

def cmpxchg_suc : Exp := hl(
  let l := ref(#5);
  cmpXchg(l, #5, #7))

iris-lean also provides a variant of cmpXchg called compare-and-set, written cas(l, v1, v2). The only difference is that cas only returns the boolean.

-- TODO (upstream — iris-lean): use the unit literal in the success
-- branches once the `hl` DSL gains a `#()` form (Rocq tutorial uses it).
def cas_example : Exp := hl(
  let l := ref(#5);
  if cas(l, #6, #7) then #0 else
    let a := !l;
    if cas(l, #5, #7) then
      let b := !l;
      (a, b)
    else
      #0)

The Rocq tutorial returns the unit value #() from the success branches; we substitute #0 here for the same reason as in the if_then_else example above.