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
Verifying Safety and Liveness for the FlexTM Hybrid Transactional Memory
Uppsala University, Sweden.
University of Rochester, U.S.A..
Linköpings universitet, Institutionen för datavetenskap, Programvara och system. Linköpings universitet, Tekniska högskolan.
Simon Fraser University, Canada.
Vise andre og tillknytning
2013 (engelsk)Inngår i: Design, Automation & Test in Europe (DATE 2013), Grenoble, France, March 18-22, 2013., IEEE , 2013, s. 785-790Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

We consider the verification of safety (strict se- rializability and abort consistency) and liveness (obstruction and livelock freedom) for the hybrid transactional memory framework FLEXTM. This framework allows for flexible imple- mentations of transactional memories based on an adaptation of the MESI coherence protocol. FLEXTM allows for both eager and lazy conflict resolution strategies. Like in the case of Software Transactional Memories, the verification problem is not trivial as the number of concurrent transactions, their size, and the number of accessed shared variables cannot be a priori bounded. This complexity is exacerbated by aspects that are specific to hardware and hybrid transactional memories. Our work takes into account intricate behaviours such as cache line based conflict detection, false sharing, invisible reads or non-transactional instructions. We carry out the first automatic verification of a hybrid transactional memory and establish, by adopting a small model approach, challenging properties such as strict serializability, abort consistency, and obstruction freedom for both an eager and a lazy conflict resolution strategies. We also detect an example that refutes livelock freedom. To achieve this, our prototype tool makes use the latest antichain based techniques to handle systems with tens of thousands of states.

sted, utgiver, år, opplag, sider
IEEE , 2013. s. 785-790
Serie
Design, Automation and Test in Europe, ISSN 1530-1591
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-92598DOI: 10.7873/DATE.2013.167ISI: 000415129400152ISBN: 978-1-4673-5071-6 (tryckt)OAI: oai:DiVA.org:liu-92598DiVA, id: diva2:621309
Konferanse
16th Design, Automation and Test in Europe Conference and Exhibition, DATE 2013; Grenoble; France
Tilgjengelig fra: 2013-05-14 Laget: 2013-05-14 Sist oppdatert: 2019-07-03

Open Access i DiVA

Fulltekst mangler i DiVA

Andre lenker

Forlagets fulltekst

Personposter BETA

Rezine, Ahmed

Søk i DiVA

Av forfatter/redaktør
Rezine, Ahmed
Av organisasjonen

Søk utenfor DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric

doi
isbn
urn-nbn
Totalt: 851 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