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)

Bidirectionality and How to Fake It

Standard

The general problem of maintaining consistency between two related sources of information is recurrent across computer science, surfacing in communities as diverse as database management (e.g. the construction of updatable views for relational databases), programming languages (e.g. invertible computations), and model-driven engineering (e.g. synchronising views of software models). The various mechanisms constructed for solving these problems and maintaining consistency have, collectively, become known as bidirectional transformations (BX), and the last decade has seen several cross-discipline initiatives to study the common challenges and underpinnings; most notably the GRACE-BX meeting in 2008 and the BX wiki and workshop series.

Some months ago (and almost certainly in one of York’s fine pubs), Richard Paige, Mike Dodds, Arend Rensink and I turned our attention to the buzz surrounding BX in one particular subcommunity: that of model transformations. This is a community concerned with making models first-class engineering artefacts, manipulated by automatic consistency-preserving translations (i.e. model transformations). Intuitively, these models could be system views at different levels of abstraction (perhaps all the way down to code), with model transformations the means of linking them, and consistency a property satisfied if all the models actually are views of the same system. These transformations are typically unidirectional, in the sense that they can translate a source model S into a target model T – but not a T into an S. It’s often quite fine that a transformation cannot do this; the reverse direction is not necessarily interesting or useful (who modifies compiled code and expects the source files to be updated?). But often it is: for example, in integrating separately-modelled systems that must be consistent; or in the database view problem, where low-level users are modifying restricted views of a database, while administrators are concurrently querying and modifying a model of the entire thing.

BX support concurrent engineering activities

BX support concurrent engineering activities

Bidirectional model transformations (BX) that solve such problems simultaneously describe transformations in both directions – from S to T and T to S – and are consistency-preserving by construction. This property makes BX scientifically fascinating (for myself and many others), but whether they are a productive means of solving problems in model-driven engineering is quite another issue. The inherent complexity that BX must encode make them very difficult to implement; so much so, that many transformation languages do not support them at all, or do so with strings attached and severe restrictions (e.g. bijective transformations only). Perhaps worse, while the QVT-R language (part of an OMG standard) does support them, it does so with an ambiguous semantics and limited tool support.

At some point, one starts to ask: does the difficulty in expressing and executing BX actually outweigh the practical benefits arising from their consistency guarantees? And if engineers aren’t writing BX to solve the problems that they are intended to solve… what are they writing instead? For the latter question, the answer is typically “pairs of unidirectional transformations”. These are certainly easier to write than BX, and a pair of transformations could still maintain consistency; but the emphasis here is on could – we lack the guarantee. Arend, Mike, Richard and I, however, began to wonder whether this could be automatically checked. And we were not alone:

“If a framework existed in which it were possible to write the directions of a transformation separately and then check, easily, that they were coherent, we might be able to have the best of both worlds.” — Perdita Stevens

We have come to believe that the Epsilon family of model management languages has all of the ingredients necessary to facilitate such checks. BX can be “faked” in Epsilon as pairs of update-in-place transformations that separately manipulate the source and target models, with an inter-model constraint expressing precisely what it means for the two models to be consistent. The idea is that immediately after an update of the source (resp. target) model, the constraint is violated, and the corresponding update of the target (resp. source) model is triggered. We claim that a fake BX in this sense is indistinguishable from a true BX, if it can be proven that the constraint is invariant under executions of the transformations in both directions. Furthermore, we conjecture that we will be able to check this, automatically, using rigorous proof techniques adapted from graph rewriting.

We explored these ideas further in our short paper, Towards Rigorously Faking Bidirectional Model Transformations, presented by Richard on our behalf at AMT 2014. We applied them successfully to a small conceptual example, but whether they work more generally, and prove to be a practical alternative to true BX, remains to be evaluated. We are certainly on the case, but would appreciate your thoughts, suggestions, and criticisms in the meantime.

Paper postprint (.pdf)

Paper postprint (.pdf)

Presentation slides (.pdf)

Presentation slides (.pdf)

Verifying Graph Transformations: Paths, Bipartiteness, and Beyond

Standard

For several years I have maintained an interest in graph transformation, which combines the strengths of graphs and rules into a single, abstract computational model. In this setting, the state of a computation is represented as a graph, and the computational steps are applications of graph rewrite rules (akin to applications of rules in Chomsky string grammars, but lifted to the richer domain of graphs).

Some rules, a program, and an example execution

Some rules, a program, and an example execution

Consider for example the figure to the right, which contains a set of rules, a program constructed over them, and an example execution on the empty graph Ø. Even without giving the formal semantics, it may already be clear – simply from the graphical nature of the rules – that executing the program on the empty graph will construct a tree. Such an execution will apply the rule init exactly once, which dutifully (and unconditionally) creates a fresh node. Then, as demanded by the iteration construct !, the rule grow is repeatedly and nondeterministically applied until some (unspecified) termination condition is satisfied. Each application of this rule requires a node in the graph to be matched (the number establishes which node on the right-hand side is the same one), before gluing onto it an outgoing edge and fresh node. Observe that no matter how many times (if any) the rule grow is applied, the property – or rather, invariant – of being a tree is maintained.

But how do we prove that this invariant is maintained? Or more generally, how do we verify that a program based on graph transformation is correct with respect to a given specification? One might wonder at this point whether this question is even worth answering – but to see that it is, we must look somewhat beyond our tree-generating program, which on its own, fails to convey the power and flexibility of graph transformation. Correctness counts in many of its more practical applications throughout computer science and software engineering: from the semantics and implementation of functional programming languages, to the specification and analysis of pointer structures, object-oriented systems, and model transformations.

Research in verifying graph transformations broadly belongs to one of two camps: model checking or proofs. Although the former is supported by some excellent tools (GROOVE being amongst my favourites), it is also important to explore the latter, which involves the use of logic, semantics, and proof calculi to unequivocally show that programs satisfy their specifications. The seminal work here is due to Karl-Heinz Pennemann, who paved the way to automatic correctness proofs with respect to a logic of first-order graph properties; the theory of which my thesis extended to attribute-manipulating rules.

First-order logic is too weak for graphs

First-order logic is too weak for graphs

Unfortunately, the restriction to first-order properties is quite a limiting factor in the context of graphs. In particular, it excludes the possibility of verifying so-called “non-local” properties, of which there are many familiar and important ones: the existence of arbitrary-length paths, the absence of cycles, connectedness, and bipartiteness; to name just a few. Without paths or cycles, what can we prove of interest about our tree-generating program? And in a more practical setting, it is easy to conjure scenarios in which we will suffer. How might we prove the absence of deadlock, for example, in a model of some distributed algorithm, when we cannot reason about the absence of cycles?

Detlef Plump and I set out to address this limitation in our recent paper, Verifying Monadic Second-Order Properties of Graph Programs. First, we extended Pennemann’s logic for graphs to one equivalently expressive to monadic second-order (MSO) logic – a logic very well studied in the context of graph structure (most famously by Bruno Courcelle and his colleagues). The extension allows one to quantify over sets of nodes or edges, and assert that particular nodes or edges belong to particular sets. While a conceptually simple extension, it is rather a powerful one, allowing for a large class of important non-local properties to be expressed – including all of those listed above. Then, and most importantly, we showed that the logic can be integrated into proof systems by defining, and proving correct, an effective weakest precondition construction relative to arbitrary rules and postconditions.

The paper is primarily a theoretical contribution, demonstrating (for the curious!) that this weakest precondition construction can be extended to an MSO-based graph logic. Unfortunately, all but the most trivial formulae of this logic are difficult for users to write and interpret, and the constructed preconditions are not particularly concise. A more practical approach for verification – that the paper also begins to explore – might be to work with a set of more “direct” predicates for particular non-local properties of interest, rather than full MSO. The paper, for example, explores a predicate for expressing the existence of an arbitrary-length path between two given nodes; an important non-local property, but non-trivial to specify in MSO logic. We were particularly pleased to discover that we could define the weakest precondition construction for such predicates entirely in terms of such predicates, i.e. without the need to introduce any set quantifiers.

We published and presented the work at ICGT 2014 (as part of STAF 2014) in York, UK, and would be glad to receive your comments and criticisms. The postprint and slides are available below, and the printed version can be downloaded from SpringerLink.

Paper postprint (.pdf)

Paper postprint (.pdf)

Presentation slides (.pdf)

Presentation slides (.pdf)

Petri Nets and True Concurrency

Standard

One of the first keynotes I had the pleasure of listening to as a doctoral student was given by Javier Esparza at SPIN/ICGT 2010. As a joint (or rather, parallel) meeting of the model checking and graph transformation communities, his lecture – A False History of True Concurrency – presented the key insights and developments in the history of a research area that was interesting for both: the so-called unfolding approach to model checking.

Unfoldings are a mathematical formalism that give a truly concurrent semantics to a system; that is to say, a partial-order semantics that identifies immaterial orderings of events – orderings that would otherwise be forced in concurrency defined by interleaving. They were interesting for the SPIN community as a means to alleviate state space explosion; interesting too for those at ICGT, with the technique having an analogous use in automatically verifying graph grammars. As a fresh-faced doctoral student, I was fascinated by the theory and applications that the talk examined; although I never got a chance to explore them in my own work.

A Petri net unfolding

A Petri net unfolding

I was delighted however to be able to revisit some of these ideas in the concurrency course that I teach at ETH (jointly with Sebastian Nanz and Bertrand Meyer). The second half of the course has traditionally focused on formal models and process calculi for concurrency, but has never covered the important mathematical modelling language of Petri nets; an omission that this year we addressed. In addition to covering the intuition needed for constructing and interpreting Petri nets, we also used them as a vehicle to compare a semantics based on interleaving and a semantics based on true concurrency, applying the unfolding technique directly to nets and discussing the implications for automatic analysis. Though the lecture is only short, and omits many important details (such as how to search for an appropriate finite prefix), I hope that it still might serve as a useful gentle introduction to Petri nets and true concurrency; hence this post to share it!

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).

Searching for Code Snippets in an IDE

Standard

When writing a program, developers of all skill levels routinely and repeatedly turn to search engines for answers to questions; questions like “how do I read a file line-by-line”, “read an RSS feed”, “calculate the difference between two dates”, “delete whitespace”. More generally, how do I do X, where X is a small programming task that someone – surely – has already done before, and probably already shared a solution to.

Enter the Code Snippet Search tool from Microsoft Research, now available to C# programmers as a Visual Studio add-on. It is the outcome of a research project that Yi Wei (a former member of our group who studied automated testing and fixing, and whose flat in Zürich I happened to takeover!) has been working on since 2011, and today is looking like a very promising tool. The basic idea is to streamline the process of finding reusable C# code snippets by integrating the experience into the Visual Studio IDE.

Automagically identifying, adapting, and inserting the code snippet that does the job

Automagically identifying, adapting, and inserting the code snippet that does the job

Accessed by triggering Visual Studio’s IntelliSense, the tool accepts queries in natural language (akin to the examples in my opening paragraph), processes them using Bing, then attempts to identify the most appropriate code snippet in an index built from MSDN, Stack Overflow, Dot Net Perls, and CSharp411 (taking into account various indications of quality, such as the number of votes from a particular community). Most impressively, the tool doesn’t just dump the identified code snippet and send you on your way; rather, it attempts to modify it to fit the variables and context of your program, with some reasonable success rates reported.

The Visual Studio blog has a nice overview of the technology alongside some screenshots of the add-on. If you want to see it in action without having to install the IDE, there is a web-based version (albeit with a slightly different interface) that you can play with, as well as a 2-minute video demonstration.

Support for other languages is planned to come later (I hope, apart from the obvious targets, that LaTeX finds its way onto the list!); but in the meantime, it will be interesting to observe how C# developers react to and use this technology in practice. Congratulations to Yi and his colleagues on their success!