Published: 8th April 2017|
|The Encore Programming Language: Actors, Capabilities, Garbage, ... (Invited Talk) Dave Clarke||1|
|Dependent Types for Correct Concurrent Programming (Invited Talk) Edwin Brady||2|
|Towards an Empirical Study of Affine Types for Isolated Actors in Scala Philipp Haller and Fredrik Sommar||3|
|Actors without Borders: Amnesty for Imprisoned State Elias Castegren and Tobias Wrigstad||10|
|Quantifying and Explaining Immutability in Scala Philipp Haller and Ludvig Axelsson||21|
|Inferring Types for Parallel Programs Francisco Martins, Vasco Thudichum Vasconcelos and Hans Hüttel||28|
|Multiparty Session Types, Beyond Duality (Abstract) Alceste Scalas and Nobuko Yoshida||37|
|Generating Representative Executions [Extended Abstract] Hendrik Maarand and Tarmo Uustalu||39|
|Towards a Categorical Representation of Reversible Event Structures Eva Graversen, Iain Phillips and Nobuko Yoshida||49|
|Best-by-Simulations: A Framework for Comparing Efficiency of Reconfigurable Multicore Architectures on Workloads with Deadlines Sanjiva Prasad||61|
This volume contains the proceedings of PLACES 2017, the 10th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The workshop was held in Uppsala, Sweden, on April 29th 2017, co-located with ETAPS, the European Joint Conferences on Theory and Practice of Software. The PLACES workshop series aims to offer a forum where researchers from different fields exchange new ideas on one of the central challenges for programming in the near future: the development of programming languages, methodologies, and infrastructures where concurrency and distribution are the norm rather than a marginal concern. Previous editions of PLACES were held in Eindhoven (2016), London (2015), Grenoble (2014), Rome (2013), Tallin (2012), Saarbrücken (2011), Paphos (2010) and York (2009), all co-located with ETAPS, and the first PLACES was held in Oslo and co-located with DisCoTec (2008).
The Program Committee of PLACES 2017 consisted of:
The Program Committee, after a careful and thorough reviewing process, selected 8 papers out of 9 submissions for presentation at the workshop. Each submission was evaluated by at least three referees, and the accepted papers were selected during a week-long electronic discussion. Revised versions of all the accepted papers appear in these proceedings.
In addition to the contributed papers, the workshop featured two invited talks: first, a talk by Dave Clarke, Uppsala University, entitled The Encore Programming Language: Actors, Capabilities, Garbage, ...; second, a talk by Edwin Brady, University of St Andrews, entitled Dependent Types for Correct Concurrent Programming.
PLACES 2017 was made possible by the contribution and dedication of many people. We thank all the authors who submitted papers for consideration. Thanks also to our invited speakers, Dave Clarke and Edwin Brady. We are extremely grateful to the members of the Program Committee and additional experts for their careful reviews, and the balanced discussions during the selection process. The EasyChair system was instrumental in supporting the submission and review process; the EPTCS website was similarly useful in production of these proceedings.
March 30th, 2017
Vasco T. Vasconcelos
Encore is an actor-based programming language developed in the context of the FP7 EU Project UPSCALE. Encore is aimed at general purpose parallel programming, and shuns multithreading to avoid the lack of scalability associated with it. Encore shares a run-time with the pure actor language Pony, which, in contrast to more common run-times, offers local, per-actor garbage collection. Encore includes various abstractions for parallelism and concurrency whose correct behaviour depends, surprisingly, on correct interaction with the garbage collector. To facilitate correct behaviour and allow safe communication between actors, Encore offers a novel capability language. This talk will describe Encore, how it uses and abuses the Pony run-time, the garbage-collection related problems that ensue, and the capability language that resolves them.
Modern software systems rely on communication, for example mobile applications communicating with a central server, distributed systems coordinating a telecommunications network, or concurrent systems handling events and processes in a desktop application. However, reasoning about concurrent programs is hard, since we must reason about each process and the order in which communication might happen between processes. In this talk, I will describe an approach to implementing communicating concurrent programs, inspired by Session Types, using the dependently typed programming language Idris.
I will introduce Idris, and show how its type system can be used to describe resource access protocols (such as controlling access to a file handle or managing the state transitions for logging in to a secure data store) and verify that programs correctly follow those protocols. I will then show how to use this type-driven approach to resource tracking to reason about the order of communication between concurrent processes, ensuring that each end of a communication channel follows a defined protocol.
By type-driven, I mean that the approach involves writing an explicit type describing the pattern of communication, and verifying that processes follow that pattern by type-checking. Communication channels are explicitly parameterised by their state; operations on a channel require a channel in the correct state, and update the channel's state. As a result, a well-typed program working with a communication channel is guaranteed to follow the correct protocol for that channel.