Reasoning About Recursive Tree Traversals

TL;DR

Retreet is a framework that enables precise reasoning about recursive tree traversals, allowing automatic verification of data-race-freeness and correctness of transformations on complex real-world data structures.

Contribution

It introduces a novel stack-based representation and MSO logic encoding for recursive traversals, improving analysis precision and automation over prior ad hoc methods.

Findings

Can reason about complex mutual recursion in real-world data structures

Automatically checks data-race-freeness and correctness of transformations

Effective on CSS and cycletree data structures

Abstract

Traversals are commonly seen in tree data structures, and performance-enhancing transformations between tree traversals are critical for many applications. Existing approaches to reasoning about tree traversals and their transformations are ad hoc, with various limitations on the class of traversals they can handle, the granularity of dependence analysis, and the types of possible transformations. We propose Retreet, a framework in which one can describe general recursive tree traversals, precisely represent iterations, schedules and dependences, and automatically check data-race-freeness and transformation correctness. The crux of the framework is a stack-based representation for iterations and an encoding to Monadic Second-Order (MSO) logic over trees. Experiments show that our framework can reason about traversals with sophisticated mutual recursion on real-world data structures such as CSS and cycletrees.