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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Adve, S., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer 29(12), 66–76 (1996)
Adve, S., Hill, M.: A unified formalization of four shared-memory models. IEEE Transactions on Parallel and Distributed Systems 4(6), 613–624 (1993)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: 31st POPL, January 2004, pp. 14–25 (2004)
Boehm, H., Adve, S.: The foundations of the C++ concurrency memory model. In: PLDI, Tucson, Arizona, June 2008, pp. 68–78 (2008)
Boehm, H.-J.: Threads cannot be implemented as a library. In: PLDI, Chicago, June 2005, pp. 261–268 (2005)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: 32nd POPL, January 2005, pp. 259–270 (2005)
Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: 36th POPL, Savannah, Georgia, USA, January 2009, pp. 392–403 (2009)
Brookes, S.: A grainless semantics for parallel programs with shared mutable data. Electronic Notes in Theoretical Computer Science 155, 277–307 (2006)
Brookes, S.: A semantics for concurrent separation logic. Theoretical Comp. Sci. 375(1-3), 227–270 (2007)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: 22nd LICS, July 2007, pp. 366–378 (2007)
Cenciarelli, P., Knapp, A., Sibilio, E.: The Java memory model: Operationally, denotationally, axiomatically. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 331–346. Springer, Heidelberg (2007)
Dijkstra, E.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43–112. Academic Press, London (1968)
Feng, X.: Local rely-guarantee reasoning. In: 36th POPL, January 2009, pp. 315–327 (2009)
Feng, X., Ferreira, R., Shao, Z.: On the relationship between concurrent separation logic and assume-guarantee reasoning. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 173–188. Springer, Heidelberg (2007)
Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic (extended version). Technical Report YALEU/DCS/TR-1422, Department of Computer Science, Yale University (2009), http://flint.cs.yale.edu/publications/rmm.html
Gao, G., Sarkar, V.: Location consistency – a new memory model and cache consistency protocol. IEEE Transactions on Computers 49(8), 798–813 (2000)
Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 19–37. Springer, Heidelberg (2007)
Hobor, A., Appel, A., Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers 28(9) (September 1979)
Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: 33rd POPL, January 2006, pp. 42–54 (2006)
Manson, J., Pugh, W., Adve, S.: The Java memory model. In: 32nd POPL, Long Beach, California, January 2005, pp. 378–391 (2005)
Mosberger, D.: Memory consistency models. Operating Systems Review 27(1), 18–26 (1993)
O’Hearn, P.: Resources, concurrency, and local reasoning. Theoretical Comp. Sci. 375(1-3), 271–307 (2007)
Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: 22nd TPHOLS, Munich, Germany, August 2009, pp. 391–407 (2009)
Reynolds, J.: Toward a grainless semantics for shared-variable concurrency. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 35–48. Springer, Heidelberg (2004)
Saraswat, V., Jagadeesan, R., Michael, M., von Praun, C.: A theory of memory models. In: 12th PPoPP, San Jose (March 2007)
Sevcik, J.: Program Transformations in Weak Memory Models. PhD thesis, School of Informatics, University of Edinburgh (2008)
SPARC International Inc. The SPARC Architecture Manual, Version 8. Revision SAV080SI9308 (1992)
Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)
Yang, H.: Relational separation logic. Theoretical Computer Science 375(1-3), 308–334 (2007)
Yang, H., O’Hearn, P.: A semantic basis for local reasoning. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 402–416. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferreira, R., Feng, X., Shao, Z. (2010). Parameterized Memory Models and Concurrent Separation Logic. In: Gordon, A.D. (eds) Programming Languages and Systems. ESOP 2010. Lecture Notes in Computer Science, vol 6012. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11957-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-11957-6_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11956-9
Online ISBN: 978-3-642-11957-6
eBook Packages: Computer ScienceComputer Science (R0)