Translating Concepts of the Futhark Programming Language into an Extended pi-Calculus
Authors
Jensen, Lars ; Paulsen, Chris Oliver ; Teule, Julian Jørgensen
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-15
Pages
91
Abstract
Over the past decade, consumer CPUs have grown from four cores to as many as 24. Instead of only making single cores faster, hardware now scales horizontally, so software must parallelize its work to use these cores efficiently. Futhark addresses this by providing an abstraction layer over parallel hardware: the language offers data-parallel constructs that let programmers express concurrent operations. To analyze how this concurrency behaves, the report translates a simplified subset of Futhark into π-calculus, a formal model that naturally describes concurrent systems. The report presents the design and implementation of two languages: ButF (a small version of Futhark) and Eπ (an extended π-calculus). It then simplifies the set of primitive operations to enable a cleaner translation. Finally, it shows the translation is correct by establishing an operational correspondence between the two languages.
Over det seneste årti er forbruger-CPU’er vokset fra fire kerner til så mange som 24. I stedet for kun at gøre enkeltkerner hurtigere, skalerer hardware nu horisontalt, så software må parallelisere sit arbejde for at udnytte kernerne effektivt. Futhark imødekommer dette ved at tilbyde et abstraktionslag over parallel hardware: sproget giver data-parallelle konstruktioner, der lader programmører udtrykke samtidige operationer. For at analysere, hvordan denne samtidighed opfører sig, oversætter rapporten en forenklet delmængde af Futhark til π-kalkyle (π-calculus), en formel model, der naturligt beskriver samtidige systemer. Rapporten præsenterer design og implementering af to sprog: ButF (en lille version af Futhark) og Eπ (en udvidet π-kalkyle). Derefter forenkles de primitive operationer for at gøre oversættelsen enklere. Til sidst vises oversættelsen korrekt ved at etablere en operationel korrespondance mellem de to sprog.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords