NDLI: Application of Esterel for modelling and verification of Cachet protocol on CRF memory model

Content Provider	IEEE Xplore Digital Library
Author	Phanse, S.R. Shyamasundar, R.K.
Copyright Year	2001
Description	Author affiliation: Sch. of Technol. & Comput. Sci., Tata Inst. of Fundamental Res., Mumbai, India (Phanse, S.R.)
Abstract	Synchronous languages have been widely used for the reliable design of reactive systems and synchronous circuits as it has become possible to move from the realm of simulations to that of proofs. While ESTEREL has been used for the modelling and verification of reactive systems, it has not been used that widely for the modelling and verification of cache coherency protocols. In this paper, we discuss the use of ESTEREL for the modelling and verification of cache coherence protocols, in particular on the adaptive cache coherence protocols called CACHET built on the Commit-Reconcile and Fences (CRF) distributed shared memory model. In the paper, we (i) first, model the CRF memory model along with the various CACHET micro-protocols in ESTEREL, (ii) verify properties of the CACHET micro-protocols in a graded manner reflecting the protocol design using the synchronous observer method, and (iii) highlight the experiences in overcoming limitations including state-explosion.
Sponsorship	Broadcom India
Starting Page	179
Ending Page	188
File Size	983306
Page Count	10
File Format	PDF
ISBN	0769508316
ISSN	10639667
DOI	10.1109/ICVD.2001.902658
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2001-01-07
Publisher Place	India
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Coherence Access protocols Read-write memory Cache memory Delay Writing Application software Computer science Computational modeling Computer simulation
Content Type	Text
Resource Type	Article
Subject	Electrical and Electronic Engineering Hardware and Architecture

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Application of esterel for modelling and verification of cachet protocol on crf memory model (2001).

Cache coherence in a multiport memory environment

Design verification of the S3.mp cache-coherent shared-memory system

Improving the performance of software distributed shared memory with speculation

Flexible Decoupled Transactional Memory Support

Specifying and verifying a broadcast and a multicast snooping cache coherence protocol

Write buffer design for cache-coherent shared-memory multiprocessors

Modeling Multiprocessor Cache Protocol Impact on MPI Performance

A simulation-based method for the verification of shared memory in multiprocessor systems

Application of Esterel for modelling and verification of Cachet protocol on CRF memory model

Similar Documents

Application of esterel for modelling and verification of cachet protocol on crf memory model (2001).

Cache coherence in a multiport memory environment

Design verification of the S3.mp cache-coherent shared-memory system

Improving the performance of software distributed shared memory with speculation

Flexible Decoupled Transactional Memory Support

Specifying and verifying a broadcast and a multicast snooping cache coherence protocol

Write buffer design for cache-coherent shared-memory multiprocessors

Modeling Multiprocessor Cache Protocol Impact on MPI Performance

A simulation-based method for the verification of shared memory in multiprocessor systems

Application of Esterel for modelling and verification of Cachet protocol on CRF memory model