  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 state-extended ground-tree
rewrite systems equipped with shared unbounded integer counters that can be
incremented, decremented, and compared against an integer constant. Since the
model is Turing-complete, we propose a decidable underapproximation. First,
using a restriction similar to context-bounding, we underapproximate the global
control by a weak global control (i.e. DAGs possibly with self-loops), thereby
limiting the number of synchronisations between different threads. Second, we
bound the number of reversals between non-decrementing and non-incrementing
modes of the counters. Under this restriction, we show that reachability
becomes NP-complete. In fact, it is poly-time 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) weakly-synchronised ground-tree rewrite systems, and (ii)
synchronisation/reversal-bounded concurrent pushdown systems systems with
counters. Finally, we show that, when equipped with reversal-bounded counters,
relaxing the weak control restriction by the notion of senescence results in
undecidability.
