Assuring Lock Usage in Multithreaded Programs with Fractional Permissions

Lock-based synchronization is widely used to avoid data races in multithreaded programs. However, it is hard to assure or verify the safety and correctness of lock usage because of unpredictable interferences between threads. This paper proposes to use a fractional permission system to assure the correct usage of mutual-exclusion locks, that neither data races and deadlocks occur. A permission is an abstract value associated with some piece of state in a program and it is designed to permit corresponding operations. Our permission system includes two characteristic properties: fractions and nesting. Fractions allows one permission to be split into several pieces. Nesting builds a protection relation between the nested and nester permissions. Using our system, we can express the semantics of several lock annotations and then use a permission checker to determine whether given annotations match with underlying program code.