nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Closing the Performance Gap Between Doubles and Rationals for Octagons

verfasst von : Aziem Chawdhary, Andy King

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Modular Software Fault Isolation as Abstract Interpretation

Nächstes Kapitel Verifying Properties of Differentiable Programs

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)CrossRef

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_20CrossRef

Beckschulze, E., Kowalewski, S., Brauer, J.: Access-based localization for octagons. Electron. Notes Theor. Comput. Sci. 287, 29–40 (2012)CrossRef

Bellman, R.: On a routing problem. Q. Appl. Math. 16, 87–90 (1958)MathSciNetCrossRef

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)

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

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_23CrossRef

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/

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_16CrossRefMATH

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.

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_17CrossRef

12.

Ershov, A.P.: On programming of arithmetic operations. Commun. ACM 1(8), 3–6 (1958). Translated by M. D. FriedmanCrossRef

13.

Ershov, A.P.: Programming of arithmetic operations. Doklady Akademii Nauk SSSR 118(3), 427–430 (1958)MathSciNetMATH

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_10CrossRef

15.

GNU: GNU MP Manual (2016). https://gmplib.org/manual/

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_20CrossRef

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_12CrossRef

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_52CrossRef

19.

Jourdan, J.-H.: Verasco: a formally verified C static analyzer. Ph.D. thesis, Université Paris Diderot (Paris 7) Sorbonne Paris Cité, May 2016

20.

Knuth, D.: The Art of Computer Programming, Volume 3: Sorting and Searching, 2nd edn. Addison Wesley, Reading (1998)

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)

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)

23.

Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Polytechnique En Informatique (2004)

24.

Miné, A.: The octagon abstract domain. HOSC 19(1), 31–100 (2006)MathSciNetMATH

25.

Nethercote, N.: Dynamic binary analysis and instrumentation. Ph.D. thesis, Trinity College, University of Cambridge (2004)

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_25CrossRefMATH

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)CrossRef

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)

29.

Singh, G., Püschel, M., Vechev, M.: Making numerical program analysis fast. In: PLDI, pp. 303–313. ACM Press (2015)

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_46CrossRef

31.

Venet, A., Brat, G.: Precise and efficient static array bound checking for large embedded C programs. In: PLDI, pp. 231–242 (2004)

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)

Titel: Closing the Performance Gap Between Doubles and Rationals for Octagons
verfasst von: Aziem Chawdhary
Andy King
Verlag: Springer International Publishing
Buch: Static Analysis
Print ISBN: 978-3-319-99724-7

Electronic ISBN: 978-3-319-99725-4

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-99725-4_13

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"