SHF: Small: Ordering-Based Semantics for Emerging Models of Parallel Computing

点击翻译按钮获取中文摘要

With the proliferation of multicore processors has come resurgenceof interest in parallel programming languages and models,particularly those intended to make it easier for non-expertprogrammers to correctly implement important classes of parallelapplications. 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 willbe needed in order to truly understand and reason about programs,guide language implementations, and verify implementationcorrectness. Within computer science and allied fields, formaldefinitions will facilitate the transition to ubiquitous parallelcomputing. For society at large, this transition will be essentialto 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 ofhistory-based executions to capture both the behavior of individualthreads of control and the interactions among those threads. In adeparture from previous work, the interactions are always expressedin terms of atomic blocks, which can capture arbitrarylanguage-level synchronization mechanisms. Specific topics beingaddressed include transactional memory (including the concepts ofpublication and privatization), explicit speculation, and determinism. The notion of determinism, in particular, is centralto several emerging languages and models specifically intended for non-expert programmers. A formal framework for the definition ofdeterminism will allow alternative definitions to be compared,contrasted, and correctly implemented.