Document Open Access Logo

Refinement of Parallel Algorithms down to LLVM

Author Peter Lammich

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.24.pdf
  • Filesize: 0.73 MB
  • 18 pages

Document Identifiers

Author Details

Peter Lammich
  • University of Twente, Enschede, The Netherlands

Cite AsGet BibTex

Peter Lammich. Refinement of Parallel Algorithms down to LLVM. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.24

Abstract

We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms' performance is competitive with their counterparts implemented in C/C++. Our approach is backwards compatible with the Isabelle Refinement Framework, such that existing sequential formalizations can easily be adapted or re-used. As case study, we verify a parallel quicksort algorithm, and show that it performs on par with its C++ implementation, and is competitive to state-of-the-art parallel sorting algorithms.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Semantics and reasoning
  • Computing methodologies → Parallel algorithms
Keywords
  • Isabelle
  • Concurrent Separation Logic
  • Parallel Sorting
  • LLVM

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Mikhail Asiatici, Damian Maiorano, and Paolo Ienne. How many cpu cores is an fpga worth? lessons learned from accelerating string sorting on a cpu-fpga system. Journal of Signal Processing Systems, pages 1-13, 2021. Google Scholar
  2. Yves Bertot and Pierre Castran. Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions. Springer Publishing Company, Incorporated, 1st edition, 2010. Google Scholar
  3. Stefan Blom, Saeed Darabi, Marieke Huisman, and Wytse Oortwijn. The vercors tool set: Verification of parallel and concurrent software. In Nadia Polikarpova and Steve Schneider, editors, Integrated Formal Methods, pages 102-110, Cham, 2017. Springer International Publishing. Google Scholar
  4. Boost C++ libraries. URL: https://www.boost.org/.
  5. Boost C++ libraries sorting algorithms. URL: https://www.boost.org/doc/libs/1_77_0/libs/sort/doc/html/index.html.
  6. Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. In Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '05, pages 259-270, New York, NY, USA, 2005. ACM. URL: https://doi.org/10.1145/1040305.1040327.
  7. Julian Brunner and Peter Lammich. Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reasoning, 60(1):3-21, 2018. URL: https://doi.org/10.1007/s10817-017-9418-4.
  8. C. Calcagno, P.W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS 2007, pages 366-378, July 2007. Google Scholar
  9. Jatin Chhugani, Anthony D Nguyen, Victor W Lee, William Macy, Mostafa Hagog, Yen-Kuang Chen, Akram Baransi, Sanjeev Kumar, and Pradeep Dubey. Efficient implementation of sorting on multi-core simd cpu architecture. Proceedings of the VLDB Endowment, 1(2):1313-1324, 2008. Google Scholar
  10. Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf, and Jan-Georg Smaus. A fully verified executable LTL model checker. In CAV, volume 8044 of LNCS, pages 463-478. Springer, 2013. Google Scholar
  11. Mathias Fleury, Jasmin Christian Blanchette, and Peter Lammich. A verified SAT solver with watched literals using Imperative HOL. In Proc. of CPP, pages 158-171, 2018. Google Scholar
  12. The GNU C++ library 3.4.28. URL: https://gcc.gnu.org/onlinedocs/libstdc++/.
  13. A. Nico Habermann. Parallel neighbor-sort, June 1972. URL: https://doi.org/10.1184/R1/6608258.v1.
  14. Maximilian P. L. Haslbeck and Peter Lammich. For a few dollars more - verified fine-grained algorithm analysis down to LLVM. TOPLAS, S.I. ESOP'21, 2021. to appear. Google Scholar
  15. Maximilian P. L. Haslbeck and Peter Lammich. For a few dollars more - verified fine-grained algorithm analysis down to LLVM. In Nobuko Yoshida, editor, Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12648 of Lecture Notes in Computer Science, pages 292-319. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72019-3_11.
  16. Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. Actris: Session-type based reasoning in separation logic. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371074.
  17. Nicolai M. Josuttis. The C++ Standard Library: A Tutorial and Reference. Addison-Wesley Professional, 2nd edition, 2012. Google Scholar
  18. Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program., 28:e20, 2018. URL: https://doi.org/10.1017/S0956796818000151.
  19. Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales a sectioning concept for isabelle. In Yves Bertot, Gilles Dowek, Laurent Théry, André Hirschowitz, and Christine Paulin, editors, Theorem Proving in Higher Order Logics, pages 149-165, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  20. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. Mechanised separation algebra. In ITP, pages 332-337. Springer, August 2012. Google Scholar
  21. Peter Lammich. Automatic data refinement. In ITP, volume 7998 of LNCS, pages 84-99. Springer, 2013. Google Scholar
  22. Peter Lammich. Verified efficient implementation of gabow’s strongly connected component algorithm. In International Conference on Interactive Theorem Proving, pages 325-340. Springer, 2014. Google Scholar
  23. Peter Lammich. Refinement to Imperative/HOL. In ITP, volume 9236 of LNCS, pages 253-269. Springer, 2015. Google Scholar
  24. Peter Lammich. Efficient verified (UN)SAT certificate checking. In Proc. of CADE. Springer, 2017. Google Scholar
  25. Peter Lammich. The GRAT tool chain - efficient (UN)SAT certificate checking with formal correctness guarantees. In SAT, pages 457-463, 2017. Google Scholar
  26. Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:19, Dagstuhl, Germany, 2019. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.22.
  27. Peter Lammich. Efficient verified implementation of introsort and pdqsort. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 307-323. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51054-1_18.
  28. Peter Lammich and S. Reza Sefidgar. Formalizing the Edmonds-Karp algorithm. In Proc. of ITP, pages 219-234, 2016. Google Scholar
  29. Peter Lammich and S. Reza Sefidgar. Formalizing network flow algorithms: A refinement approach in Isabelle/HOL. J. Autom. Reasoning, 62(2):261-280, 2019. URL: https://doi.org/10.1007/s10817-017-9442-4.
  30. Peter Lammich and Thomas Tuerk. Applying data refinement for monadic programs to Hopcroft’s algorithm. In Lennart Beringer and Amy P. Felty, editors, ITP 2012, volume 7406 of LNCS, pages 166-182. Springer, 2012. Google Scholar
  31. Glen Mével and Jacques-Henri Jourdan. Formal verification of a concurrent bounded queue in a weak memory model. Proc. ACM Program. Lang., 5(ICFP), August 2021. URL: https://doi.org/10.1145/3473571.
  32. DAVID R. MUSSER. Introspective sorting and selection algorithms. Software: Practice and Experience, 27(8):983-993, 1997. URL: https://doi.org/10.1002/(SICI)1097-024X(199708)27:8<983::AID-SPE117>3.0.CO;2-#.
  33. Peter W. O'Hearn. Resources, concurrency and local reasoning. In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, pages 49-67, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. Google Scholar
  34. Mohsen Safari and Marieke Huisman. A generic approach to the verification of the permutation property of sequential and parallel swap-based sorting algorithms. In International Conference on Integrated Formal Methods, pages 257-275. Springer, 2020. Google Scholar
  35. Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, and Lars Birkedal. Transfinite iris: Resolving an existential dilemma of step-indexed separation logic. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 80-95, 2021. Google Scholar
  36. Intel oneapi threading building blocks. URL: https://software.intel.com/en-us/intel-tbb.
  37. Verified software toolchain project web page. URL: https://vst.cs.princeton.edu/.
  38. Simon Wimmer and Peter Lammich. Verified model checking of timed automata. In TACAS 2018, pages 61-78, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact