Verifying determinism in sequential programs

Download: PDF, slides (PDF), slides (Keynote), extended version (PDF), implementation, experimental data.

“Verifying determinism in sequential programs” by Rashmi Mudduluru, Jason Waataja, Suzanne Millstein, and Michael D. Ernst. In ICSE 2021, Proceedings of the 43rd International Conference on Software Engineering, (Madrid, Spain), May 2021, pp. 37-49.
An extended version appeared as “Verifying determinism in sequential programs (extended version)” by Rashmi Mudduluru, Jason Waataja, Suzanne Millstein, and Michael D. Ernst. University of Washington Paul G. Allen School of Computer Science and Engineering technical report UW-CSE-2021-02-01, (Seattle, WA, USA), Feb. 2021.

Abstract

When a program is nondeterministic, it is difficult to test and debug. Nondeterminism occurs even in sequential programs: e.g., by iterating 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-of-the-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, the Determinism Checker, warns if a program is nondeterministic or verifies that the program is deterministic. In case studies of 90097 lines of code, the Determinism Checker found 87 previously-unknown nondeterminism errors, even in programs that had been heavily vetted by developers who were greatly concerned about nondeterminism errors. In experiments, the Determinism Checker found all of the non-concurrency-related nondeterminism that was found by state-of-the-art dynamic approaches for detecting flaky tests.

Download: PDF, slides (PDF), slides (Keynote), extended version (PDF), implementation, experimental data.

BibTeX entry:

@inproceedings{MudduluruWME2021,
   author = {Rashmi Mudduluru and Jason Waataja and Suzanne Millstein and
	Michael D. Ernst},
   title = {Verifying determinism in sequential programs},
   booktitle = {ICSE 2021, Proceedings of the 43rd International
	Conference on Software Engineering},
   pages = {37-49},
   address = {Madrid, Spain},
   month = may,
   year = {2021}
}

(This webpage was created with bibtex2web.)

Back to Michael Ernst's publications.