BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:TSO-CC and Coherence protocol verification - Marco Elver (Edinburg
 h)
DTSTART:20141029T130000Z
DTEND:20141029T140000Z
UID:TALK55827@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:The outline of the talk would be as follows:\n\n* (25 min) Tal
 k on TSO-CC\, published earlier this year:\n  http://homepages.inf.ed.ac.u
 k/s0787712/res/research/tsocc/hpca14_tso-cc.pdf\n\n* (10 min) Motivate tha
 t existing verification techniques do not apply\n  for consistency directe
 d protocols.  Challenges\, open questions\, and\n  possible directions for
  verification of such protocols and the memory\n  subsystem in general.\n\
 n* (rest) Discussion.\n\nAbstract:\n\n"Traditional directory coherence pro
 tocols are designed for the\nstrictest consistency model\, sequential cons
 istency (SC). When they are\nused for chip multiprocessors (CMPs) that sup
 port relaxed memory\nconsistency models\, such protocols turn out to be un
 necessarily strict.\nUsually this comes at the cost of scalability (in ter
 ms of per core\nstorage)\, which poses a problem with increasing number of
  cores in\ntoday's CMPs\, most of which no longer are sequentially consist
 ent."\n\n"Because of the wide adoption of Total Store Order (TSO) and its\
 nvariants in x86 and SPARC processors\, and existing parallel programs\nwr
 itten for these architectures\, we propose TSO-CC\, a cache coherence\npro
 tocol for the TSO memory consistency model. TSO-CC does not track\nsharers
 \, and instead relies on self-invalidation and detection of\npotential acq
 uires using timestamps to satisfy the TSO memory\nconsistency model lazily
 . Our results show that TSO-CC achieves average\nperformance comparable to
  a MESI directory protocol\, while TSO-CC's\nstorage overhead per cache li
 ne scales logarithmically with increasing\ncore count."\n\n"While investig
 ating options for formally verifying the TSO-CC coherence\nprotocol agains
 t the target consistency model (TSO)\, it became apparent\nthat typical ve
 rification methodologies for coherence protocols are not\napplicable. The 
 talk concludes with a discussion on the possible\ndirections for consisten
 cy directed coherence protocol verification."\n
LOCATION:nonstandard room: SS03
END:VEVENT
END:VCALENDAR