TSO-CC and Coherence protocol verification

Add to your list(s) Download to your calendar using vCal

• Marco Elver (Edinburgh)
• Wednesday 29 October 2014, 13:00-14:00
• nonstandard room: SS03.

If you have a question about this talk, please contact Peter Sewell.

nonstandard room: SS03

The outline of the talk would be as follows:

• (25 min) Talk on TSO -CC, published earlier this year: http://homepages.inf.ed.ac.uk/s0787712/res/research/tsocc/hpca14_tso-cc.pdf

• (10 min) Motivate that existing verification techniques do not apply for consistency directed protocols. Challenges, open questions, and possible directions for verification of such protocols and the memory subsystem in general.

• (rest) Discussion.

Abstract:

“Traditional directory coherence protocols are designed for the strictest consistency model, sequential consistency (SC). When they are used for chip multiprocessors (CMPs) that support relaxed memory consistency models, such protocols turn out to be unnecessarily strict. Usually this comes at the cost of scalability (in terms of per core storage), which poses a problem with increasing number of cores in today’s CMPs, most of which no longer are sequentially consistent.”

“Because of the wide adoption of Total Store Order (TSO) and its variants in x86 and SPARC processors, and existing parallel programs written for these architectures, we propose TSO -CC, a cache coherence protocol for the TSO memory consistency model. TSO -CC does not track sharers, and instead relies on self-invalidation and detection of potential acquires using timestamps to satisfy the TSO memory consistency model lazily. Our results show that TSO -CC achieves average performance comparable to a MESI directory protocol, while TSO -CC’s storage overhead per cache line scales logarithmically with increasing core count.”

“While investigating options for formally verifying the TSO -CC coherence protocol against the target consistency model (TSO), it became apparent that typical verification methodologies for coherence protocols are not applicable. The talk concludes with a discussion on the possible directions for consistency directed coherence protocol verification.”

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• nonstandard room: SS03

Note that ex-directory lists are not shown.