c - Promela でモデルをキャッシュする

Question

キャッシュの一貫性を含め、マルチコア プロセッサのキャッシュをモデル化しようとしています。そのような PROMELA 実装は既に存在しますか? 私はそれを検索しようとしましたが、何も見つかりませんでした。次に、自分で実装する必要がある場合、PROMELA でキャッシュ構造を表すために非常に大きな配列を宣言することは可能ですか?

Answer 1

私は個人的に、そのような既存のプロメラ モデルを知りません。さらに、大規模なアレイ構造は、深刻な状態の爆発のように聞こえます。

表示したいプロパティに応じて、可能な限り現実から抽象化することをお勧めします。現実世界と比較して高い精度で物事をモデル化することは、通常、Promela で行うべきことではありません。

2 つの代替案:

• Java でキャッシュをモデル化し、KeY 証明システムで一次アサーションを証明します
• Coq証明アシスタントを使用して数学的方法でキャッシュをモデル化し、Coqで目的の定理を証明します

Answer 2

[これは非公開のタイプの質問です…しかし、Promela/SPIN の質問に答える人は多くないので、5 票は得られません。]

Google 検索で「正式な検証キャッシュ コヒーレンス スピン」を検索すると、SPIN が数回使用されることがわかります。

毎年SPIN ワークショップがあります。過去 14 年間の完全な論文がリストされています。