ECOOP Summer School
Controlling Mutation & Aliases with Fractional Permissions
John Boyland
Mutation and aliases are a hallmark of imperative concurrent programming but can lead to confusion and to hard-to-detect and hard-to-repat race conditions. Fractional permissions allow one to specify mutation and aliasing restrictions using both simple flow-insensitive and complex flow-sensitive reasoning. The talk introduces fractional permissions with practical motivation and then shows how they can be used to encode concepts such as uniqueness, ownership and effects. Then discussion will move into larger concepts such as object invariants, mutation control in iterators, synchronization and reasoning with Java's volatiles. The last part of the talk will open the floor for a general discussion on other mutation patterns to see how fractional permissions can be applied in new ways.
ECOOP
Time: 10:30–12:00, June 15
Room: Conference 8
John Boyland is an Associate Professor at the University of Wisconsin-Milwaukee. He does research in the verification of aliasing restrictions and in proof systems. He received his doctorate under the direction of Susan Graham at Berkeley in 1996 in the area of attribute grammars. He was a post-doctoral fellow at Carnegie Mellon.
C# formally
Gavin Bierman & Claudio Russo
C# is a modern, type-safe, OO language, designed for the Microsoft .NET platform. It has grown in popularity and is now in use by millions of developers around the world. But what sort of language is it? We prefer a precise, formal, mathematical answer. In this tutorial, we will show that C# can be given a formal description using familiar tools from the PL community: including subtyping by coercions, and type-directed and syntactic translations. We will show you how a middleweight core fragment can be formalized, and then how various C# extensions can be captured accurately; including LINQ (C# 3.0), dynamic (C# 4.0) and asynchronous programming (C# 5.0).
ECOOP
Time: 13:30–15:00, June 15
Room: Conference 8
Gavin Bierman is a senior researcher in the Programming Principles and Tools Group at Microsoft Research in Cambridge, UK. Prior to joining MSR, he was a faculty member at the University of Cambridge. He has a PhD from the University of Cambridge and a BSc from Imperial College, London. His interests include programming languages, database systems and big data.
Claudio Russo is a researcher in the Programming Principles and Tools Group at Microsoft Research in Cambridge, UK. He has a PhD and BSc from the University of Edinburgh and has worked on .NET generics, type systems for functional and object-oriented languages and concurrency abstractions.
Maxine: A Virtual Machine For, and In, Java
Christian Wimmer & Laurent Daynès
Writing a VM in Java makes it more approachable. VM implementation is facilitated by the palette of features supported by Java, most notably type and memory safety, garbage collection, exception handling, reflection, and annotations. The Maxine VM is a meta-circular VM implementation that aggressively uses these features. It is co-designed with a custom debugging companion tool, the Maxine VM Inspector, that combines inspection of a running VM image with debugging features. We believe that this approach makes Maxine one of the most approachable VMs, and therefore a good basis for academic research and teaching. Graal is the optimizing JIT that originated from the JIT compiler in Maxine, but is now a self-contained OpenJDK project and also integrated in HotSpot. We will present the architecture and design decisions behind Maxine and Graal, and give an introduction to the source code so that researchers can get started writing their own extensions and optimizations.
ECOOP
Time: 15:30–17:00, June 15
Room: Conference 8
Christian Wimmer is a researcher at Oracle Labs, working on the Maxine VM, on the Graal compiler project, as well as on other projects that involve dynamic compilation and optimizations. His research interests span from compilers, virtual machines, and secure systems to component-based software architectures.
Laurent Daynès is a member of the Maxine project at Oracle Labs. He is working on garbage collection and meta-circular implementation of virtual machine for modern programming languages. Prior to joining the Maxine project, he worked in the Barcelona project where he was the main contributor to MVM, the multi-tasking virtual machine.
Javascript's Meta-Object Protocol
Tom Van Cutsem
In this talk, we will give a fast-paced tutorial on the Javascript programming language. Subsequently, we introduce a new reflection API that will be added in the next standard edition of Javascript. This API enables Javascript programmers to create proxies, which are essentially objects with a customizable meta-object protocol. Proxies are a cornerstone technology enabling among others transparent sandboxing of applications, virtualizing browser APIs and language extensions such as higher-order contracts. By mastering this API, you will gain a better insight into the true nature of Javascript's object model.
ECOOP
Time: 8:30–10:00, June 16
Room: Conference 8
Tom Van Cutsem is a researcher at the Vrije Universiteit Brussel, Belgium. He finished his PhD in 2008 on the topic of AmbientTalk, a distributed object-oriented scripting language for mobile phones. Since 2010, he serves on the ECMAScript standardization committee, where he designed the Javascript Proxy API in close collaboration with Mark S. Miller (Google).
Abstract Reasoning about Concurrent Modules
Philippa Gardner
Reasoning about concurrent programs has long been recognised as challenging. Whereas programmers understand how to think modularly about programs, the reasoning has not matched this modular thinking. Abstraction is the key to modular reasoning. I will describe recent work on program logics for reasoning abstractly about concurrent modules. This work is part of a stream of work on local reasoning about concurrent programs, initiated by the work on concurrent separation logic. Concurrent separation logic provides course-grained reasoning about concurrent modules, for example reasoning about a whole set. RGSep and deny-guarantee reasoning provides fine-grained reasoning about, for example, elements of the linked list, but cannot abstract to fine-grained reasoning about elements of a set. I will describe recent work on fine-grained abstract reasoning about concurrent modules, using recent work by myself and others on concurrent abstract predicates and views.
ECOOP
Time: 10:30–12:00, June 16
Room: Conference 8
Philippa Gardner is a Professor at Imperial College London. Her work unifies a range of research areas, including program verification, logic, concurrency, databases and the Web. She previously held a Microsoft/Royal Academy of Engineering Senior Research Fellowship at Imperial at Cambridge working on process models with Robin Milner. She completed a PhD on type theory and logical frameworks at Edinburgh, supervised by Gordon Plotkin.
The Scandinavian Approach
Ole Lehrmann Madsen
SIMULA, the first OO language, was originally motivated by problems in operational research and simulation. The aim of providing a language for modeling as well as programming was also a major goal in the design of BETA. In BETA, language mechanisms such as class and method were unified into the pattern mechanism; the notion of virtual pattern (class) was introduced just as BETA further developed the SIMULA notion of quasi-parallel systems into full concurrency. In addition, a conceptual framework for proving a basis for OO modeling was developed. Current mainstream languages for modeling and programming are diverging. On one hand developers who would like to apply OO design to obtain a suitable model end up with the challenge of maintaining both model and program artifacts. And, since many modeling languages are at the same level of abstraction as programming languages, there is little benefit to using a separate modeling language. On the other hand we see that developers write a considerable amount of code with little appreciation of design and development disciplines. In the talk I describe the Scandinavian approach to OO, including lessons from SIMULA and BETA, the approach to object-oriented modeling, the associated conceptual framework, as well as problems and issues related to OO modeling and programming.
ECOOP
Time: 13:00–15:00, June 16
Room: Conference 8
Ole Lehrmann Madsen is a Professor of Computer Science at Aarhus University, and managing director of the Alexandra Institute Ltd. — a non-profit company doing application-oriented research within ICT in partnership with universities, companies and public institutions. He has worked with object-technology for more than 25 years starting with Simula programming. He developed the BETA programming language together with Kristen Nygaard, Birger Møller-Pedersen and Bent Bruun Kristensen.