Writing Interpreters for Dynamic Languages Using PyPy (and Getting Them Fast)

(Bristol, Sala Bellini)

Antonio Cuni, Università di Genova, Italy

Carl Friedrich Bolz, Armin Rigo, Heinrich-Heine-Universität Düsseldorf, Germany

We propose to give a tutorial on how to use the PyPy project to write interpreters for dynamic languages. PyPy supports compiling such interpreters to various target environments (like .NET or C/Posix) and automatically generating a Just-In-Time compiler for them. PyPy is thus an emerging tool to help implement fast, portable multi-platform interpreters with less effort.

Crystal-izing Sophisticated Code Analyses

(Palazzo Ducale, Sala Camino)

Ciera Jaspan, Kevin Bierhoff, Jonathan Aldrich, Carnegie Mellon University, USA

In recent years we have seen many researchers and practitioners build tools which statically analyze object-oriented programs. These code analyses have become incredibly sophisticated: they are often based on complex algorithms and type systems, require a dataflow analysis, use annotations, summaries, or other mechanisms to achieve precision in reasoning about method calls, and take advantage of conditional tests in the program or are even path-sensitive. These techniques typically interact with the language being analyzed in nontrivial ways. This makes it almost impossible to turn analyses into tools for widely used programming languages without support from an Integrated Development Environment (IDE) such as Eclipse or a code analysis frameworks like FindBugs. But the effort for the analysis writer is still high: IDEs facilitate interaction with the developer of the program being analyzed, but they provide no support for performing sophisticated analyses. On the other hand, code analysis frameworks typically do provide support for performing dataflow analyses, but interacting with the programmer becomes difficult. Additionally, the intricacies of dealing with a real language are generally left to the analysis writer, and popular techniques such as taking advantage of conditionals are not facilitated by many analysis frameworks. This tutorial presents our experience in writing static code analyses for Java using the Crystal analysis framework, which we developed and refined over the last four years. Crystal is itself a plugin to the Eclipse IDE and builds on Eclipse's well-tested AST. Thus its code base is relatively small and allows analysis writers to leverage the Eclipse platform where needed. Originally developed for teaching dataflow analysis techniques in a classroom setting, Crystal is built for simplicity. The interfaces are based upon the theoretical principles of static analysis and make it simple to transition from theory to prototype. In our experience, the framework allows rapid development of even sophisticated static analyses.

Flexible Task Graphs: A Framework for Experimental Real Time Programming in Java

(Palazzo Ducale, Sala Camino)

Joshua Auerbach, IBM Research, USA

This ECOOP 2009 tutorial will show how to use the newly available open-source Flexible Task Graphs (Flexotask) framework to develop real-time Java applications and as a test-bed for new ideas in real-time scheduling, and model-driven real-time programming. Participants interested in real-time will gain a tool that will be immediately useful in their own research. Participants who are merely curious about the emerging real-time support in Java will get a survey of the field (the Real Time Specification For Java, real-time garbage collection) followed by an in-depth look at "restricted thread programming models" for Java (Eventrons, Reflexes, Exotasks, StreamFlex, and especially Flexotask, which was designed to unify and subsume the others). The tutorial will be presented by Joshua Auerbach who will take overall responsibility. If available, one or more of Jan Vitek, Jesper Honig Spring, and/or David Bacon may assist.

Project Fortress: A Multicore Language for Scientists and Engineers

(Palazzo Ducale, Sala Camino)

Sukyoung Ryu, Jan-Willem Maessen, Sun Microsystems, USA

The computing world is currently undergoing dramatic changes. More powerful computers have brought high-performance computing (HPC), an endeavor historically relegated to national labs and government institutions, to the mainstream. At the same time, microchip manufacturers are designing new chips that contain increasing numbers of cores on a single chip to improve performance. Yet unfortunately, modern programming languages are ill-equipped for these changes. Most languages do not directly support any notion of parallelism and even languages with support for parallelism, such as the JavaTM Programming Language, support only course-grained notions of parallelism, best suited for tasks such as networking and GUI programming. Fortress is a new programming language designed for HPC with high programmability. It provides mathematical syntax to enable scientists and engineers to write programs in a notation they are accostomed to. It also provides built-in support for parallel programming. Fortress is designed for growth by community participation and development and its syntax and semantics have been formally designed and specified. This tutorial will introduce Project Fortress, which is an open-source project with a reference implementation of the Fortress programming language. Anyone who works on scientific programming, parallel programming, quality-critical software development, or open-source projects will find this tutorial of interest.

Program verification using the Spec# Programming System

(Palazzo Ducale, Sala Camino)

K. Rustan M. Leino, Microsoft Research, USA

Rosemary Monahan, National University of Ireland, Ireland

The Spec# Programming System consists of the Spec# programming language which is an extension of C#, the Spec# compiler which is integrated into the Microsoft Visual Studio development environment and the Spec# static program verifier which translates Spec# programs into logical verification conditions. The result is an automatic verification environment which establishes the correctness of a program before allowing it to be executed. In addition to the run-time checking traditionally found in the design by contract approach, Spec# offers the possibility to verify contracts statically. The goal of this analysis is to help programmers to detect errors more quickly than they might be found by traditional methods, hence providing an opportunity to correct the errors when they are still relatively cheap to fix. A unique feature of the Spec# Programming System is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads and interobject relationships. In addition, the Spec# Programming System has been extended so that programs that involve the mathematical domains that are so familiar to textbook examples (such as sum, count, product, min, and max) may be verified.

In this tutorial, we give an overview of the Spec# Programming System. We focus on writing programs and their specifications, so that users develop experience in verifying C# programs. Maintaining object invariants in the presence of callbacks, threads, and inter-object relationships will be presented with examples, exploring the more difficult aspects of program verification in an object-oriented environment.

Object Teams: Programming with Contextual Roles

(Palazzo Ducale, Sala Camino)

Stephan Herrmann, Technische Universität Berlin, Germany

From the early days of object orientation it is well-known that inheritance between classes and delegation between objects provide similar capabilities. While each approach has its specific strengths and limitations, only few programming languages support a combination of both. The concept of roles provides an excellent intuition for objects that are instances of a class and also delegate to a base or parent object. Early attempts of integrating the role concept into an object oriented language add accidental complexity to programs because one important property of roles had been neglected: roles depend on context. More recent languages thus reify the context in which roles live as "teams" (ObjectTeams/Java (OT/J)) or "institutions" (powerJava) etc. Of these languages OT/J is an excellent representative due to the maturity of the language and its tools. Steimann has identified 15 criteria from what various authors had considered relevant for the role concept. OT/J supports all 15 criteria. OT/J has been thoroughly integrated with Java, accounting for all relevant features of Java up-to version 6, as documented in the comprehensive language definition. Furthermore, team inheritance treats roles as virtual classes and fully implements the concept of family polymorphism, with additional options towards more strictness (in terms of object confinement) and towards more flexibility (in terms of migration between teams). For typesafe substitution of roles and bases, OT/J introduces translation polymorphism, realized by the implicit translations "lifting" and "lowering". With smart lifting a powerful mechanism is provided for mapping an inheritance hierarchy of base classes to a similar, but potentially different, hierarchy of role classes. Finally, several mechanisms for activating and deactivating a team support the notion that roles can be interpreted as a specific form of disciplined aspects, where aspect bindings utilize and extend the power of Java generics to overcome typing issues that have been identified in AspectJ. Summarizing, OT/J is a modern extension of the object oriented paradigm, borrowing from several approved concepts, combining all into a mature language. This language is supported by an industrial strength development environment based on and deeply integrated with the Eclipse JDT.

VeriFast: A Simple, Sound Verifier for Rich Separation Logic Contracts

(Palazzo Ducale, Sala Camino)

Bart Jacobs, Jan Smans, Katholieke Universiteit Leuven, Belgium

VeriFast is a program verification tool for single-threaded and multi-threaded C and Java programs that we are developing. Successful verification guarantees absence of hard to catch programming errors such as data races and memory leaks, as well as compliance with rich preconditions and postconditions specified by the programmer in source code annotations in a form of separation logic. To enable rich specifications, the programmer may define inductive datatypes, primitive recursive pure functions over these datatypes, and abstract separation logic predicates. To enable verification of these rich specifications, the programmer may write lemma routines, i.e., routines that serve only as proofs that their precondition implies their postcondition. The verifier checks that lemma routines terminate and do not have side-effects. The tool takes an annotated program as input and reports success or failure without further interaction. The tool verifies each function/method separately, by symbolic execution, where values are represented as terms of first-order logic with a set of equality and inequality constraints, and memory is represented as a separate conjunction of concrete and abstract elements. Since neither VeriFast itself nor the underlying SMT solver need to do any significant search, verification time is predictable and low. We have written and verified various example programs, including data-race-freedom of a small multithreaded chat server, and full functional correctness of a linked list implementation with iterators, a binary tree implementation, and an implementation of the Composite pattern. We have developed an IDE that allows the user to step through a failed symbolic execution path, inspecting the symbolic values of locals and the symbolic heap at each point.