Sciweavers

ESOP
2010
Springer

Parameterized Memory Models and Concurrent Separation Logic

14 years 8 months ago
Parameterized Memory Models and Concurrent Separation Logic
Formal reasoning about concurrent programs is usually done with the assumption that the underlying memory model is sequentially consistent, i.e. the execution outcome is equivalent to an interleaving of instructions according to the program order. However, memory models in reality are weaker in order to accommodate compiler and hardware optimizations. To simplify the reasoning, many memory models provide a guarantee that data-race-free programs behave in a sequentially consistent manner, the so-called DRFguarantee. The DRF-guarantee removes the burden of reasoning about relaxations when the program is well-synchronized. 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 obtaine...
Rodrigo Ferreira, Xinyu Feng and Zhong Shao
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where ESOP
Authors Rodrigo Ferreira, Xinyu Feng and Zhong Shao
Comments (0)