Automatic Verification of Cache Coherence Protocols
via
Infinite-state Constraint-based Model Checking


Giorgio Delzanno giorgio@disi.unige.it

Contents


Introduction

In a shared-memory multiprocessor system local caches are used to reduce memory access latency and network traffic. Each processor is connected to a fast memory `backed up' by a large (and slower) main memory. This configuration enables processors to work on local copies of main memory blocks, greatly reducing the number of memory accesses that the processor must perform during program execution. Although local caches improve system performance, they introduce the cache coherence problem: multiple cached copies of the same block of memory must be consistent at any time during a run of the system.

A cache coherence protocol ensure the data consistency of the system: the value returned by a read must be always the last value written to that location (cf. [AB86,Han93]). Coherence policies are typically described as finite state machines that specify the way a single cache reacts to events like read and write requests. As an example, let us consider a CC-UMA (Uniform-Memory-Access with local Caches model) multiprocessor system, i.e., a system in which all processors have a local cache connected to the main memory via a shared bus. In write-invalidate protocols whenever a processor modifies its cache block a bus invalidation signal is sent to all other caches in order to invalidate their content. In write-update protocols, instead, a copy of the new data is sent to all caches that share the old data.

Verification. Due to the increasing complexity of hardware architectures and of the corresponding cache coherence policies, the development of automatic verification techniques is becoming a major goal to help discovering errors at an early stage of protocol design (see e.g. [CGH93]). In particular, one of the main challenges is to develop techniques for validating protocols independently from the number of processors in the system. (see e.g. [EN98,PD95]).

Our approach. Taking inspiration from recent works on verification of parameterized concurrent systems [GS92,EN98] we propose a new method for the verification of parameterized cache coherence protocols at the behavior (specification) level. As mentioned before, in this context a multiprocessor system can be modeled as a collection of many identical finite-state caches. We model such a system as an Extended Finite State Machines (EFSM) [CK97]. EFSMs are a particular class of infinite-state systems obtained by extending finite automata with (possibly unbounded) data variables ranging over integers. Intuitively, a configuration in the ESFM associated to a coherence protocol keeps track of the number of caches in every possible state of the protocol. We use then arithmetic constraints to implicitly represent (potentially infinite) sets of global states (global state=collection of the states of the local caches). This way, we achieve the following goals: (1) we represent all symmetric global states using a single EFSM-state; (2) we are able to represent safety properties independently from the number of processors; (3) we reduce the verification problem for parameterized cache coherence protocols to a reachability problem for EFSMs. The last problem can be attacked using general purpose, infinite-state symbolic model checking methods defined for integers or real arithmetics (see e.g. [BGP97,BW98,Hal93,HHWT97,DP99,SKR98]). In our approach we apply efficient tools based on real arithmetics (thus applying a relaxation from integers to reals during the analysis) to automatically check safety properties like data-consistency for snoopy, write-invalidate and write-update cache coherence protocols for CC-UMA multiprocessors [AB86,Han93].


Experimental results.

In preliminary experiments using symbolic model checkers for infinite-state systems based on real arithmetics HyTech [HHWT97] and DMC [DP99]) we have automatically verified safety properties for parameterized versions of widely implemented cache coherence policies like the Mesi, Berkeley RISC, Univesity of Illinois, DEC Firefly and Xerox PARC Dragon, and Futurebus+ protocols[Han93].

In the paper Automatic Verification of Cache Coherence Protocol (gzipped-ps) we give a formal description of the Synapse, Mesi, Moesi, Illinois, Dragon, Firefly, and Berkeley protocols using a description via a special kind of finite-state machines. Furthermore, we show how to translate the models into extended finite-state machines.

In the paper Verification of Consistency Protocols via Infinite-state Symbolic Model Checking - A Case Study - we give a formal description of the IEEE Futurebus+ protocol with a single bus

A description of the EFSM for the previous protocols using the specification language of HyTech and DMC is given below:

  1. Synapse HyTech code, DMC code;
  2. MESI HyTech code, DMC code;
  3. MOESI HyTech code, DMC code;
  4. Illinois HyTech code, DMC code;
  5. Berkeley HyTech code, DMC code;
  6. Firefly HyTech code, DMC code;
  7. Dragon HyTech code, DMC code;
  8. Futurebus+ HyTech code, DMC code.

The safety properties specified in the previous examples can be checked automatically using the tools HyTech [HHWT97] and DMC[DP99].


References

[ACJT96] P. A. Abdulla, K. Cerans, B. Jonsson and Y.-K. Tsay.
General Decidability Theorems for Infinite-State Systems.
In Proc. LICS'96, pages 313--321.
IEEE Computer Society Press, 1998.

[AB86] P. A. Archibald and J. Baer.
Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model.
ACM Transactions on Computer Systems 4(4): 273--298. 1986.

[BGP97] T. Bultan, R. Gerber, and W. Pugh.
{S}ymbolic {M}odel {C}hecking of {I}nfinite-state {S}ystems using {P}resburger {A}rithmetics.
In Proc. of CAV'97, LNCS 1254, pages 400--411.
Springer, 1997.

[BW98] B. Boigelot and P. Wolper.
{V}erifying {S}ystems with {I}nfinite but {R}egular {S}tate {S}pace.
In Proceedings of CAV'98, volume 1427 of LNCS, pages 88--97.
Springer, 1998.

[CK97] K.-T. Cheng and A. S. Krishnakumar,
Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model.
ACM Transactions on Design Automation of Electronic Systems 1(1):57--79, 1996.

[CGH93] E.M. Clarke, O. Grumberg, H. Hiraishi,
S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness.
Verification of the Futurebus+cache coherence protocol.
In Proc. of the Int'l Symposium on Computer Hardware Description Languages
and their Applications.
North-Holland, April 1993.

[DP99]G. Delzanno and A. Podelski
Model Checking in CLP.
In Proc. of TACAS'99, LNCS 1579, pages 223--239.
Springer, 1999.

[DP99b] G. Delzanno and A. Podelski
Constraint-based Deductive Model Checking (Draft)
Accepted for publication on the journal of Software Tools for Technology Transfer.
February 2000.

[EN98] E. A. Emerson and K. S. Namjoshi.
On {M}odel {C}hecking for {N}on-deterministic {I}nfinite-state {S}ystems.
In Proceedings of LICS '98, pages 70--80.
IEEE Computer Society Press, 1998.

[EFM99] J. Esparza, A. Finkel, and R. Mayr.
On the Verification of Broadcast Protocols.
In Proceedings of LICS'99, pages 352--359.
IEEE Computer Society Press, 1999.

[GS92] S. M. German, A. P. Sistla.
Reasoning about Systems with Many Processes.
JACM 39(3): 675--735 (1992)

[Hal93] N. Halbwachs.
Delay analysis in synchronous programs.
In Proceedings of CAV'93, volume 697 of LNCS.
Springer, 1993.

[Han93] J. Handy.
The Cache Memory Book.
Academic Press, 1993.

[HHW97] T. A. Henzinger, P.-H. Ho, and H. Wong-Toi.
HyTech: a Model Checker for Hybrid Systems.
In Proc. of CAV'97 LNCS 1254, pages 460--463.
Springer, 1997.

[PD97] F. Pong, M. Dubois.
Verification Techniques for Cache Coherence Protocols.
ACM Computing Surveys 29(1): 82--126 (199).

[PD93] F . Pong, M. Dubois.
The Verification of Cache Coherence Protocols.
In Proceedings of SPAA 93, pages 11--20.
ACM Press, 1993.

[PD95] F. Pong, M. Dubois.
A New Approach for the Verification of Cache Coherence Protocols.
IEEE Transactions on Parallel and Distributed Systems 6(8), August 1995

[SKR98] T. R. Shiple, J. H. Kukula, and R. K. Ranjan.
A Comparison of Presburger Engines for EFSM Reachability.
In Proceedings of CAV'98, volume 1427 of LNCS, pages 280--292.
Springer, 1998.