NDLI: TSOtool: a program for verifying memory systems using the memory consistency model

Content Provider	IEEE Xplore Digital Library
Author	Hangal, S. Vahia, D. Manovit, C. Lu, J.-Y.J. Narayanan, S.
Copyright Year	2004
Description	Author affiliation: Processor & Network Products, Sun Microsyst. India Private Ltd., Bangalore, India (Hangal, S.)
Abstract	In this paper, we describe TSOtool, a program to check the behavior of the memory subsystem in a shared memory multiprocessor. TSOtool runs pseudo-randomly generated programs with data races on a system compliant with the total store order (TSO) memory consistency model; it then checks the results of the program against the formal TSO specification. Such analysis can expose subtle memory errors like data corruption, atomicity violation and illegal instruction ordering. While verifying TSO compliance completely is an NP-complete problem, we describe a new polynomial time algorithm which is incorporated in TSOtool. In spite of being incomplete, it has been successful in detecting several bugs in the design of commercial microprocessors and systems, during both pre-silicon and post-silicon phases of validation.
Sponsorship	ACM SIGARCH IEEE Comput. Soc. TCCA
Starting Page	114
Ending Page	123
File Size	359258
Page Count	10
File Format	PDF
ISBN	0769521436
ISSN	10636897
DOI	10.1109/ISCA.2004.1310768
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2004-06-23
Publisher Place	Germany
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Computer bugs Protocols Programming profession Hardware Sun Polynomials Phase detection Microprocessors Multithreading Surface-mount technology
Content Type	Text
Resource Type	Article

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

TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model

Supporting fine-grained synchronization on a simultaneous multithreading processor

A dualthreaded Java processor for Java multithreading

Tracking down software bugs using automatic anomaly detection

Mapping Out a Path from Hardware Transactional Memory to Speculative Multithreading

Toward transparent selective sequential consistency in distributed shared memory systems

An Online Model Checking Tool for Safety and Liveness Bugs

Memory Leak Detection in Sun Solaris OS

Automated Security Debugging Using Program Structural Constraints

TSOtool: a program for verifying memory systems using the memory consistency model

Similar Documents

TSOtool: A Program for Verifying Memory Systems Using the Memory Consistency Model

Supporting fine-grained synchronization on a simultaneous multithreading processor

A dualthreaded Java processor for Java multithreading

Tracking down software bugs using automatic anomaly detection

Mapping Out a Path from Hardware Transactional Memory to Speculative Multithreading

Toward transparent selective sequential consistency in distributed shared memory systems

An Online Model Checking Tool for Safety and Liveness Bugs

Memory Leak Detection in Sun Solaris OS

Automated Security Debugging Using Program Structural Constraints

TSOtool: a program for verifying memory systems using the memory consistency model