Godson-T缓存一致性协议分析

发表于 更新于 分类于 阅读次数：

Godson-T 是中国科学院计算技术研究所设计并实现的一个众核处理器系统。Godson-T 缓存一致性协议 (简称Godson-T协议) 是Godson-T 众核处理器所使用的缓存一致性协议。

本文将详细分析该协议的数据结构及迁移规则 （Murphi语言）

介绍

Godson-T 是中国科学院计算技术研究所设计并实现的一个众核处理器系统。其中，Godson-T 缓存一致性协议 (简称Godson-T协议) 是Godson-T 众核处理器所使用的缓存一致性协议。该协议旨在解决处理核、缓存和内存三者之间的数据一致性问题。

对该协议进行Murphi建模，其难点在于它不同于通常的基于地址或基于总线的模型，因此对它的状态分析、迁移规则分析都需要从更抽象的角度。

下面，将对其Murphi建模进行详细的介绍，希望对大家有启发。

类型结构

该协议中用到的数据结构大致可分为四大类：

CACHE

1
2
3
4
5
CACHE: record
    state: CACHE_STATE;  -- cache状态
    addr: TYPE_ADDR;   -- 对应的地址
    data: TYPE_DATA;   -- 对应的数据
end;

初始状态

1
state: Invalid

NODE

1
2
3
4
5
NODE: record
    cache: array [TYPE_CACHE] of CACHE;   -- 节点包含的cache （一或多）
    hasLock: boolean;   				  -- 是否有锁
    firstRead: array [TYPE_ADDR] of boolean;   -- 是否是第一次读
end;

初始：

1
2
hasLock : false   -- 没锁
firstRead : true   -- 一开始肯定是第一次读

LOCK

1
2
3
4
5
LOCK: record
    owner: TYPE_NODE;
    beUsed: boolean;
    inProtection: array [TYPE_ADDR] of boolean;
end;

初始：

1
2
beUsed : false   -- 一开始锁还没被使用
inProtection[a] : false;    --每个地址都不在保护范围内

MEMORY

1
2
3
MEMORY: record
    data: TYPE_DATA;
end;

存储着一个数据

协议结构

把刚刚所说的四个类型结构组合起来，就是如下的协议结构：

可以看到，这个协议既不是一个directory-based，也不是bus-based结构，而是region-based 结合全局锁的协议。

下面看看它的迁移规则是如何进行的。

迁移规则

Godson-T 协议没有使用基于目录的cache 一致性协议, 它选择了弱一致性中基于锁的域一致性（region-based）作为片上的存储模型。也就是说，它没有一个全局的控制器，而是用锁来管理需要互斥的内容，然后用replace这个复杂的操作来选择cache。

Godson-t的Murphi建模中，共有24条规则，都标示在图中。

其中，可以看到，主要有两大类行为： no lock 和with lock ，每个类别中又可以分为read 和 write两种请求。比较复杂的是带锁的读，因为要涉及是否是首次读。

下面对这些操作进行具体的解读。

临界区外的读操作(不带锁的读)

判断Cache中是否有该副本:

  • 若有, 则直接读取;

  • 若无, 对Cache当前副本执行Replace 操作, 再从Memory 中读取, 写入Cache 中

临界区外的写操作(不带锁的写)

采用写回 (write-back)策略, 判断Cache 中是否有该副本：

  • 若有, 则将新值写入Cache 中, 修改Cache 状态为Dirty
  • 若无, 对Cache当前副本执行Replace 操作, 再将新值写入Cache 中, 修改Cache 状态为Dirty

临界区内的读操作(带锁的读)

判断Cache中是否有该副本：

  • 若有该副本，判断是否为首次读：
    • 若是, replace所有包含该地址的cache, 再从Memory 中读取, 写入该Cache，再从cache中读
    • 若不是首次读，则直接从cache中读取

  • 若没有该副本，依然判断是否为首次读：
    - 若是，replace所有包含该地址的cache，从memory中读入数据，从该节点的cache中选择一个cache，写入该cache，再从cache中读取 （注意，这里与有副本的首次读的区别是，这里需要选取cache，但是上面的情况已经选定了cache，所以不用再选了）
    - 若无，直接从memory中读，并写入cache

临界区内的写操作(带锁的写)

采用写穿透（write-through）策略。判断cache中是否有该副本：

  • 若有， 写入cache 和memory中
  • 若无，将新值直接写入Memory

缓存的选择和替换操作(Replace)

替换操作分为几种情况：

  • 需要替换全部包含该地址的cache （repAll）：
    • 将所有节点中的所有cache中包含该地址的全都写会memory
  • 不需要替换全部：
    • 该节点中是否存在invalid的节点
      • 若有，则用该节点进行替换
      • 若无，随机选取（designate）一个非invalid 的cache，判断其是否dirty：
        • 若是，则将该cache中的dirty data写会memory，再将其置为invalid，用于替换
        • 若否，则直接替换它

锁操作

锁操作比较简单

  • 获取锁：锁没被用，且该节点还没有锁 （一个节点只能有一个锁）：给该结点锁，并记录
  • 释放锁：锁被结点i使用：直接释放，修改记录

不变式 / 性质

锁不能嵌套

保证当不需要replace操作且结点node有锁的情况下，一定存在一个全局锁是被该node结点使用的；并且不会有两个锁同时锁该结点

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
ruleset i: TYPE_NODE do
    invariant "DeadlockFree"
    (
        replace = NON &
        node[i].hasLock
    ) -> (
        exists l: TYPE_LOCK do
            lock[l].beUsed &
            lock[l].owner = i
        endexists &
        forall m: TYPE_LOCK; n: TYPE_LOCK do
            m = n |
            !lock[m].beUsed |
            !lock[n].beUsed |
            lock[m].owner != i |
            lock[n].owner != i
        endforall
    )
end;

一致性

有锁的非首次读的缓存中存储的数据，一定与memory中的数据一致。

1
2
3
4
5
6
7
8
9
10
11
ruleset i: TYPE_NODE; j: TYPE_CACHE; a: TYPE_ADDR do
    invariant "Coherence"
    (
        replace = NON &
        node[i].hasLock &
        !node[i].firstRead[a] &
        node[i].cache[j].state = VALID &
        node[i].cache[j].addr = a
    ) -> 
    node[i].cache[j].data = memory[a].data
end;

参考资料

（由于资料太少了，且有些文章中说的内容与murphi代码有出入，因此大多数还是自己摸索的）

GODSON-T: AN EFFICIENT MANY-CORE PROCESSOR EXPLORING THREAD-LEVEL PARALLELISM

Godson-T 缓存一致性协议的Murphi 建模和验证

Murphi代码