Using Belief to Reason About Cache Coherence
Authors: L. Mummert, J. Wing, and M. Satyanarayanan
In Proceedings of the Symposium on Principles of Distributed Computing.
Also appears as the technical report
CMU-CS-94-151, May 1994.
The full text of this paper
is here (in Postscript).
The full text of a longer version of the paper submitted to The Chicago Journal of Theoretical
Computer Science is here (in Postscript).
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 [Burrows, Abadi, Needham] 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.