Techniques for developing verified concurrent programs based on monitors and semaphores

Fazilatunnessa (2012) Techniques for developing verified concurrent programs based on monitors and semaphores. Masters thesis, Memorial University of Newfoundland.

[English] PDF (Migrated (PDF/A Conversion) from original format: (application/pdf)) - Accepted Version Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission. Download (27MB) [English] PDF - Accepted Version Available under License - The author retains copyright ownership and moral rights in this thesis. Neither the thesis nor substantial extracts from it may be printed or otherwise reproduced without the author's permission. (Original Version)

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.

Actions (login required)

View Item