pi-par: a dependently-typed parallel language with algorithmic skeletons

Christopher Mark Brown; Adam David Barwell; Findlay Sloan

pi-par: a dependently-typed parallel language with algorithmic skeletons

Christopher Mark Brown, Adam David Barwell, Findlay Sloan

School of Computer Science

Research output: Contribution to conference › Paper › peer-review

Abstract

Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for dependently-typed languages, such as Idris, Agda, Coq, and pi-forall. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present pi-par, a prototype dependently-typed language based on pi-forall, with message-passing concurrency and built-in Pipeline and Task Farm algorithmic skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23×
on a 28-core machine.

Original language	English
Number of pages	20
Publication status	Published - 4 Jul 2024
Event	17th International Symposium on High-Level Parallel Programming and Applications - Italy, Pisa Duration: 4 Jul 2024 → … https://hlpp2024.di.unipi.it/

Conference

Conference	17th International Symposium on High-Level Parallel Programming and Applications
Abbreviated title	HLPP 2024
City	Pisa
Period	4/07/24 → …
Internet address	https://hlpp2024.di.unipi.it/

Keywords

Dependent types
piforall
Parallelism
Skeletons

Access to Document

HLPP_2024___DT_Skeletons-4
Copyright © 2024 the Author(s). This work has been made available online in accordance with publisher policies or with permission. Permission for further reuse of this content should be sought from the publisher or the rights holder. This is the author created accepted manuscript following peer review and may differ slightly from the final published version.
Accepted author manuscript, 395 KB

Cite this

@conference{5b57de154fde4cb58c6bf297ea8d27a1,

title = "pi-par: a dependently-typed parallel language with algorithmic skeletons",

abstract = "Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for dependently-typed languages, such as Idris, Agda, Coq, and pi-forall. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present pi-par, a prototype dependently-typed language based on pi-forall, with message-passing concurrency and built-in Pipeline and Task Farm algorithmic skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23×on a 28-core machine.",

keywords = "Dependent types, piforall, Parallelism, Skeletons",

author = "Brown, {Christopher Mark} and Barwell, {Adam David} and Findlay Sloan",

year = "2024",

month = jul,

day = "4",

language = "English",

note = "17th International Symposium on High-Level Parallel Programming and Applications, HLPP 2024 ; Conference date: 04-07-2024",

url = "https://hlpp2024.di.unipi.it/",

}

TY - CONF

T1 - pi-par: a dependently-typed parallel language with algorithmic skeletons

AU - Brown, Christopher Mark

AU - Barwell, Adam David

AU - Sloan, Findlay

PY - 2024/7/4

Y1 - 2024/7/4

N2 - Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for dependently-typed languages, such as Idris, Agda, Coq, and pi-forall. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present pi-par, a prototype dependently-typed language based on pi-forall, with message-passing concurrency and built-in Pipeline and Task Farm algorithmic skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23×on a 28-core machine.

AB - Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for dependently-typed languages, such as Idris, Agda, Coq, and pi-forall. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present pi-par, a prototype dependently-typed language based on pi-forall, with message-passing concurrency and built-in Pipeline and Task Farm algorithmic skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23×on a 28-core machine.

KW - Dependent types

KW - piforall

KW - Parallelism

KW - Skeletons

M3 - Paper

T2 - 17th International Symposium on High-Level Parallel Programming and Applications

Y2 - 4 July 2024

ER -

pi-par: a dependently-typed parallel language with algorithmic skeletons

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this