{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:54Z","timestamp":1780994454745,"version":"3.54.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2107289, CCF-1910568, CCF-1943456, CCF-2107280, CCF-1901381, CCF-2115104, CCF-2119352, CCF-2107241, CCF-2216971, and CCF-2106699"],"award-info":[{"award-number":["CCF-2107289, CCF-1910568, CCF-1943456, CCF-2107280, CCF-1901381, CCF-2115104, CCF-2119352, CCF-2107241, CCF-2216971, and CCF-2106699"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>Many concurrent programs assign priorities to threads to improve responsiveness. When used in conjunction with synchronization mechanisms such as mutexes and condition variables, however, priorities can lead to priority inversions, in which high-priority threads are delayed by low-priority ones. Priority inversions in the use of mutexes are easily handled using dynamic techniques such as priority inheritance, but priority inversions in the use of condition variables are not well-studied and dynamic techniques are not suitable.<\/jats:p>\n          <jats:p>In this work, we use a combination of static and dynamic techniques to prevent priority inversion in code that uses mutexes and condition variables. A type system ensures that condition variables are used safely, even while dynamic techniques change thread priorities at runtime to eliminate priority inversions in the use of mutexes. We prove the soundness of our system, using a model of priority inversions based on cost models for parallel programs. To show that the type system is practical to implement, we encode it within the type systems of Rust and C++, and show that the restrictions are not overly burdensome by writing sizeable case studies using these encodings, including porting the Memcached object server to use our C++ implementation.<\/jats:p>","DOI":"10.1145\/3591249","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"712-735","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Responsive Parallelism with Synchronization"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3210-9727","authenticated-orcid":false,"given":"Stefan K.","family":"Muller","sequence":"first","affiliation":[{"name":"Illinois Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-3588-2215","authenticated-orcid":false,"given":"Kyle","family":"Singer","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-3343-6961","authenticated-orcid":false,"given":"Devyn Terra","family":"Keeney","sequence":"additional","affiliation":[{"name":"Illinois Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-6709-2464","authenticated-orcid":false,"given":"Andrew","family":"Neth","sequence":"additional","affiliation":[{"name":"Illinois Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5882-6647","authenticated-orcid":false,"given":"Kunal","family":"Agrawal","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0687-5508","authenticated-orcid":false,"given":"I-Ting Angelina","family":"Lee","sequence":"additional","affiliation":[{"name":"Washington University in St. Louis, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2623-4986","authenticated-orcid":false,"given":"Umut A.","family":"Acar","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"https:\/\/memcached.org\/ Accessed","year":"2019","unstructured":"2009. Memcached. https:\/\/memcached.org\/ Accessed in July 2019 2009. Memcached. https:\/\/memcached.org\/ Accessed in July 2019"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192391"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000101"},{"key":"e_1_2_1_4_1","first-page":"397","article-title":"L^ 3","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed , Matthew Fluet , and Greg Morrisett . 2007 . L^ 3 : A Linear Language with Locations. Fundam. Inform. , 77 , 4 (2007), 397 \u2013 449 . Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^ 3: A Linear Language with Locations. Fundam. Inform., 77, 4 (2007), 397\u2013449.","journal-title":"A Linear Language with Locations. Fundam. Inform."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434299"},{"key":"e_1_2_1_6_1","unstructured":"Arvind and K. P. Gostelow. 1978. The Id Report: An Asychronous Language and Computing Machine. Department of Information and Computer Science University of California Irvine. \t\t\t\t  Arvind and K. P. Gostelow. 1978. The Id Report: An Asychronous Language and Computing Machine. Department of Information and Computer Science University of California Irvine."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01088832"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/224164.224210"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 1st ACM SIGPLAN International Conference on Functional Programming. ACM, 213\u2013225","author":"Guy","unstructured":"Guy E. Blelloch and John Greiner. 1996. A provable time and space efficient implementation of NESL . In Proceedings of the 1st ACM SIGPLAN International Conference on Functional Programming. ACM, 213\u2013225 . Guy E. Blelloch and John Greiner. 1996. A provable time and space efficient implementation of NESL. In Proceedings of the 1st ACM SIGPLAN International Conference on Functional Programming. ACM, 213\u2013225."},{"key":"e_1_2_1_10_1","volume-title":"International Static Analysis Symposium. 55\u201372","author":"Boyland John","year":"2003","unstructured":"John Boyland . 2003 . Checking interference with fractional permissions . In International Static Analysis Symposium. 55\u201372 . John Boyland. 2003. Checking interference with fractional permissions. In International Static Analysis Symposium. 55\u201372."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/321812.321815"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1248648.1248652"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094852"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/36072.36073"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the 9th International Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT","author":"Cucinotta Tommaso","year":"2013","unstructured":"Tommaso Cucinotta . 2013 . Priority Inheritance on Condition Variables . Proceedings of the 9th International Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT 2013). Tommaso Cucinotta. 2013. Priority Inheritance on Condition Variables. Proceedings of the 9th International Workshop on Operating Systems Platforms for Embedded Real-Time applications (OSPERT 2013)."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.21127"},{"key":"e_1_2_1_18_1","first-page":"5","article-title":"Implicitly threaded parallelism in Manticore","volume":"20","author":"Fluet Matthew","year":"2011","unstructured":"Matthew Fluet , Mike Rainey , John Reppy , and Adam Shaw . 2011 . Implicitly threaded parallelism in Manticore . Journal of Functional Programming , 20 , 5 - 6 (2011), 1\u201340. Matthew Fluet, Mike Rainey, John Reppy, and Adam Shaw. 2011. Implicitly threaded parallelism in Manticore. Journal of Functional Programming, 20, 5-6 (2011), 1\u201340.","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_1_19_1","first-page":"690","volume-title":"Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming (DAMP \u201907)","author":"Fluet Matthew","year":"2007","unstructured":"Matthew Fluet , Mike Rainey , John Reppy , Adam Shaw , and Yingqi Xiao . 2007 . Manticore: A Heterogeneous Parallel Language . In Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming (DAMP \u201907) . 37\u201344. isbn:978-1-59593- 690 - 695 Matthew Fluet, Mike Rainey, John Reppy, Adam Shaw, and Yingqi Xiao. 2007. Manticore: A Heterogeneous Parallel Language. In Proceedings of the 2007 Workshop on Declarative Aspects of Multicore Programming (DAMP \u201907). 37\u201344. isbn:978-1-59593-690-5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4478"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/800055.802017"},{"key":"e_1_2_1_24_1","volume-title":"Operating system principles","author":"Hansen Per Brinch","unstructured":"Per Brinch Hansen . 1973. Operating system principles . Prentice-Hall, Inc. . Per Brinch Hansen. 1973. Operating system principles. Prentice-Hall, Inc.."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1109\/TSE.1975.6312840","article-title":"The programming language concurrent pascal","author":"Hansen Per Brinch","year":"1975","unstructured":"Per Brinch Hansen . 1975 . The programming language concurrent pascal . IEEE Transactions on Software Engineering , 199 \u2013 207 . Per Brinch Hansen. 1975. The programming language concurrent pascal. IEEE Transactions on Software Engineering, 199\u2013207.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"e_1_2_1_26_1","volume-title":"FTfJP\u201911","author":"Heule Stefan","year":"2011","unstructured":"Stefan Heule , Rustan Leino , Peter M\u00fcller , and Alexander J. Summers . 2011. Fractional Permissions without the Fractions . In FTfJP\u201911 , July 26, 2011 , Lancaster, UK.. Stefan Heule, Rustan Leino, Peter M\u00fcller, and Alexander J. Summers. 2011. Fractional Permissions without the Fractions. In FTfJP\u201911, July 26, 2011, Lancaster, UK.."},{"key":"e_1_2_1_27_1","volume-title":"Monitors: An operating system structuring concept. In The origin of concurrent programming","author":"Richard Hoare Charles Antony","year":"1974","unstructured":"Charles Antony Richard Hoare . 1974 . Monitors: An operating system structuring concept. In The origin of concurrent programming . Springer , 272\u2013294. Charles Antony Richard Hoare. 1974. Monitors: An operating system structuring concept. In The origin of concurrent programming. Springer, 272\u2013294."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2647508.2647514"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358824"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062370"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236790"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386013"},{"key":"e_1_2_1_33_1","volume-title":"Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee, and Umut A. Acar.","author":"Muller Stefan K.","year":"2023","unstructured":"Stefan K. Muller , Kyle Singer , Devyn Terra Keeney , Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee, and Umut A. Acar. 2023 . Responsive Parallelism with Synchronization . arxiv:2304.03753. Stefan K. Muller, Kyle Singer, Devyn Terra Keeney, Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee, and Umut A. Acar. 2023. Responsive Parallelism with Synchronization. arxiv:2304.03753."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP","author":"Muller Stefan K.","year":"2019","unstructured":"Stefan K. Muller , Sam Westrick , and Umut A. Acar . 2019. Fairness in Responsive Parallelism . In Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019 ). Stefan K. Muller, Sam Westrick, and Umut A. Acar. 2019. Fairness in Responsive Parallelism. In Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming (ICFP 2019)."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103722"},{"key":"e_1_2_1_36_1","volume-title":"Chakravarty","author":"Peyton Jones Simon L.","year":"2008","unstructured":"Simon L. Peyton Jones , Roman Leshchinskiy , Gabriele Keller , and Manuel M. T . Chakravarty . 2008 . Harnessing the Multicores : Nested Data Parallelism in Haskell. In FSTTCS. 383\u2013414. Simon L. Peyton Jones, Roman Leshchinskiy, Gabriele Keller, and Manuel M. T. Chakravarty. 2008. Harnessing the Multicores: Nested Data Parallelism in Haskell. In FSTTCS. 383\u2013414."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951935"},{"key":"e_1_2_1_38_1","volume-title":"Programming Symposium, Proceedings Colloque sur la Programmation","author":"Reynolds John C.","year":"1974","unstructured":"John C. Reynolds . 1974 . Towards a theory of type structure . In Programming Symposium, Proceedings Colloque sur la Programmation , Paris, France , April 9-11, 1974. 408\u2013423. John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974. 408\u2013423."},{"key":"e_1_2_1_39_1","doi-asserted-by":"crossref","unstructured":"Mads Rosendahl. 1989. Automatic complexity analysis. In FPCA \u201989: Functional Programming Languages and Computer Architecture. ACM 144\u2013156. \t\t\t\t  Mads Rosendahl. 1989. Automatic complexity analysis. In FPCA \u201989: Functional Programming Languages and Computer Architecture. ACM 144\u2013156.","DOI":"10.1145\/99370.99381"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/645388.757552"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"e_1_2_1_42_1","volume-title":"Peter Baer Galvin, and Greg Gagne","author":"Silberschatz Abraham","year":"2005","unstructured":"Abraham Silberschatz , Peter Baer Galvin, and Greg Gagne . 2005 . Operating system concepts (7. ed.). Wiley . Abraham Silberschatz, Peter Baer Galvin, and Greg Gagne. 2005. Operating system concepts (7. ed.). Wiley."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3350755.3400236"},{"key":"e_1_2_1_44_1","volume-title":"Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900)","author":"Smith Frederick","unstructured":"Frederick Smith , David Walker , and J. Gregory Morrisett . 2000 . Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900) . Springer-Verlag, London, UK, UK. 366\u2013381. Frederick Smith, David Walker, and J. Gregory Morrisett. 2000. Alias Types. In Proceedings of the 9th European Symposium on Programming Languages and Systems (ESOP \u201900). Springer-Verlag, London, UK, UK. 366\u2013381."},{"key":"e_1_2_1_45_1","volume-title":"Proceedings of the 47th Annual ACM Symposium on Principles of Programming Languages (POPL).","author":"Westrick Sam","unstructured":"Sam Westrick , Rohan Yadav , Matthew Fluet , and Umut A. Acar . 2020. Disentanglement in Nested-Parallel Programs . In Proceedings of the 47th Annual ACM Symposium on Principles of Programming Languages (POPL). Sam Westrick, Rohan Yadav, Matthew Fluet, and Umut A. Acar. 2020. Disentanglement in Nested-Parallel Programs. In Proceedings of the 47th Annual ACM Symposium on Principles of Programming Languages (POPL)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591249","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591249","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":45,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591249"],"URL":"https:\/\/doi.org\/10.1145\/3591249","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}