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.




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 )


Oystein Thorsen
Dr. Charles Wallace Last modified 3/3/06