LARA

Reachability in the Heap as a Motivation for WS1S

Many programs manipulate linked data structures (lists, trees)

To express many important properties of such programs we need a logic that supports transitive closure.

Example: Consider 

class Node {
  Node next;
  Object data;
}
class Program {
  static Node root;
  static boolean member(Object x) {
    Node current = root;
    while (current != null) {
      if (current==x) return true;
      current = current.next;
    }
    return false;
  }
}

As part of the loop invariant, we need to say that the object $current$ is reachable from the $root$ of the linked list. We can write this reachability condition as follows:

\begin{equation*} (root, current) \in \{(x,y).\ x \neq null\ \land\ next(x)=y \}^* \end{equation*}

Expressing Data Structure Correctness Properties

Data structure has no cycles

The set of objects in the data structure does not change when we balance a binary search tree

When we insert an object into a data structure, the set of reachable objects is increased by the given object

Correctness of removal from doubly linked list

Examples and references:

Prove that two parts of program will touch disjoint heap locations

  • ensure that properties of an object on heap hold after a procedure call
    • prove that the object is not reachable from procedure paramters and globals
  • automated parallelization
    • prove that if an object is reachable in one procedure, it is not reachable in another
  • Scala actor programs
    • to ensure absence of data races, actors should not access same region of state
    • again need to show that if an object is reachable in one actor, it is not reachable in another actor

WS1S as a Logic for Reachability

Questions we aim to answer:

  • What is the syntax and semantics of logics that we can use to express such conditions?
  • How do we prove verification conditions in such logic?

We look at one such logic: Weak Monadic Second-Order Logic of One Successor (WS1S). We show its decidability by using automata to describe the set of models of WS1S formulas.

In our case, we look at reachability over the graph representing program heap. In some other applications, one can look at the sequence of states through which the system goes, i.e. considering reachability on computation graph.

This technique we applies in many other cases, in particular for model checking and synthesis of finite state systems that satisfy given specification.