Cache models in Promela

Question

I am looking to model cache for multicore processors, including cache coherence. Do such PROMELA implementations already exist. I tried to search for it, but couldn't find any. Secondly, if I have to implement it myself, is it feasible in PROMELA to declare very large arrays as in to represent cache structures?

Answer 1

I personally don't know of such existing Promela models. Moreover, large array structures sounds like a serious state blow-up.

Depending on what properties you want to show, I would suggest to abstract from reality as much as possible. Modeling things with a high precision compared to the real world is typically nothing one should do in Promela.

Two alternative suggestions:

• Model your cache in Java and prove first-order assertions with the KeY proof system
• Model your cache in a mathematical fashion using the Coq proof assistant and prove the desired theorems with Coq

Answer 2

[This is the type of question that would be closed… but there aren't many people answering Promela/SPIN questions so you won't get 5 close votes.]

Google Search for 'formal verification cache coherence spin' notes SPIN use a couple of times.

There is a yearly SPIN Workshop; full papers are listed for the last 14 years.