Promela的緩存模型

Question

我期待爲多核處理器建立緩存模型，包括緩存一致性。這樣的PROMELA實現已經存在。我試圖搜索它，但找不到任何。其次，如果我必須自己實現它，在PROMELA中聲明非常大的數組以表示緩存結構是否可行？

Answer 1

我個人不知道這種現有的Promela模型。而且，大型陣列結構聽起來像是一種嚴重的狀態爆炸。

根據你想要顯示的屬性，我建議儘可能從現實中抽象出來。在Promela中，與現實世界相比，以高精度對事物進行建模通常是無人能夠做到的。

兩個備選建議：

• 型號你用Java緩存和證明與KeY proof system
• 型號一階斷言你在數學的方式高速緩存使用Coq proof assistant並證明與勒柯克
所需定理

Answer 2

[這是將被關閉的問題類型...但不會有太多的人回答PROMELA/SPIN的問題，所以你不會得到5票接近]

Google Search for 'formal verification cache coherence spin'筆記SPIN使用一對夫婦倍。

有一年一度的SPIN Workshop;全文已列在過去的14年。