Model Checking Cache Coherence in System-Level Code

Cache coherence is a key consistency requirement between the shared main memory and individual caches for a multiprocessor framework. Several months ago, we started a project to verify the cache coherence of a system-level C codebase (50,000+ lines), which runs in an environment that does not provide hardware-level guarantees, requiring programmers to ensure correct cache coherence manually through explicit FLUSH and INVALIDATE operations. After initial evaluation and comparison of many model checking tools, we believe that SPIN is the most suitable one. However, pure model checking is not sufficiently scalable to verify such a large codebase. Therefore, we are currently investigating a hybrid model checking solution with some static analysis techniques to reduce the model size via abstraction and program slicing, and restrict the interleavings explored. In this talk, we will share our model checking experiences. In particular, we will discuss (1) our evaluation of different model checking tools, (2) the Promela model we use to verify the cache coherence, (3) initial model checking experience for verifying the coherence in concurrent quicksort algorithm, and (4) the automatic model extraction from large codebase in C.