SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Thu 21 Oct 2021 14:20 - 14:35 at Zurich C - Implementation of special Paradigms Chair(s): Frank Tip
Thu 21 Oct 2021 22:20 - 22:35 at Zurich C - Implementation of special Paradigms - mirror Chair(s): Steve Blackburn

\emph{Probabilistic programming languages} aid developers performing Bayesian inference. These languages provide programming constructs and tools for probabilistic modeling and automating the process of developing a probabilistic inference procedure. Prior work introduced a probabilistic programming language, ProbZelus, to extend probabilistic programming functionality to unbounded streams of data. A key innovation of ProbZelus was to demonstrate that the \emph{delayed sampling} inference algorithm could be extended to work in a streaming context. ProbZelus showed that while delayed sampling could be effectively deployed on some programs, depending on the probabilistic model under consideration, delayed sampling is not guaranteed to use a bounded amount of memory over the course of the execution of the program.

In this paper, we the present conditions on a probabilistic program’s execution under which delayed sampling will execute in bounded memory. The two conditions are dataflow properties of the core operations of delayed sampling: the \emph{$m$-consumed property} and \emph{the unseparated path property}. A program executes in bounded memory under delayed sampling if, and only if, it satisfies the $m$-consumed and unseparated path properties. We propose a static analysis that abstracts over these properties to soundly ensure that any program that passes the analysis satisfies these properties, and thus executes in bounded memory under delayed sampling.