Bounded Context Switching for Valence Systems
We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in NPTIME, independent of the memory (the graph monoid). Our proof is genuinely algebraic, and therefore contributes a new way to think about BCS. In addition, we exhibit a class of storage mechanisms for which BCS reachability belongs to PTIME.
valence systems
graph monoids
bounded context switching
Theory of computation~Parallel computing models
Theory of computation~Formal languages and automata theory
Theory of computation~Logic and verification
12:1-12:18
Regular Paper
https://arxiv.org/abs/1803.09703
Roland
Meyer
Roland Meyer
TU Braunschweig, Germany
https://orcid.org/0000-0001-8495-671X
Sebastian
Muskalla
Sebastian Muskalla
TU Braunschweig, Germany
https://orcid.org/0000-0001-9195-7323
Georg
Zetzsche
Georg Zetzsche
IRIF (Université Paris-Diderot, CNRS), France
https://orcid.org/0000-0002-6421-4388
Supported by a fellowship of the Fondation Sciences Mathématiques de Paris and partially funded by the DeLTA project (ANR-16-CE40-0007).
10.4230/LIPIcs.CONCUR.2018.12
IJ. J. Aalbersberg and H. J. Hoogeboom. Characterizations of the decidability of some problems for regular trace languages. Mathematical Systems Theory, 22(1):1-19, 1989.
P. A. Abdulla, C. Aiswarya, and M. F. Atig. Data multi-pushdown automata. In CONCUR, volume 85 of LIPIcs, pages 38:1-38:17. Dagstuhl, 2017.
P. A. Abdulla, C. Aiswarya, M. F. Atig, M. Montali, and O. Rezine. Recency-bounded verification of dynamic database-driven systems. In PODS, pages 195-210. ACM, 2016.
P. A. Abdulla, M. F. Atig, A. Bouajjani, and T. P. Ngo. Context-bounded analysis for POWER. In TACAS, volume 10206 of LNCS, pages 56-74. Springer, 2017.
P. A. Abdulla, M. F. Atig, R. Meyer, and M. S. Salehi. What’s decidable about availability languages? In FSTTCS, volume 45 of LIPIcs, pages 192-205. Dagstuhl, 2015.
C. Aiswarya. Verification of communicating recursive programs via split-width. thesis, École normale supérieure de Cachan, France, 2014.
C. Aiswarya, P. Gastin, and K. N. Kumar. MSO decidability of multi-pushdown systems via split-width. In CONCUR, volume 7454 of LNCS, pages 547-561. Springer, 2012.
C. Aiswarya, P Gastin, and K. N. Kumar. Controllers for the verification of communicating multi-pushdown systems. In CONCUR, volume 8704 of LNCS, pages 297-311. Springer, 2014.
S. Akshay, P. Gastin, and S. N. Krishna. Analyzing timed systems using tree automata. In CONCUR, volume 59 of LIPIcs, pages 27:1-27:14. Dagstuhl, 2016.
S. Akshay, P. Gastin, S. N. Krishna, and I. Sarkar. Towards an efficient tree automata based technique for timed systems. In CONCUR, volume 85 of LIPIcs, pages 39:1-39:15. Dagstuhl, 2017.
M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2etime-complete. In DLT, volume 5257 of LNCS, pages 121-133. Springer, 2008.
M. F. Atig, A. Bouajjani, K. N. Kumar, and P. Saivasan. On bounded reachability analysis of shared memory systems. In FSTTCS, volume 29 of LIPIcs, pages 611-623. Dagstuhl, 2014.
M. F. Atig, A. Bouajjani, and G. Parlato. Getting rid of store-buffers in TSO analysis. In CAV, volume 6806 of LNCS, pages 99-115. Springer, 2011.
M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. In TACAS, volume 5505 of LNCS, pages 107-123. Springer, 2009.
M. F. Atig, A. Bouajjani, and T. Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, volume 5201 of LNCS, pages 356-371. Springer, 2008.
A. Bouajjani and M. Emmi. Bounded phase analysis of message-passing programs. STTT, 16(2):127-146, 2014.
A. Bouajjani, M. Emmi, and G. Parlato. On sequentializing concurrent programs. In SAS, volume 6887 of LNCS, pages 129-145. Springer, 2011.
L. Breveglieri, A. Cherubini, C. Citrini, and S. Crespi-Reghizzi. Multi-push-down languages and grammars. Int. J. Found. Comput. Sci., 7(3):253-292, 1996.
P. Buckheister and Georg Zetzsche. Semilinearity and context-freeness of languages accepted by valence automata. In MFCS, volume 8087 of LNCS, pages 231-242. Springer, 2013.
P. Chini, J. Kolberg, A. Krebs, R. Meyer, and P. Saivasan. On the complexity of bounded context switching. In ESA, volume 87 of LIPIcs, pages 27:1-27:15. Dagstuhl, 2017.
P. Chini, R. Meyer, and P. Saivasan. Fine-grained complexity of safety verification. In TACAS, volume 87 of LNCS. Springer, 2018.
D. Chistikov, W. Czerwinski, P. Hofman, M. Pilipczuk, and M. Wehar. Shortest paths in one-counter systems. In FOSSACS, pages 462-478, 2016.
E. D'Osualdo, R. Meyer, and G. Zetzsche. First-order logic with reachability for infinite-state systems. In LICS, pages 457-466. ACM, 2016.
M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In POPL, pages 411-422. ACM, 2011.
J. Esparza, P. Ganty, and R. Majumdar. A perfect model for bounded verification. In LICS, pages 285-294. IEEE, 2012.
J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM ToPLaS, 36(3):9:1-9:29, 2014.
F. Furbach, R. Meyer, K. Schneider, and M. Senftleben. Memory-model-aware testing: A unified complexity analysis. ACM Trans. Embedded Comput. Syst., 14(4):63:1-63:25, 2015.
P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. In CAV, volume 6174 of LNCS, pages 600-614. Springer, 2010.
S. Ginsburg and E. Spanier. Bounded ALGOL-like languages. Trans. Amer. Math. Soc., 113:333-–368, 1964.
M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of LNCS, pages 260-276. Springer, 2012.
A. Heussner, J. Leroux, A. Muscholl, and G. Sutre. Reachability analysis of communicating pushdown systems. LMCS, 8(3), 2012.
Martin Huschenbett, Dietrich Kuske, and Georg Zetzsche. The monoid of queue actions. Semigroup Forum, 95:475-508, 2017.
O. Inverso, T. L. Nguyen, B. Fischer, S. La Torre, and G. Parlato. Lazy-CSeq: A context-bounded model checking tool for multi-threaded C-programs. In ASE, pages 807-812. IEEE, 2015.
C. Köcher. Rational, recognizable, and aperiodic sets in the partially lossy queue monoid. In STACS, LIPIcs, pages 45:1-45:14. Dagstuhl, 2018.
C. Köcher and D. Kuske. The transformation monoid of a partially lossy queue. In CSR, volume 10304 of Lecture Notes in Computer Science, pages 191-205. Springer, 2017.
S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE, 2007.
S. La Torre, P. Madhusudan, and G. Parlato. Context-bounded analysis of concurrent queue systems. In TACAS, volume 4963 of LNCS, pages 299-314. Springer, 2008.
S. La Torre, P. Madhusudan, and G. Parlato. Reducing context-bounded concurrent reachability to sequential reachability. In CAV, volume 5643 of LNCS, pages 477-492. Springer, 2009.
S. La Torre, P. Madhusudan, and G. Parlato. The language theory of bounded context-switching. In LATIN, pages 96-107. Springer, 2010.
S. La Torre, P. Madhusudan, and G. Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV, volume 6174 of LNCS, pages 629-644. Springer, 2010.
S. La Torre and M. Napoli. Reachability of multistack pushdown systems with scope-bounded matching relations. In CONCUR, volume 6901 of LNCS, pages 203-218. Springer, 2011.
A. Lal and T. W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. In CAV, volume 5123 of LNCS, pages 37-51. Springer, 2008.
M. Lohrey and B. Steinberg. The submonoid and rational subset membership problems for graph groups. Journal of Algebra, 320(2):728-755, 2008.
M. Lohrey and G. Zetzsche. Knapsack in graph groups. Theory of Computing Systems, 62:192-246, 2018.
S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In ASPLOS, pages 329-339. ACM, 2008.
P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, pages 283-294. ACM, 2011.
R. Meyer, S. Muskalla, and G. Zetzsche. Bounded Context Switching for Valence Systems. ArXiv e-prints, 2018. URL: http://arxiv.org/abs/1803.09703.
http://arxiv.org/abs/1803.09703
M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455. ACM, 2007.
T. L. Nguyen, P. Schrammel, B. Fischer, S. La Torre, and G. Parlato. Parallel bug-finding in concurrent programs via reduced interleaving instances. In ASE, pages 753-764. IEEE, 2017.
S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005.
S. Qadeer and D: Wu. KISS: Keep it simple and sequential. In PLDI, pages 14-24. ACM, 2004.
E. Tomasco, O. Inverso, B. Fischer, S. La Torre, and G. Parlato. Verifying concurrent programs by memory unwinding. In TACAS, volume 9035 of LNCS, pages 551-565. Springer, 2015.
K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational Horn clauses. In CADE, volume 3632 of LNCS, pages 337-352. Springer, 2005.
E. S. Wolk. A note on "the comparability graph of a tree". Proceedings of the American Mathematical Society, 16(1):17-20, 1965.
G. Zetzsche. Silent transitions in automata with storage. In ICALP, volume 7966 of LNCS, pages 434-445. Springer, 2013.
G. Zetzsche. Monoids as storage mechanisms. Bulletin of the EATCS, 120:237-249, 2016.
G. Zetzsche. Monoids as Storage Mechanisms. PhD thesis, Technische Universität Kaiserslautern, 2016.
G. Zetzsche. The emptiness problem for valence automata over graph monoids, 2018. To appear in Information and Computation.
Roland Meyer, Sebastian Muskalla, and Georg Zetzsche
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode