Re: [isabelle] who knows theorem-proving about cache protocols



There hasn't been a lot of work with theorem provers on shared-memory protocols.
One example is Seungjoon Park's work at Stanford. See

   http://pvs.csl.sri.com/users.shtml

for some pointers to his work.

Jason Yang used higher order logic to specify memory orderings in

   http://www.cs.utah.edu/~slind/papers/itanium.html

Google also tells me that J Moore published a paper entitled

   "An ACL2 proof of Write-Invalidate Cache Coherence"

in LNCS 1427 (Proceedings of CAV'98).

However, most people who verify such things use Murphi, or other explicit-state model checkers. For example, a student of mine, Sudhindra Pandav, recently came
up with counterexample-based techniques (using UCLID) and applied them
to FLASH and German.

   http://www.cs.utah.edu/~slind/papers/charme05.html

Konrad.


On Sep 16, 2005, at 6:22 AM, yongjian Li wrote:


who know who has theorem-proving tehniques for proving invariants for cache protocol, especially for parameter
protocols such as FLASH and German?
I look for Isabelle's formalization for such problem, but it seems no result. I only look for Nipkow's result of I/O automata for ditributed computation (about 8 years before).






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.