Scholarlink

<p>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 <i>dependently-typed languages</i>, such as Idris, Agda and Coq. 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 <Emphasis FontCategory="NonProportional">pi-par</Emphasis>, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in <i>Pipeline</i> and <i>Task Farm</i> skeletons. We evaluate <Emphasis FontCategory="NonProportional">pi-par</Emphasis> on a series of standard <i>Task Farm</i> and <i>Pipeline</i> examples, achieving speedups of up to 23.35<InlineEquation ID="IEq1"> <InlineMediaObject> <ImageObject Color="BlackWhite" FileRef="10766_2025_794_Article_IEq1.gif" Format="GIF" Height="13" Rendition="HTML" Resolution="72" Type="Linedraw" Width="19" /> </InlineMediaObject> <EquationSource Format="TEX">\(\times \)</EquationSource> <EquationSource Format="MATHML"><math> <mo>×</mo> </math></EquationSource> </InlineEquation> on a 28-core machine.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

pi-par: A Dependently-Typed Parallel Language with Algorithmic Skeletons

  • 期刊论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年2月25日

查看全文
  • Christopher Brown,
  • Adam D. Barwell

摘要

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 and Coq. 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 Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 \(\times \) × on a 28-core machine.