Detecting Assumptions on Deterministic Implementations of Non-deterministic Specifications

Some commonly used methods have nondeterministicspecifications, e.g., iterating through a set canreturn the elements in any order. However, non-deterministicspecifications typically have deterministic implementations, e.g.,iterating through two sets constructed in the same way mayreturn their elements in the same order. We use the termADINS code to refer to code that Assumes a DeterministicImplementation of a method with a Non-deterministic Specification. Such ADINS code can behave unexpectedly whenthe implementation changes, even if the specification remainsthe same. Further, ADINS code can lead to flaky tests -- teststhat pass or fail seemingly non-deterministically. We present a simple technique, called NONDEX, for detectingflaky tests due to ADINS code. We implemented NONDEX forJava: we found 31 methods with non-deterministic specificationsin the Java Standard Library, manually built non-deterministicmodels for these methods, and used a modified Java VirtualMachine to explore various non-deterministic choices. We evaluatedNONDEX on 195 open-source projects from GitHub and 72student submissions from a programming homework assignment.NONDEX detected 60 flaky tests in 21 open-source projects and110 flaky tests in 34 student submissions.