Formal Verification of a Reader-Writer Lock Implementation in C

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.