记录了一些拍脑袋的想法。

1、stateful / stateless。

现在看来，就算 stateful 也不能搞这么重的 state。有点太多余了。

想到一个事实上的等价性标准，那就是，如果在同一 interleaving 下两个 localstate 对 sharedstate 会产生相同的影响，那么称状态等价。

这意味着，只需要：

  • rip = rip

  • 抽象状态相等

  • inbuffer 相等

2、正确性

对于 raft 而言，也许只需要证明其在有限几个任期内的正确性，就足以说明问题。

3、解开 guest.h。单文件其实包含了三个方面的内容：elf，thread(process)，snapshot。但是，目前全都混在一起写了。

4、用户的 choose 有没有更加简洁的表示方式？