模型检查 / 基准测试 / 出行

风雨飘摇的一周。抑或说连绵不断的一周。早几天就想要开始动笔，总是想着把手头的事告一段落就开写，然后手头的事就有了新的情况。

把Alloy的文档看了个七七八八。对于要怎么做的想法逐渐清晰了些。就姑且称为模型检查企划吧。

跟ℒ磕磕绊绊地讨论了几个来回，逐渐接受了他的构思开始着手实施。一般来说这是很好的迹象。不过这块也不是ℒ的拿手领域。不过再不拿手也比我靠谱多了吧。

总还是觉得把顺序方面的性质放在分布式系统当中有点不够用。本来放在文件系统里就已经不是很够用了，这下更不够用了。

以事件驱动作为本地模型的边界已经把一大部分麻烦事给分离掉了（比如网络模型之类的）。也许还可以把更多的麻烦事塞进这个夹层里面，比如说，证明状态在处理完了一串事件以后恢复了之前的某种属性（反映出来就是回到了某个类型）。但是感觉有点过于异想天开了。

说到底，手动把模型映射到实现，这本来就是一个模糊的，可以灵活实现的需求。灵活的代价就是更难令人信服。

---

除此之外，想了一个新的关于对DHT做基准测试的企划。这倒是浅显易懂，不用做什么展开描述。ℒ觉得动机不够充分。也许吧，不过这么简单干净的工作，也许能通过讨人喜欢来降低一点对动机的要求，但愿。

---

思来想去最后加入了卡皮巴拉项目。明天第一次开正式的会。

这个项目是那种应该做的程度超过想做的程度的项目。思来想去也还是这样。磨练一下自己吧。再怎么说好歹也是Rust呢。

---

把neatworks又从头开始折腾了一遍。但是感觉没有太多时间拿来折腾。希望别太耽误事了。

---

隔壁做形式化验证的组集体翘班去了，给p2p形式化验证的点子暂且搁置。

这周最重要的结论大概是OSDI真的不赶了。另外还订了去开SOSP的机票。第一天的酒店还没订到，等会处理一下。