一句话：提出一种类型系统，在编译期可靠验证顺序程序的计算是确定、非确定还是序非确定的，并在大型程序中检出未知缺陷。
非确定性程序难以测试和调试，即使顺序程序也会出现非确定性，例如遍历哈希表元素可能导致测试结果不一致。现有非确定性检测工具依赖观察运行时输出，因而不可靠（unsound）。本文提出一种类型系统，能够表达一个计算是确定的、非确定的，还是序非确定的（如集合），并在编译期对确定性进行可靠验证。作者实现了该类型系统，并用其在一个已有24,000行、经过开发者严格审查的程序中发现了此前未知的非确定性错误，表明该方法能有效捕捉实际缺陷。
A nondeterministic program is difficult to test and debug. Nondeterminism occurs even in sequential programs: for example, iterating over the elements of a hash table can result in diverging test results. We have created a type system that can express whether a computation is deterministic, nondeterministic, or ordernondeterministic (like a set). While state-of-the-art nondeterminism detection tools unsoundly rely on observing run-time output, our approach soundly verifies determinism at compile time. Our implementation found previously-unknown nondeterminism errors in a 24,000 line program that had been heavily vetted by its developers.
DOI 原文 ·
@inproceedings{paperbot5232,
title = {Verifying Determinism in Sequential Programs},
author = {Rashmi Mudduluru},
booktitle = {ASE},
year = {2019},
doi = {10.1109/ase.2019.00159}
}