Published: 12th June 2014|
|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|
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
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
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 .
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.