Using Belief to Reason About Cache Coherence

Abstract

The notion of belief has been useful in reasoning about authentication protocols. In this paper, we show how the notion of belief can be applied to reasoning about cache coherence in a distributed file system. To the best of our knowledge, this is the first formal analysis of this problem. We used an extended subset of a logic of authentication to help us analyze three cache coherence protocols: a validate-on-use protocol, an invalidation-based protocol, and a new large granularity protocol for use in weakly connected environments. In this paper, we present two runs from the large granularity protocol. Using our variant of the logic of authentication, we were able to find flaws in the design of the large granularity protocol. We found the notion of belief not only intuitively appealing for reasoning about our protocols, but also practical given the optimistic nature of our system model.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1994
Accession Number
ADA280060

Entities

People

  • Jeannette Wing
  • Lily B. Mummert
  • Mahadev Satyanarayanan

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Air Platforms
  • Autonomy
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Agreements
  • Authentication
  • Computer Programming
  • Computer Science
  • Computers
  • Damage Detection
  • Detection
  • Environment
  • Information Systems
  • Language
  • Notation
  • Operating Systems
  • Security Protocols
  • Software Development
  • Standards
  • Validation
  • Verification

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Computer Networking
  • Parallel and Distributed Computing.