Jeremy
I attach my answer
Ganesh
> Hi folks. Slightly off topic, but this seems like a good list to send
> this to.
>
> I was wondering what description languages and verifiers people knew of
> for memory models in general. I am aware of Murphi, which has been used
> to help verify the CRF JMM and SPARC/RMO, and some implementations for TLA
> (I cannot find information about what these may have been used to help
> verify).
>
> I was wondering what others might be out there, and what they might have
> been used to evaluate.
>
> Thanks for any help you can give!
>
> Jeremy
> -------------------------------
> JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
We have used Berkeley VIS/Verilog (our CAV'98 paper - LNCS 1427) to
verify a model of the HP Runway bus for coherence and some elements of
sequential consistency. We have also used SPIN and PV (PV is our own
explicit-state model-checker - often gives one or two orders of
magnitude state reduction over SPIN, due to PV's new partial order
reduction - PV can be downloaded from our URL
http://www.cs.utah.edu/formal_verification. Send email to my student
Robert Palmer - rpalmer@cs.utah.edu - for help with PV. You will get,
with PV, `Test Model-checking Code' implementing Collier's test
programs.)
The use of PV is reported in a forthcoming Formal Methods in System
Design paper (May '02) and also in LNCS 1522 (FMCAD'98). We have used
TLC (TLA's model-checker) which is written in Java. TLC was too slow
for our needs (state-generation of 1400 states of ~500 bits per
minute). Send email to my student Ritwik Bhattacharya for info on his
experience with TLC (ritwik@cs.utah.edu).
So we're using Murphi for now. We've ported Parallel Murphi
(originally written by Stern and Dill) to work on MPI. This code will
be released soon by us (ask my student hemanth@cs.utah.edu for an
advance copy). We've run Parallel Murphi on the ~200 node Utah Network
Testbed (http://www.emulab.net) built by my faculty colleague Jay
Lepreau (lepreau@cs.utah.edu). So far we can use only 16 nodes due
to various reasons (MPI crashes being in them). We are rewriting
Parallel Murphi with new features soon to be announced.
More than the tools we've also investigated two techniques to verify
memory models. One is called 'test model-checking' - basically creates
finite-state non-deterministic abstractions to many of Collier's test
programs. This appears in CAV'98 and FMPPTA'2000 (LNCS 1800). The
other is model-checking based refinement checking. This will appear in
CAV 2002 (please send mail to my student Prosenjit Chatterjee -
prosen@cs.utah.edu - or myself - for an advance copy). We used our
Parallel Murphi in this.
Last but not least, a student jointly advised by myself and Prof. Gary
Lindstrom, Jason Yang (yyang@cs.utah.edu) has captured the CRF model
in Murphi and is working on many other topics concerning Java Memory Models
using Murphi as well.
As for others: Seungjoon Park and Dill at Stanford have used Murphi
and PVS. Ken McMillan at Cadence Berkeley Labs has used his own tool
Cadence SMV (see Charme'2001- LNCS 2144). Steven German at IBM uses
Murphi. Tamara Arons and Pnueli at Weizmann used PVS. My former
student Mike Jones (now a prof at BYU - jones@cs.byu.edu) has used
Mona for the PCI bus ordering rules. He also wrote a model-checker
Picasso by building on Murphi. Qadeer, Rajamani, and Henzinger at
Berkeley used Mocha (CAV'99, LNCS 1633). We've once modeled the
classic Kai-Li/Hudak paper protocols in CMU SMV (now rewritten as
NuSMV).
I'll be happy to provide additional info if needed,
Ganesh
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:39 EDT