The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
To make the development of efficient multi-core applications easier, libraries, such as Grand Central Dispatch (GCD), have been proposed. In GCD, the programmer separtes its code into chunks, i.e., functionally separate units, so-called blocks, and dispatches them, using synchronous or asynchronous calls, to several types of waiting queues. An OS-level scheduler is then responsible for dispatching those blocks on the available cores. In addition to synchronization by synchronous calls, all running blocks can synchronize via global memory. Thus, GCD and similar libraries permit complex patterns of causal interaction between concurrently running blocks and stronlgy require the help of formal methods to assure correctness criteria for GCD-based programs.
We propose Queue-Dispatch Asynchronous Systems (QDAS) as a mathematical model that faithfully formalizes the synchronization mechanisms and the behavior of the scheduler in those systems.
This allows to uncover the relationship of this type of models to classical ones such as pushdown systems, Petri nets, fifo systems, and counter systems. Our main technical contributions are precise worst-case complexity results for the Parikh coverability problem for several subclasses of our model.
We further give an outlook on ongoing and future work that focusses approximative approaches to verification and the addition of quantitative aspects.
This is joint work with Gilles Geeraerts and Jean-François Raskin.