Published: 12th June 2014
DOI: 10.4204/EPTCS.155
ISSN: 2075-2180

EPTCS 155

Proceedings 7th Workshop on
Programming Language Approaches to Concurrency and Communication-cEntric Software
Grenoble, France, 12 April 2014

Edited by: Alastair F. Donaldson and Vasco T. Vasconcelos

Preface
Invited Presentation: Finding Concurrency Bugs Under Imprecise Harnesses
Akash Lal
Multiparty Sessions based on Proof Nets
Dimitris Mostrous
1
Sessions as Propositions
Sam Lindley and J. Garrett Morris
9
Towards Reversible Sessions
Francesco Tiezzi and Nobuko Yoshida
17
Session Types for Broadcasting
Dimitrios Kouzapas, Ramūnas Gutkovas and Simon J. Gay
25
Multiparty Session Actors
Rumyana Neykova and Nobuko Yoshida
32
Lightening Global Types
Tzu-chun Chen
38
Verifying Parallel Loops with Separation Logic
Stefan Blom, Saeed Darabi and Marieke Huisman
47
Towards Composable Concurrency Abstractions
Janwillem Swalens, Stefan Marr, Joeri De Koster and Tom Van Cutsem
54
Session Type Isomorphisms
Mariangiola Dezani-Ciancaglini, Luca Padovani and Jovanka Pantovic
61

Preface

This volume contains the post-proceedings of PLACES 2014, the seventh Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software. The workshop was held in Grenoble, France, on April 12th 2014, 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 Rome (2013), Tallin (2012), Saarbrüken (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 2014 consisted of:

The Program Committee, after a careful and thorough reviewing process, selected 9 papers out of 12 submissions for presentation at the workshop and inclusion in the preliminary proceedings. Each submission was evaluated by three referees (with one paper receiving a fourth review), and the accepted papers were selected during a week-long electronic discussion. One of the nine accepted papers was conditionally accepted subject to a process of shepherding by a PC member, which was successful and led to the paper's full acceptance. Revised versions of all the accepted papers appear in these post-proceedings.

In addition to the contributed papers, the workshop featured an invited talk by Akash Lal, Microsoft Research India, entitled Finding Concurrency Bugs Under Imprecise Harnesses. The abstract for this talk appears in these post-proceedings. The workshop concluded with a panel discussion on the topic: The Pathway to Mainstream Programming with Session Types; the panel consisted of Simon Gay, Alan Mycroft, Luca Padovani and Nobuko Yoshida.

PLACES 2014 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 speaker, Akash Lal. 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 and the production of the pre-proceedings; the EPTCS website was similarly useful in production of these post-proceedings.

May 28th, 2014
Alastair F. Donaldson
Vasco T. Vasconcelos


Finding Concurrency Bugs Under Imprecise Harnesses

Akash Lal (Microsoft Research, India)

One way of scaling verification technology to real software is to reduce the code size under analysis. Instead of applying verification to the entire system, one can pick a single component and apply verification to it. While this can dramatically help reduce analysis time, it can lead to false alarms when, for instance, the test harness does not set up the initial state properly before calling into the component.

In this work, we explore the possibility of automatically filtering away (or prioritizing) warnings that result from imprecision in the harness. We limit our attention to the scenario when one is interested in finding bugs due to concurrency. We define a warning to be an interleaved bug when it manifests on an input for which no sequential interleaving produces a warning. We argue that limiting a static analysis to only consider interleaved bugs greatly reduces false positives during static concurrency analysis in the presence of an imprecise harness.

The talk is based on joint work with Saurabh Joshi and Shuvendu K. Lahiri [1].

Biography

Akash Lal is a researcher at Microsoft Research, Bangalore. His interests are in the area of programming languages and program analysis, with a focus on building bug-finding tools for concurrent programs. He joined Microsoft in 2009 after completing his PhD from University of Wisconsin-Madison under the supervision of Prof. Thomas Reps. For his thesis, he received the Outstanding Graduate Researcher Award, given by the Computer Sciences Department of UW-Madison, and the ACM SIGPLAN Outstanding Doctoral Dissertation Award. He completed his Bachelor's degree from IIT-Delhi in 2003.

References

  1. Saurabh Joshi, Shuvendu K. Lahiri & Akash Lal (2012): Underspecified harnesses and interleaved bugs. In: John Field & Michael Hicks, editors: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, doi:10.1145/2103656.2103662.