Software Engineering Conference, Australian (2009)
Gold Coast, Australia
Apr. 14, 2009 to Apr. 17, 2009
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASWEC.2009.43
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.
fractional permission, lock usage
J. Boyland and Y. Zhao, "Assuring Lock Usage in Multithreaded Programs with Fractional Permissions," 2009 Australian Software Engineering Conference (ASWEC 2009)(ASWEC), Gold Coast, QLD, 2009, pp. 277-286.