**Decidable Models of Integer-Manipulating Programs with Recursive Parallelism.** / Hague, Matthew; Lin, Anthony.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

E-pub ahead of print

**Decidable Models of Integer-Manipulating Programs with Recursive Parallelism.** / Hague, Matthew; Lin, Anthony.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Hague, M & Lin, A 2016, Decidable Models of Integer-Manipulating Programs with Recursive Parallelism. in *Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings.* vol. 9899, Lecture Notes in Computer Science, vol. 9899, Springer International Publishing, pp. 148-162. https://doi.org/10.1007/978-3-319-45994-3_11

Hague, M., & Lin, A. (2016). Decidable Models of Integer-Manipulating Programs with Recursive Parallelism. In *Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings *(Vol. 9899, pp. 148-162). (Lecture Notes in Computer Science; Vol. 9899). Springer International Publishing. https://doi.org/10.1007/978-3-319-45994-3_11

Hague M, Lin A. Decidable Models of Integer-Manipulating Programs with Recursive Parallelism. In Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings. Vol. 9899. Springer International Publishing. 2016. p. 148-162. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-45994-3_11

@inproceedings{e4c6283910604a82aa036eff46799129,

title = "Decidable Models of Integer-Manipulating Programs with Recursive Parallelism",

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.",

author = "Matthew Hague and Anthony Lin",

year = "2016",

month = sep,

day = "13",

doi = "10.1007/978-3-319-45994-3_11",

language = "English",

isbn = "978-3-319-45993-6",

volume = "9899",

series = "Lecture Notes in Computer Science",

publisher = "Springer International Publishing",

pages = "148--162",

booktitle = "Reachability Problems",

}

TY - GEN

T1 - Decidable Models of Integer-Manipulating Programs with Recursive Parallelism

AU - Hague, Matthew

AU - Lin, Anthony

PY - 2016/9/13

Y1 - 2016/9/13

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-45994-3_11

DO - 10.1007/978-3-319-45994-3_11

M3 - Conference contribution

SN - 978-3-319-45993-6

VL - 9899

T3 - Lecture Notes in Computer Science

SP - 148

EP - 162

BT - Reachability Problems

PB - Springer International Publishing

ER -