Multicore Rapid: Extending a Native Idris 2 Compiler and Runtime for Parallelism

This thesis covers the extension of the existing Rapid codebase to support native compilation of Idris programs which can make full use of multiple processor cores. After giving an outline of the current architecture I describe the required changes to the compiler and runtime system.

Idris is a high-level, general purpose, functional programming language supporting dependent and linear types, focusing on fast compilation and execution. Dependent types are a promising approach for several use cases, from increasing confidence in the correctness of selected code sections to formally verified proofs of complete programs.

Rapid is a compiler backend plugging into the main Idris compiler, capable of generating native machine code and aiming for full compatibility with existing programs written in Idris. Rapid’s runtime system provides the generated code with interfaces to the OS and includes a generational tracing garbage collector for automatic memory management.

Performance measurements of CPU-bound workloads indicate good efficiency at thread counts typical for personal computing devices. While the marginal performance gains decrease with higher core counts, opportunities for further improvements are presented.