DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2024.22

Distributed Parallel Build for the Isabelle Archive of Formal Proofs

Authors: Fabian Huch and Makarius Wenzel

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract

Motivated by the continuously growing performance demands for the Isabelle Archive of Formal Proofs (AFP), we introduce distributed cluster computing to the Isabelle platform. Parallel build time on a single node has approached 4h-8h in recent years: by supporting multiple nodes, without shared memory nor shared file-systems, we target at a substantial speedup factor to get below the critical limit of 45min total elapsed time. Our distributed build tool is part of the regular Isabelle distribution, but specifically adapted to cope with the structure of projects seen in the AFP. In this work, we address two main challenges: (1) the distributed system architecture that has been implemented in Isabelle/Scala, and (2) the build schedule optimization problem for multi-threaded tasks on multiple compute nodes. We introduce a heuristic tuned to the typical AFP session structure, which can generate good schedules in a few seconds. We reached a total speedup factor of over 100, which is a milestone never before reached. Using this approach, we could build the Isabelle distribution in 8min 10s elapsed time, and the AFP in 35min 40s, or 1h 59min 13s including very slow sessions.

Cite as

Fabian Huch and Makarius Wenzel. Distributed Parallel Build for the Isabelle Archive of Formal Proofs. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{huch_et_al:LIPIcs.ITP.2024.22,
  author =	{Huch, Fabian and Wenzel, Makarius},
  title =	{{Distributed Parallel Build for the Isabelle Archive of Formal Proofs}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.22},
  URN =		{urn:nbn:de:0030-drops-207505},
  doi =		{10.4230/LIPIcs.ITP.2024.22},
  annote =	{Keywords: Interactive theorem proving, Isabelle, Archive of Formal Proofs, Theorem prover technology, Distributed computing, Schedule optimization}
}

Search Results

Documents authored by Huch, Fabian

Distributed Parallel Build for the Isabelle Archive of Formal Proofs

Abstract

Cite as

Thanks for your feedback!

Could not send message