<p>Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel <i>semi-implicit</i> parallel model, called <i>Elysium</i>, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code. Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine.</p>

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

East of Eden: Parallel Functional Programming in Idris

  • Christopher Brown,
  • Adam D. Barwell

摘要

Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel semi-implicit parallel model, called Elysium, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code. Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine.