Oct 06, 2015: Stijn de Gouw: Showing that Android's, Java's and Python's sorting algorithm is broken, and fixing it formally

October 06, 2015Showing that Android's, Java's and Python's sorting algorithm is broken, and fixing it formally
Room: HB 2AStijn de Gouw
12:30-13:30

Tim Peters developed the Timsort hybrid sorting algorithm in 2002. TimSort is today used as the default sorting algorithm for Android SDK, Sun's JDK, OpenJDK, Python, Apache Hadoop and many other languages and frameworks. Given the popularity of these platforms, the number of computers, cloud services and mobile phones that use TimSort for sorting is well into the billions.

Fast forward to 2015. After we had successfully verified Counting and Radix sort implementations in Java with a formal verification tool called KeY, we were looking for a new challenge. TimSort seemed to be the ideal candidate for several reasons: it is rather complex, widely used, had a bug history but was reported as fixed in Java 8, and was extensively tested. Unfortunately, we weren't able to prove its correctness. A closer analysis showed that this was, quite simply, because TimSort was broken and our theoretical considerations finally led us to a path towards finding the bug. We show how we did it, derive a mechanically verified bug-free version and discuss the reactions of the developer communities involved in the implementation of the Java and Python standard libraries.