Paper Accepted at Coordination 2016

Standard

An Interference-Free Programming Model for Network Objects by Mischael Schill, myself, and Bertrand Meyer was accepted for publication at the 18th IFIP International Conference on Coordination Models and Languages (COORDINATION 2016).

Network objects are a simple and natural abstraction for distributed object-oriented programming. Languages that support network objects, however, often leave synchronization to the user, along with its associated pitfalls, such as data races and the possibility of failure. In this paper, we present D-SCOOP, a distributed programming model that allows for interference-free and transaction-like reasoning on (potentially multiple) network objects, with synchronization handled automatically, and network failures managed by a compensation mechanism. We achieve this by leveraging the runtime semantics of a multi-threaded object-oriented concurrency model, directly generalizing it with a message-based protocol for efficiently coordinating remote objects. We present our pathway to fusing these contrasting but complementary ideas, and evaluate the performance overhead of the automatic synchronization in D-SCOOP, finding that it comes close to—or outperforms—explicit locking-based synchronization in Java RMI.

Paper postprint (.pdf)

Paper postprint (.pdf)

Paper Accepted at FASE 2016

Standard
FASE at ETAPS 2016

FASE at ETAPS 2016

A Graph-Based Semantics Workbench for Concurrent Asynchronous Programs by Claudio Corrodi, Alexander Heußner, and myself was accepted for publication at the International Conference on Fundamental Approaches to Software Engineering (FASE 2016).

A number of novel programming languages and libraries have been proposed that offer simpler-to-use models of concurrency than threads. It is challenging, however, to devise execution models that successfully realise their abstractions without forfeiting performance or introducing unintended behaviours. This is exemplified by SCOOP—a concurrent object-oriented message-passing language—which has seen multiple semantics proposed and implemented over its evolution. We propose a “semantics workbench” with fully and semi-automatic tools for SCOOP, that can be used to analyse and compare programs with respect to different execution models. We demonstrate its use in checking the consistency of semantics by applying it to a set of representative programs, and highlighting a deadlock-related discrepancy between the principal execution models of the language. Our workbench is based on a modular and parameterisable graph transformation semantics implemented in the GROOVE tool. We discuss how graph transformations are leveraged to atomically model intricate language abstractions, and how the visual yet algebraic nature of the model can be used to ascertain soundness.

Paper postprint (.pdf)

Paper postprint (.pdf)

Presentation slides (.pdf)

Presentation slides (.pdf)

Paper Accepted at GPCE 2015

Standard
GPCE 2015

GPCE 2015

Contract-Based General-Purpose GPU Programming by Alexey Kolesnichenko, myself, Sebastian Nanz, and Bertrand Meyer was accepted for publication at the International Conference on Generative Programming: Concepts and Experiences (GPCE 2015).

Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. The solution is integrated with the design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into the program text. We show that our library leads to modular and maintainable code that is accessible to GPGPU non-experts, while providing performance that is comparable with hand-written CUDA code. Furthermore, runtime contract checking turns out to be feasible, as the contracts can be executed on the GPU.

Paper postprint (.pdf)

Paper postprint (.pdf)

Paper Accepted at F-IDE 2015

Standard

The AutoProof Verifier: Usability by Non-Experts and on Standard Code by Carlo A. Furia, myself, and Julian Tschannen was accepted for publication at the Formal Integrated Development Environment Workshop (F-IDE 2015).

Formal verification tools are often developed by experts for experts; as a result, their usability by programmers with little formal methods experience may be severely limited. In this paper, we discuss this general phenomenon with reference to AutoProof: a tool that can verify the full functional correctness of object-oriented software. In particular, we present our experiences of using AutoProof in two contrasting contexts representative of non-expert usage. First, we discuss its usability by students in a graduate course on software verification, who were tasked with verifying implementations of various sorting algorithms. Second, we evaluate its usability in verifying code developed for programming assignments of an undergraduate course. The first scenario represents usability by serious non-experts; the second represents usability on “standard code”, developed without full functional verification in mind. We report our experiences and lessons learnt, from which we derive some general suggestions for furthering the development of verification tools with respect to improving their usability.

Paper postprint (.pdf)

Paper postprint (.pdf)

Presentation slides (.pdf)

Presentation slides (.pdf)

Paper Accepted at GaM 2015

Standard
GaM 2015

GaM 2015

Towards Practical Graph-Based Verification for an Object-Oriented Concurrency Model by Alexander Heußner, myself, Claudio Corrodi, and Benjamin Morandi was accepted for publication at the Graphs as Models Workshop (GaM 2015).

To harness the power of multi-core and distributed platforms, and to make the development of concurrent software more accessible to software engineers, different object-oriented concurrency models such as SCOOP have been proposed. Despite the practical importance of analysing SCOOP programs, there are currently no general verification approaches that operate directly on program code without additional annotations. One reason for this is the multitude of partially conflicting semantic formalisations for SCOOP (either in theory or by-implementation). Here, we propose a simple graph transformation system (GTS) based run-time semantics for SCOOP that grasps the most common features of all known semantics of the language. This run-time model is implemented in the state-of-the-art GTS tool GROOVE, which allows us to simulate, analyse, and verify a subset of SCOOP programs with respect to deadlocks and other behavioural properties. Besides proposing the first approach to verify SCOOP programs by automatic translation to GTS, we also highlight our experiences of applying GTS (and especially GROOVE) for specifying semantics in the form of a run-time model, which should be transferable to GTS models for other concurrent languages and libraries.

Paper postprint (.pdf)

Paper postprint (.pdf)

Lessons of Wirth on his 80th Birthday

Standard

With colleagues from the Chair of Software Engineering, I had the great pleasure of organising the recent symposium in honour of Professor Niklaus Wirth’s 80th birthday. Likely you will have some familiarity with – if not his name – his many contributions to computer science, which this quote from the symposium website quite nicely summarises:

Niklaus Wirth mid-presentation (Photo credit: Julian Tschannen)

Niklaus Wirth mid-presentation (Photo credit: Julian Tschannen)

Niklaus Wirth was a Professor of Computer Science at ETH Zürich, Switzerland, from 1968 to 1999. His principal areas of contribution were programming languages and methodology, software engineering, and design of personal workstations. He designed the programming languages Algol W, Pascal, Modula-2, and Oberon, was involved in the methodologies of structured programming and stepwise refinement, and designed and built the workstations Lilith and Ceres. He published several text books for courses on programming, algorithms and data structures, and logical design of digital circuits. He has received various prizes and honorary doctorates, including the Turing Award, the IEEE Computer Pioneer, and the Award for outstanding contributions to Computer Science Education.

The symposium was held as a full-day scientific event with an impressive array of invited speakers, opening with “father of the Internet” Vint Cerf, and closing with Niklaus Wirth himself. Many of the speakers in-between were former PhD students of Wirth, but even the ones that weren’t had clearly been influenced by him throughout their careers; whether by his overarching stride for simplicity and clarity, or by the scientific insights that his papers so eloquently conveyed.

Carroll Morgan on "Stepwise refinement: from common sense to common practice" (Photo credit: Julian Tschannen)

Carroll Morgan on “Stepwise refinement: from common sense to common practice” (Photo credit: Julian Tschannen)

Of the latter, Carroll Morgan gave a wonderful talk that traced the influence of Wirth’s 1971 paper, Program Development by Stepwise Refinement. This paper put into words a principle that today would seem like common sense – that programs can be constructed by repeatedly refining tasks into subtasks that gradually approach executable instructions of the language. This insight subsequently inspired a rich mathematical exploration; a journey over four decades that Morgan’s presentation then illustrated for us. He concluded with some principles of his own behind his experimental undergraduate course, (In-)formal methods: The lost art: that students should be positioned to want to hear about the conceptual tools (and ways of thinking) of formal refinement. That they should be subjected to the pain of programming – exercises with which they will struggle and whose solutions will not satisfy them. To paraphrase: create a hole in their brains, then fill it with the conceptual tools that do the same job but with the elegance and satisfaction that the first attempts missed – only then will these tools find appreciation.

Simplicity, elegance, and clarity in language design – as promoted by Wirth – formed perhaps the most recurring theme of the day, with several of the speakers elaborating on how it guided their own work; from Clemens Szyperski’s at Microsoft on designing query languages for non-developers, to Hans Eberle’s at Oracle on designing minimalistic network switches and processors. The latter of these two presentations included a quote – due to Antoine de Saint-Exupéry – that seemed to really capture this aspect of the event:

“You know you’ve achieved perfection in design, not when you have nothing more to add, but when you have nothing more to take away.”

Bertrand Meyer too addressed the theme of simplicity in language design, but advocated instead a somewhat contrasting view: that good languages are the ones built around and consistent to a productive central metaphor; that languages should evolve in the direction of “less surprise”. He illustrated his principle through (of course!) the object-oriented language Eiffel – with more than a few little entertaining digs at the likes of C++.

The final session of the symposium concluded with a presentation from Wirth himself, who elaborated on his recent work to revive and revise Project Oberon, his 1992 book that described the entirety of the Oberon language and operating system. These recent efforts included the designing of his own processor, the construction of a new compiler and linker, and the subsequent rewriting of much of his book; this revival offering an opportunity for engineering education (an up-to-date description of an entire operating system, all the way down to the processor). Wirth’s final slide – included below – summarised the lessons of his long career in computer science, and was followed by a very warm standing ovation.

The lessons of Niklaus Wirth's career

The lessons of Niklaus Wirth’s career

With this short post I have only attempted to convey the general spirit of this special event; there were very many more “Lessons of Wirth” (yes, there’s a terrible pun here if you know of the call-by-name/value anecdote) to take away from the presentations – both from those that I mentioned and those that I didn’t. Should you happen to have a few spare moments, then I would highly recommend exploring the materials we have just put online: video recordings (of all of the talks), as well as some slides (for a few).