Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Verification of Cache Coherence Protocols wrt. Trace Filters
Uppsala University.
Uppsala University.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, The Institute of Technology.
Show others and affiliations
2015 (English)Conference paper, Published paper (Refereed)
Abstract [en]

We address the problem of parameterized verification of cache coherence protocols for hardware accelerated transactional memories. In this setting, transactional memories leverage on the versioning capabilities of the underlying cache coherence protocol. The length of the transactions, their number, and the number of manipulated variables (i.e., cache lines) are parameters of the verification problem. Caches in such systems are finite-state automata communicating via broadcasts and shared variables. We augment our system with filters that restrict the set of possible executable traces according to existing conflict resolution policies. We show that the verification of coherence for parameterized cache protocols with filters can be reduced to systems with only a finite number of cache lines. For verification, we show how to account for the effect of the adopted filters in a symbolic backward reachability algorithm based on the framework of constrained monotonic abstraction. We have implemented our method and used it to verify transactional memory coherence protocols with respect to different conflict resolution policies.

Place, publisher, year, edition, pages
IEEE, 2015.
National Category
Computer Science
Identifiers
URN: urn:nbn:se:liu:diva-128860ISBN: 9780983567851 (print)OAI: oai:DiVA.org:liu-128860DiVA: diva2:932678
Conference
Formal Methods in Computer-Aided Design (FMCAD)
Available from: 2016-06-02 Created: 2016-06-02 Last updated: 2017-03-20

Open Access in DiVA

No full text

Other links

link

Search in DiVA

By author/editor
Ganjei, ZeinabRezine, Ahmed
By organisation
Software and SystemsFaculty of Science & EngineeringThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

Total: 83 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf