This Article Full Text (OnlineFirst PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to Saved Citations Download to citation manager Request Permissions Request Reprints Add to My Marked Citations Citing Articles Citing Articles via Scopus Google Scholar Articles by Marurngsith, W. Articles by Ibbett, R. N. Social Bookmarking                         What's this?

Specification-based Verification in a Distributed Shared Memory Simulation Model

¹ Department of Computer Science, Faculty of Science and Technology, Thammasat University, Pathum Thani, 12121, Thailand
² Edinburgh Parallel Computing Centre, University of Edinburgh, Edinburgh, UK

^* To whom correspondence should be addressed. E-mail: wmrs{at}cs.tu.ac.th.

	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.

First published on October 22, 2009
SIMULATION 2009, doi:10.1177/0037549709349843


CiteULike    Complore    Connotea    Del.icio.us    Digg    Reddit    Technorati    Twitter    What's this?