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

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

Modern computers have parallel multicore architectures sharing ahierarchy of caches and memories from fast and expensive ones to largeand cheaper ones. The consequence is that not all cores runningconcurrently see the shared memory in the same way: some see newlystored values while others see older ones. This is called weakconsistency models for shared memory on a single chip or memorydistributed 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 allmachines 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.