For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM

Maximilian P.L. Haslbeck*, Peter Lammich

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)
38 Downloads (Pure)

Abstract

We present a framework to verify both, functional correctness and (amortized) worst-case complexity of practically efficient algorithms. We implemented a stepwise refinement approach, using the novel concept of resource currencies to naturally structure the resource analysis along the refinement chain, and allow a fine-grained analysis of operation counts. Our framework targets the LLVM intermediate representation. We extend its semantics from earlier work with a cost model. As case studies, we verify the amortized constant time push operation on dynamic arrays and the O(nlog n) introsort algorithm, and refine them down to efficient LLVM implementations. Our sorting algorithm performs on par with the state-of-the-art implementation found in the GNU C++ Library, and provably satisfies the complexity required by the C++ standard.
Original languageEnglish
Article number14
Number of pages36
JournalACM Transactions on Programming Languages and Systems (TOPLAS)
Volume44
Issue number3
Early online date15 Jul 2022
DOIs
Publication statusPublished - 30 Sept 2022

Keywords

  • 2023 OA procedure

Fingerprint

Dive into the research topics of 'For a Few Dollars More: Verified Fine-Grained Algorithm Analysis Down to LLVM'. Together they form a unique fingerprint.

Cite this