Newtonian Program Analysis of Probabilistic Programs

TL;DR

This paper introduces NPA-PMA, a novel interprocedural dataflow analysis framework for probabilistic programs that employs a generalized Newton's method, enabling efficient, non-iterative analysis of complex control flows.

Contribution

It develops NPA-PMA, a non-iterative analysis framework based on Newtonian Program Analysis, handling multiple confluence types and unstructured control flow in probabilistic programs.

Findings

NPA-PMA outperforms Kleene iteration in experiments.

The framework is highly general for designing program analyses.

Introduces $mbda$-continuous pre-Markov algebras for analysis.

Abstract

Due to their quantitative nature, probabilistic programs pose non-trivial challenges for designing compositional and efficient program analyses. Many analyses for probabilistic programs rely on iterative approximation. This article presents an interprocedural dataflow-analysis framework, called NPA-PMA, for designing and implementing (partially) non-iterative program analyses of probabilistic programs with unstructured control-flow, nondeterminism, and general recursion. NPA-PMA is based on Newtonian Program Analysis (NPA), a generalization of Newton's method to solve equation systems over semirings. The key challenge for developing NPA-PMA is to handle multiple kinds of confluences in both the algebraic structures that specify analyses and the equation systems that encode control flow: semirings support a single confluence operation, whereas NPA-PMA involves three confluence operations (conditional, probabilistic, and nondeterministic). Our work introduces $\omega$-continuous pre-Markov algebras ($\omega$PMAs) to factor out common parts of different analyses; adopts regular infinite-tree expressions to encode program-execution paths in control-flow hyper-graphs; and presents a linearization method that makes Newton's method applicable to the setting of regular-infinite-tree equations over $\omega$PMAs. NPA-PMA allows analyses to supply a non-iterative strategy to solve linearized equations. Our experimental evaluation demonstrates that (i) NPA-PMA holds considerable promise for outperforming Kleene iteration, and (ii) provides great generality for designing program analyses.