Bachelor Thesis
Changes to existing software can often lead to unpredicted behaviour or faults. In particular in theorem proving, changes to the inner machinery can have a large impact. In Isabelle, we address this problem with a large system test where the whole archive of formal proofs is built. It is thus desirable to check such a large body of formalizations quickly.
As a truly parallel interactive theorem prover, Isabelle can take advantage of a large degree of parallelism [1]. A single build can be distributed on multiple worker threads, which – up to a certain threshold on the number of parallel threads (typically 8 to 16) – increases performance greatly. Moreover, multiple independent sessions can be built in parallel on a single machine.
In the past, this meant that large server CPUs with hundreds of cores were a suitable choice for a build system to achieve short build times; however, nowadays performance gravitates towards high-speed consumer hardware, which allows only limited parallelism.
As a result, utilizing multiple individual consumer CPUs would yield much shorter build times than a single high-performance system, while being much more economical at the same time.
The scope of this thesis is designing and implementing a platform that enables this, so that builds can be distributed on a (potentially heterogeneous) cluster of worker machines. The main problems to solve are state management, scheduling, and handling of node outages.
Programming language: Scala, Shell
Prerequisites: Familiarity with Scala or similar language; English; Good linux experience
Supervisor
Fabian Huch, email {huch} AT [in.tum.de]
Professor
Prof. Tobias Nipkow, email {nipkow} AT [in.tum.de]
Literature
[1]: Wenzel, Makarius. “Parallel proof checking in Isabelle/Isar.” PLMMS (2009): 13-29