Formal Specification of the OpenMP Memory Model Metadata

Metadata describes a digital item, providing (if known) such information as creator, publisher, contents, size, relationship to other resources, and more. Metadata may also contain "preservation" components that help us to maintain the integrity of digital files over time.

Title

  • Main Title Formal Specification of the OpenMP Memory Model

Creator

  • Author: Bronevetsky, G
    Creator Type: Personal
  • Author: de Supinski, B
    Creator Type: Personal

Contributor

  • Sponsor: United States. Department of Energy.
    Contributor Type: Organization

Publisher

  • Name: Lawrence Livermore National Laboratory
    Place of Publication: Livermore, California
    Additional Info: Lawrence Livermore National Laboratory (LLNL), Livermore, CA

Date

  • Creation: 2006-12-19

Language

  • English

Description

  • Content Description: OpenMP [2] is an important API for shared memory programming, combining shared memory's potential for performance with a simple programming interface. Unfortunately, OpenMP lacks a critical tool for demonstrating whether programs are correct: a formal memory model. Instead, the current official definition of the OpenMP memory model (the OpenMP 2.5 specification [2]) is in terms of informal prose. As a result, it is impossible to verify OpenMP applications formally since the prose does not provide a formal consistency model that precisely describes how reads and writes on different threads interact. We expand on our previous work that focused on the formal verification of OpenMP programs through a formal memory model [?]. As in that work, our formalization, which is derived from the existing prose model [2], provides a two-step process to verify whether an observed OpenMP execution is conformant. This paper extends the model to cover the entire specification. In addition to this formalization, our contributions include a discussion of ambiguities in the current prose-based memory model description. Although our formal model may not capture the current informal memory model perfectly, in part due to these ambiguities, our model reflects our understanding of the informal model's intent. We conclude with several examples that may indicate areas of the OpenMP memory model that need further refinement, however it is specified. Our goal is to motivate the OpenMP community to adopt those refinements eventually, ideally through a formal model, in later OpenMP specifications.
  • Physical Description: PDF-file: 41 pages; size: 0.8 Mbytes

Subject

  • Keyword: Specifications
  • Keyword: Programming
  • STI Subject Categories: 99 General And Miscellaneous
  • STI Subject Categories: 99 General And Miscellaneous
  • Keyword: Verification
  • Keyword: Performance

Source

  • Journal Name: International Journal of Parallel Programming, vol. 35, no. 4, January 8, 2007, pp. 335-392; Journal Volume: 35; Journal Issue: 4

Collection

  • Name: Office of Scientific & Technical Information Technical Reports
    Code: OSTI

Institution

  • Name: UNT Libraries Government Documents Department
    Code: UNTGD

Resource Type

  • Article

Format

  • Text

Identifier

  • Report No.: UCRL-JRNL-226950
  • Grant Number: W-7405-ENG-48
  • Office of Scientific & Technical Information Report Number: 936974
  • Archival Resource Key: ark:/67531/metadc894092