Tobias Wrigstad @ Uppsala
Static checking of thread-locality for Java-like languages.
Uppsala Programming for Multicore Architectures.
The Thorn Programming language.
> If you turn your back on science, it'll take > you from behind -- Dr. Tiki CURRENTLY OPEN POSITIONS:
* 1-2 PhD positions in the UpScale project * 1 Postdoc position in the UpScale project
Below is an introduction to some of my award-winning work on object-oriented programming, scripting, etc.
My main body of work falls withing the field of alias management. Aliasing, the fact that an object can be multiply referenced, is inherent in object-oriented programming. When combined with mutable state and stable object identities, aliasing introduces problems for local reasoning. Object-oriented programs are constructed from complex graphs of millions of object nodes communicating via reference edges. Object nodes are created and destroyed frequently, as well as reference edges. If two unrelated objects references a common object, they can affect each other accidentally, and it is impossible to reason about the correctness of one of them without also considering the other.
My research on alias management does not attempt to ban aliasing, but control their effect, and capture aliasing constraints in program code. Program annotations allow programmers to capture aliasing constraints in the code, and code can be automatically checked for violations of these constraints, statically. On a high-level, this work is about constraining the possible shapes of object graphs to facilitate reasoning (manual or automatic) without overly reducing expressiveness.
I've done early work on read-only capabilities [SW01,SW02] which separate the right to reference another object from the right to modify it. Consequently, it is possible to express aliasing situations where data can be read by others but not modified.
Ownership types, created by Dave Clarke et al. in 1998, allows the isolation of a subgraph in the object graph dominated by a single node, which establishes an easily identified boundary of objects which must be considered when doing verification. The constraints imposed by ownership types are sadly too strong for most programs, which is tackled by my work. For my thesis work, I developed a system for safely moving objects between isolated subgraphs without breaking their respective isolation [CW03a,CW03b,Wrigstad 06, Wrigstad 04]. Together with Johan Östlund I developed systems for allowing subgraphs which are multiply dominated in tractable ways [OW11a,OW12] or split further [OW11b]. With Nick Cameron and James Noble, I developed a way in which different annotations systems, with different constraints on the object graph can be plugged into a program effortlessly [CNW10]. With Dave Clarke, I extended ownership to work with type specialisation without incurring run-time overheads [WC07].
with Johan Östlund, Dave Clarke and Beatrice Åkerblom, I have worked on combining capabilities and ownership [OWCA07,OWCA08] in ways which allows flexible alias management: read-only lists of mutable objects, mutable lists of read-only objects, etc.
I am an active and opinionated [WC11] member of the research community in this field and have served on the PC of the flagship conferences and workshops in the area, (e.g., ECOOP, OOPSLA, IWACO, and FTfJP) and sit on the steering committee of IWACO — the international workshop on aliasing, ownership and confinement. My current undertaking in this area is that of generalisation and unification of existing systems, and the development of a unified theory of alias management.
Scripting languages are a class of programming languages suitable for prototyping. Scripting languages are highly dynamic and allow executing complete subparts of unfinished programs, do not require lengthy recompiles following changes, and provide powerful programming abstractions focussed on programmer productivity rather than performance. However, when scripts “grow up”, they must be transitioned into programs which not only allow expressing high-performing data structures and algorithms, but also facilitate bug finding and maintaining code. The way this is currently done is either by rewriting the script from scratch in a systems' programming language, or not at all.
There are many examples of scripts that have outgrown themselves. An example relevant for Sweden is the Swedish Pension Agency (Pensionsmyndigheten) who manages premium pensions for all Swedish citizens in Pluto, a program written in Perl. The critical nature of all operations in this program forced the developers to develop a performance-heavy system for checking input and output values of functions at run-time, moving the running time of the batch system ever closer to the 24 hour window in which operations had to complete. However, due to rapidly changing legislation which introduced fixed, law-bound deadlines, staying with Perl was strategically important.
My work in this area started during my postdoc at Purdue and concerns the integration of scripting and systems' languages. Together with IBM TJ Watson Research, the Purdue team developed the Thorn programming language [WORVBFNS10,WEFNV09], which approached scripting from a systems' language perspective with the ultimate goal of allowing developing script prototypes which could be incrementally transitioned into programs within a single language. In the same context, I was part of a team including my great friend Francesco Zappa Nardelli to develop a novel type system for integrating typed and untyped code [WZNLOV10], something which is imperative for allowing the aforementioned incremental transition.
I am a frequent reviewer of work in this area on flagship conferences and workshops (e.g., ECOOP, OOPSLA, POPL, DLS), and have served on the PC on e.g. the Dynamic Language Symposium and STOP. I am a founder and steering committee member of the STOP workshop. My current work in this area is studying the dynamic behaviour of Python programs. In the future, I hope to study software engineering aspects of working with scripting languages, and how to enrich systems' language with features that will benefit prototyping and rapid application development.
Parallel programming is becoming increasingly important following the transition to multicore CPUs. Correct parallel computation is famously difficult, and also an under-studied field of science where serial computation has been prevalent until recently.
In the area of object-oriented programming, the standard way of expressing parallel computation is by multiple threads with a shared memory, and the de facto standard way of synchronising object accesses is by using various locks. This is brittle, and code using locks suffers in compositionality, since locking behaviours are hidden deep inside data structures and unfortunate object combinations, and unfortunate thread inter-leavings, can cause deadlocks and data races that lead to a wealth of problems.
Together with my collaborators, I have developed two programming systems for facilitating parallel programming in object-oriented languages. The Loci system [WPMZV09] allows a programmer to express what parts of a computation takes place within a single thread, which avoid locking, simplifies garbage collection and allows sequential reasoning about program behaviour. The Joelle system [CWOBJ08a,CWOBJ08b] departs from the standard thread-model by partitioning a program into several isolated objects executing in parallel and communicating asynchronously. As a result, deadlocks and races cannot take place due to low-level thread interleaving, and all code can be reasoned about sequentially.
With Johan Östlund, I am currently further developing the Joelle system and bringing in results from my work on ownership to allow the system to automatically deduce when computations could be run in parallel without breaking the sequential reasoning model. By basing our work on the Java language, we hope to provide a migration path to a safer parallel programming model for existing Java code. The keys are safety, expressiveness and determinism.
Pluggable type systems, proposed by Bracha in 2004, are type systems which can be added and removed from a program at different stages of development, for specific program parts, or specialised domains, which restricts the class of valid programs without altering their run-time semantics. Many research papers in the aforementioned fields (e.g. alias management) are presented as type system extensions on-top of a class-based statically typed object-oriented programming language. The lack of a standard semantics however make papers hard to read and results hard to combine, since they are expressed in seemingly incompatible models. One recent popular standard semantics, Featherweight Java, encodes Java as a functional language, which makes many matters simple, but obscure many of the most important features of object-oriented programming: aliasing, shared mutable state and side-effects. I have developed Welterweight Java [OW10] which stays true to the imperative core of Java, and models these important features.
As future work, I want to make a simple mechanised proof for Welterweight Java available to promote mechanised proofs for “product line type systems”.
Virtual classes provide a powerful means of extending programs without creating unfortunate opportunities for errors introduced by subtyping, among other things. Furthermore, it allows capturing object relations, such as “this point belongs to this grid, and that point belongs to that grid” in a statically enforceable manner which can avoid programmer mistakes and make code easier to read. Virtual class systems are however extremely complicated to formalise, esp. with respect to proving completeness. I have developed the Tribe system [CDNW07] which simplifies existing formal treatments of virtual classes, which leads to increasingly expressive types and naturally ties in with expressing aliasing properties [CNW10].
MIC, Room 1338 Visiting hours: send me an email to make an appointment Department of Information Technology Polacksbacken (Lägerhyddsvägen 2) 751 05 Uppsala SWEDEN Last modified 2010-06-24 09:15 GTM+1