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.

翻译：许多并发程序通过为线程分配优先级来提升响应性。然而，当与互斥锁、条件变量等同步机制结合使用时，优先级可能导致优先级反转——高优先级线程被低优先级线程延迟。互斥锁使用中的优先级反转可通过优先级继承等动态技术轻松处理，但条件变量使用中的优先级反转尚未得到充分研究，且动态技术并不适用。在本工作中，我们结合静态与动态技术，防止使用互斥锁和条件变量的代码中出现优先级反转。类型系统确保条件变量的安全使用，同时运行时通过动态技术改变线程优先级以消除互斥锁使用中的优先级反转。我们基于并行程序成本模型构建优先级反转模型，并证明系统的可靠性。为展示类型系统的实际可行性，我们将其编码至Rust和C++的类型系统中，并通过编写大规模案例研究（包括将Memcached对象服务器移植至我们的C++实现）证明其限制并不过于苛重。