Supervision : Michèle SORIA

Co-supervision : PESCHANSKI Fréderic

Resources analysis for concurrent and dynamic systems

Computer programs and systems have a growing need for dynamic resources: communication channels that are created and destroyed at will, connections to databases, memory areas, computational resources, etc. In this work, we are interested in both the qualitative and quantitative analysis of such resources in the context of concurrent and dynamic systems.
Our study is organized on the basis of a prototype programming language, named Piccolo, which was implemented in the context of the thesis. It allows one to program machines with multicore CPU using abstractions based on the pi-calculus process algebra. Piccolo programs are then very close to pi-calculus models that can be analyzed with verification tools.
In this work, we first address the issue of constructing explicit state-spaces for pi-calculus processes. Given the expressivity of the formalism, this is in fact a non-trivial problem, especially when considering the case of labelled transition semantics. We propose a new algorithm (and a prototype tool) based on the symbolic transitions rather than the early semantics. We then observe experimentally an important reduction of the generated state-spaces. We also introduce a variant of the pi-calculus, named slice-pi, that provides an intermediate between the labelled transition semantics on the one side and the reduction semantics on the other side. This allows to "open up" some parts of a system while "keeping closed" the other parts, selectively.
The central part of the thesis is concerned with the development of a resource analysis framework for concurrent and dynamic systems. This framework is based, at the theoretical level, on a new model of automata, named nu-automata, that are a variant of the finite memory automata. They allow one to model the behavior of the systems from the point of view of their resource usage. We show how to obtain a nu-automaton from a pi-calculus (or slice-pi) model, but their use is not restricted to the context of the process algebra. Based on this automata-theoretic foundation, we develop an algorithmic framework for the quantitative analysis of the nu-automata, and thus for the systems they model. In particular, we introduce the omniscient garbage collector (OGC) that is able to compute a worst-case minimal bound for the resource consumption of a system. A prototype tool has been developed to experiment the analysis algorithms in practice.

2014-2016 Publications

• 2016
  • A. Deharbe : “Analyse statique de programmes concurrents et dynamiques”, thesis, phd defence 09/21/2016, supervision Soria, Michèle, co-supervision : Peschanski, Fréderic (2016)
• 2014
  • A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector : a Resource Analysis Framework”, ACSD 2014 - 14^th International Conference on Application of Concurrency to System Design, La Marsa, Tunisia, pp. 102-111, (IEEE) (2014)
  • A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector: a Resource Analysis Framework”, (2014)