Title: Automatic Verification of Message-Passing Concurrency

Speaker: Luke Ong (University of Oxford)

　　    www.cs.ox.ac.uk/people/luke.ong/personal

Time: 14:30, 24th April 2014

Venue: Lecture Room (334), 3rd Floor, Building #5, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences

Abstract:

We study the reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers, a model of computation for (message-passing) concurrency-oriented programming languages such as Erlang. Our goal is to relax the common restriction that messages can only be retrieved by a pushdown process when its call stack is empty. We introduce a new class of concurrent pushdown systems--Asynchronously Partially Commutative Pushdown Systems--with a shape constraint on the stacks for which the coverability problem is decidable. Stacks that satisfy the shape constraint may reach arbitrary heights; furthermore a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. This class extends previous computational models for asynchronous procedural calls, and enables the safety verification of a large class of recursively-defined message-passing programs.

This talk will begin with a survey of a recent project [1], Soter, to verify safety properties of Erlang programs by abstract interpretation and infinite-state model checking, and a discussion of the lessons learn. The rest of the talk describes an approach to address a source of imprecision of the Soter method, building on and extending [2]. This is joint work with Jonathan Kochems and Emanuele D'Osualdo.

[1] http://mjolnir.cs.ox.ac.uk/soter

[2] Jonathan Kochems, C.-H. Luke Ong: Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. CONCUR 2013: 288-302