Publication
Formal Verification of a Reader-Writer Lock Implementation in C
Mark Hillebrand; Dirk Leinenbach
In: Proceedings of the 4th International Workshop on Systems Software Verification. International Workshop on Systems Software Verification (SSV-2009), June 22-24, Aachen, Germany, Pages 123-141, Electronic Notes in Theoretical Computer Science, Vol. 254, Elsevier Science B.V. 2009.
Abstract
We present the formal verification of a reader-writer lock implementation, which is a widely used synchronization primitive in multithreaded code. Specifications are given at the level of C code in the annotation language of Microsoft's Verifying C Compiler (VCC); VCC generates and discharges all verification conditions automatically. In addition to lock acquisition and release, we also deal with lock initialization. To accommodate different lock initialization patterns in client code, initialization is modeled in two phases. This work is part of a larger effort to specify and verify Microsoft's hypervisor Hyper-V at the code level in the context of the Verisoft XT project. Our results have been successfully transferred to the real lock implementation of Hyper-V and successfully used in the verification of client code.