Newtonian Program Analysis of Probabilistic Programs

Di Wang, Thomas Reps
Object-oriented Programming, Systems, Languages, and Applications · 2024

@article{OOPSLA:WR24,
  author  = {Wang, Di and Reps, Thomas},
  doi     = {10.1145/3649822},
  journal = {Proc.\ ACM Program.\ Lang.},
  month   = {April},
  issue   = {OOPSLA1},
  title   = {{Newtonian Program Analysis of Probabilistic Programs}},
  volume  = {8},
  number  = {105},
  year    = {2024}
}

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 -continuous pre-Markov algebras (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 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.