liu.seSearch for publications in DiVA
Endre søk
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Verification of Cache Coherence Protocols wrt. Trace Filters
Uppsala University.
Uppsala University.
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska fakulteten.
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska högskolan.
Vise andre og tillknytning
2015 (engelsk)Konferansepaper, Publicerat paper (Fagfellevurdert)
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.

sted, utgiver, år, opplag, sider
IEEE, 2015.
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-128860ISBN: 9780983567851 (tryckt)OAI: oai:DiVA.org:liu-128860DiVA, id: diva2:932678
Konferanse
Formal Methods in Computer-Aided Design (FMCAD)
Tilgjengelig fra: 2016-06-02 Laget: 2016-06-02 Sist oppdatert: 2018-01-10

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

link

Personposter BETA

Ganjei, ZeinabRezine, Ahmed

Søk i DiVA

Av forfatter/redaktør
Ganjei, ZeinabRezine, Ahmed
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric

isbn
urn-nbn
Totalt: 880 treff
RefereraExporteraLink to record
Permanent link

Direct link
Referera
Referensformat
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Annet format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annet språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf