See reference paper for description.
Notes on implementation
The implementation is experimental and is only tested on the testcases that
comes with the program. Please contact the author if you find any bugs or
if you have any problems running the program.
- Unpack sourcecode using tar.
- Modify the makefile so that the paths to the where he program is stored
is correct. If you use your own version of zChaff make sure that path is
updated as well.
- 'make all' will compile all sourcode
- Install the graph visualization package from graphviz.
- Run the program 'run execution_trace -view'.
- More information is available in the README that comes with the
Automated Verification of UPC Memory Consistency
M.S. Thesis, Michigan Technological University, Department of
UPC is a shared memory extension to ANSI
C. Its memory consistency model is relaxed, allowing for optimization, but also
permitting behavior which may be surprising to the naive programmer. To
allow better understanding of this memory model, we present a tool for
analyzing the behavior of UPC programs. Given an execution trace, the
tool determines whether the results are compatible with the UPC memory model.
The tool is targeted at newcomers to UPC who want to learn about its memory model and at
developers who want to verify possible behaviors of their programs.
Dr. Charles Wallace
Last modified 3/3/06