Techniques for developing verified concurrent programs based on monitors and semaphores

Abstract

In concurrent programming, mutual exclusion algorithms are used to avoid the simultaneous access of a common resource. Monitors are objects that can be used safely by more than one thread, as their methods are executed with mutual exclusion. In order for threads to wait for some condition to be met, monitors also provide a mechanism for threads to temporarily give up exclusive access. Monitors also have a mechanism for signaling other threads that some condition has been met. -- In this thesis, a general approach to monitors specification and verification code is developed which can be used for solving synchronization problems in an operating system. Specifications are given at the level of C code using the annotation language of Microsoft's Verifying C Compiler (VCC). VCC takes the annotated C program and tries to prove that the program meets these specifications. Later the proposed methodology is demonstrated with example applications.