Using Belief to Reason About Cache Coherence
L. Mummert, J.M. Wing, and M. Satyanarayanan
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.