Responsive Parallelism with Synchronization (Video, PLDI 2023)
Stefan K. Muller, Kyle Singer, Devyn Terra Keeney, Andrew Neth, Kunal Agrawal, I-Ting Angelina Lee, and Umut A. Acar
(Illinois Institute of Technology, USA; Washington University in St. Louis, USA; Illinois Institute of Technology, USA; Illinois Institute of Technology, USA; Washington University in St. Louis, USA; Washington University in St. Louis, USA; Carnegie Mellon University, USA)
Abstract: 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.
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.
Article: https://doi.org/10.1145/3591249
Supplementary archive: https://doi.org/10.5281/zenodo.7706984 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)
ORCID: https://orcid.org/0000-0002-3210-9727, https://orcid.org/0009-0004-3588-2215, https://orcid.org/0009-0006-3343-6961, https://orcid.org/0009-0003-6709-2464, https://orcid.org/0000-0001-5882-6647, https://orcid.org/0000-0002-0687-5508, https://orcid.org/0000-0002-2623-4986
Video Tags: condition variables, priority inversions, type systems, cost semantics, pldi23main-p172-p, doi:10.1145/3591249, doi:10.5281/zenodo.7706984, orcid:0000-0002-3210-9727, orcid:0009-0004-3588-2215, orcid:0009-0006-3343-6961, orcid:0009-0003-6709-2464, orcid:0000-0001-5882-6647, orcid:0000-0002-0687-5508, orcid:0000-0002-2623-4986, Artifacts Available, Artifacts Evaluated — Reusable
Presentation at the PLDI 2023 conference, June 17–21, 2023, https://pldi23.sigplan.org/
Sponsored by ACM SIGPLAN,
Информация по комментариям в разработке