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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:20 - 16:00
Concurrency 3POPL at Amphitheater 44
Chair(s): Adam Chlipala MIT
14:20
25m
Talk
Parallel Functional Arrays
POPL
Ananya Kumar , Guy E. Blelloch Carnegie Mellon University, Robert Harper
14:45
25m
Talk
A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
POPL
Igor Konnov TU Wien, Marijana Lazić TU Wien, Helmut Veith TU Wien, Josef Widder TU Wien
DOI Pre-print
15:10
25m
Talk
Analyzing divergence in bisimulation semantics
POPL
Xinxin Liu Institute of software, Chinese academy of sciences, Tingting Yu , Wenhui Zhang Institute of software, Chinese academy of sciences
15:35
25m
Talk
Fencing off Go: Liveness and Safety for Channel-Based Programming
POPL
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UK
Pre-print