Nondeterminism and the Correctness of Parallel Programs.

Abstract

This paper presents the weakest preconditions which describe weak correctness, blocking, deadlock, and starvation for nondeterministic programs. A procedure for converting parallel programs to nondeterministic programs is described, and the correctness of various example parallel programs is treated in this manner. Among these are a busy-wait mutual exclusion scheme, and the problem of the Five Dining Philosophers.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1977
Accession Number
ADA043450

Entities

People

  • Lawrence Flon
  • Norihisa Suzuki

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Computer Programming
  • Computer Science
  • Computers
  • Guarantees
  • Nutrition Disorders
  • Operating Systems
  • Scientific Research
  • Semantics
  • Sequences
  • Universities

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.