科研路上，什么让人高兴？答案：发现非常有意义的理论方法。
那又有什么让人沮丧呢？答案：自己发现的理论方法已经被人发现了。

仅仅一个上午，我就亲身经历了一次从“喜”到“悲”的过程，把它记下来，缓解一下失落，重新振作起来。

--------------------------------------------------------

故事的源头来自HPCA的文章，其中有一个Review问我们如何保障DMA Cache和CPU Cache使用不同的一致性协议时的正确性。一开始，用枚举的方法画了一个表证明没有错误。但直觉上，我觉得这是一个很重要的问题——“如何保障一个采用异构Cache一致性的系统不会存在错误？”

我用“Heterogeneous，Cache Coherence Protocol”去搜索了，找到了少许资料，但当时没有找到一些理论上的文献。因此，我当时的调研结论是：有一些系统实现，但是没有理论分析。我也就这个问题和Erlin、tgm提起过，为此Erlin还专门帮我借了一本分布式算法的书。我也把本科教材《Theory of Computation》重新翻了出来。

周六上午提交完HPCA的论文，终于轻松了一些，也开始认真思考起这个问题。灵感来自周日的一个下午，我觉得可以将现在的一致性协议拆成一个“主自动机+影子自动机”，然后通过寻找两个自动机状态之间的关系，那么就可以把它们归约为一个自动机。

周一，我把Erlin借来的分布式算法书从头到尾翻了一遍，学习到了一些分布式理论的基本概念，但是没有找到可以直接用的，当然可能是因为自己翻得太粗了。但是晚上，我想到了一个方法，认为可以先定义哪些Cache状态可以共存，如果Modified只能和Invalid共存，两个Shared可以共存……

今天早上，我搬到了5楼空中花园，专心思考这个问题。在画了4张草稿纸后，我突然想到了定义一个“数据的Cache全局状态”，也就是一份数据在所有Cache中的状态，一下子感觉问题找到了突破点，非常兴奋。我用MOESI作为例子，手工构造了全局状态，即（1）MI+，（2）EI+，（3）OS+I+，（4）S+I+，（5）I+。然后把MOESI转换为仅包含这些全局状态图的状态机，所有问题一下子明朗了。我在纸上记下，“下一步工作就是从原始状态机构造出全局状态机了，这包括两个步骤，一是构造全局状态，二是构造状态转换图”。
此时的我是非常的兴奋，我忽然间觉得自己有了一个大发现。

从5楼跑回工位，保守起见，我又去google搜了一下，这次我使用的关键字是“Global state, Cache coherence protocol”。天啊，很不幸看到了一篇论文中有这个字样。1992年SPAA上的一篇论文“The Verification of Cache Coherence Protocols”，我下载下来后一看，简直不能相信自己的眼睛。他们也用了这种全局状态方法，连状态表示方式都是几乎一样，如（shared,invalid+),(exclusive, invalid*)，基于这种全局状态得到的状态机也几乎是一样的…… 我又跟踪查了一下，发现他们在1998年发表在Journal of 
the ACM上的文章总结了这个方法，并且把异构Cache一致性协议也考虑进去了。我的心情一下落到了低谷……

--------------------------------------------------------

这次经历只能算是做了一次头脑体操吧。但不管如何，还是需要总结一些经验教训：

1. 这次主要的问题在于调研工作做的不够，要不然根本不会出现这样起伏。而且，我还可以直接将这个方法用到HPCA论文的协议证明中去，不必再被人说不严密。

2. 我还是增加了一些驾驭理论知识的信心。理论知识，数学知识，其实也是工具，当问题需要的时候，不要惧怕它们。

3. 这种经历结果也许并不理想，但过程的确还是非常跌宕起伏，像是在虚拟世界中体验了一把成功科研的感受，体验短暂的自我陶醉感。更重要的是，至少增加了一次独立求解问题的经历，增加了信心。

4. 最后，还是该清醒了，寻找下一个更好的经历……