When a program is nondeterministic, it is difficult to test and debug. Nondeterminism occurs even in sequential programs: e.g., byiterating over the elements of a hash table. We have created a type system that expresses determinism specifications in a program. The key ideas in the type system are type qualifiers for nondeterminism, order-nondeterminism, and determinism; type well-formedness rules to restrict collection types; and enhancements to polymorphism that improve precision when analyzing collection operations. While state-ofthe- art nondeterminism detection tools rely on observing output from specific runs, our approach soundly verifies determinism at compile time.

We implemented our type system for Java. Our type checker, DTC, warns if a program is nondeterministic or verifies that the program is deterministic. In case studies of 87895 lines of code, DTC found 58 previously-unknown nondeterminism errors, even in in programs that had been heavily vetted by developers who were greatly concerned about nondeterminism errors. In experiments, DTC found all of the non-concurrency-related nondeterminism that was found by state-of-the-art dynamic approaches for detecting flaky tests.