Advertisement

Closing the Performance Gap Between Doubles and Rationals for Octagons

  • Aziem Chawdhary
  • Andy KingEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Octagons have enduring appeal because their domain operations are simple, readily mapping to for-loops which apply max, min and sum to the entries of a Difference Bound Matrix (DBM). In the quest for efficiency, arithmetic is often realised with double-precision floating-point, albeit at the cost of the certainty provided by arbitrary-precision rationals. In this paper we show how Compact DBMs (CoDBMs), which have recently been proposed as a memory refinement for DBMs, enable arithmetic calculation to be short-circuited in various domain operations. We also show how comparisons can be avoided by changing the tables which underpin CoDBMs. From the perspective of implementation, the optimisations are attractive because they too are conceptually simple, following the ethos of Octagons. Yet they can halve the running time on rationals, putting CoDBMs on rationals on a par with DBMs on doubles.

Notes

Acknowledgements

We thank Colin King at Canonical and Laurie Tratt at Kings for their help with the performance analysis which underpinned this work. We thank Oleg Kiselyov for his help navigating soviet computer science literature. This work was funded by EPSRC EP/K032585/1 and EPSRC EP/N020243/1.

References

  1. 1.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Formal Methods Syst. Des. 35(3), 279–323 (2009)CrossRefGoogle Scholar
  2. 2.
    Banterle, F., Giacobazzi, R.: A fast implementation of the octagon abstract domain on graphics hardware. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 315–332. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74061-2_20CrossRefGoogle Scholar
  3. 3.
    Beckschulze, E., Kowalewski, S., Brauer, J.: Access-based localization for octagons. Electron. Notes Theor. Comput. Sci. 287, 29–40 (2012)CrossRefGoogle Scholar
  4. 4.
    Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87–90 (1958)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196–207 (2003)Google Scholar
  6. 6.
    Bühler, D., Cuoq, P., Yakobowski, B., Lemerre, M., Maroneze, A., Perrelle, V., Prevosto, V.: The EVA Plug-in. CEA LIST, Software Reliability Laboratory, Saclay, France (2017). https://frama-c.com/download/frama-c-value-analysis.pdf
  7. 7.
    Chawdhary, A., King, A.: Compact difference bound matrices. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 471–490. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-71237-6_23CrossRefGoogle Scholar
  8. 8.
    Chawdhary, A., King, A.: Closing the performance gap between doubles and rationals for octagons. Technical report 67227, University of Kent (2018). https://kar.kent.ac.uk/67227/
  9. 9.
    Chawdhary, A., Robbins, E., King, A.: Simple and efficient algorithms for octagons. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 296–313. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-12736-1_16CrossRefzbMATHGoogle Scholar
  10. 10.
    Chawdhary, A., Robbins, E., King, A.: Incrementally closing octagons. Formal Methods Syst. Des. 1–46 (2018).  https://doi.org/10.1007/s10703-017-0314-7
  11. 11.
    Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197–212. Springer, Heidelberg (1990).  https://doi.org/10.1007/3-540-52148-8_17CrossRefGoogle Scholar
  12. 12.
    Ershov, A.P.: On programming of arithmetic operations. Commun. ACM 1(8), 3–6 (1958). Translated by M. D. FriedmanCrossRefGoogle Scholar
  13. 13.
    Ershov, A.P.: Programming of arithmetic operations. Doklady Akademii Nauk SSSR 118(3), 427–430 (1958)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Exploiting sparsity in difference-bound matrices. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 189–211. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53413-7_10CrossRefGoogle Scholar
  15. 15.
    GNU: GNU MP Manual (2016). https://gmplib.org/manual/
  16. 16.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_20CrossRefGoogle Scholar
  17. 17.
    Heo, K., Oh, H., Yang, H.: Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 237–256. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53413-7_12CrossRefGoogle Scholar
  18. 18.
    Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_52CrossRefGoogle Scholar
  19. 19.
    Jourdan, J.-H.: Verasco: a formally verified C static analyzer. Ph.D. thesis, Université Paris Diderot (Paris 7) Sorbonne Paris Cité, May 2016Google Scholar
  20. 20.
    Knuth, D.: The Art of Computer Programming, Volume 3: Sorting and Searching, 2nd edn. Addison Wesley, Reading (1998)Google Scholar
  21. 21.
    Lassez, J.-L., Huynh, T., McAloon, K.: Simplication and elimination of redundant linear arithmetic constraints. In: Constraint Logic Programming, pp. 73–87. MIT Press (1993)Google Scholar
  22. 22.
    Measche, M., Berthomieu, B.: Time Petri-nets for analyzing and verifying time dependent communication protocols. In: Rudin, H., West, C. (eds.) Protocol Specification, Testing and Verification III, pp. 161–172. North-Holland, Amsterdam (1983)Google Scholar
  23. 23.
    Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique En Informatique (2004)Google Scholar
  24. 24.
    Miné, A.: The octagon abstract domain. HOSC 19(1), 31–100 (2006)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Nethercote, N.: Dynamic binary analysis and instrumentation. Ph.D. thesis, Trinity College, University of Cambridge (2004)Google Scholar
  26. 26.
    Oh, H., Brutschy, L., Yi, K.: Access analysis-based tight localization of abstract memories. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 356–370. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_25CrossRefzbMATHGoogle Scholar
  27. 27.
    Oh, H., Heo, K., Lee, W., Park, D., Kang, J., Yi, K.: Global sparse analysis framework. ACM TOPLAS 36(3), 8:1–8:44 (2014)CrossRefGoogle Scholar
  28. 28.
    Oh, H., Lee, W., Heo, K., Yang, H., Yi, K.: Selective context-sensitivity guided by impact pre-analysis. In: PLDI, pp. 475–484 (2014)Google Scholar
  29. 29.
    Singh, G., Püschel, M., Vechev, M.: Making numerical program analysis fast. In: PLDI, pp. 303–313. ACM Press (2015)Google Scholar
  30. 30.
    Urban, C.: FuncTion: an abstract domain functor for termination. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 464–466. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_46CrossRefGoogle Scholar
  31. 31.
    Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: PLDI, pp. 231–242 (2004)Google Scholar
  32. 32.
    Williams Jr., L.F.: A modification to the half-interval search (binary search) method. In: Proceedings of the 14th ACM Southeast Conference, pp. 95–101 (1976)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of KentCanterburyUK

Personalised recommendations