Document Open Access Logo

Verified Analysis of List Update Algorithms

Authors Maximilian P. L. Haslbeck, Tobias Nipkow

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2016.49.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Program Verification
  • Algorithm Analysis
  • Online Algorithms

Metrics

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

Abstract

This paper presents a machine-verified analysis of a number of classical algorithms for the list update problem: 2-competitiveness of move-to-front, the lower bound of 2 for the competitiveness of deterministic list update algorithms and 1.6-competitiveness of the randomized COMB algorithm, the best randomized list update algorithm known to date. The analysis is verified with help of the theorem prover Isabelle; some low-level proofs could be automated.

Cite As Get BibTex

Maximilian P. L. Haslbeck and Tobias Nipkow. Verified Analysis of List Update Algorithms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.49

Author Details

Maximilian P. L. Haslbeck
Tobias Nipkow

References

  1. Susanne Albers. Improved randomized on-line algorithms for the list update problem. SIAM J. Comput., 27(3):682-693, 1998. Google Scholar
  2. Susanne Albers, Bernhard von Stengel, and Ralph Werchner. A combined BIT and TIMESTAMP algorithm for the list update problem. Inf. Process. Lett., 56(3):135-139, 1995. Google Scholar
  3. Christoph Ambühl. Offline list update is NP-hard. In Mike Paterson, editor, Algorithms - ESA 2000, volume 1879 of LNCS, pages 42-51. Springer, 2000. Google Scholar
  4. Christoph Ambühl, Bernd Gärtner, and Bernhard von Stengel. Optimal projective algorithms for the list update problem. In U. Montanari, J. Rolim, and E. Welzl, editors, Automata, Languages and Programming (ICALP 2000), volume 1853 of LNCS, pages 305-316. Springer, 2000. Google Scholar
  5. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Santiago Zanella Béguelin. Computer-aided cryptographic proofs. In L. Beringer and A. Felty, editors, Interactive Theorem Proving (ITP 2012), volume 7406 of LNCS, pages 11-27. Springer, 2012. Google Scholar
  6. Allan Borodin and Ran El-Yaniv. Online Computation and Competitive Analysis. Cambridge University Press, 1998. Google Scholar
  7. Arthur Charguéraud and François Pottier. Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation. In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pages 137-153. Springer, 2015. Google Scholar
  8. Martin Erwig and Steve Kollmansberger. Functional pearls: Probabilistic functional programming in Haskell. Journal of Functional Programming, 16(1):21-34, 2006. Google Scholar
  9. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In S. Blazy, C. Paulin-Mohring, and D. Pichardie, editors, Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pages 163-179. Springer, 2013. Google Scholar
  10. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. A formal proof of the Kepler conjecture. CoRR, abs/1501.02155, 2015. Google Scholar
  11. G. Hardy, J.E. Littelwood, and G. Pólya. Inequalities. Cambridge University Press, 1934. Google Scholar
  12. Maximilian P.L. Haslbeck and Tobias Nipkow. Analysis of list update algorithms. Archive of Formal Proofs, 2016. http://isa-afp.org/entries/List_Update.shtml, Formal proof development.
  13. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14, 2012. Google Scholar
  14. Johannes Hölzl, Andreas Lochbihler, and Dmitriy Traytel. A formalized hierarchy of probabilistic system types. In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pages 203-220. Springer, 2015. Google Scholar
  15. Joe Hurd. Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge, 2002. Google Scholar
  16. Joe Hurd. Verification of the Miller-Rabin probabilistic primality test. J. Logic Algebraic Programming, 56(1-2):3-21, 2003. Google Scholar
  17. Joe Hurd, Annabelle McIver, and Carroll Morgan. Probabilistic guarded commands mechanized in HOL. Theoretical Computer Science, 346(1):96-112, 2005. Google Scholar
  18. Sandy Irani. Two results on the list update problem. Inf. Process. Lett., 38(6):301-306, 1991. Google Scholar
  19. Shahin Kamali and Alejandro López-Ortiz. A survey of algorithms and models for list update. In A. Brodnik, A. López-Ortiz, V. Raman, and A. Viola, editors, Space-Efficient Data Structures, Streams, and Algorithms, volume 8066 of LNCS, pages 251-266. Springer, 2013. Google Scholar
  20. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. sel4: Formal verification of an OS kernel. In Jeanna Neefe Matthews and Thomas E. Anderson, editors, Proc. 22nd ACM Symposium on Operating Systems Principles 2009, pages 207-220. ACM, 2009. Google Scholar
  21. Alexander Krauss and Tobias Nipkow. Proof pearl: Regular expression equivalence and relation algebra. J. Automated Reasoning, 49:95-106, 2012. Published online March 2011. Google Scholar
  22. Xavier Leroy. A formally verified compiler back-end. J. Automated Reasoning, 43:363-446, 2009. Google Scholar
  23. Alejandro López-Ortiz, Marc P. Renault, and Adi Rosén. Paid exchanges are worth the price. In E. W. Mayr and N. Ollinger, editors, Symposium on Theoretical Aspects of Computer Science, STACS 2015, volume 30 of LIPIcs, pages 636-648. Schloss Dagstuhl, 2015. Google Scholar
  24. Tobias Nipkow. Amortized complexity verified. In C. Urban and X. Zhang, editors, Interactive Theorem Proving (ITP 2015), volume 9236 of LNCS, pages 310-324. Springer, 2015. Google Scholar
  25. Tobias Nipkow and Gerwin Klein. Concrete Semantics with Isabelle/HOL. Springer, 2014. URL: http://concrete-semantics.org.
  26. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  27. Benjamin C. Pierce and Stephanie Weirich, editors. Special Issue: The PoplMark Challenge, volume 49(3) of J. Automated Reasoning. 2012. Google Scholar
  28. Nick Reingold and Jeffery Westbrook. Optimum off-line algorithms for the list update problem. Technical Report 805, Yale University, Department of Computer Science, 1990. Google Scholar
  29. Nick Reingold and Jeffery Westbrook. Off-line algorithms for the list update problem. Inf. Process. Lett., 60(2):75-80, 1996. Google Scholar
  30. Daniel D. Sleator and Robert E. Tarjan. Amortized efficiency of list update and paging rules. Comm. ACM, 28(2):202-208, 1985. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact