With the proliferation of multicore processors has come resurgence of interest in parallel programming languages and models, particularly those intended to make it easier for non-expert programmers to correctly implement important classes of parallel applications. Unfortunately, most such languages and models are informally -- and thus imprecisely -- defined. The aim of the sponsored research is to develop more formal definitions, which will be needed in order to truly understand and reason about programs, guide language implementations, and verify implementation correctness. Within computer science and allied fields, formal definitions will facilitate the transition to ubiquitous parallel computing. For society at large, this transition will be essential to maintain the momentum of the IT revolution, across government, industry, science, the arts, and entertainment.
The technical core of the sponsored research is the use of history-based executions to capture both the behavior of individual threads of control and the interactions among those threads. In a departure from previous work, the interactions are always expressed in terms of atomic blocks, which can capture arbitrary language-level synchronization mechanisms. Specific topics being addressed include transactional memory (including the concepts of publication and privatization), explicit speculation, and determinism. The notion of determinism, in particular, is central to several emerging languages and models specifically intended for non-expert programmers. A formal framework for the definition of determinism will allow alternative definitions to be compared, contrasted, and correctly implemented.
