Specification-based Verification in a Distributed Shared Memory Simulation Model

Abstract

The emergence of chip multiprocessors is leading to rapid advances in hardware and software systems to provide distributed shared memory (DSM) programming models, so-called DSM systems. A DSM system provides programming advantages within a scalable and cost-effective hardware solution. This benefit derives from the fact that a DSM system creates a shared-memory abstraction on top of a distributed-memory machine by caching data replicas locally. In this respect, a coherence protocol is a vital component responsible for assuring data consistency across all replicas. The design of coherence protocols impacts a DSM system in terms of both performance and accuracy. Performance is often measured via simulation and various verification techniques have been proposed to deal with protocol accuracy. Nevertheless, integrating accuracy verification into a DSM cluster simulation to ensure correct simulation results is still an open issue. In this paper, we address three properties of a coherence protocol (safety, liveness, and inclusion) without which errors may occur in the simulation results. We propose a specification-based parameter—model interaction (SPMI) technique to detect these cases in a particular DSM cluster simulator called DSiMCluster. Our experimental results demonstrate that with SPMI, DSiMCluster can ensure the coherence protocol properties and provides a correct reflection of memory characteristics in shared-memory and DSM multiprocessors.

Keywords

distributed shared memory DSM cluster coherence protocol verification technique.

Get full access to this article

View all access options for this article.

References

Marathe, J. , F. Mueller and B. R. de Supinski. 2006. Analysis of cache-coherence bottlenecks with hybrid hardware/software techniques . ACM Transactions on Architecture and Code Optimization, 3(4): 390-423.

Moga, A. and M. Dubois. 2009. A comparative evaluation of hybrid distributed shared-memory systems. Journal of Systems Architecture, 55(1): 43-52.

Bennett, A.J. , T. Field and P. Harrison. 1996. Modelling and validation of shared memory coherency protocols. Performance Evaluation , 27-28: 541-563.

Field, A. , P. Harrison and K. Kanani. 1998. Automatic generation of verifiable cache coherence simulation models from high-level specifications. In Australian Computer Science Communications, 20: 261-275.

Sorin, D.J. , M. Plakal , A.E. Condon , M.D. Hill , M.M.K. Martin and D.A. Wood. 2002. Specifying and verifying a broadcast and a multicast snooping cache coherence protocol. IEEE Transactions on Parallel and Distributed Systems, 13(6): 556-578.

Pong, F. and M. Dubois. 1997. Verification techniques for cache coherence protocols . ACM Computing Surveys, 29(1): 82-126.

Delzanno, G. 2003. Constraint-based verification of parameterized cache coherence protocols. Formal Methods in System Design, 23(3):257-301.

Pong, F. and M. Dubois. 2000. Formal automatic verification of cache coherence in multiprocessors with relaxed memory models. IEEE Transactions on Parallel and Distributed Systems, 11(9): 989-1006.

Stoy, J.E. , X. Shen and Arvind. 2001. Proofs of correctness of cache coherence protocols. In FME 2001: Proceedings of Formal Methods Europe 2001 on Formal Methods for Increasing Software Productivity, Berlin, Germany, volume 2021 of Lecture Notes in Computer Science, Springer Verlag, pp. 43-71.

10.

Tasiran, S. , Y. Yu and B. Batson. 2003. Using a formal specification and a model checker to monitor and direct simulation. In DAC’03: Proceedings of the 40th conference on Design automation, Anaheim, CA , USA, ACM Press, pp. 356-361.

11.

Lv, Y. , H. Lin and H. Pan. 2007. Computing invariants for parameter abstraction. In MEMOCODE ’07: Proceedings of the 5th IEEE/ACM International Conference on Formal Methods and Models for Codesign, Washington, DC, USA, IEEE Computer Society, pp. 29-38.

12.

Qu,W. , Y. Guo , Z. Pang and X. Yang. 2008. Efficient verification of parameterized cache coherence protocols. In ICYCS 2008: Proceedings of the 9th International Conference for Young Computer Scientists 2008, IEEE Computer Society, pp. 154-159.

13.

Chame, J. and M. Dubois. 1993. Cache inclusion and processor sampling in multiprocessor simulations. In SIGMETRICS’93: Proceedings of the 1993 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems, San Diego, CA, USA, ACM Press, pp. 36-47.

14.

Baer, J.-L. and W.-H. Wang. 1988. On the inclusion properties for multi-level cache hierarchies . In ISCA ’88: Proceedings of the 15th Annual International Symposium on Computer architecture, Honolulu , Hawaii, IEEE Computer Society Press, pp. 73-80.

15.

Yilmaz, L. 2004 Verifying collaborative behavior in component-based DEVS models. Simulation: Transactions of the Society for Modeling and Simulation International, 80(7): 399-415.

16.

Marathe, J. , A. Nagarajan and F. Mueller. 2004. Detailed cache coherence characterization for OpenMP benchmarks . In ICS’04: Proceedings of the 18th Annual ACM International Conference on Supercomputing, Saint-Malo , France, ACM Press, pp. 287- 297.

17.

Martin, M.M.K. , D.J. Sorin , B.M. Beckmann , M.R. Marty , M. Xu , A.R. Alameldeen , K.E. Moore , M.D. Hill and D.A. Wood. 2005. Multifacet’s general execution-driven multiprocessor simulator (GEMS) toolset. ACM SIGARCH Computer Architecture News, 33(4): 92-99.

18.

Wainer, G. , L. Morihama and V. Passuello. 2002. Automatic verification of DEVS models. In SIW 2002: Proceedings of SISO Spring Interoperability Workshop , Orlando, FL, USA, Simulation Interoperability Standards Organization’s (SISO).

19.

Marurngsith, W. and R.N. Ibbett. 2009. DSiMCluster: a simulation model for efficient memory analysis experiments of DSM clusters. Simulation Transactions of the Society for Modeling and Simulation International , 85(6): 355-374.

20.

Borodin, D. and B. Juurlink. 2008. A low-cost cache coherence verification method for snooping systems. In DSD ’08: Proceedings of the 11th Euromicro Conference on Digital System Design Architectures, Methods and Tools , Parma, Italy, IEEE Computer Society Press, pp. 219-227.

21.

Dill, D.L. , A.J. Drexler , A.J. Hu and C.H. Yang. 1992. Protocol verification as a hardware design aid. In ICCD ’92: Proceedings of the 1992 IEEE International Conference on Computer Design on VLSI in Computer & Processors, Cambridge, MA, USA, IEEE Computer Society, pp.522-525.

22.

Marurngsith, W. 2006. Simulation Modelling of Distributed-Shared Memory Multiprocessors, PhD Thesis, Institute of Computing Systems Architecture, School of Informatics, University of Edinburgh, Edinburgh, UK.

23.

Shen, X. 2000. Design and Verification of Adaptive Cache Coherence Protocols , PhD Thesis, Massachusetts Institute of Technology, USA.

24.

Marurngsith, W. and R.N. Ibbett. 2005. Specification-based parameter-model interaction: towards a correct reflection of memory characteristics in a DSM cluster simulation. In SCSC’05: proceedings of The 2005 Summer Computer Simulation Conference, Philadelphia, USA, The Society for Modeling and Simulation International (SCS), pp.18-25.

25.

Jin, H. , M. Frumkin and J. Yan. 1999. The OpenMP Implementation of NAS Parallel Benchmarks and its Performance, NAS Technical Report NAS-99-011, NASA Ames Research Center, October 1999.

26.

Charlesworth, A. 2001. The sun fireplane system interconnect. In Supercomputing ’01: Proceedings of the 2001 ACM/IEEE Conference on Supercomputing (CDROM), Denver, Colorado, USA, ACM Press, pp. 7-7.