University of Cambridge > Talks.cam > REMS lunch > TSO-CC and Coherence protocol verification

TSO-CC and Coherence protocol verification

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

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

nonstandard room: SS03

The outline of the talk would be as follows:

  • (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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity