Fixpoint iteration constitutes the algorithmic core of static analyzers. Parallelizing the fixpoint engine can significantly reduce analysis times. Previous approaches typically fix the granularity of tasks upfront, e.g., at the level of program threads or procedures - yielding an engine permanently stuck in one gear. Instead, we propose to parallelize a generic fixpoint engine in a way that is parametric in the task granularity - meaning that our engine can be run in different gears. We build on the top-down solver TD, extended with support for mixed-flow sensitivity, and realize two competing philosophies for parallelization, both building on a task pool that schedules tasks to a fixed number of workers. The nature of tasks differs between the philosophies. In the immediate approach, all tasks access a single thread-safe hash table maintaining solver state, while in the independent approach, each task has its own state and exchanges data with other tasks via a publish/subscribe data structure. We have equipped the fixpoint engine of the static analysis framework Goblint with implementations following both philosophies and report on our results for large real-world programs.

翻译：不动点迭代构成了静态分析器的算法核心。并行化不动点引擎可显著缩短分析时间。先前的方法通常预先固定任务粒度，例如在程序线程或过程层面——这导致引擎永久卡在单一档位。相反，我们提出以任务粒度参数化的方式并行化通用不动点引擎——这意味着我们的引擎可在不同档位运行。我们基于支持混合流敏感性的扩展型自上而下求解器TD构建，并实现了两种并行化理念，二者均基于向固定数量工作线程调度任务的任务池。两种理念的任务性质存在差异：在即时方法中，所有任务访问维护求解器状态的单个线程安全哈希表；而在独立方法中，每个任务拥有独立状态，并通过发布/订阅数据结构与其他任务交换数据。我们已在静态分析框架Goblint的不动点引擎中配备了遵循两种理念的实现，并报告了针对大型实际程序的实验结果。