Verifying Programs That Use Causally-Ordered Message-Passing

Abstract

We give an operational model of causally-ordered message-passing primitives. Based on this model, we formulate a Hoare-style proof system for causally-ordered delivery. To illustrate the use of this proof system and to demonstrate the feasibility of applying invariant-based verification techniques to algorithms that depend on causally-ordered delivery, we verify an- asynchronous variant of the distributed termination detection algorithm of Dijkstra, Feijen, and van Gasteren. Verification, Message-passing, Causal delivery.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 15, 1994
Accession Number
ADA280121

Entities

People

  • Fred B. Schneider
  • Scott D. Stoller

Organizations

  • Cornell University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Classification
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Detection
  • Iterations
  • Language
  • Military Research
  • Notation
  • Programming Languages
  • Reasoning
  • Software Development
  • Universities
  • Verification

Fields of Study

  • Computer science

Readers

  • Control Systems Engineering.
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.