Foundations of Multi-Core Memory Models

Foundations of Multi-Core Memory Models

Seminar in Theoretical CS, Summer Semester 2012

News

22.12.2011 - Setup of this web site

23.01.2012 - Changed to bi-weekly scheduling of talks (see specific dates below)


Schedule

13 January 16:00 Introduction to seminar (incl. assignment of topics)
at seminar room of I2
-10 weeks Table of contents due
-8 weeks Preliminary version of report due
-4 weeks Final version of report due
-2 weeks Preliminary version of slides due
-1 week Final version of slides due
(relative to date of
presentation)

Overview

The current and future trend to multi-core computing systems suggests that within the next decade, concurrent multi-threaded programming will replace sequential programming as the standard programming paradigm. However, concurrency and modern computer architecture do not go together easily:

  • Current programming language memory models are still incomplete. Mainstream languages such as Java increasingly promise sequential consistency for data-race-free programs. But we do not know how to handle data races in a way that supports reasonable performance, security, and debuggability.
  • Hardware specifications are so informal that it is very hard to know whether we have a correct implementation of the language specifications (if we knew how to specify those fully).
  • The concurrent algorithms that are now being developed, and which are key to exploiting multiprocessors (via high-performance operating systems, hypervisor kernels, and concurrency libraries), are very subtle, so informal reasoning cannot give high confidence in their correctness.
  • While there is a rich literature on concurrency theory, and extensive prior work on software verification for concurrency software (including process calculi, model-checking, temporal logics, rely-guarantee reasoning, and separation logic), almost all of it assumes a global notion of time, unrealistic though that is for these systems and algorithms.

The memory (consistency) model is at the heart of the concurrency semantics of a shared-memory program. It defines the interface between the program and any hardware or software that may transform that program.

In this seminar, the following topics will be considered:

  1. Survey of problem domain: state of the practice in multi-core-programming and state of the art in memory consistency models.
  2. Application of concurrency theory approaches to reveal underlying concepts of parallelism, reordering, causality, and consistency.
  3. Formal approaches to memory consistency models and semantics of multithreaded programming.

More information on formal models for multi-core memory is available from the CACM article by Adve and Boehm.


Topics

(Double presentations start at 16:00 in the I2 seminar room, and will roughly take 90 mins)

  • B. Historical accounts to shared memory computing: The papers in this section give an historical account of attempts towards formalization of shared-memory computations, and are of relevance to understand and judge modern approaches for multi-core memory models.
    • The first two papers are rather classical. Lamport presents two theorems for a shared memory setting in which one process at a time can modify the data, but concurrent readings and writings are possible. Misra presents the weakest axioms for a similar setting to facilitate correctness proofs of shared memory programs.
    • Shasha and Snir describe an approach to determine the minimal delay within a process such as to accommodate sequential consistency.
    • Ahamad et al. give a first formalisation of a so-called weak memory model. Such model allows for more concurrent memory accesses than for sequentially consistent memories. Besides the formalisation, an implementation is described in detail.

  • C. Semantics: All papers in this section are devoted to providing a formal semantics to memory models for either actual programming languages such as Java and C++, as well as for modern multi-core processors and optimising compilers.
    • Manson et al. define the semantics of multithreaded Java programs and partially determines legal implementations of Java virtual machines and compilers. It provides a simple interface for correctly synchronized programs -- it guarantees sequential consistency to data-race-free programs. Flaws in this model were found and (partially) repaired by Aspinall and 各vč?k.
    • Saraswat et al. establish that all models in their mathematical framework satisfy the following (fundamental) property of relaxed memory models: programs whose sequentially consistent (SC) executions have no races must have have only SC executions.
    • Recently, Jagadeesan and co-workers presented an attempt to fit relaxed memory models into structured operational semantics and showed that the basic properties of the Java Memory Model hold in their formalisation.
    • An alternative approach to that of Jagadeesan et al. is followed by Boudol and Petri:
    • A popular technique in "optimising" compilers for multi-core machines is so-called speculative re-ordering of instructions. This speeds up program execution as it allows more concurrency. Boudol and Petri recently gave a first formalisation of this technique.
    • The last two papers of this section (intended for a single seminar) present two approaches towards the mathematical semantics of C++ concurrency.
  • D. Verification: All papers in this section intend to verify (using different means) basic properties of shared memory systems, with or without local caches.
    • Brinksma gives a process algebraic account to proving the correctness of a lazy caching algorithm. The proof is based on refinement.
    • Model checking transactional memories (TMs) is difficult because of the unbounded number, length, and delay of concurrent transactions, as well as the unbounded size of the memory. Recently, Guerraoui et al. showed that, under certain conditions satisfied by most TMs, the model checking problem can be reduced to a finite-state problem.
    • Atig et al. define abstract operational models for three different weak memory models. Their models are based on state machines with (potentially unbounded) FIFO buffers. The authors investigate the decidability of their reachability and their repeated reachability problems.
    • At Microsoft, they developed a monitor algorithm that can detect the presence of program executions that are not sequentially consistent due to store buffers. Such monitor is combined with a stateless model checker that verifies that every sequentially consistent execution is correct. Practical results are provided.


Additional Material


Contact

Thomas Noll <noll at cs.rwth-aachen.de>


AltStyle によって変換されたページ (->オリジナル) /