Abstract
Implicit parallel programming models typically give less control to the programmer over the parallelism properties of the program, but require less specialisedexpertise. Explicit parallel models, on the other hand, give much greater control over the parallelism behaviour, but require much more significant expertisefrom the programmer. In this paper, we introduce a novel semi-implicit parallelmodel for an emerging class of languages known as dependently-typed languages.These dependently-typed languages encourage safer software via their ability toexpress strong logical guarantees, in the form of proofs, directly in code. Oursemi-implicit approach is based on a process model that uses dependent typesto guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, such as farms,pipelines and divide and conquer skeletons. We evaluate our process skeletonapproach on a number of examples, achieving speedups of up to 21.8 times on a28-core machine.
| Original language | English |
|---|---|
| Pages | 1-19 |
| Number of pages | 19 |
| Publication status | Published - 3 Jul 2025 |
| Event | High-Level Parallel Programming and Applications - Austria Duration: 3 Jul 2025 → … https://hlpp-conference.github.io/hlpp-2025/ |
Conference
| Conference | High-Level Parallel Programming and Applications |
|---|---|
| Abbreviated title | HLPP |
| Period | 3/07/25 → … |
| Internet address |
Keywords
- Idris
- Parallelism
- Dependent types
- Concurrency
- Skeletons
- Implicit
- Explicit
- Processes