Parameterized Memory Models and
Concurrent Separation Logic
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
Copyright © 2011 Xinyu Feng
|