Using flow specifications of parameterized cache coherence protocols for verifying deadlock freedom

Divjyot Sethi, Muralidhar Talupur, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

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.

Parametrized verification techniques work by using sound abstractions to reduce the unbounded model to a bounded model. Efficient abstractions which work well for industrial scale protocols typically bound the model by replacing the state of most of the agents by an abstract environment, while keeping just one or two agents as is. However, leveraging such efficient abstractions becomes a challenge for s-deadlock: a violation of s-deadlock is a state in which the transitions of all of the unbounded number of agents cannot occur and so a simple abstraction like the one above will not preserve this violation. Authors of a prior paper, in fact, proposed using a combination of over and under abstractions for verifying such properties. While quite promising for a large class of deadlock errors, simultaneously tuning over and under abstractions can become complex.

In this work we address this challenge by presenting a technique which leverages high-level information about the protocols, in the form of message sequence diagrams referred to as flows, for constructing invariants that are collectively stronger than s-deadlock. Further, violations of these invariants can involve only one or two interacting agents: thus they can be verified using efficient abstractions like the ones described above.We show how such invariants for the German and Flash protocols can be successfully derived using our technique and then be verified.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings
EditorsFranck Cassez, Jean-François Raskin
PublisherSpringer Verlag
Pages330-347
Number of pages18
ISBN (Electronic)9783319119359
DOIs
StatePublished - Jan 1 2014
Event12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia
Duration: Nov 3 2014Nov 7 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8837
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
CountryAustralia
CitySydney
Period11/3/1411/7/14

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Using flow specifications of parameterized cache coherence protocols for verifying deadlock freedom'. Together they form a unique fingerprint.

  • Cite this

    Sethi, D., Talupur, M., & Malik, S. (2014). Using flow specifications of parameterized cache coherence protocols for verifying deadlock freedom. In F. Cassez, & J-F. Raskin (Eds.), Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings (pp. 330-347). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8837). Springer Verlag. https://doi.org/10.1007/978-3-319-11936-6_24