Talk title: On verifying concurrent programs under weakly consistent memory models.
Abstract: Developing correct and performant concurrent systems is a major challenge. When programming an application over a memory/storage system, a natural expectation would be that each memory update is immediately visible to all concurrent threads, which means that the views of the different threads are (strongly) consistent. However, for performance reasons, only weaker guarantees can be ensured by memory systems, defined by what sets of updates can be made visible to each thread at any moment, and by the order in which these updates are made visible. The conditions on the visibility order guaranteed by a memory system corresponds to its consistency memory model. Weak consistency models admit complex and unintuitive behaviors where memory access operations (reads and writes) may be reordered in various ways w.r.t. the order in which they appear in programs. This makes the task of application programmers extremely hard. It is therefore important to determine an adequate level of consistency for each given application, i.e., a level that is weak enough to ensure high performance, but also strong enough to ensure correctness of the application w.r.t its specification. This leads to the consideration of several important verification problems:
- the correctness of an application program running over a weak consistency model;
- the robustness of an application program w.r.t. consistency weakening;
- the fact that an implementation of a system (memory, storage system) guarantees a given (weak) consistency model.
The talk gives a broad presentation of these issues and some results in this research area. The talk is based on several joint works with students and colleagues during the last few years.
Talk title: How to Use Polyhedral Reduction for the Verification of Petri nets.
Abstract: I will describe a new concept, called polyhedral reduction, that takes advantage of structural reductions to accelerate the verification of reachability properties on Petri nets. This approach relies on a state space abstraction which involves sets of linear arithmetic constraints between the marking of places.
We have been using polyhedral reductions to solve several problems. I will consider three of them. First, how to use reductions to efficiently compute the number of reachable markings of a net. Then how to use polyhedral reduction in combination with a SMT-based model checker. Finally, I will define a new data-structure, called Token Flow Graph (TFG), that captures the particular structure of constraints that we generate with our approach. I will show how we can leverage TFGs to efficiently compute the concurrency relation of a net, that is all pairs of places that can be marked together in some reachable marking.
Talk title: Asymptotic Analysis of Probabilistic VASS Programs.
Abstract: Vector Addition Systems with States (VASS) are a natural abstraction for programs operating over unbounded integer variables. We overview recently discovered algorithms and techniques for analyzing the asymptotic complexity of non-deterministic VASS. Furthermore, we examine possible extensions of these results to probabilistic VASS programs. We show that the standard concepts used for finite-state probabilistic programs (such as the expected termination time) are not entirely appropriate and propose some alternatives.