Ändra sökning
RefereraExporteraLänk till posten
Permanent länk

Direktlänk
Referera
Referensformat
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Annat format
Fler format
Språk
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Annat språk
Fler språk
Utmatningsformat
  • html
  • text
  • asciidoc
  • rtf
Verifying safety and liveness for the FlexTM hybrid transactional memory
Uppsala universitet, Teknisk-naturvetenskapliga vetenskapsområdet, Matematisk-datavetenskapliga sektionen, Institutionen för informationsteknologi, Datorteknik.
University of Rochester, U.S.A..
Linköping University.
Simon Fraser University, Canada .
Visa övriga samt affilieringar
2013 (Engelska)Konferensbidrag, Publicerat paper (Refereegranskat)
Abstract [en]

We consider the verification of safety (strict serializability and abort consistency) and liveness obstruction and livelock freedom) for the hybrid transactional memory framework FlexTM. This framework allows for flexible implementations 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 of the latest antichain based techniques to handle systems with tens of thousands of states.

Ort, förlag, år, upplaga, sidor
Grenoble, France, 2013. 785-790 s.
Nationell ämneskategori
Datorsystem
Identifikatorer
URN: urn:nbn:se:uu:diva-213232ISBN: 978-1-4503-2153-2 (tryckt)OAI: oai:DiVA.org:uu-213232DiVA: diva2:681394
Konferens
Design, Automation and Test in Europe, DATE 13, Grenoble, France, March 18-22, 2013
Projekt
UPMARC
Tillgänglig från: 2013-12-19 Skapad: 2013-12-19 Senast uppdaterad: 2016-05-01

Open Access i DiVA

Fulltext saknas

Av organisationen
Datorteknik
Datorsystem

Sök vidare utanför DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetricpoäng

isbn
urn-nbn
Totalt: 451 träffar
RefereraExporteraLänk till posten
Permanent länk

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