Projects per year
Abstract
We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is stateextended groundtree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turingcomplete, we propose a decidable underapproximation. First, using a restriction similar to contextbounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with selfloops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between nondecrementing and nonincrementing modes of the counters. Under this restriction, we show that reachability becomes NPcomplete. In fact, it is polytime reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weaklysynchronised groundtree rewrite systems, and (ii) synchronisation/reversalbounded concurrent pushdown systems with counters. Finally, we show that, when equipped with reversalbounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.
Original language  English 

Title of host publication  Reachability Problems 
Subtitle of host publication  10th International Workshop, RP 2016, Aalborg, Denmark, September 1921, 2016, Proceedings 
Publisher  Springer International Publishing 
Pages  148162 
Number of pages  15 
Volume  9899 
ISBN (Electronic)  9783319459943 
ISBN (Print)  9783319459936 
DOIs  
Publication status  Epub ahead of print  13 Sept 2016 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer International Publishing 
Volume  9899 
ISSN (Print)  03029743 
Projects
 1 Finished

Verification of Concurrent and HigherOrder Recursive Programs
Eng & Phys Sci Res Council EPSRC
1/05/13 → 30/04/18
Project: Research