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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:20 - 16:00
|Parallel Functional Arrays
|A Short Counterexample Property for Safety and Liveness Verification of Fault-tolerant Distributed Algorithms
|Analyzing divergence in bisimulation semantics
|Fencing off Go: Liveness and Safety for Channel-Based Programming
Julien Lange Imperial College London, Nicholas Ng Imperial College London, Bernardo Toninho Imperial College London, Nobuko Yoshida Imperial College London, UKPre-print