SwePub
Sök i LIBRIS databas

  Utökad sökning

WFRF:(Ros Alberto)
 

Sökning: WFRF:(Ros Alberto) > Mending fences with...

  • Abdulla, Parosh AzizUppsala universitet,Datorteknik,Avdelningen för datorteknik (författare)

Mending fences with self-invalidation and self-downgrade

  • Artikel/kapitelEngelska2018

Förlag, utgivningsår, omfång ...

  • 2018
  • printrdacarrier

Nummerbeteckningar

  • LIBRIS-ID:oai:DiVA.org:uu-347675
  • https://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-347675URI
  • https://doi.org/10.23638/LMCS-14(1:6)2018DOI

Kompletterande språkuppgifter

  • Språk:engelska
  • Sammanfattning på:engelska

Ingår i deldatabas

Klassifikation

  • Ämneskategori:ref swepub-contenttype
  • Ämneskategori:art swepub-publicationtype

Anmärkningar

  • Cache coherence protocols based on self-invalidation and self-downgrade have recently seen increased popularity due to their simplicity, potential performance efficiency, and low energy consumption. However, such protocols result in memory instruction reordering, thus causing extra program behaviors that are often not intended by the programmers. We propose a novel formal model that captures the semantics of programs running under such protocols, and features a set of fences that interact with the coherence layer. Using the model, we design an algorithm to analyze the reachability and check whether a program satisfies a given safety property with the current set of fences. We describe a method for insertion of optimal sets of fences that ensure correctness of the program under such protocols. The method relies on a counter-example guided fence insertion procedure. One feature of our method is that it can handle a variety of fences (with different costs). This diversity makes optimization more difficult since one has to optimize the total cost of the inserted fences, rather than just their number. To demonstrate the strength of our approach, we have implemented a prototype and run it on a wide range of examples and benchmarks. We have also, using simulation, evaluated the performance of the resulting fenced programs.

Ämnesord och genrebeteckningar

Biuppslag (personer, institutioner, konferenser, titlar ...)

  • Atig, Mohamed FaouziUppsala universitet,Datorteknik,Avdelningen för datorteknik(Swepub:uu)mohat117 (författare)
  • Kaxiras, StefanosUppsala universitet,Datorarkitektur och datorkommunikation,Avdelningen för datorteknik(Swepub:uu)steka984 (författare)
  • Leonardsson, CarlUppsala universitet,Datorteknik,Avdelningen för datorteknik(Swepub:uu)carle968 (författare)
  • Ros, Alberto (författare)
  • Zhu, YunyunUppsala universitet,Datorteknik,Avdelningen för datorteknik(Swepub:uu)yunzh803 (författare)
  • Uppsala universitetDatorteknik (creator_code:org_t)

Sammanhörande titlar

  • Ingår i:Logical Methods in Computer Science14:11860-5974

Internetlänk

Hitta via bibliotek

Till lärosätets databas

Sök utanför SwePub

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.

 
pil uppåt Stäng

Kopiera och spara länken för att återkomma till aktuell vy