POPL 2014: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages San Diego, USA January 22-24, 2014

POPL 2014 Tutorials

On Monday, 20 January 2014, POPL will host a number of tutorials. These are 90 min talks oriented towards students in particular and other POPL attendees in general. The list of available tutorials are:

1. Relaxed separation logic (Viktor Vafeiadis)
2. An introduction to Rust (Nicholas Matsakis)
3. Architecture-agnostic compilation of high-level languages (Dan R. Ghica)
4. Principles and practice of session types (Vasco T. Vasconcelos and Nobuko Yoshida)
5. Differential privacy: Language-based approaches (Marco Gaboardi)
6. Semantics and verification for GPU Kernels (Nathan Chong)

To avoid conflicts, each tutorial will be given twice according to the following schedule:

Time	Presidential Salon D	Sycuan Room	Executive Room
09:00-10:30	4. Session types	1. Relaxed Sep. Logic	3. Compilation
11:00-12:30	4. Session types	6. GPU kernels	2. Rust
14:00-15:30	5. Diff. privacy	6. GPU kernels	3. Compilation
16:00-17:30	5. Diff. privacy	1. Relaxed Sep. Logic	2. Rust

[Hotel floor plans PDF]

Tutorial 1. Relaxed separation logic

Presenter: Viktor Vafeiadis, MPI-SWS

When/where: Monday 20 January, 9:00-10:30 and 16:00-17:30, Sycuan room

Abstract: This tutorial will cover the emerging topic of relaxed memory concurrency and how program logics can provide us with a handle to understand relaxed memory programming. More specifically, the tutorial will introduce the basics of the recent C/C++ memory model, and will show how it supports reasoning based on resource ownership and ownership transfer. The tutorial will then describe relaxed separation logic (RSL), a suitable extension of separation logic that encompasses such ownership-based reasoning and can be used to verify programs running under the C/C++ memory model. The presentation will be illustrated with a number of concurrent programming idioms and will conclude with a discussion of possible future work in terms of program logics for relaxed concurrency.

The tutorial should be accessible to both beginners and experts alike. In particular, no knowledge of relaxed memory concurrency or separation logic will be assumed. More information about relaxed separation logic can be found at the following URL:

http://www.mpi-sws.org/~viktor/rsl/

Objectives: The attendees will learn how to write programs involving the recent C/C++ atomics, and how to reason about the correctness of such programs.

Additional material: [Tutorial slides]

Bio: Since October 2010, Viktor Vafeiadis is a tenure-track researcher at the Max Planck Institute for Software Systems (MPI-SWS) specializing on the verification of concurrent programs and compilers. He received his Ph.D. from the University of Cambridge and, prior to joining MPI-SWS, held post-doctoral researcher positions at the University of Cambridge and at Microsoft Research Cambridge. His Ph.D. dissertation developed RGSep, a program logic combining separation logic and rely-guarantee reasoning, and received the 2008 ACM SIGPLAN outstanding dissertation award.

Tutorial 2. An introduction to Rust

Presenter: Nicholas Matsakis, Mozilla Research

When/where: Monday 20 January, 11:00-12:30 and 16:00-17:30, Executive room

Abstract: Rust is a new programming language for developing reliable and efficient systems. It's designed to support concurrency and parallelism in building platforms that take full advantage of modern hardware. Its static type system is safe and expressive and it provides strong guarantees about isolation, concurrency, execution, and memory safety.

Rust combines powerful and flexible modern programming constructs with a clear performance model to make program efficiency predictable and manageable. One important way it achieves this is by allowing fine-grained control over memory allocation through contiguous records and stack allocation. This control is balanced with the absolute requirement of safety: Rust's type system and runtime guarantee the absence of data races, buffer overflow, stack overflow, or access to uninitialized or deallocated memory.

This tutorial introduces Rust with a focus on the advanced type system features. We begin by installing Rust and working through a variety of examples, beginning with simple type definitions and proceeding through Rust's approach to affine and region types.

Objectives: Introduce Rust syntax and concepts, with a focus on type system machinery for achieving memory safety and data-race freedom

Additional material: [Rust installation instructions] [Example]

Bio: Nicholas Matsakis is a senior researcher at Mozilla research. Before joining Mozilla, he completed a PhD under Thomas Gross at ETH Zurich. He focuses on safe support for parallelism in programming languages. He is currently working on the Rust programming language as well as Parallel JavaScript.

Tutorial 3. Architecture-agnostic compilation of high-level languages

Presenter: Dan R. Ghica, University of Birmingham

When/where: Monday 20 January, 09:00-10:30 and 14:00-15:30, Executive room

Abstract: Is it possible to compile conventional programming languages with the usual functional and imperative features on unconventional architectures? Or do we need to have an array of domain-specific languages (DSLs) for distributed architectures, reconfigurable architectures, client-server architectures, etc.? Is it possible, in a world of rapidly evolving architectures, to stick to the principles of machine-independent programming languages which revolutionized computing in the 1960s and 1970s and led to the introduction of FORTRAN, ALGOL, C, LISP, etc., or do we need to go back to a world where each computing device comes with its own specialized programming language?

The tension is, as it was in the 1960s and 1970s, between a belief that generic higher-level languages are inherently inefficient on the one hand, and the idea that such languages compensate any potential loss in computer efficiency by a much greater increase in programmer productivity. Beyond these quantitative concerns there is also now, as it was then, a general lack of awareness about the theoretical frameworks that can make possible the compilation (and optimisation) of machine-independent languages to specific machines.

In this hands-on tutorial we will see how to compile a simple functional language with concurrent and imperative features (Reynolds's Syntactic Control of Interference) to two unconventional architectures: reconfigurable circuits (FPGAs) and distributed platforms (via MPI). Throughout the tutorial the attendees will become exposed to the two main theoretical frameworks that make AAC compilation possible: sub-structural type systems and interaction-based (game) semantics.

Objectives: Following this tutorial the audience should be able to:

1. Understand the basic principles of architecture-agnostic compilation (AAC)
2. Be able to implement a simple AAC system for a functional programming language
3. Gain awareness of the way certain programming language features aid or hinder AAC
4. Use types to control resource usage
5. Become exposed to the theoretical underpinnings of AAC in game semantics

As this is an emergent research topic, the participants will be also exposed to a variety of open research problems.

Additional material: [Tutorial slides]

Bio: Dan R. Ghica is a Senior Lecturer in the School of Computer Science, University of Birmingham, UK, which he joined in 2005. Between 2006-2001 Dan was an EPSRC Advanced Research Fellow. Prior to joining Birmingham he was a Research Fellow in the Oxford Computing Laboratory. He obtained his PhD from Queen's University, Canada in 2002. His current research interests focus on the use of semantic and types-based methods for the compilation of conventional languages to unconventional architectures. In the last few years has been an invited speaker at LICS 2009, LOLA 2010, MEMOCODE 2011, MPC 2012, TGC 2012. Find out more about his research interests on his research blog, The Lab Lunch.

Tutorial 4. Principles and practice of session types

Presenters: Vasco T. Vasconcelos, University of Lisbon
Nobuko Yoshida, Imperial College London

When/where: Monday 20 January, 9:00-10:30 and 11:00-12:30, Presidential Salon D

Abstract: Session types have gone a long way since their introduction in the nineties. They are now to be routinely found on programming languages, on protocol description languages, associated with security issues, and web services. But what are session types? Presented by lead scientists on the field, this tutorial introduces the principles and the practice of a instrument that can no longer be dissociated from concurrent and distributed programming. Attendees will be exposed to the basic theory of session types, and will then be made to exercise the ideas with concrete tools used in educations and industries.

Objectives: At the end of the tutorial attendees will know what session types are, the different realms on which they may be useful, and how can they be used in disciplining concurrent and distributed computations. They will also become acquainted with two different tools, taken from a wide range of such applications currently available. Attendees will then be able to incorporate the concepts in the theory of session types into their own research.

Additional material: [Tutorial slides]

Bio: Vasco T. Vasconcelos is currently a full professor at the Department of Informatics, University of Lisbon where he has been lecturing since March 1996. He received the M.Sc. and Ph.D. degrees in computer science from Keio University (1992, 1995), and the habilitation title in informatics from New University of Lisbon (2003). His research work centers on programming languages for concurrent and distributed programming, type systems, process calculi, and specification and verification of computer systems.

Nobuko Yoshida is a professor of computing in Department of Computing, Imperial College London. From 2002, she has pioneered modelling and verifying web services and business protocols using the pi-calculus and session types and worked with several standardisation bodies via collaborations with industry partners. She was an official invited expert of the W3C standardisation for a Web Services Choreography Description Language (WS-CDL) with Robin Milner and Kohei Honda. Her current collaborators who are using Scribble include Ocean Observatories Initiatives, Red Hat, Cognizant and VMware.

Tutorial 5. Differential privacy: Language-based approaches

Presenter: Marco Gaboardi, University of Dundee

When/where: Monday 20 January, 14:00-15:30 and 16:00-17:30, Presidential Salon D

Abstract: Differential Privacy is becoming a standard approach in data privacy: it offers ways to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Many specific queries have been shown to be differentially private, but manually checking that a given query is differentially private can be both tedious and rather subtle. Moreover, this process becomes unfeasible when large programs are considered.

In this tutorial I will introduce the basics of differential privacy and some of the fundamental mechanisms for building differentially private programs. Additionally, I will present three different language-based approaches developed to help a programmer to certify his programs differentially private. The first approach is based on a simple program analysis; the second one on the use of type systems; finally, the third one on the use of relational Hoare logic implemented on top of a proof assistant.

Objectives: The attendees will learn the basics of differential privacy and the primary blocks that can be used to develop differentially private programs. They will also learn the state of the art programming techniques for ensuring programs differentially private.

Bio: Marco Gaboardi is a lecturer and Marie Curie fellow at the University of Dundee. He received his Ph.D. in Computer Science from the Università di Torino and the Institut National Polytechnique de Lorraine. Prior to joining the University of Dundee as a lecturer he was a research associate at the University of Torino, University of Paris Nord, University of Bologna and University of Pennsylvania. Marco's research interests center on the use of type systems to ensure strong program properties like: differential privacy, implicit complexity and resource consumption.

Tutorial 6. Semantics and verification for GPU kernels

Presenter: Nathan Chong, Imperial College London

When/where: Monday 20 January, 11:00-12:30 and 14:00-15:30, Sycuan room

Abstract: Semantics and Verification for GPU Kernels is a tutorial on recent and promising progress in the semantics and verification of massively-parallel GPU kernels. We will focus on how the theory, algorithms and tools of the verification community can be brought to bear on this interesting and important new domain. The tutorial will cover the formal semantics of GPU programs as well as domain-specific features and modelling techniques that can be exploited to make race-checking in this domain practical. Despite the parallel verification context we will show how the problem can be reduced to a sequential setting, therefore enabling scalable and automatic verification.

This tutorial is aimed at researchers and practitioners in software verification who would be interested in seeing how a practical implementation of automated Hoare Logic can be built using standard components in the verification community. These standard components include abstraction, invariant generation, the Boogie intermediate verification language, and SMT solvers. The tutorial will not assume a background in GPU programming.

Additional material: [Available here]

Bio: Nathan Chong is a researcher in the Department of Computing at Imperial College London, where he is a member of the Multicore Programming and Software Performance Optimisation groups, led by Alastair Donaldson and Paul H. J. Kelly, respectively. His research interests include parallel programming, computer architecture and formal reasoning, and is particularly interested in specifications and problems at the hardware/software boundary. He is a key contributor to GPUVerify, a verification technique and tool for the automatic analysis of GPU kernels written in OpenCL and CUDA. Before joining Imperial, Nathan was a researcher for ARM and worked on hardware and software at different levels of the system stack, including proofs of correctness for cache-coherence protocols, weak memory models, and CPU virtualisation. His work is supported by the FP7 CARP (Correct and Efficient Accelerator Programming) and EPSRC PSL (Particle Science Language) projects.