Assure Parallel Interference Patterns in Multithreaded Programs with Permissions

This paper proposes to use permissions to assure some important parallel interference patterns in multithreaded programs. With pre-defined annotations, programmers are able to express their design intent which could be interpreted 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. There are two inherent transformations among permissions: fraction and nesting, such that the former allows one permission to be split into several pieces, while the latter builds a protection relation between the nested and nester permissions. Based on the permission interpretation and reasoning, we are able to tell whether the high level annotations match with the low level program code and hence some important interference patterns in multithreaded programs could be assured.