c - Promela 中的缓存模型

Question

我正在寻找为多核处理器建模缓存，包括缓存一致性。这样的 PROMELA 实现是否已经存在。我试图搜索它，但找不到任何东西。其次，如果我必须自己实现它，在 PROMELA 中声明非常大的数组来表示缓存结构是否可行？

Answer 1

我个人不知道这种现有的 Promela 模型。此外，大型阵列结构听起来像是严重的状态爆炸。

根据您要显示的属性，我建议尽可能从现实中抽象出来。与现实世界相比，对事物进行高精度建模通常不是在 Promela 中应该做的事情。

两个替代建议：

• 用 Java 对缓存建模并使用Key 证明系统证明一阶断言
• 使用Coq 证明助手以数学方式对缓存建模，并使用Coq 证明所需的定理

Answer 2

[这是将被关闭的问题类型……但回答 Promela/SPIN 问题的人并不多，因此您不会获得 5 票。]

Google 搜索“正式验证缓存一致性旋转”说明 SPIN 使用了几次。

每年举办一次SPIN 研讨会；列出了过去 14 年的完整论文。