Document Open Access Logo

Bounded Context Switching for Valence Systems

Authors Roland Meyer , Sebastian Muskalla , Georg Zetzsche

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.12.pdf
  • Filesize: 497 kB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Parallel computing models
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
Keywords
  • valence systems
  • graph monoids
  • bounded context switching

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

Roland Meyer, Sebastian Muskalla, and Georg Zetzsche. Bounded Context Switching for Valence Systems. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.12

Author Details

Roland Meyer
  • TU Braunschweig, Germany
Sebastian Muskalla
  • TU Braunschweig, Germany
Georg Zetzsche
  • IRIF (Université Paris-Diderot, CNRS), France

Funding

  • Zetzsche, Georg: Supported by a fellowship of the Fondation Sciences Mathématiques de Paris and partially funded by the DeLTA project (ANR-16-CE40-0007).

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. C. Aiswarya. Verification of communicating recursive programs via split-width. thesis, École normale supérieure de Cachan, France, 2014. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. 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. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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. Google Scholar
  16. A. Bouajjani and M. Emmi. Bounded phase analysis of message-passing programs. STTT, 16(2):127-146, 2014. Google Scholar
  17. A. Bouajjani, M. Emmi, and G. Parlato. On sequentializing concurrent programs. In SAS, volume 6887 of LNCS, pages 129-145. Springer, 2011. Google Scholar
  18. 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. Google Scholar
  19. 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. Google Scholar
  20. 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. Google Scholar
  21. P. Chini, R. Meyer, and P. Saivasan. Fine-grained complexity of safety verification. In TACAS, volume 87 of LNCS. Springer, 2018. Google Scholar
  22. D. Chistikov, W. Czerwinski, P. Hofman, M. Pilipczuk, and M. Wehar. Shortest paths in one-counter systems. In FOSSACS, pages 462-478, 2016. Google Scholar
  23. E. D'Osualdo, R. Meyer, and G. Zetzsche. First-order logic with reachability for infinite-state systems. In LICS, pages 457-466. ACM, 2016. Google Scholar
  24. M. Emmi, S. Qadeer, and Z. Rakamaric. Delay-bounded scheduling. In POPL, pages 411-422. ACM, 2011. Google Scholar
  25. J. Esparza, P. Ganty, and R. Majumdar. A perfect model for bounded verification. In LICS, pages 285-294. IEEE, 2012. Google Scholar
  26. J. Esparza, P. Ganty, and T. Poch. Pattern-based verification for multithreaded programs. ACM ToPLaS, 36(3):9:1-9:29, 2014. Google Scholar
  27. 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. Google Scholar
  28. P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. In CAV, volume 6174 of LNCS, pages 600-614. Springer, 2010. Google Scholar
  29. S. Ginsburg and E. Spanier. Bounded ALGOL-like languages. Trans. Amer. Math. Soc., 113:333-–368, 1964. Google Scholar
  30. 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. Google Scholar
  31. A. Heussner, J. Leroux, A. Muscholl, and G. Sutre. Reachability analysis of communicating pushdown systems. LMCS, 8(3), 2012. Google Scholar
  32. Martin Huschenbett, Dietrich Kuske, and Georg Zetzsche. The monoid of queue actions. Semigroup Forum, 95:475-508, 2017. Google Scholar
  33. 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. Google Scholar
  34. C. Köcher. Rational, recognizable, and aperiodic sets in the partially lossy queue monoid. In STACS, LIPIcs, pages 45:1-45:14. Dagstuhl, 2018. Google Scholar
  35. 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. Google Scholar
  36. S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE, 2007. Google Scholar
  37. 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. Google Scholar
  38. 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. Google Scholar
  39. S. La Torre, P. Madhusudan, and G. Parlato. The language theory of bounded context-switching. In LATIN, pages 96-107. Springer, 2010. Google Scholar
  40. 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. Google Scholar
  41. 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. Google Scholar
  42. 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. Google Scholar
  43. M. Lohrey and B. Steinberg. The submonoid and rational subset membership problems for graph groups. Journal of Algebra, 320(2):728-755, 2008. Google Scholar
  44. M. Lohrey and G. Zetzsche. Knapsack in graph groups. Theory of Computing Systems, 62:192-246, 2018. Google Scholar
  45. 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. Google Scholar
  46. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, pages 283-294. ACM, 2011. Google Scholar
  47. R. Meyer, S. Muskalla, and G. Zetzsche. Bounded Context Switching for Valence Systems. ArXiv e-prints, 2018. URL: http://arxiv.org/abs/1803.09703.
  48. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446-455. ACM, 2007. Google Scholar
  49. 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. Google Scholar
  50. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  51. S. Qadeer and D: Wu. KISS: Keep it simple and sequential. In PLDI, pages 14-24. ACM, 2004. Google Scholar
  52. 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. Google Scholar
  53. 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. Google Scholar
  54. E. S. Wolk. A note on "the comparability graph of a tree". Proceedings of the American Mathematical Society, 16(1):17-20, 1965. Google Scholar
  55. G. Zetzsche. Silent transitions in automata with storage. In ICALP, volume 7966 of LNCS, pages 434-445. Springer, 2013. Google Scholar
  56. G. Zetzsche. Monoids as storage mechanisms. Bulletin of the EATCS, 120:237-249, 2016. Google Scholar
  57. G. Zetzsche. Monoids as Storage Mechanisms. PhD thesis, Technische Universität Kaiserslautern, 2016. Google Scholar
  58. G. Zetzsche. The emptiness problem for valence automata over graph monoids, 2018. To appear in Information and Computation. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact