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:

• Jade Alglave, University College London, UK
• Michele Bugliesi, Università Ca' Foscari Venezia, IT
• Alastair Donaldson, Imperial College London, UK (co-chair)
• Benedict Gaster, Qualcomm, USA
• Simon Gay, University of Glasgow, UK
• Thomas Hildebrandt, IT University of Copenhagen, DK
• Jeroen Ketema, Imperial College London, UK
• Hans-Wolfgang Loidl, Heriot-Watt University, UK
• Etienne Lozes, ENS Cachan & University of Kassel, FR & DE
• Francisco Martins, University of Lisbon, PT
• Alan Mycroft, University of Cambridge, UK
• Luca Padovani, Università di Torino, IT
• Shaz Qadeer, MSR Redmond, USA
• Vasco T. Vasconcelos, University of Lisbon, PT (co-chair)

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

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.