Verifying Concurrent Programs with Shared Data Classes.

Abstract

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 Hoare's axiomatic style. Several examples are verified, including two versions of the readers and writers problem and a dynamic resource allocator. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1977
Accession Number
ADA048637

Entities

People

  • Susan Owicki

Organizations

  • Stanford University

Tags

Communities of Interest

  • Space
  • Weapons Technologies

DTIC Thesaurus Topics

  • Air Force
  • Air Force Facilities
  • Computer Science
  • Computers
  • Electrical Engineering
  • Electronics
  • Electronics Laboratories
  • Engineering
  • Guarantees
  • Indexes
  • Language
  • Materials
  • Military Research
  • New York
  • Operating Systems
  • Standards
  • Test And Evaluation

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Computer Science.
  • Database Systems and Applications