Résumé | We consider asynchronous programs consisting of multiple recursive threads (modeled as pushdown systems) running in parallel. Each of the threads is equipped with a multi-set. The threads can create tasks and post them onto the multi-sets or read a task from their own. In addition, they can synchronize through a finite set of locks. We examine the decidability of the state reachability problem for this model. The problem is already known to be undecidable for a system consisting of two recursive threads (and no tasks) and we examine a decidable subclass.
In the first half of the talk we survey, quickly, the previous results for recursive programs communicating via locks and in the second half we will describe our results on the asynchronous program model.
Based on Joint work with M.F. Atig, A. Bouajjani and P. Saivasan. |