一句话：提出首个实用的模块化验证技术，基于分离逻辑与模块不变式推理全局变量及其初始化
许多命令式语言用全局变量实现缓存、计数器等公共功能，而这些变量由模块初始化器（如 Java 静态初始化块）在运行时自动初始化，其执行时机与顺序通常无法静态、模块化地得知；初始化器还可带任意副作用并存在循环依赖，因此现有模块化验证技术要么不支持全局状态，要么施加主流语言与程序无法满足的严格限制。本文提出首个可对全局状态及其初始化进行形式化、模块化推理的实用验证技术：以分离逻辑为基础，用模块不变式刻画全局变量的所有权与取值，并借助模块与方法上的偏序，在无需知道初始化器确切运行时刻的情况下判定何时可以安全假设某模块不变式成立；技术同时支持线程局部与共享全局状态，对初始化语义仅作最小假设，从而适用于多种语言。作者将其形式化为 Iris 程序逻辑并在 Rocq 中证明可靠性，并在现有 Java 与 Go 验证器中实现，在全局状态典型用例及一个实现互联网路由器的大型代码库上展示了有效性。
Many imperative programming languages offer global variables to implement common functionality such as global caches and counters. Global variables are typically initialized by module initializers (e.g., static initializers in Java), code blocks that are executed automatically by the runtime system. When or in what order these initializers run is typically not known statically and modularly. For instance in Java, initialization is triggered dynamically upon the first use of a class, while in Go, the order depends on all packages of a program. As a result, reasoning modularly about global variables and their initialization is difficult, especially because module initializers may perform arbitrary side effects and may have cyclic dependencies. Consequently, existing modular verification techniques either do not support global state or impose drastic restrictions that are not satisfied by mainstream languages and programs. In this paper, we present the first practical verification technique to reason formally and modularly about global state and its initialization. Our technique is based on separation logic and uses module invariants to specify ownership and values of global variables. A partial order on modules and methods allows us to reason modularly about when a module invariant may be soundly assumed to hold, irrespective of when exactly the module initializer establishing it runs. Our technique supports both thread-local and shared global state. We formalize it as a program logic in Iris and prove its soundness in Rocq. We make only minimal assumptions about the initialization semantics, making our technique applicable to a wide range of programming languages. We implemented our technique in existing verifiers for Java and Go and demonstrate its effectiveness on typical uses cases of global state as well as a substantial codebase implementing an Internet router.
@article{paperbot2903,
title = {Modular Reasoning about Global Variables and Their Initialization},
author = {João Pereira and Isaac van Bakel and Patricia Firlejczyk and Marco Eilers and Peter Müller},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763133}
}