Abstract

https://youtu.be/OkX6YKSLNQ0

Many problems can be concisely expressed as finding the least fixed point of a monotone map, including graph reachability, static analysis by abstract interpretation, regular expression matching, and parsing. There is a straightforward way to compute these fixpoints: iterate the function. Unfortunately, this is inefficient, for at least two reasons: first, it performs redundant work during each iteration; second, it is inherently single-threaded.

In this talk, I will show how to solve the first of these problems using seminaive evaluation, a technique that iterates to a fixed point faster by computing only the differences between iterations. I will also discuss work in progress on the second problem using a simple graph based model of concurrent monotone computation. Unfortunately, I do not know how to reconcile these two approaches and achieve an implementation strategy for monotone fixed points that is both incremental and concurrent.