Advertisement

Proving JDK’s Dual Pivot Quicksort Correct

  • Bernhard Beckert
  • Jonas Schiffl
  • Peter H. Schmitt
  • Mattias UlbrichEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10712)

Abstract

Sorting is a fundamental functionality in libraries, for which efficiency is crucial. Correctness of the highly optimised implementations is often taken for granted. De Gouw et al. have shown that this certainty is deceptive by revealing a bug in the Java Development Kit (JDK) implementation of TimSort.

We have formally analysed the other implementation of sorting in the JDK standard library: A highly efficient implementation of a dual pivot quicksort algorithm. We were able to deductively prove that the algorithm implementation is correct. However, a loop invariant which is annotated to the source code does not hold.

This paper reports on how an existing piece of non-trivial Java software can be made accessible to deductive verification and successfully proved correct, for which we use the Java verification engine KeY.

References

  1. 1.
    Proving JDK’s dual pivot quicksort correct. Blog post, companion website. https://www.key-project.org/2017/08/17/dual-pivot/
  2. 2.
    Abano, C., Chu, G., Eiseman, G., Fu, J., Yu, T.: Lab report, Rutgers UniversityGoogle Scholar
  3. 3.
    Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification: The KeY Book. From Theory to Practice. LNCS, vol. 10001. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-319-49812-6 Google Scholar
  4. 4.
    Beckert, B., Bormer, T., Grahl, D.: Deductive verification of legacy code. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 749–765. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47166-2_53 CrossRefGoogle Scholar
  5. 5.
    Black, P.E., Becker, G., Murray, N.V.: Formal verification of a merge sort program with static semantics. ACM SIGPLAN Not. 30(4), 51–60 (1995)CrossRefGoogle Scholar
  6. 6.
    Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24730-2_15 CrossRefGoogle Scholar
  7. 7.
    Galeotti, J.P., Furia, C.A., May, E., Fraser, G., Zeller, A.: Inferring loop invariants by mutation, dynamic analysis, and static checking. IEEE Trans. Softw. Eng. 41(10), 1019–1037 (2015)CrossRefGoogle Scholar
  8. 8.
    de Gouw, S., de Boer, F.S., Rot, J.: Verification of counting sort and radix sort. In: Ahrendt, et al. [3], pp. 609–618Google Scholar
  9. 9.
    de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., Hähnle, R.: OpenJDK’s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273–289. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_16 CrossRefGoogle Scholar
  10. 10.
    Hoare, C.A.R.: Quicksort. Comput. J. 5(1), 10–16 (1962)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Huisman, M., Ahrendt, W., Grahl, D., Hentschel, M.: Formal specification with the Java modeling language. In: Ahrendt et al. [3], pp. 193–241Google Scholar
  12. 12.
    Huisman, M., Monahan, R., Mostowski, W., Müller, P., Ulbrich, M.: VerifyThis 2017: A program verification competition. Technical Report Karlsruhe Reports in Informatics 2017–10, Karlsruhe Institute of Technology (2017)Google Scholar
  13. 13.
    Kushagra, S., López-Ortiz, A., Munro, J.I., Qiao, A.: Multi-pivot quicksort: Theory and experiments. In: Proceedings of the Meeting on Algorithm Engineering and Experiments, pp. 47–60. Society for Industrial and Applied Mathematics (2014)Google Scholar
  14. 14.
    Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M., Dietl, W.: JML Reference Manual (2013). draft Revision 2344Google Scholar
  15. 15.
    Leino, K.R.M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281–288 (2005). https://doi.org/10.1016/j.ipl.2004.10.015 MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Leino, K.R.M., Lucio, P.: An assertional proof of the stability and correctness of natural mergesort. ACM Trans. Comput. Log. 17(1), 6:1–6:22 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Scheurer, D., Hähnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 57–73. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47846-3_5 CrossRefGoogle Scholar
  18. 18.
    Schmitt, P.H.: Some notes on permutations. Technical Report 7, Department of Informatics, Karlsruhe Institute of Technology (2017). http://publikationen.bibliothek.kit.edu/1000068624
  19. 19.
    Schmitt, P.H., Bubel, R.: Theories. In: Ahrendt et al. [3], pp. 149–166Google Scholar
  20. 20.
    Wild, S., Nebel, M.E., Neininger, R.: Average case and distributional analysis of Java 7’s dual pivot quicksort. CoRR abs/1304.0988 (2013). http://arxiv.org/abs/1304.0988
  21. 21.
    Yaroslavskiy, V.: Dual-pivot quicksort algorithm (2009). http://codeblab.com/wp-content/uploads/2009/09/DualPivotQuicksort.pdf. published online

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Bernhard Beckert
    • 1
  • Jonas Schiffl
    • 1
  • Peter H. Schmitt
    • 1
  • Mattias Ulbrich
    • 1
    Email author
  1. 1.Karlsruhe Institute of TechnologyKarlsruheGermany

Personalised recommendations