Search code examples
cmultithreadingmulticorespinpromela

Cache models in Promela

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?

Solution

  • 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