SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 14:00 - 14:18 at Room II - program analysis 1 Chair(s): Manu Sridharan

Pathwidth and treewidth are standard and well-studied graph sparsity parameters which intuitively model the degree to which a given graph resembles a path or a tree, respectively. It is well-known that the control-flow graphs of structured goto-free programs have a tree-like shape and bounded treewidth. This fact has been exploited to design considerably more efficient algorithms for a wide variety of static analysis and compiler optimization problems, such as register allocation, $\mu$-calculus model-checking and parity games, data-flow analysis, cache management, and liftetime-optimal redundancy elimination. However, there is no bound in the literature for the \emph{pathwidth} of programs, except the general inequality that the pathwidth of a graph is at most $O(\lg n)$ times its treewidth, where $n$ is the number of vertices of the graph.

In this work, we prove that control-flow graphs of structured programs have bounded pathwidth and provide a linear-time algorithm to obtain a path decomposition of small width. Specifically, we establish a bound of $2 \cdot d$ on the pathwidth of programs with nesting depth $d.$ Since real-world programs have small nesting depth, they also have bounded pathwidth. This is significant for a number of reasons: (i)~pathwidth is a strictly stronger parameter than treewidth, i.e.~any graph family with bounded pathwidth has bounded treewidth, but the converse does not hold; (ii)~any algorithm that is designed with treewidth in mind can be applied to bounded-pathwidth graphs with no change; (iii)~there are problems that are fixed-parameter tractable with respect to pathwidth but not treewidth; (iv)~verification algorithms that are designed based on treewidth would become significantly faster when using pathwidth as the parameter; and (v)~it is easier to design algorithms based on bounded pathwidth since one does not have to consider the often-challenging case of merge nodes in treewidth-based dynamic programming. Thus, we invite the static analysis and compiler optimization communities to adopt pathwidth as their parameter of choice instead of, or in addition to, treewidth. Intuitively, control-flow graphs are not only tree-like, but also path-like and one can obtain simpler and more scalable algorithms by relying on path-likeness instead of tree-likeness.

As a motivating example, we provide a simpler and more efficient algorithm for spill-free register allocation using bounded pathwidth instead of treewidth. Our algorithm reduces the runtime from $O(n \cdot r^{{2 \cdot tw \cdot r + 2 \cdot r}})$ to $O(n \cdot pw \cdot r^{{pw\cdot r + r + 1}})$, where $n$ is the number of lines of code, $r$ is the number of registers, $pw$ is the pathwidth of the control-flow graph and $tw$ is its treewidth. We provide extensive experimental results showing that our approach is applicable to a wide variety of real-world embedded benchmarks from SDCC and obtains runtime improvements of 2-3 orders of magnitude. This is because the pathwidth is equal to the treewidth, or one more, in the overwhelming majority of real-world CFGs and thus our algorithm provides an exponential runtime improvement. As such, the benefits of using pathwidth are not limited to the theoretical side and simplicity in algorithm design, but are also apparent in practice.

Thu 26 Oct

Displayed time zone: Lisbon change

14:00 - 15:30
program analysis 1OOPSLA at Room II
Chair(s): Manu Sridharan University of California at Riverside
14:00
18m
Talk
The Bounded Pathwidth of Control-Flow Graphs
OOPSLA
Giovanna Kobus Conrado Hong Kong University of Science and Technology, Amir Kafshdar Goharshady Hong Kong University of Science and Technology, Chun Kit Lam Hong Kong University of Science and Technology
DOI
14:18
18m
Talk
How Profilers Can Help Navigate Type Migration
OOPSLA
Ben Greenman University of Utah, Matthias Felleisen Northeastern University, Christos Dimoulas Northwestern University
DOI
14:36
18m
Talk
Synthesizing Precise Static Analyzers for Automatic Differentiation
OOPSLA
Jacob Laurel University of Illinois at Urbana-Champaign, Siyuan Brant Qian University of Illinois at Urbana-Champaign; Zhejiang University, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research, Sasa Misailovic University of Illinois at Urbana-Champaign
DOI
14:54
18m
Talk
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis
OOPSLA
DOI Pre-print
15:12
18m
Talk
Static Analysis of Memory Models for SMT Encodings
OOPSLA
Thomas Haas TU Braunschweig, René Maseli TU Braunschweig, Roland Meyer TU Braunschweig, Hernán Ponce de León Huawei
DOI