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 is reachable from the
of the linked list. We can write this reachability condition as follows:
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:
A Related Use: Non-Interference
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.