Lock inference for systems software

John Regehr, Alastair Reid
University of Utah
[pdf]

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

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.

BibTeX

@inproceedings{tsl-acp4is2003 , 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.} , affiliation = {University of Utah} , ar_file = {ACP4IS_03} , ar_shortname = {ACP4IS 03} , author = {John Regehr and Alastair Reid} , booktitle = {Proceedings of the Second AOSD Workshop on Aspects, Components, and Patterns for Infrastructure Software (ACP4IS)} , day = {17} , file = {tsl-acp4is.pdf} , location = {Boston, MA, USA} , month = {March} , title = {{L}ock inference for systems software} , year = {2003} }