Checking Parameterized Promela Models of Cache Coherence Protocols

Checking Parameterized Promela Models of Cache Coherence Protocols

This paper introduces a method for scalable verification of cache coherence protocols described in the Promela language. Scalability means that resources spent on verification (first of all, machine time and memory) do not depend on the number of processors in the system under verification. The meth...

Full description

Bibliographic Details
Main Authors: V. S. Burenkov, A. S. Kamkin
Format: Article
Language:English
Published: Ivannikov Institute for System Programming of the Russian Academy of Sciences 2018-10-01
Series:Труды Института системного программирования РАН
Subjects:
многоядерные микропроцессоры, мультипроцессоры с разделяемой памятью, протоколы когерентности памяти, проверка моделей, spin, promela
Online Access:https://ispranproceedings.elpub.ru/jour/article/view/139

Similar Items

Similar Items