Lock inference for systems software

John Regehr Alastair Reid
regehr@cs.utah.edu    reid@cs.utah.edu   

University of Utah, School of Computing
50 South Central Campus Drive, Room 3190
Salt Lake City, Utah 84112-9205
http://www.cs.utah.edu/flux/

Abstract

We have developed task scheduler logic (TSL) to automate reasoning about scheduling and concurrency in systems software. TSL can detect race conditions and other errors as well as supporting lock inference: the derivation of an appropriate lock implementation for each critical section in a system. Lock inference solves a number of problems in creating flexible, reliable, and efficient systems software. TSL is based on a notion of asymmetrical preemption relations and it exploits the hierarchical inheritance of scheduling properties that is common in systems software.

In Proceedings of the Second AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software (ACP4IS), Boston, MA, March 17 2003.

This paper is © ACM 2003.


John Regehr <regehr@cs.utah.edu>