借助Rust的异步语法编写适合模型检查的RPC风格分布式协议

这是我在SOSP’24第三天里面提到的给Verus老哥讲的点子。基本上题目就涵盖了它的全部内容。自行展开略。

今天给ℒ讲了一下，顺便理顺了一下叙事。ℒ觉得两方面的动机都需要加以验证

• 人们喜爱用RPC风格编写分布式协议。这个我基本可以打包票。
• RPC风格编写的分布式协议不容易/不适合被拿来模型检查。这个我确实还没想清楚，就只是觉得既然大家都不做模型检查，那大概是做起来麻烦吧。但是说不定只是单纯的懒呢。

这么说的话，大概应该把目标定更大一点，一个能尽可能降低模型检查门槛的编写分布式协议的框架。支持RPC风格只是其中的一环。