Decidable models of integer-manipulating programs with recursive parallelism. / Hague, Matthew; Lin, Anthony.

In: Theoretical Computer Science, 30.04.2018.

Research output: Contribution to journalArticle

E-pub ahead of print

Documents

  • main-plain

    Accepted author manuscript, 193 KB, PDF-document

    Embargo ends: 30/04/20

    Licence: CC BY-NC-ND Show licence

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 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 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.
Original languageEnglish
Number of pages14
JournalTheoretical Computer Science
Early online date30 Apr 2018
DOIs
StateE-pub ahead of print - 30 Apr 2018

Research outputs

This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 30004504