As a course project, a partner and I at UIUC have developed a tool for
analyzing a program in a simple bytecode machine (not the full JVM) and
generate the set of allowed traces by both the Manson/Pugh and Adve
models. We think we have the Adve model completed (minus the detail
about P' in the last part), and we're close to having a complete
executable specification of the other model. We don't yet deal with the
final field semantics, and there's obviously restrictions on the allowed
programs that we can evaluate, but we can execute and check all the
programs listed in the "New Approach" paper. We've been asked as part
of another course to extend this work. We have a few ideas:
1. Try to model more of Java (e.g. we don't yet even model objects).
2. Check what compiler reorderings are allowed for a given program.
3. Model a simple machine with a relaxed memory model that is designed
from an architecture perspective and check how the executions it
generates compare to the allowable executions by both memory models.
We've also considered trying to formally prove that the set of
executable specifications allowed by each memory model are equivalent,
but that looks hard.
So our question is twofold: Would any of the above ideas actually be
useful to people working on the memory model? Secondly, if an idea does
seem useful, what resources should we turn to where people have done
similar work?
Thank you for any help,
Joe Hendrix
jhendrix@uiuc.edu
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:44 EDT