Ä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
Counter-Example Guided Fence Insertion under TSO
Uppsala University, Sweden.
Uppsala University, Sweden.
Academia Sinica, Taiwan.
Uppsala University, Sweden.
Visa övriga samt affilieringar
2012 (Engelska)Ingår i: TACAS 2012, Berlin, Heidelberg: Springer , 2012Konferensbidrag, Publicerat paper (Refereegranskat)
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.

Ort, förlag, år, upplaga, sidor
Berlin, Heidelberg: Springer , 2012.
Serie
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 7214
Nationell ämneskategori
Data- och informationsvetenskap
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
Konferens
18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2012), Tallinn, Estonia, March 24 - April 1, 2012
Tillgänglig från: 2012-05-10 Skapad: 2012-05-10 Senast uppdaterad: 2018-01-25

Open Access i DiVA

Fulltext saknas i DiVA

Övriga länkar

Förlagets fulltext

Sök vidare i DiVA

Av författaren/redaktören
Rezine, Ahmed
Av organisationen
ESLAB - Laboratoriet för inbyggda systemTekniska högskolan
Data- och informationsvetenskap

Sök vidare utanför DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetricpoäng

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