The Permission Approach to Comprehend Lock-Based Synchronization Policy

Lock-based synchronization is widely used to avoid data races in multithreaded programs. However, it is usually painful to verify the safety and correctness of lock usage because there may be some unpredictable interferences among different threads in parallel. In order to assure the usage of mutual-exclusion locks, we propose to interpret the synchronization policy as permission representations. A permission is a value associated with some piece of state in a program and it is designed to permit certain operations. Permission includes a characteristic property: "nesting," such that one permission may be designed to be nested into the other, with which we are able to simulate lock protection annotations and hence detect whether high level annotations match with underlying program code.