ACL2 Scripts for
An ACL2 Proof of Write Invalidate Cache Coherence
J Strother Moore
CAV'98
Abstract
As a pedagogical exercise in ACL2, we formalize and prove the correctness of
a write invalidate cache scheme. In our formalization, an arbitrary number of
processors, each with its own local cache, interact with a global memory
via a bus which is snooped by the caches.
The paper refers to three ACL2
books. Here they are: