See reference paper for description.
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.
Automated Verification of UPC Memory Consistency
M.S. Thesis, Michigan Technological University, Department of
Computer
Science (2006)
Author(s): O. Thorsen
Abstract: 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.
(
pdf )