ACL2 Scripts for
An ACL2 Proof of Write Invalidate Cache Coherence

J Strother Moore


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: