HieraGen: Automated Generation of Concurrent, Hierarchical Cache Coherence Protocols

被引:6
作者
Oswald, Nicolai [1 ]
Nagarajan, Vijay [1 ]
Sorin, Daniel J. [2 ]
机构
[1] Univ Edinburgh, Edinburgh, Midlothian, Scotland
[2] Duke Univ, Durham, NC 27706 USA
来源
2020 ACM/IEEE 47TH ANNUAL INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE (ISCA 2020) | 2020年
关键词
D O I
10.1109/ISCA45697.2020.00077
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We present HieraGen, a new tool for automatically generating hierarchical cache coherence protocols. HieraGen's inputs are the simple, atomic, stable state protocols for each level of the hierarchy. HieraGen's output is a highly concurrent hierarchical protocol, in the form of the finite state machines for all of the cache and directory controllers. HieraGen thus reduces the complexity that architects face, by offloading the challenging tasks of composing protocols and managing concurrency. Experiments show that HieraGen can automatically generate correct-by-construction MOESI family of hierarchical protocols with dozens of states and hundreds of transitions. We have verified all of the generated protocols for safety and deadlock freedom using a model checker.
引用
收藏
页码:888 / 899
页数:12
相关论文
共 23 条
  • [1] Alsop J, 2016, INT SYMP MICROARCH
  • [2] [Anonymous], 2010, MICRO
  • [3] [Anonymous], 2016, THESIS
  • [4] [Anonymous], 2011, ICCD
  • [5] [Anonymous], 2011, SYNTHESIS LECT COMPU
  • [6] [Anonymous], 2018, DATE
  • [7] [Anonymous], 2013, TRANSIT SPECIFYING P
  • [8] Beu JG, 2011, INT SYMP MICROARCH, P226
  • [9] Automatic synthesis of cache-coherence protocol processors using Bluespec
    Dave, N
    Ng, MC
    Arvind
    [J]. Third ACM & IEEE International Conference on Formal Methods and Models for Co-Design, Proceedings, 2005, : 25 - 34
  • [10] Dill DavidL., 1996, P 8 INT C COMPUTER A, P390