The Schorr-Waite-Algorithm

Abstract

The Schorr-Waite graph marking algorithm named after its inventors Schorr and Waite [1967] has become an unofficial benchmark for the verification of programs dealing with linked data structures.

It has been originally designed with a LISP garbage collector as application field in mind and thus, its main characteristic is low additional memory consumption. The original design claimed only two markers per data object and, more important, only three auxiliary pointers at all during the algorithm’s runtime. It is the latter point, where most other graph marking algorithms lose against Schorr-Waite and need to allocate (often implicitly as part of the method stack) additional memory linear in the number of nodes in the worst case. These resources are used to log the taken path for later backtracking when a circle is detected or a sink reached.

Schorr and Waite’s trick is to keep track of the path by reversing traversed edges offset by one and restoring them afterwards in the backtracking phase of the algorithm. A detailed description including the Java implementation to be verified is given in Section 15.1.

Formal treatment of Schorr-Waite is challenging as reachability issues are involved. Transitive closure resp. reachability is beyond pure first-order logic and some extra effort has to be spent to deal with this kind of problems (see [Beckert and Trentelman, 2005] for a detailed discussion). On the other side, the algorithm is small and simple enough to serve as a testbed for different approaches. We introduce a notion of reachability as part of Sect. 15.2 and come back to it for the actual verification, which makes up most of Sect. 15.3.