Verifying Cache Coherence in ACL2

Ben Selfridge, ACL2 Seminar, October 12, 2015

Abstract:

Virtually all processors use caches to temporarily house certain
memory locations, in order to avoid expensive memory accesses when
those locations are frequently read from/written to by the
processor. However, in a multiprocessor setting, we need to ensure
that we have ``cache coherence'' -- i.e., that no two cores/processors
may have the same memory location in their cache in a writable
state. This can lead to different processors ``seeing'' different
values for the same location, an obvious source of potential bugs. To
achieve this, modern multiprocessor architectures use cache coherence
protocols to manage the read/write status of a cache line across
multiple cores, in order to ensure that cache coherence is maintained
at all times.

This begs the question: How do we know that our cache coherence
protocol is correct, and does indeed forbid any two cores from writing
to the same (cached) location simultaneously? Generally, cache
protocols are verified with the help of model checkers; however, we
propose that a theorem prover like ACL2 could play an useful role in
the verification of such protocols, particularly when the size of the
protocol renders a naive application of model checking impractical due
to state explosion. We show that ACL2 can be used to verify cache
coherence for a very simple cache protocol, and we discuss how the
techniques developed in this verification effort could be used to
attack protocols that are too complex to be verified by a model
checker in a reasonable amount of time.