More Web Proxy on the site http://driver.im/

article

Memory Model = Instruction Reordering + Store Atomicity

Authors:

Jan-Willem MaessenAuthors Info & Claims

ACM SIGARCH Computer Architecture News, Volume 34, Issue 2

Pages 29 - 40

https://doi.org/10.1145/1150019.1136489

Published: 01 May 2006 Publication History

Abstract

We present a novel framework for defining memory models in terms of two properties: thread-local Instruction Reordering axioms and Store Atomicity, which describes inter-thread communication via memory. Most memory models have the store atomicity property, and it is this property that is enforced by cache coherence protocols. A memory model with Store Atomicity is serializable; there is a unique global interleaving of all operations which respects the reordering rules. Our framework uses partially ordered execution graphs; one graph represents many instruction interleavings with identical behaviors. The major contribution of this framework is a procedure for enumerating program behaviors in any memory model with Store Atomicity. Using this framework, we show that address aliasing speculation introduces new program behaviors; we argue that these new behaviors should be permitted by the memory model specification. We also show how to extend our model to capture the behavior of non-atomic memory models such as SPARC R TSO.

References

[1]

{1} S. V. Adve and K. Gharachorloo. Shared Memory Consistency Models: A Tutorial. IEEE Computer, pages 66-76, Dec. 1996.

Digital Library

[2]

{2} S. V. Adve and M. D. Hill. Weak Ordering - A New Definition. In Proceedings of the 17th International Symposium on Computer Architecture, pages 2-14. ACM, May 1990.

Digital Library

[3]

{3} Y. Afek, G. Brown, and M. Merritt. Lazy caching. ACM Trans. Program. Lang. Syst., 15(1):182-205, 1993.

Digital Library

[4]

{4} R. Alur, K. McMillan, and D. Peled. Model-checking of correctness conditions for concurrent objects. In LICS '96: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, page 219, Washington, DC, USA, 1996. IEEE Computer Society.

Digital Library

[5]

{5} J. D. Bingham, A. Condon, and A. J. Hu. Toward a decidable notion of sequential consistency. In SPAA '03: Proceedings of the fifteenth annual ACM symposium on Parallel algorithms and architectures, pages 304-313, New York, NY, USA, 2003. ACM Press.

Digital Library

[6]

{6} W. W. Collier. Reasoning about parallel architectures. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1992.

Digital Library

[7]

{7} A. E. Condon and A. J. Hu. Automatable verification of sequential consistency. In SPAA '01: Proceedings of the thirteenth annual ACM symposium on Parallel algorithms and architectures, pages 113-121, New York, NY, USA, 2001. ACM Press.

Digital Library

[8]

{8} M. Frigo. The weakest reasonable memory model. Master's thesis, MIT, Oct. 1997.

[9]

{9} M. Frigo and V. Luchangco. Computation-centric memory models. In Proceedings of the 10th ACM Symposium on Parallel Algorithms and Architectures, June/July 1998.

Digital Library

[10]

{10} G. R. Gao and V. Sarkar. Location Consistency - A New Memory Model and Cache Coherence Protocol. Technical Memo 16, CAPSL Laboratory, Department of Electrical and Computer Engineering, University of Delaware, Feb. 1998.

[11]

{11} K. Gharachorloo, D. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. Hennessy. Memory Consistency and Event Ordering in Scalable Shared-memory Multiprocessors. In Proceedings of the 17th International Symposium on Computer Architecture, pages 15-26. ACM, May 1990.

Digital Library

[12]

{12} S. Hangal, D. Vahia, C. Manovit, and J.-Y. J. Lu. Tsotool: A program for verifying memory systems using the memory consistency model. In ISCA '04: Proceedings of the 31st annual international symposium on Computer architecture , page 114, Washington, DC, USA, 2004. IEEE Computer Society.

Digital Library

[13]

{13} T. A. Henzinger, S. Qadeer, and S. K. Rajamani. Verifying sequential consistency on shared-memory multiprocessor systems. In CAV '99: Proceedings of the 11th International Conference on Computer Aided Verification, pages 301-315, London, UK, 1999. Springer-Verlag.

Digital Library

[14]

{14} M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures. In ISCA '93: Proceedings of the 20th annual international symposium on Computer architecture, pages 289-300, New York, NY, USA, 1993. ACM Press.

Digital Library

[15]

{15} M. D. Hill. Multiprocessors should support simple memory-consistency models. IEEE Computer, 31(8):28- 34, 1998.

Digital Library

[16]

{16} Intel, editor. Intel IA-64 Architecture Software Developer's Manual. Intel Corporation, Jan. 2000.

[17]

{17} JSR 133. Java memory model and thread specification revision. http://jcp.org/jsr/detail/133.jsp, Sept. 2004.

[18]

{18} P. Keleher, A. Cox, and W. Zwaenepoel. Lazy Release Consistency for Software Distributed Shared Memory. In Proceedings of the 19th International Symposium on Computer Architecture, pages 13-21. ACM, May 1992.

Digital Library

[19]

{19} L. Lamport. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Transactions on Computers, C-28(9):690-691, Sept. 1979.

Digital Library

[20]

{20} V. Luchangco. Memory Consistency Models for High Performance Distributed Computing. PhD thesis, MIT, Cambridge, MA, Sep 2001.

Digital Library

[21]

{21} J.-W. Maessen, Arvind, and X. Shen. Improving the Java memory model using CRF. In Proceedings of the 15th Annual Conference on Object-Oriented Programming Systems, Languages and Applications, pages 1-12, Minneapolis, MN, Oct 2000.

Digital Library

[22]

{22} J. Manson, W. Pugh, and S. Adve. The Java memory model. In Proceedings of the ACM Symposium on Principles of Programming Languages, pages 378-391, Long Beach, CA, Jan. 2005. ACM SIGPLAN.

Digital Library

[23]

{23} M. M. K. Martin, D. J. Sorin, H. W. Cain, M. D. Hill, and M. H. Lipasti. Correctly implementing value prediction in microprocessors that support multithreading or multiprocessing. In MICRO 34: Proceedings of the 34th annual ACM/IEEE international symposium on Microarchitecture , pages 328-337, Washington, DC, USA, 2001. IEEE Computer Society.

Digital Library

[24]

{24} C. May, E. Silha, R. Simpson, and H. Warren, editors. The PowerPC Architecture: A Specification for A New Family of RISC Processors. Morgan Kaufmann, 1994.

Digital Library

[25]

{25} S. Qadeer. Verifying sequential consistency on shared-memory multiprocessors by model checking. IEEE Trans. Parallel Distrib. Syst., 14(8):730-741, 2003.

Digital Library

[26]

{26} A. Sezgin and G. Gopalakrishnan. On the decidability of shared memory consistency validation. In MEMOCODE '2005: Proceedings of the Third ACM-IEEE Conference on Formal Methods and Models for Codesign, 2005.

Digital Library

[27]

{27} D. Shasha and M. Snir. Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst., 10(2):282-312, 1988.

Digital Library

[28]

{28} X. Shen, Arvind, and L. Rudolph. Commit-Reconcile & Fences (CRF): A New Memory Model for Architects and Compiler Writers. In Proceedings of the 26th International Symposium on Computer Architecture, Atlanta, GA, May 1999. ACM.

Digital Library

[29]

{29} D. L. Weaver and T. Germond, editors. The SPARC Architecture Manual (Version 9). Prentice-Hall, 1994.

Digital Library

Cited By

Geeson LBrotherston JDijkstra WDonaldson ASmith LSorensen TWickerson J(2024)Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ImplementationsProceedings of the ACM on Programming Languages10.1145/36897278:OOPSLA2(442-467)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689727
Colvin R(2021)Parallelized Sequential Composition and Hardware Weak Memory ModelsSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_12(201-221)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_12
Pulte CFlur SDeacon WFrench JSarkar SSewell P(2017)Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8Proceedings of the ACM on Programming Languages10.1145/31581072:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158107
Show More Cited By

Index Terms

Memory Model = Instruction Reordering + Store Atomicity
1. Hardware
  1. Integrated circuits
    1. Logic circuits
    2. Semiconductor memory
      1. Dynamic memory

Recommendations

Memory Model = Instruction Reordering + Store Atomicity
ISCA '06: Proceedings of the 33rd annual international symposium on Computer Architecture

We present a novel framework for defining memory models in terms of two properties: thread-local Instruction Reordering axioms and Store Atomicity, which describes inter-thread communication via memory. Most memory models have the store atomicity ...
Store Atomicity for Transactional Memory

We extend the notion of Store Atomicity [Arvind and Jan-Willem Maessen. Memory model = instruction reordering + store atomicity. In ISCA '06: Proceedings of the 33rd annual International Symposium on Computer Architecture, 2006] to a system with atomic ...
Weak atomicity for the x86 memory consistency model

We consider the interaction of weakly atomic Software Transactional Memory (STM) providing single global lock atomicity with the x86 memory consistency model. We show that a practical design for such an STM requires that some program behaviour be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGARCH Computer Architecture News

ACM SIGARCH Computer Architecture News Volume 34, Issue 2

May 2006

383 pages

ISSN:0163-5964

DOI:10.1145/1150019

Issue’s Table of Contents

ISCA '06: Proceedings of the 33rd annual international symposium on Computer Architecture
June 2006
383 pages
ISBN:076952608X

Copyright © 2006 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2006

Published in SIGARCH Volume 34, Issue 2

Check for updates

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
1,102
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)3

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Geeson LBrotherston JDijkstra WDonaldson ASmith LSorensen TWickerson J(2024)Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics ImplementationsProceedings of the ACM on Programming Languages10.1145/36897278:OOPSLA2(442-467)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689727
Colvin R(2021)Parallelized Sequential Composition and Hardware Weak Memory ModelsSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_12(201-221)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_12
Pulte CFlur SDeacon WFrench JSarkar SSewell P(2017)Simplifying ARM concurrency: multicopy-atomic axiomatic and operational models for ARMv8Proceedings of the ACM on Programming Languages10.1145/31581072:POPL(1-29)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158107
Lee DBertacco V(2017)MTraceCheckACM SIGARCH Computer Architecture News10.1145/3140659.308023545:2(201-213)Online publication date: 24-Jun-2017
https://dl.acm.org/doi/10.1145/3140659.3080235
Lustig DTrippel CPellauer MMartonosi M(2015)ArMORACM SIGARCH Computer Architecture News10.1145/2872887.275037843:3S(388-400)Online publication date: 13-Jun-2015
https://dl.acm.org/doi/10.1145/2872887.2750378
Manerkar YLustig DPellauer MMartonosi MPrvulovic M(2015)CCICheckProceedings of the 48th International Symposium on Microarchitecture10.1145/2830772.2830782(26-37)Online publication date: 5-Dec-2015
https://dl.acm.org/doi/10.1145/2830772.2830782
Lustig DTrippel CPellauer MMartonosi MMarr DAlbonesi D(2015)ArMORProceedings of the 42nd Annual International Symposium on Computer Architecture10.1145/2749469.2750378(388-400)Online publication date: 13-Jun-2015
https://dl.acm.org/doi/10.1145/2749469.2750378
Mammo BBertacco VDeOrio AWagner I(2015)Post-Silicon Validation of Multiprocessor Memory ConsistencyIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2015.240217134:6(1027-1037)Online publication date: 1-Jun-2015
https://dl.acm.org/doi/10.1109/TCAD.2015.2402171
Hechtman BSorin DMendelson A(2013)Exploring memory consistency for massively-threaded throughput-oriented processorsProceedings of the 40th Annual International Symposium on Computer Architecture10.1145/2485922.2485940(201-212)Online publication date: 23-Jun-2013
https://dl.acm.org/doi/10.1145/2485922.2485940
Dongol BTravkin ODerrick JWehrheim H(2013)A High-Level Semantics for Program Execution under Total Store Order MemoryTheoretical Aspects of Computing – ICTAC 201310.1007/978-3-642-39718-9_11(177-194)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39718-9_11
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents