{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:04Z","timestamp":1751660524131,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T00:00:00Z","timestamp":1617667200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T00:00:00Z","timestamp":1617667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a thread-modular proof method for <jats:italic>complexity and resource bound analysis<\/jats:italic> of concurrent, shared-memory programs. To this end, we lift Jones\u2019 rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. The compositionality (thread-modularity) of this framework allows us to reason about parameterized programs, i.e., programs that execute arbitrarily many concurrent threads. We automate reasoning in our logic by reducing bound analysis of concurrent programs to the sequential case. As an application, we automatically infer time complexity for a family of fine-grained concurrent algorithms, <jats:italic>lock-free data structures<\/jats:italic>, to our knowledge for the first time.\n<\/jats:p>","DOI":"10.1007\/s10703-021-00370-8","type":"journal-article","created":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T20:02:55Z","timestamp":1617739375000},"page":"270-302","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Rely-guarantee bound analysis of parameterized concurrent shared-memory programs"],"prefix":"10.1007","volume":"57","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-0248","authenticated-orcid":false,"given":"Thomas","family":"Pani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0143-632X","authenticated-orcid":false,"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,4,6]]},"reference":[{"issue":"3","key":"370_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi M, Lamport L (1995) Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3):507\u2013534","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"370_CR2","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Haziza F, Hol\u00edk L, Jonsson B, Rezine A (2013) An integrated specification and verification technique for highly concurrent data structures. In: TACAS, Lecture Notes in Computer Science, vol. 7795, pp. 324\u2013338. Springer","DOI":"10.1007\/978-3-642-36742-7_23"},{"key":"370_CR3","doi-asserted-by":"crossref","unstructured":"Albert E, Arenas P, Genaim S, G\u00f3mez-Zamalloa M, Puebla G (2012) Automatic inference of resource consumption bounds. In: LPAR, Lecture Notes in Computer Science, vol. 7180, pp. 1\u201311. Springer","DOI":"10.1007\/978-3-642-28717-6_1"},{"issue":"2","key":"370_CR4","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert E, Arenas P, Genaim S, Puebla G (2011) Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2):161\u2013203","journal-title":"J. Autom. Reason."},{"issue":"1","key":"370_CR5","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s10817-016-9400-6","volume":"59","author":"E Albert","year":"2017","unstructured":"Albert E, Flores-Montoya A, Genaim S, Martin-Martin E (2017) Rely-guarantee termination and cost analyses of loops with concurrent interleavings. J. Autom. Reason. 59(1):47\u201385","journal-title":"J. Autom. Reason."},{"key":"370_CR6","doi-asserted-by":"crossref","unstructured":"Alias C, Darte A, Feautrier P, Gonnord L (2010) Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: SAS, Lecture Notes in Computer Science, vol. 6337, pp. 117\u2013133. Springer","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"370_CR7","doi-asserted-by":"crossref","unstructured":"Berdine J, Lev-Ami T, Manevich R, Ramalingam G, Sagiv S (2008) Thread quantification for concurrent shape analysis. In: CAV, Lecture Notes in Computer Science, vol. 5123, pp. 399\u2013413. Springer","DOI":"10.1007\/978-3-540-70545-1_37"},{"issue":"2","key":"370_CR8","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/s10703-011-0111-7","volume":"38","author":"A Bouajjani","year":"2011","unstructured":"Bouajjani A, Bozga M, Habermehl P, Iosif R, Moro P, Vojnar T (2011) Programs with lists are counter automata. Formal Methods Syst. Des. 38(2):158\u2013192","journal-title":"Formal Methods Syst. Des."},{"key":"370_CR9","doi-asserted-by":"crossref","unstructured":"Brockschmidt M, Emmes F, Falke S, Fuhs C, Giesl J (2016) Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4):13:1-13:50","DOI":"10.1145\/2866575"},{"key":"370_CR10","doi-asserted-by":"crossref","unstructured":"Calcagno C, Distefano D, O\u2019Hearn PW, Yang H (2009) Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289\u2013300. ACM","DOI":"10.1145\/1594834.1480917"},{"key":"370_CR11","doi-asserted-by":"crossref","unstructured":"Calcagno C, Parkinson MJ, Vafeiadis V (2007) Modular safety checking for fine-grained concurrency. In: SAS,Lecture Notes in Computer Science, vol. 4634, pp. 233\u2013248. Springer","DOI":"10.1007\/978-3-540-74061-2_15"},{"key":"370_CR12","doi-asserted-by":"crossref","unstructured":"Carbonneaux Q, Hoffmann J, Reps TW, Shao Z (2017) Automated resource analysis with coq proof objects. In: CAV (2), Lecture Notes in Computer Science, vol. 10427, pp. 64\u201385. Springer","DOI":"10.1007\/978-3-319-63390-9_4"},{"key":"370_CR13","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V (2015) Aspect-oriented linearizability proofs. Logical Methods Comput Sci 11(1)","DOI":"10.2168\/LMCS-11(1:20)2015"},{"key":"370_CR14","unstructured":"Coachman. https:\/\/github.com\/thpani\/coachman (2019)"},{"key":"370_CR15","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2007) Proving thread termination. In: PLDI, pp. 320\u2013330. ACM","DOI":"10.1145\/1273442.1250771"},{"key":"370_CR16","doi-asserted-by":"crossref","unstructured":"Doherty S, Groves L, Luchangco V, Moir M (2004) Formal verification of a practical lock-free queue algorithm. In: FORTE, Lecture Notes in Computer Science, vol. 3235, pp. 97\u2013114. Springer","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"370_CR17","doi-asserted-by":"crossref","unstructured":"Fiedor T, Hol\u00edk L, Rogalewicz A, Sinn M, Vojnar T, Zuleger F (2018) From shapes to amortized complexity. In: VMCAI, Lecture Notes in Computer Science, vol. 10747, pp. 205\u2013225. Springer","DOI":"10.1007\/978-3-319-73721-8_10"},{"key":"370_CR18","doi-asserted-by":"crossref","unstructured":"Flanagan C, Freund SN, Qadeer S (2002) Thread-modular verification for shared-memory programs. In: ESOP, Lecture Notes in Computer Science, vol. 2305, pp. 262\u2013277. Springer","DOI":"10.1007\/3-540-45927-8_19"},{"key":"370_CR19","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN, Lecture Notes in Computer Science, vol. 2648, pp. 213\u2013224. Springer","DOI":"10.1007\/3-540-44829-2_14"},{"key":"370_CR20","doi-asserted-by":"crossref","unstructured":"Flores-Montoya A, H\u00e4hnle R (2014) Resource analysis of complex programs with cost equations. In: APLAS, Lecture Notes in Computer Science, vol. 8858, pp. 275\u2013295. Springer","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"370_CR21","doi-asserted-by":"crossref","unstructured":"Gotsman A, Berdine J, Cook B, Sagiv M (2007) Thread-modular shape analysis. In: PLDI, pp. 266\u2013277. ACM","DOI":"10.1145\/1273442.1250765"},{"key":"370_CR22","doi-asserted-by":"crossref","unstructured":"Gotsman A, Cook B, Parkinson MJ, Vafeiadis V (2009) Proving that non-blocking algorithms don\u2019t block. In: POPL, pp. 16\u201328. ACM","DOI":"10.1145\/1594834.1480886"},{"key":"370_CR23","doi-asserted-by":"crossref","unstructured":"Gulwani S, Zuleger F (2010) The reachability-bound problem. In: PLDI, pp. 292\u2013304. ACM","DOI":"10.1145\/1809028.1806630"},{"key":"370_CR24","doi-asserted-by":"crossref","unstructured":"Hendler D, Shavit N, Yerushalmi L (2004) A scalable lock-free stack algorithm. In: SPAA, pp. 206\u2013215. ACM","DOI":"10.1145\/1007912.1007944"},{"key":"370_CR25","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, USA"},{"key":"370_CR26","doi-asserted-by":"crossref","unstructured":"Hol\u00edk L, Meyer R, Vojnar T, Wolff S (2017) Effect summaries for thread-modular analysis - sound analysis despite an unsound heuristic. In: SAS, Lecture Notes in Computer Science, vol. 10422, pp. 169\u2013191. Springer","DOI":"10.1007\/978-3-319-66706-5_9"},{"key":"370_CR27","doi-asserted-by":"crossref","unstructured":"Jia X, Li W, Vafeiadis V (2015) Proving lock-freedom easily and automatically. In: CPP, pp. 119\u2013127. ACM","DOI":"10.1145\/2676724.2693179"},{"key":"370_CR28","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332. North-Holland\/IFIP"},{"key":"370_CR29","doi-asserted-by":"crossref","unstructured":"Malkis A, Podelski A, Rybalchenko A (2006) Thread-modular verification is cartesian abstract interpretation. In: ICTAC, Lecture Notes in Computer Science, vol. 4281, pp. 183\u2013197. Springer","DOI":"10.1007\/11921240_13"},{"key":"370_CR30","doi-asserted-by":"crossref","unstructured":"McMillan KL (1999) Circular compositional reasoning about liveness. In: CHARME, Lecture Notes in Computer Science, vol. 1703, pp. 342\u2013345. Springer","DOI":"10.1007\/3-540-48153-2_30"},{"key":"370_CR31","doi-asserted-by":"crossref","unstructured":"Michael MM, Scott ML (1996) Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267\u2013275. ACM","DOI":"10.1145\/248052.248106"},{"key":"370_CR32","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2011) Static analysis of run-time errors in embedded critical parallel C programs. In: ESOP, Lecture Notes in Computer Science, vol. 6602, pp. 398\u2013418. Springer","DOI":"10.1007\/978-3-642-19718-5_21"},{"key":"370_CR33","doi-asserted-by":"crossref","unstructured":"Pani T, Weissenbacher G, Zuleger F (2018) Rely-guarantee reasoning for automated bound analysis of lock-free algorithms. In: FMCAD, pp. 1\u20139. IEEE","DOI":"10.23919\/FMCAD.2018.8603020"},{"key":"370_CR34","doi-asserted-by":"crossref","unstructured":"Petrank E, Musuvathi M, Steensgaard B (2009) Progress guarantee for parallel programs via bounded lock-freedom. In: PLDI, pp. 144\u2013154. ACM","DOI":"10.1145\/1543135.1542493"},{"key":"370_CR35","unstructured":"Reynolds JC (2002) Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society"},{"issue":"1","key":"370_CR36","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn M, Zuleger F, Veith H (2017) Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason 59(1):3\u201345","journal-title":"J. Autom. Reason"},{"issue":"1","key":"370_CR37","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10817-016-9389-x","volume":"58","author":"T Str\u00f6der","year":"2017","unstructured":"Str\u00f6der T, Giesl J, Brockschmidt M, Frohn F, Fuhs C, Hensel J, Schneider-Kamp P, Aschermann C (2017) Automatically proving termination and memory safety for programs with pointer arithmetic. J. Autom. Reason 58(1):33\u201365","journal-title":"J. Autom. Reason"},{"key":"370_CR38","unstructured":"Treiber RK (1986) Systems programming: Coping with parallelism. Tech. Rep. RJ 5118, IBM Almaden Research Center"},{"key":"370_CR39","doi-asserted-by":"crossref","unstructured":"Vafeiadis V (2009) Shape-value abstraction for verifying linearizability. In: VMCAI, Lecture Notes in Computer Science, vol. 5403, pp. 335\u2013348. Springer","DOI":"10.1007\/978-3-540-93900-9_27"},{"key":"370_CR40","doi-asserted-by":"crossref","unstructured":"Vafeiadis V (2010) Automatically proving linearizability. In: CAV, Lecture Notes in Computer Science, vol. 6174, pp. 450\u2013464. Springer","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"370_CR41","doi-asserted-by":"crossref","unstructured":"Vafeiadis V (2010) Rgsep action inference. In: VMCAI, Lecture Notes in Computer Science, vol. 5944, pp. 345\u2013361. Springer","DOI":"10.1007\/978-3-642-11319-2_25"},{"issue":"2","key":"370_CR42","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu Q, de Roever WP, He J (1997) The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2):149\u2013174","journal-title":"Formal Asp. Comput."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00370-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00370-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00370-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T18:12:38Z","timestamp":1636481558000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00370-8"}},"subtitle":["With an application to proving that non-blocking algorithms are bounded lock-free"],"short-title":[],"issued":{"date-parts":[[2021,4,6]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["370"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00370-8","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2021,4,6]]},"assertion":[{"value":"6 April 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}