Using Flow Specifications of Parameterized Cache Coherence Protocols for Verifying Deadlock Freedom

Autor:	Muralidhar Talupur, Sharad Malik, Divjyot Sethi
Rok vydání:	2014
Předmět:	Model checking Hardware_MEMORYSTRUCTURES Theoretical computer science CPU cache Computer science Parameterized complexity Mutual exclusion Cache Parallel computing Software_PROGRAMMINGTECHNIQUES Deadlock Deadlock prevention algorithms Cache coherence
Zdroj:	Automated Technology for Verification and Analysis ISBN: 9783319119359 ATVA
DOI:	10.1007/978-3-319-11936-6_24
Popis:	We consider the problem of verifying deadlock freedom for symmetric cache coherence protocols. While there are multiple definitions of deadlock in the literature, we focus on a specific form of deadlock which is useful for the cache coherence protocol domain and is consistent with the internal definition of deadlock in theMurphi model checker: we refer to this deadlock as a system-wide deadlock (s-deadlock). In s-deadlock, the entire system gets blocked and is unable to make any transition. Cache coherence protocols consist of N symmetric cache agents, where N is an unbounded parameter; thus the verification of s-deadlock freedom is naturally a parameterized verification problem.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::b0320b490cd5d2358b919f8920f18bd1 https://doi.org/10.1007/978-3-319-11936-6_24 Zobrazit plný text záznamu