Abstract
Memory models of shared memory concurrent programs define the values a read of a shared memory location is allowed to see. Such memory models are typically weaker than the intuitive sequential consistency semantics to allow efficient execution. In this paper, we present WOMM (abbreviation for Weak Operational Memory Model) that formally unifies two sources of weak behavior in hardware memory models: reordering of instructions and weakly consistent memory. We show that a large number of optimizations are allowed by WOMM. We also show that WOMM is weaker than a number of hardware memory models. Consequently, if a program behaves correctly under WOMM, it will be correct with respect to those hardware memory models. Hence, WOMM can be used as a formally specified abstraction of the hardware memory models. Moreover, unlike most weak memory models, WOMM is described using operational semantics, making it easy to integrate into a model checker for concurrent programs. We further show that WOMM has an important property - it has sequential consistency semantics for datarace-free programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)
Weaver, D.L., Germond, T.: The SPARC Architecture Manual: Version 9. Prentice Hall, Englewood Cliffs (1994)
Adve, S.V., Gharachorloo, K.: Shared memory consistency models: A tutorial. IEEE Computer 29(12), 66–76 (1996)
Intel: Intel® 64 and ia-32 architectures software developer’s manual volume 3a: System Programming Guide, http://www.intel.com/Assets/PDF/manual/253668.pdf
AMD: Amd64 architecture programmer’s manual (2007)
Sarkar, S., Sewell, P., Nardelli, F.Z., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-cc multiprocessor machine code. In: POPL 2009: Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 379–391. ACM, New York (2009)
Gao, G.R., Sarkar, V.: Location consistency — a new memory model and cache consistency protocol. IEEE Trans. Comput. 49(8), 798–813 (2000)
Intel: A formal specification of intel ® itanium ® processor family memory ordering (October 2002), http://www.intel.com/design/itanium/downloads/251429.htm
Manson, J., Pugh, W., Adve, S.V.: The java memory model. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 378–391. ACM, New York (2005)
Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: Proceedings of the Annual International Symposium on Computer Architecture, pp. 15–26 (May 1990)
Shen, X., Arvind, Rudolph, L.: Commit-reconcile & fences (crf): a new memory model for architects and compiler writers. SIGARCH Comput. Archit. News 27(2), 150–161 (1999)
Nardelli, F.Z., Sewell, P., Sevcik, J., Sarkar, S., Owens, S., Maranget, L., Batty, M., Alglave, J.: Relaxed memory models must be rigorous. In: Exploiting Concurrency Efficiently and Correctly Workshop (2009)
Mador-Haim, S., Alur, R., Martin, M.M.: Specifying relaxed memory models for state exploration tools. In: Exploiting Concurrency Efficiently and Correctly Workshop (2009)
Boudol, G., Petri, G.: Relaxed memory models: an operational approach. In: POPL 2009: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Smposium on Principles of Programming Languages, pp. 392–403. ACM, New York (2009)
Burckhardt, S., Alur, R., Martin, M.M.K.: Checkfence: checking consistency of concurrent data types on relaxed memory models. In: PLDI 2007: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 12–21. ACM, New York (2007)
Huynh, T.Q., Roychoudhury, A.: Memory model sensitive bytecode verification. Form. Methods Syst. Des. 31(3), 281–305 (2007)
De, A., Roychoudhury, A., D’Souza, D.: Java memory model aware software validation. In: PASTE 2008: Proceedings of the 8th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, pp. 8–14. ACM, New York (2008)
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
De, A., Roychoudhury, A., D’Souza, D. (2010). WOMM: A Weak Operational Memory Model. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification, and Validation. ISoLA 2010. Lecture Notes in Computer Science, vol 6415. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16558-0_43
Download citation
DOI: https://doi.org/10.1007/978-3-642-16558-0_43
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16557-3
Online ISBN: 978-3-642-16558-0
eBook Packages: Computer ScienceComputer Science (R0)