Home         Authors   Papers   Year of conference   Themes   Organizations        To MES conference

A Method for Scalable Verification of PROMELA Models of Cache Coherence Protocols
Authors
	Kamkin A.S.
	Burenkov V.S.
Date of publication
	2016
Abstract
	This paper introduces a method for scalable functional verification of cache coherence protocols described in the PROMELA language. Scalability means that verification efforts does not depend on the model size (that is, the number of processors in the system under verification). The method is comprised of three main steps. First, a PROMELA specification written for a certain configuration of the system under verification is generalized to the specification parameterized with the number of processors (to do it, some assumptions on the protocol are used as well as simple induction rules). Second, the parameterized specification is abstracted from the number of processors (it is done by syntax transformation of the specification). Finally, the abstract specification is verified with the SPIN model checker in a usual way. The method has been successfully applied to verification of the MOSI protocol implemented in the Elbrus computer systems.
Keywords
	multicore microprocessors, shared memory multiprocessors, cache coherence protocols, model checking, SPIN, PROMELA.
Library reference
	Kamkin A.S., Burenkov V.S. A Method for Scalable Verification of PROMELA Models of Cache Coherence Protocols // Problems of Perspective Micro- and Nanoelectronic Systems Development - 2016. Proceedings / edited by A. Stempkovsky, Moscow, IPPM RAS, 2016. Part 2. P. 54-60.
URL of paper
	http://www.mes-conference.ru/data/year2016/pdf/D109.pdf