{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:34:15Z","timestamp":1767929655506,"version":"3.49.0"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Runtime predictive analyses enhance coverage of traditional dynamic analyses based bug detection techniques by identifying a space of feasible reorderings of the observed execution and determining if any reordering in this space witnesses the violation of some desired safety property. The most popular approach for modelling the space of feasible reorderings is through Mazurkiewicz\u2019s trace equivalence. The simplicity of the framework also gives rise to efficient predictive analyses, and has been the de facto means for obtaining space and time efficient algorithms for monitoring concurrent programs.<\/jats:p><jats:p>In this work, we investigate how to enhance the predictive power of trace-based reasoning, while still retaining the algorithmic benefits it offers. Towards this, we extend trace theory by naturally embedding a class of prefixes, which we call <jats:italic>strong trace prefixes<\/jats:italic>. We formally characterize strong trace prefixes using an enhanced dependence relation, study its predictive power and establish a tight connection to the previously proposed notion of synchronization-preserving correct reorderings developed in the context of data race and deadlock prediction. We then show that despite the enhanced predictive power, strong trace prefixes continue to enjoy the algorithmic benefits of Mazurkiewicz traces in the context of prediction against co-safety properties, and derive new algorithms for synchronization-preserving data races and deadlocks with better asymptotic space and time usage. We also show that strong trace prefixes can capture more violations of pattern languages. We implement our proposed algorithms and our evaluation confirms the practical utility of reasoning based on strong prefix traces.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_9","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"182-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Predictive Monitoring with\u00a0Strong Trace Prefixes"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-0214-3462","authenticated-orcid":false,"given":"Zhendong","family":"Ang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7610-0660","authenticated-orcid":false,"given":"Umang","family":"Mathur","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Ang, Z., Mathur, U.: Predictive monitoring against pattern regular languages. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632915, https:\/\/doi.org\/10.1145\/3632915","DOI":"10.1145\/3632915"},{"key":"9_CR2","unstructured":"Ang, Z., Mathur, U.: Predictive monitoring with strong trace prefixes (2024). https:\/\/arxiv.org\/abs\/2405.10499"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Bertoni, A., Mauri, G., Sabadini, N.: Membership problems for regular and context-free trace languages. Inf. Comput. 82(2), 135\u2013150 (1989). https:\/\/doi.org\/10.1016\/0890-5401(89)90051-5, https:\/\/www.sciencedirect.com\/science\/article\/pii\/0890540189900515","DOI":"10.1016\/0890-5401(89)90051-5"},{"issue":"6","key":"9_CR4","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/2666356.2594323","volume":"49","author":"S Biswas","year":"2014","unstructured":"Biswas, S., Huang, J., Sengupta, A., Bond, M.D.: Doublechecker: efficient sound and precise atomicity checking. ACM SIGPLAN Not. 49(6), 28\u201339 (2014)","journal-title":"ACM SIGPLAN Not."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Blackburn, S.M., et al.: The dacapo benchmarks: java benchmarking development and analysis. In: OOPSLA (2006)","DOI":"10.1145\/1167515.1167488"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Cai, Y., Yun, H., Wang, J., Qiao, L., Palsberg, J.: Sound and efficient concurrency bug prediction. In: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 255\u2013267 (2021)","DOI":"10.1145\/3468264.3468549"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Diekert, V.: A partial trace semantics for petri nets. Theor. Comput. Sci. 134(1), 87\u2013105 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90280-1","DOI":"10.1016\/0304-3975(94)90280-1"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Do, H., Elbaum, S.G., Rothermel, G.: Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empir. Softw. Eng. 10(4), 405\u2013435 (2005). https:\/\/doi.org\/10.1007\/S10664-005-3861-2","DOI":"10.1007\/S10664-005-3861-2"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware java runtime. In: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, pp. 245-255. Association for Computing Machinery, New York (2007). https:\/\/doi.org\/10.1145\/1250734.1250762","DOI":"10.1145\/1250734.1250762"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Farchi, E., Nir, Y., Ur, S.: Concurrent bug patterns and how to test them. In: 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 22-26 April 2003, Nice, France, CD-ROM\/Abstracts Proceedings, pp.\u00a0286. IEEE Computer Society (2003). https:\/\/doi.org\/10.1109\/IPDPS.2003.1213511","DOI":"10.1109\/IPDPS.2003.1213511"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70545-1_8","volume-title":"Computer Aided Verification","author":"A Farzan","year":"2008","unstructured":"Farzan, A., Madhusudan, P.: Monitoring atomicity in concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 52\u201365. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70545-1_8"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Farzan, A., Mathur, U.: Coarser equivalences for causal concurrency. Proc. ACM Program. Lang. 8(POPL) (2024). https:\/\/doi.org\/10.1145\/3632873","DOI":"10.1145\/3632873"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Freund, S.N.: Fasttrack: efficient and precise dynamic race detection. In: Proceedings of the 30th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, pp. 121-133. Association for Computing Machinery, New York (2009). https:\/\/doi.org\/10.1145\/1542476.1542490, https:\/\/doi.org\/10.1145\/1542476.1542490","DOI":"10.1145\/1542476.1542490"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Huang, J., Luo, Q., Rosu, G.: Gpredict: generic predictive concurrency analysis. In: Proceedings of the 37th International Conference on Software Engineering, ICSE 2015, vol. 1. pp. 847-857. IEEE Press (2015)","DOI":"10.1109\/ICSE.2015.96"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 337-348. Association for Computing Machinery, New York (2014). https:\/\/doi.org\/10.1145\/2594291.2594315","DOI":"10.1145\/2594291.2594315"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Itzkovitz, A., Schuster, A., Zeev-Ben-Mordehai, O.: Toward integration of data race detection in dsm systems. J. Parallel Distributed Comput. 59(2), 180\u2013203 (1999). https:\/\/doi.org\/10.1006\/jpdc.1999.1574, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0743731599915745","DOI":"10.1006\/jpdc.1999.1574"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Jannesari, A., Bao, K., Pankratius, V., Tichy, W.F.: Helgrind+: an efficient dynamic race detector. In: 2009 IEEE International Symposium on Parallel & Distributed Processing, pp. 1\u201313. IEEE (2009)","DOI":"10.1109\/IPDPS.2009.5160998"},{"issue":"6","key":"9_CR18","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1145\/1543135.1542489","volume":"44","author":"P Joshi","year":"2009","unstructured":"Joshi, P., Park, C.S., Sen, K., Naik, M.: A randomized dynamic program analysis technique for detecting real deadlocks. ACM Sigplan Not. 44(6), 110\u2013120 (2009)","journal-title":"ACM Sigplan Not."},{"key":"9_CR19","unstructured":"Jula, H., Tralamazza, D.M., Zamfir, C., Candea, G.: Deadlock immunity: Enabling systems to defend against deadlocks. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, 8-10 December 2008, San Diego, California, USA, Proceedings, pp. 295\u2013308. USENIX Association (2008). http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/jula\/jula.pdf"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Kalhauge, C.G., Palsberg, J.: Sound deadlock prediction. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276516","DOI":"10.1145\/3276516"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear-time. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pp. 157-170, Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3062341.3062374","DOI":"10.1145\/3062341.3062374"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Kulkarni, R., Mathur, U., Pavlogiannis, A.: Dynamic data-race detection through the fine-grained lens. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0203, pp. 16:1\u201316:23. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.16, https:\/\/drops.dagstuhl.de\/entities\/document\/10.4230\/LIPIcs.CONCUR.2021.16","DOI":"10.4230\/LIPIcs.CONCUR.2021.16"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Legunsen, O., Hassan, W.U., Xu, X., Ro\u015fu, G., Marinov, D.: How good are the specs? a study of the bug-finding effectiveness of existing java api specifications. In: 2016 31st IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 602\u2013613 (2016)","DOI":"10.1145\/2970276.2970356"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Mathur, U., Kini, D., Viswanathan, M.: What happens-after the first race? enhancing the predictive power of happens-before based dynamic race detection. Proc. ACM Program. Lang. 2(OOPSLA) (2018). https:\/\/doi.org\/10.1145\/3276515","DOI":"10.1145\/3276515"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Mathur, U., Pavlogiannis, A., Viswanathan, M.: The complexity of dynamic data race prediction. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2020, pp. 713-727. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3373718.3394783","DOI":"10.1145\/3373718.3394783"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Mathur, U., Pavlogiannis, A., Viswanathan, M.: Optimal prediction of synchronization-preserving races. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434317","DOI":"10.1145\/3434317"},{"key":"9_CR27","doi-asserted-by":"crossref","unstructured":"Mathur, U., Viswanathan, M.: Atomicity checking in linear time using vector clocks. In: Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 183\u2013199 (2020)","DOI":"10.1145\/3373376.3378475"},{"key":"9_CR28","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-0-387-09766-4_491","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency","author":"A Mazurkiewicz","year":"1987","unstructured":"Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) Petri Nets: Applications and Relationships to Other Models of Concurrency, pp. 278\u2013324. Springer, Berlin Heidelberg, Berlin, Heidelberg (1987). https:\/\/doi.org\/10.1007\/978-0-387-09766-4_491"},{"key":"9_CR29","doi-asserted-by":"crossref","unstructured":"M\u00fcehlenfeld, A., Wotawa, F.: Fault detection in multi-threaded c++ server applications. In: Proceedings of the 12th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pp. 142\u2013143 (2007)","DOI":"10.1145\/1229428.1229457"},{"key":"9_CR30","first-page":"56","volume":"27","author":"E Ochma\u0144ski","year":"1985","unstructured":"Ochma\u0144ski, E.: Regular behaviour of concurrent systems. Bull. EATCS 27, 56\u201367 (1985)","journal-title":"Bull. EATCS"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Pavlogiannis, A.: Fast, sound, and effectively complete dynamic race prediction. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371085","DOI":"10.1145\/3371085"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/3-540-60084-1_87","volume-title":"Automata, Languages and Programming","author":"J-E Pin","year":"1995","unstructured":"Pin, J.-E., Weil, P.: Polynomial closure and unambiguous product. In: F\u00fcl\u00f6p, Z., G\u00e9cseg, F. (eds.) ICALP 1995. LNCS, vol. 944, pp. 348\u2013359. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60084-1_87"},{"key":"9_CR33","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-44881-0_35","volume-title":"Rewriting Tech. Appli.","author":"G Ro\u015fu","year":"2003","unstructured":"Ro\u015fu, G., Viswanathan, M.: Testing extended regular language membership incrementally by rewriting. In: Nieuwenhuis, R. (ed.) Rewriting Tech. Appli., pp. 499\u2013514. Springer, Berlin Heidelberg, Berlin, Heidelberg (2003)"},{"key":"9_CR34","doi-asserted-by":"crossref","unstructured":"Said, M., Wang, C., Yang, Z., Sakallah, K.: Generating data race witnesses by an smt-based analysis. In: Proceedings of the Third International Conference on NASA Formal Methods, NFM 2011, pp. 313\u2013327. Springer-Verlag, Berlin (2011). http:\/\/dl.acm.org\/citation.cfm?id=1986308.1986334","DOI":"10.1007\/978-3-642-20398-5_23"},{"key":"9_CR35","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-35632-2_16","volume-title":"Runtime Verification","author":"TF \u015eerb\u0103nu\u0163\u0103","year":"2013","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Chen, F., Ro\u015fu, G.: Maximal causal models for sequentially consistent systems. In: Qadeer, S., Tasiran, S. (eds.) Runtime Verification, pp. 136\u2013150. Springer, Berlin Heidelberg, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_16"},{"key":"9_CR36","doi-asserted-by":"crossref","unstructured":"Serebryany, K., Iskhodzhanov, T.: Threadsanitizer: data race detection in practice. In: WBIA 2009 (2009)","DOI":"10.1145\/1791194.1791203"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Shi, Z., Mathur, U., Pavlogiannis, A.: Optimistic prediction of synchronization-reversal data races. In: Proceedings of the IEEE\/ACM 46th International Conference on Software Engineering, ICSE 2024, Association for Computing Machinery, New York (2024). https:\/\/doi.org\/10.1145\/3597503.3639099","DOI":"10.1145\/3597503.3639099"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., Flanagan, C.: Sound predictive race detection in polynomial time. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 387-400. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2103656.2103702, https:\/\/doi.org\/10.1145\/2103656.2103702","DOI":"10.1145\/2103656.2103702"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"Smith, L.A., Bull, J.M., Obdrz\u00e1lek, J.: A parallel java grande benchmark suite. In: Proceedings of the 2001 ACM\/IEEE Conference on Supercomputing, SC 2001, p. 8. ACM, New York (2001). https:\/\/doi.org\/10.1145\/582034.582042","DOI":"10.1145\/582034.582042"},{"key":"9_CR40","doi-asserted-by":"crossref","unstructured":"Tun\u00e7, H.C., Mathur, U., Pavlogiannis, A., Viswanathan, M.: Sound dynamic deadlock prediction in linear time. Proc. ACM Program. Lang. 7(PLDI), 1733\u20131758 (2023)","DOI":"10.1145\/3591291"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65630-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:03:17Z","timestamp":1721858597000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}