Skip to content

Lecture 7.3: Reasoning about Mutability

Now that we have mutable variables, how should we reason about them? Let's take this program from last time as an example:

let f (x : int ref) (y : int ref) : int = 
    y := 3;
    !x

Our specification of this program is that f x y always:

  • returns the initial contents of x;
  • modifies y to 3; and
  • leaves the contents of x unchanged.

Is this specification true of f? No, because x and y might alias, and set the contents of x equal to 3 (and hence return 3). Indeed, no function can implement this spec, for this reason.

However, it we allow f to fail if x and y alias, then we can implement this spec. Here's one attempt: 

let f2 (x : int ref) (y : int ref) : int option = 
    if x = y then  None else 
        Some (y := 3; !x)

While this f2 is sound, it rejects too many inputs. Indeed, if we call f2 like this: 

let x = ref 2 in 
let y = ref 2 in 
f2 x y
We want f2 to return Some here --- since x and y do not alias --- however, it will return None. Why is this, and how can we fix it?

Structural vs Physical Equality

The reason f2 returns None in this case --- and the solution to this problem --- lies in the difference between structural and physical equality. OCaml's = is structural, meaning that the only thing that matters are values: when we compare pointers, we compare the contents of these pointers. Thus, (ref 2) = (ref 2) returns true, even though the two references created are distinct. 

 utop # let x = ref 2;;
val x : int ref = {contents = 2}

utop # let y = ref 2;;
val y : int ref = {contents = 2}

utop # x = y;;
- : bool = true

utop # x := 3;;
- : unit = ()

utop # x = y;;
- : bool = false

The opposite is physical equality, written ==, where references (along with various other values) are compared via their underlying representations. For pointers, this can be used to determine aliasing: 

utop # let x = ref 2;;
val x : int ref = {contents = 2}

utop # let y = ref 2;;
val y : int ref = {contents = 2}

utop # let z = y ;;
val z : int ref = {contents = 2}

utop # x = y;;
- : bool = true

utop # x == y;;
- : bool = false

utop # y = z;;
- : bool = true

utop # y == z;;
- : bool = true

We can now re-implement f2 to check aliasing: 

let f3 (x : int ref) (y : int ref) : int option = 
    if x == y then None else 
        Some (y := 3; !x)

We can see it now works with two copies of the same reference: 

utop # let x = ref 2;;
val x : int ref = {contents = 2}

utop # let y = ref 2;;
val y : int ref = {contents = 2}

utop # f3 x x;;
- : int option = None

utop # f3 x y;;
- : int option = Some 2

utop # !y;;
- : int = 3

Now, what should be the specification of f3? There are two cases, given inputs x and y:

  • If and only if x == y, it should return None;
  • Otherwise, it should increment y and return Some v, where v equals the contents of x.

How can we use PBT via forall to check if f3 satisfies its specification? One thing we could do is write a generator for the inputs to f3 (which would be of type int ref * int ref), and check that f3 behaves properly on these inputs. While this could work, the issue is that f3 might mutate these inputs while it runs; thus, if we want to return these inputs as counter-examples, the returned inputs might not be useful.

Instead, we can take a different approach. We know how to test the correctness of pure functions using forall: just run them many times until the property we want is false. Thus, we will convert the problem of testing a stateful function into testing a pure function. Let's create a function called f3_wrap: 

let f3_wrap (v_x : int) (v_y : int) (alias : bool) = 
    let (x, y) = if alias then 
                    let r = ref v_x in 
                    (r, r)
                 else (ref x, ref y)
    in
    let o = f3 x y in 
    (o, !x, !y)

What f3_wrap does is, in a sense, set up a testing harness that initializes the mutable memory that f3 will touch. Since we care about what f3 will do both on aliasing and non-aliasing references, we will include a boolean about this choice. Then, we will: create the inputs x and y for f3; call f3 on these inputs; and return the return value of f3, along with the new values inside of x and y.

Now, we can see that f3 meets its specification if and only if, for all inputs v_x, v_y and alias, if we let (o, v_x', v_y') = f3_wrap v_x v_y alias, then:

  • If alias = true, then o = None and v_x' = v_x, and v_y' = v_y; and
  • If alias = false, then o = Some v, v = v_y' = v_y + 1, and v_x' = v_x.

We can now test the correctness of f3_wrap using our same techniques as earlier in the class. 

let gen_inputs () : int * int * bool = 
    (Random.int 50, Random.int 50, Random.bool ())

let my_prop (p : int * int * bool) : bool = 
    let (v_x, v_y, alias) = p in 
    let (o, v_x', v_y') = f3_wrap v_x v_y alias in 
    if alias then 
        o = None && v_x = v_x' && v_y = v_y'
    else 
        match o with
        | None -> false
        | Some v -> v = v_y' && v = v_y + 1 && v_x' = v_x

let forall gen prop num = 
    if num <= 0 then None else
        let x = gen () in 
        if prop x then forall gen prop (num - 1) else Some x

let f3_pbt () = 
    forall gen_inputs my_prop 1000

Our moral? If a stateful function's behavior can be specified using a single execution, then create a testing harness that converts it into a pure function, and then use PBT on it.

Temporal Specs

However, not all functions can be specified in this way. What about the below program? 

let counter : unit -> int = 
    let y = ref (-1) in
    fun () -> 
        y := y + 1;
        !y

This function's behavior is not best captured by a specification about a single function call, but rather how the results of the function change over time. How should we specify the above program? One thing we could do is state that it always returns a number at least zero. While this is true, it's not very informative: indeed, fun _ -> 1 also fits here.

Instead, we want to capture the idea that the function always returns a larger number than the previous call. Is there a way to test for this? Here's one idea: we can instrument the function with a "logging" feature to check if this is the case. 

let rec check_decreasing xs = 
    match xs with 
    | [] -> true
    | x :: [] -> true
    | x :: y :: xs' -> x > y && check_decreasing (y :: xs')

let wrap_counter  (ctr : unit -> int) : unit -> int = 
    let log : (int list) ref = ref [] in 
    fun () -> 
        let v = ctr () in 
        log := v :: !log;
        if check_decreasing !log then 
            v
        else 
            failwith "ERROR: Specification not met: counter did not return larger number"

let checked_counter = wrap_counter counter

Here, we create a "wrapper" for the counter which logs the results created from the counter. Each time we access the counter, we re-check that the log only holds strictly decreasing values (since we are adding to the front of the log). If we ever find a log that does not decrease, we throw an error.

Bonus: Circular Data Structures

Using references, a number of data structures not easily expressible with ADTs alone quickly becomes expressible. Let's create a linked list: 

type linked_list = End | Link of int * (linked_list ref)

Then, let's create a circle of the following values: 

let rec create_circle (beginning : linked_list ref) (xs : int list) : linked_list = 
    match xs with
    | x :: [] -> Link (x, beginning)
    | x :: xs' -> Link (x, ref (create_circle beginning xs'))
    | [] -> failwith "Should not reach here"

let my_circular_list : linked_list ref = 
    let r = ref End in 
    let rest = ref (create_circle r [1; 2; 3]) in 
    r := !rest;
    r

let rec take (n : int) (r : linked_list ref) = 
    if n <= 0 then [] else 
        match !r with
        | End -> []
        | Link (x, rest) ->
            x :: take (n - 1) rest

let f () = take 10 my_circular_list (* [1; 2; 3; 1; 2; 3; 1; 2; 3; 1..] *)

let test () = 
    (* Runs forever, since structural equality will traverse the list *) 
    my_circular_list = my_circular_list

let test2 () = 
    (* Returns true, since the references are indeed pointing to the same memory location *)
    my_circular_list == my_circular_list