Treffer: Fast and generalized polynomial time memory consistency verification
Title:
Fast and generalized polynomial time memory consistency verification
Source:
Computer aided verification (18th international conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006)0CAV 2006. :503-516
Publisher Information:
Berlin; New York: Springer, 2006.
Publication Year:
2006
Physical Description:
print, 16 ref 1
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Logiciel, Software, Génie logiciel, Software engineering, Complexité algorithme, Algorithm complexity, Complejidad algoritmo, Exécution programme, Program execution, Ejecución programa, Microprocesseur, Microprocessor, Microprocesador, Modélisation, Modeling, Modelización, Multitâche, Multithread, Multitarea, Méthode polynomiale, Polynomial method, Método polinomial, Problème NP difficile, NP hard problem, Problema NP duro, Temps polynomial, Polynomial time, Tiempo polinomial, Vérification programme, Program verification, Verificación programa
Document Type:
Konferenz
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Intel Corporation, United States
ISSN:
0302-9743
Rights:
Copyright 2007 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.19150380
Database:
PASCAL Archive
Weitere Informationen
The problem of verifying multi-threaded execution against the memory consistency model of a processor is known to be an NP hard problem. However polynomial time algorithms exist that detect almost all failures in such execution. These are often used in practice for microprocessor verification. We present a low complexity and fully parallelized algorithm to check program execution against the processor consistency model. In addition our algorithm is general enough to support a number of consistency models without any degradation in performance. An implementation of this algorithm is currently used in practice to verify processors in the post silicon stage for multiple architectures.