The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Parameterized Memory Models and Concurrent Separation Logic

Last modified: Thu Jun 24 21:43:41 2010 GMT.

Authors

Rodrigo Ferreira
Xinyu Feng
Zhong Shao

Abstract

In this paper, we formalize relaxed memory models by giving a parameterized operational semantics to a concurrent programming language. Behaviors of a program under a relaxed memory model are defined as behaviors of a set of related programs under the sequentially consistent model. This semantics is parameterized in the sense that different memory models can be obtained by using different relations between programs. We present one particular relation that is weaker than many memory models and accounts for the majority of sequential optimizations. We then show that the derived semantics has the DRF-guarantee, using a notion of race-freedom captured by an operational grainless semantics. Our grainless semantics bridges concurrent separation logic (CSL) and relaxed memory models naturally, which allows us to finally prove the folklore theorem that CSL is sound with relaxed memory models.

Published

  • Proc. 19th European Symposium on Programming (ESOP'10), Paphos, Cyprus, March 2010. Lecture Notes in Computer Science Vol. 6012, pages 267-286. © 2010 Springer-Verlag. [PDF]

  • Technical Report YALEU/DCS/TR-1422 (Extended Version) [PDF]

Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page
colophon