POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 14:20 - 14:45 at Amphitheater 44 - Concurrency 3 Chair(s): Adam Chlipala

The goal of our paper is to come up with functional arrays (sequences) that are as efficient as imperative arrays, can be used in parallel, and have well defined cost-semantics. Our approach is to consider arrays with functional value semantics but non functional cost semantics. Because the value semantics is functional, “updating” an array returns a new array. We allow operations on “older” arrays (called interior arrays) to be more expensive than operations on the ``most recent" arrays (called leaf arrays) .

We embed sequences in a language that supports fork join parallelism. Because we support fork-join parallelism, the cost of programs is non-deterministic and depends on the order in which operations are interleaved. This is because the ordering of operations can affect whether a sequence is a leaf or interior. Consequently the concurrent costs of such programs are difficult to analyze. Our main result is the derivation of a deterministic evaluational dynamics which makes analyzing the costs much easier. Our theorems are not array-specific and can be applied to any data type with different costs for operating on interior and leaf versions.

We give a wait-free concurrent sequence implementation which requires constant work for accessing and updating leaf arrays and bounded work for operations on interior arrays. We sketch out our proof of correctness for the array implementation. The key advantages of our sequence approach compared to current approaches is that our implementation requires no changes to existing programming languages, supports nested parallelism, and has well defined cost semantics. At the same time, it allows for functional implementations of algorithms like depth-first search with the same asymptotic complexity as imperative implementations.

Fri 20 Jan

POPL-2017-papers
14:20 - 16:00: POPL - Concurrency 3 at Amphitheater 44
Chair(s): Adam ChlipalaMIT
POPL-2017-papers14:20 - 14:45
Talk
Ananya Kumar, Guy E. BlellochCarnegie Mellon University, Robert Harper
POPL-2017-papers14:45 - 15:10
Talk
Igor KonnovTU Wien, Marijana LazićTU Wien, Helmut VeithTU Wien, Josef WidderTU Wien
DOI Pre-print
POPL-2017-papers15:10 - 15:35
Talk
Xinxin LiuInstitute of software, Chinese academy of sciences, Tingting Yu, Wenhui ZhangInstitute of software, Chinese academy of sciences
POPL-2017-papers15:35 - 16:00
Talk
Julien LangeImperial College London, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London, UK
Pre-print