SHF: Small: Semantics, Static Analysis, and Refencing of Concurrent Programs with Weak Memory Models

New York University, New York NY

Investigators

Abstract

Modern computers have parallel multicore architectures sharing a hierarchy of caches and memories from fast and expensive ones to large and cheaper ones. The consequence is that not all cores running concurrently see the shared memory in the same way: some see newly stored values while others see older ones. This is called weak consistency models for shared memory on a single chip or memory distributed on several chips or on networks. This modern design makes the task of designing and programming parallel computers very complex. In particular the same program may have very different behaviors when running on different architectures whereas the same program had the same effect on all machines of the previous generation. This project define a generic formal semantics of parallel programs with weak consistency models parameterized by a formal definition of the computer architecture. Based on this parameterized semantics, the project investigates invariance proof methods to be used by programmers and verification tools to prove properties of parallel programs with weak consistency models. The project contributes to formal methods and tools for concurrent programming which, by the foreseeable evolution of hardware design, will be inevitable in the future. The publications and prototypes from this project are widely disseminated.