Automated Verification of UPC Memory Consistency

Workshop on Verified Software: Theories, Tools, Experiments (VSTTE), Seattle, WA, 2006

Author(s): O. Thorsen, C. Wallace
Abstract:The UPC programming language is a shared memory extension to ANSI C. Its memory consistency model is relaxed, allowing for a high degree of optimization, but also permitting behavior which may be surprising to the newcomersve 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 )

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 )

The UPC memory model: Problems and prospects.

International Parallel and Distributed Processing Symposium (IPDPS), Santa Fe, NM, 2004, 16a (10 pages).

Author(s): W. Kuchera and C. Wallace
Abstract: The memory consistency model underlying the Unified Parallel C (UPC) language remains a promising but underused feature. We report on our efforts to understand the UPC memory model and assess its potential benefits. We describe problems we have uncovered in the current language specification. These results have inspired an effort in the UPC community to create an alternative memory model definition that avoids these problems. We give experimental results confirming the promise of performance gains afforded by the memory model's relaxed constraints on consistency.
( pdf )

Illuminating the UPC memory model

M.S. Thesis, Michigan Technological University, Department of Computer Science (December 12th, 2003)

Author(s): W. Kuchera
Abstract: Shared memory multiprocessors offer superior computational power to single processor machines. The interaction between processors and the memory system on such a platform must be well understood by programmers. Memory (consistency) models reduce the level of nondeterminism in shared-memory systems, by guaranteeing what can be read from memory based on the previous behavior of the system.
Unified Parallel C (UPC), an extension of ANSI C with support for parallel programming, includes a memory model in its specification. Programmers must have a clear understanding of the UPC memory model to write efficient and correct programs. Language implementors mus understand the memory model to know when UPC programs can be optimized.
This work formalizes the memory consistency model of UPC using ASMs. In doing so, we point out some problems with the current UPC memory model definition. Abstract State Machines (ASMs) are an operational sematics methodology which have been applied to several problem domains, including a variety of memory consistency models. Our formalization has helped design tests which show invalid behavior under the memory model and unexpected valid behavior. We also examined the performance potential of the memory model with sample UPC programs.
( pdf | ps.gz )

Toward a programmer-friendly formal specification of the UPC memory model.

Technical Report 03-01, Michigan Technological University, Department of Computer Science, 2003.

Author(s): W. Kuchera and C. Wallace
( pdf | ps.gz )

Illustrative test cases for the UPC memory model.

Technical Report 03-02, Michigan Technological University, Department of Computer Science, 2003.

Author(s): W. Kuchera and C. Wallace
( pdf | ps.gz )

Toward a programmer-friendly formal specification of the UPC memory model.

Poster presented at Supercomputing 2002.

Author(s): W. Kuchera and C. Wallace
( html )