Résumé | We consider multi-threaded systems which combine recursion, or even higher-order recursion, with dynamic thread creation. Communication between threads is via global variables as well as via local variables that are shared between a thread and its sub-threads. Reading and writing are atomic operations, while we do not allow locks or operations of the type compare-and-set. The resulting systems are still too expressive to be decidable. As an abstraction, we therefore replace thread creation with parametric thread creation and show for the resulting systems, that the reachability problem is decidable.
This is joint work with Anca Muscholl and Helmut Seidl. |