  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.
