Tue 19 Jun 2018 14:00 - 14:35 at Grand Ballroom C - Types and Correctness

Array algorithms where operations are applied to disjoint parts
of an array lend themselves well to parallelism, since parallel
threads can operate on the parts of the array without
synchronisation. However, implementing such algorithms requires
programmer diligence to verify that a thread does not
accidentally access an element of the array while another thread
is updating the same element. An off-by-one error can lead to
data-races and non-deterministic bugs which are notoriously hard
to track down.
Previous work on Kappa, a capability-based type system,
provides data-race freedom for concurrent, object-oriented
programs, even in the presence of concurrent mutating accesses
to the same object. In this paper we show how Kappa can be
extended to handle concurrent programming with arrays. By
defining array capabilities which grant access to (parts of) an
array, we can piggy-back on the existing type system in a
straightforward fashion.
We illustrate how split and merge operations integrate with
Kappa in practise by discussing the implementation of a
divide-and-conquer quicksort algorithm. We explore the semantics
of the Kappa extension by using a simple imperative calculus
and sketch on how it could be implemented efficiently.

Tue 19 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:45
Types and CorrectnessARRAY at Grand Ballroom C
Parallel Programming with Arrays in Kappa 
Beatrice Åkerblom Stockholm University, Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University
Rank Polymorphism Viewed as a Constraint Problem
Justin Slepak Northeastern University, Panagiotis Manolios Northeastern University, Olin Shivers Northeastern University, USA
Proving a Core Code for FDM Correct by 2 + dw Tests
Magne Haveraaen University of Bergen, Norway