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.