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
Counter-Example Guided Fence Insertion under TSO
Uppsala University, Sweden.
Uppsala University, Sweden.
Academia Sinica, Taiwan.
Uppsala University, Sweden.
Vise andre og tillknytning
2012 (engelsk)Inngår i: TACAS 2012, Berlin, Heidelberg: Springer , 2012Konferansepaper, Publicerat paper (Fagfellevurdert)
Abstract [en]

We give a sound and complete fence insertion procedure for concurrentfinite-state programs running under the classical TSO memory model. Thismodel allows “write to read” relaxation corresponding to the addition of an unboundedstore buffer between each processor and the main memory. We introducea novel machine model, called the Single-Buffer (SB) semantics, and show thatthe reachability problem for a program under TSO can be reduced to the reachabilityproblem under SB. We present a simple and effective backward reachabilityanalysis algorithm for the latter, and propose a counter-example guided fence insertionprocedure. The procedure is augmented by a placement constraint thatallows the user to choose places inside the program where fences may be inserted.For a given placement constraint, we automatically infer all minimal setsof fences that ensure correctness. We have implemented a prototype and run itsuccessfully on all standard benchmarks together with several challenging examplesthat are beyond the applicability of existing methods.

sted, utgiver, år, opplag, sider
Berlin, Heidelberg: Springer , 2012.
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 7214
HSV kategori
Identifikatorer
URN: urn:nbn:se:liu:diva-77285DOI: 10.1007/978-3-642-28756-5_15ISI: 000342900100015ISBN: 978-3-642-28755-8 (tryckt)ISBN: 978-3-642-28756-5 (tryckt)OAI: oai:DiVA.org:liu-77285DiVA, id: diva2:526205
Konferanse
18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia, March 24 - April 1, 2012
Tilgjengelig fra: 2012-05-10 Laget: 2012-05-10 Sist oppdatert: 2018-01-25

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: 738 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