Verifying Determinism in Sequential Programs

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 order-nondeterministic (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.