Verifying Concurrent Programs with Shared Data Classes.
STANFORD UNIV CALIF DIGITAL SYSTEMS LAB
Pagination or Media Count:
Monitors are a valuable tool for organizing operations on shared data in concurrent programs. In some cases, however, the mutually exclusive procedure calls provided by monitors are overly restrictive. Such applications can be programmed using shared classes, which do not enforce mutual exclusion. This paper presents a method of verifying parallel programs containing shared classes. One first proves that each class procedure performs correctly when executed by itself, then shows that simultaneous execution of other class procedures can not interfere with its correct operation. Once a class has been verified, calls to its procedures may be treated as uninterruptible actions this simplifies the proof of higher-level program components. Proof rules for classes and procedure calls are given in Hoares axiomatic style. Several examples are verified, including two versions of the readers and writers problem and a dynamic resource allocator. Author
- Computer Programming and Software
- Computer Systems