关于全局变量及其初始化的模块化推理

《Proceedings of the ACM on Programming Languages》：Modular Reasoning about Global Variables and Their Initialization

模块化验证技术通过分离逻辑和模块不变式解决全局变量初始化顺序不确定问题，形式化证明其正确性，并成功应用于Java、Go及路由代码。

　　

摘要

许多命令式编程语言提供了全局变量，以实现常见的功能，如全局缓存和计数器。全局变量通常由模块初始化器（例如 Java 中的静态初始化器）进行初始化，这些初始化器由运行时系统自动执行。这些初始化器何时以及以何种顺序执行通常是不可静态预测的。例如，在 Java 中，初始化是在类首次被使用时动态触发的；而在 Go 中，其顺序取决于程序中的所有包。因此，从模块化的角度对全局变量及其初始化进行推理是困难的，特别是因为模块初始化器可能会产生任意的副作用，并且可能存在循环依赖关系。因此，现有的模块化验证技术要么不支持全局状态，要么施加了主流语言和程序无法满足的严格限制。

在本文中，我们提出了第一种实用的验证技术，可以正式且模块化地处理全局状态及其初始化问题。我们的技术基于分离逻辑，并使用模块不变量来指定全局变量的所有权和值。通过对模块和方法进行偏序处理，我们可以从模块化的角度推断出某个模块不变量是否可以合理地假设为成立，而无需关心建立该不变量的模块初始化器具体在何时执行。我们的技术同时支持线程局部和共享的全局状态。我们将该技术形式化为 Iris 语言中的程序逻辑，并在 Rocq 框架中证明了其正确性。我们对初始化语义仅做了最少的假设，使得我们的技术适用于广泛的编程语言。我们已经在现有的 Java 和 Go 验证器中实现了该技术，并展示了其在典型全局状态用例以及实现互联网路由器的代码库中的有效性。