POPL 2011 PC Workshop

Sunday, October 3, 2010

Computer Science Instructional Center, Room 1122
University of Maryland, College Park


Directions

Here are directions to the CS department at UMCP. We will have the meeting in room 1122 of the Computer Science Instructional Center (CSIC). Here is location information on CSIC. Click the "Find on the map" link to see a campus map to the building. Here are floorplans of CSIC. You can park in the CSIC lot on Sunday.


Agenda

Arrival and Coffee: 9:00-9:30

Session 1: 9:30-10:20
Oege de Moor (Oxford University Computing Laboratory)
TBA

Philippa Gardner (Imperial College, London)
Abstraction and refinement in Local Reasoning

Break: 10:20 - 10:45

Session 2: 10:45 - 12:00
Sumit Gulwani (Microsoft Research)
Program Synthesis for End-users and Education

Eran Yahav (IBM Research)
TBA

Anders Moeller (Aarhus University)
Analyzing JavaScript Web Applications

Lunch: 12:00 - 1:30

12:45-1:30 - Discussion, "What can we do better to make POPL/PLDI more relevant for the next generation"? Led by Sumit Gulwani.

Session 3: 1:30 - 2:45

Jan Vitek (Purdue University)
Real-time Garbage Collection it's easy as 1, 2, 3

G. Ramalingam (Microsoft Research)
Safe Programmable Speculative Parallelism

Peter Mueller (ETH Zurich)
Verification of Concurrent Programs in Chalice

Break: 2:45 - 3:10

Session 4: 3:10-4:00
Naoki Kobayashi (Tohoku University)
Model-Checking Higher-Order Programs

Hongseok Yang (Queen Mary, University of London)
Abstraction for Concurrent Objects


Abstracts


TBA
Oege de Moor (Oxford University Computing Laboratory)


Abstraction and refinement in Local Reasoning
Philippa Gardner (Imperial College, London)

Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state. We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations. We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level `fiction' of locality.

This is joint work with Thomas Dinsdale-Young and Wheelhouse.


Program Synthesis for End-users and Education
Sumit Gulwani (Microsoft Research)

There has been recent surge in research on program synthesis techniques and they been applied successfully to scenarios such as discovery of new algorithms and easing of software development tasks. However, the most revolutionary potential of program synthesis (coupled with advances in natural language processing and human computer interaction) can be in the areas of automating end-user programming and automating education. The former can enable non-programmers to realize their creative potential by programming computational devices using natural intent expression mechanisms such as examples and natural language. The latter can lead to development of automated problem solving technology that can give hints to students in problem solving, help generate new problems of a measured difficulty level, automatically grade solutions, point out errors, suggest fixes, etc. In this talk, I will describe the role that logic, PL, and synthesis are set to play in these inter-disciplinary initiatives.


Model-Checking Higher-Order Programs
Naoki Kobayashi (Tohoku University)


Analyzing JavaScript Web Applications
Anders Moeller (Aarhus University)


Verification of Concurrent Programs in Chalice
Peter Mueller (ETH Zurich)


Safe Programmable Speculative Parallelism
G. Ramalingam (Microsoft Research)

In this talk, we consider the use of speculation, by programmers, as an algorithmic paradigm to parallelize seemingly sequential code. Execution order constraints imposed by dependences can serialize computation, preventing parallelisation of code and algorithms. Speculating on the value(s) carried by dependences is one way to break such critical dependences. We present language constructs that enable programmers to declaratively express speculative parallelism in programs. In general, speculation requires a runtime mechanism to undo the effects of speculative computation in the case of mispredictions. We describe a set of conditions under which such rollback can be avoided. We utilize a static analysis to check if a given program satisfies these conditions to enable safe use of these constructs without the overheads required for rollback.


TBA
Eran Yahav (IBM Research)


Real-time Garbage Collection it's easy as 1, 2, 3
Jan Vitek (Purdue University)

In this talk, which I intend to be at a tutorial level, I will argue that a high-performance real-time garbage collection algorithm can be assembled out of three simple techniques: (1) copying replication, (2) fragmented allocation, and (3) concurrent mark-region.


Abstraction for Concurrent Objects
Hongseok Yang (Queen Mary, University of London)

Concurrent data structures are usually designed to satisfy correctness conditions such as sequential consistency and linearizability. The purpose of this talk is to explain our answer to the following fundamental question: what guarantees are provided by these conditions for client programs? In the talk, I will focus on linearizability, and explain how linearizability can be understood in terms of abstraction of dependency between computation steps of client programs. With this new understanding, I will then show that linearizability is equivalent to observational refinement.

This is joint work with Ivana Filipovic, Peter O'Hearn and Noam Rinetzky.