skip to main content
article

Specifying memory consistency of write buffer multiprocessors

Published: 01 February 2007 Publication History

Abstract

Write buffering is one of many successful mechanisms that improves the performance and scalability of multiprocessors. However, it leads to more complex memory system behavior, which cannot be described using intuitive consistency models, such as Sequential Consistency. It is crucial to provide programmers with a specification of the exact behavior of such complex memories. This article presents a uniform framework for describing systems at different levels of abstraction and proving their equivalence. The framework is used to derive and prove correct simple specifications in terms of program-level instructions of the sparc total store order and partial store order memories.The framework is also used to examine the sparc relaxed memory order. We show that it is not a memory consistency model that corresponds to any implementation on a multiprocessor that uses write-buffers, even though we suspect that the sparc version 9 specification of relaxed memory order was intended to capture a general write-buffer architecture. The same technique is used to show that Coherence does not correspond to a write-buffer architecture. A corollary, which follows from the relationship between Coherence and Alpha, is that any implementation of Alpha consistency using write-buffers cannot produce all possible Alpha computations. That is, there are some computations that satisfy the Alpha specification but cannot occur in the given write-buffer implementation.

References

[1]
Adir, A., Attiya, H., and Shurek, G. 2003. Information-flow models for shared memory with an application to the PowerPC architecture. IEEE Trans. Parallel Distrib. Syst. 14, 5, 502--515.]]
[2]
Ahamad, M., Bazzi, R., John, R., Kohli, P., and Neiger, G. 1993. The power of processor consistency. In Proceedings of the 5th International on Parallel Algorithms and Architectures. ACM, New York, 251--260. (Technical Report GIT-CC-92/34, College of Computing, Georgia Institute of Technology.)]]
[3]
Ahamad, M., Neiger, G., Burns, J., Kohli, P., and Hutto, P. 1995. Causal memory: Definitions, implementations, and programming. Distrib. Comput. 9, 37--49.]]
[4]
Anger, F. 1989. On Lamport's interprocessor communication model. ACM Trans. Prog. Lang. Syst. 11, 404--417.]]
[5]
Attiya, H., Chaudhuri, S., Friedman, R., and Welch, J. 1998. Shared memory consistency conditions for non-sequential execution: Definitions and programming strategies. SIAM J. Comput. 27, 1 (Feb.), 65--89.]]
[6]
Attiya, H. and Friedman, R. 1992. A correctness condition for high performance multiprocessors. In Proceedings of the 24th International Symposium on Theory of Computing. ACM, New York, 679--690.]]
[7]
Attiya, H. and Friedman, R. 1994. Programming DEC-Alpha based multiprocessors the easy way. In Proceedings of the 6th International Symposium on Parallel Algorithms and Architectures. ACM, New York, 157--166. (Technical Report LPCR 9411, Computer Science Department, Technion.)]]
[8]
Compaq Computer Corporation 1998. The Alpha Architecture Handbook. Compaq Computer Corporation. Order number: EC-QD2KC-TE.]]
[9]
Dubois, M., Scheurich, C., and Briggs, F. 1986. Memory access buffering in multiprocessors. In Proceedings of the 13th International Symposium on Computer Architecture. ACM, New York, 434--442.]]
[10]
Friedman, R. 1995. Implementing hybrid consistency with high-level synchronization operations. Distr. Comput. 9, 3 (Dec.), 119--129.]]
[11]
Frigo, M. 1998. The weakest reasonable memory model. M.S. dissertation. Department of Electrical Engineering and Computer Science, MIT, Cambridge, MA.]]
[12]
Gibbons, P. and Merritt, M. 1992. Specifying nonblocking shared memories. In Proceedings of the 4th International Symposium on Parallel Algorithms and Architectures. ACM, New York, 306--315.]]
[13]
Gontmakher, A. and Schuster, A. 2000. Java consistency: Nonoperational characterizations for Java memory behavior. ACM Trans. Comput. Syst. 18, 4, 333--386.]]
[14]
Goodman, J. 1989. Cache consistency and sequential consistency. Tech. Rep. 61, IEEE Scalable Coherent Interface Working Group. March.]]
[15]
Herlihy, M. and Wing, J. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Prog. Lang. Syst. 12, 3 (July), 463--492.]]
[16]
Higham, L. and Kawash, J. 1998. Java: Memory consistency and process coordination (extended abstract). In Proceedings of the 12th International Symposium on Distributed Computing. Lecture Notes in Computer Science, vol. 1499. Springer-Verlag, New York, 201--215.]]
[17]
Higham, L. and Kawash, J. 2000. Memory consistency and process coordination for SPARC multiprocessors. In Proceedings of the 7th International Conference on High Performance Computing. Lecture Notes in Computer Science, vol. 1970, Springer-Verlag, New York, 355--366.]]
[18]
Higham, L. and Kawash, J. 2005. Process coordination in the absence of sequential consistency. In Preparation.]]
[19]
Hoare, C. A. R. 1972. Towards a theory of parallel programming. In Operating System Techniques, C. A. R. Hoare and R. H. Perrott, Eds. Academic Press, Orland, FL.]]
[20]
Intel Corporation 2002. Intel itanium architecture software developer's manual, Volume 2: System architecture. http://www.intel.com/.]]
[21]
International Business Machines Corporation 1997. PowerPC microprocessor family: The programming environments for 32-bit microprocessor. http://www-3.ibm.com/chips/techlib/techlib.nsf/productfamilies/PowerPC.]]
[22]
Kawash, J. 2000. Limitations and capabilities of weak memory consistency systems. Ph.D. dissertation, Department of Computer Science, The University of Calgary, Calgary, B.L., Canada.]]
[23]
Kohli, P., Neiger, G., and Ahamad, M. 1993. A characterization of scalable shared memories. In Proceedings of the 1993 International Conference on Parallel Processing.]]
[24]
Lamport, L. 1978. Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 7 (July), 558--565.]]
[25]
Lamport, L. 1979a. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28, 9 (Sept.), 690--691.]]
[26]
Lamport, L. 1979b. A new approach to proving the correctness of multiprocess programs. ACM Trans. Prog. Lang. Syst. 1, 1 (July), 84--97.]]
[27]
Lamport, L. 1986a. The mutual exclusion problem (Parts I and II). J. ACM 33, 2 (Apr.), 313--326 and 327--348.]]
[28]
Lamport, L. 1986b. On interprocess communication (Parts I and II). Distr. Comput. 1, 2, 77--85 and 86--101.]]
[29]
Lamport, L. 1997. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Comput. 46, 7 (July), 779--782.]]
[30]
Lynch, N. 1996. Distributed Algorithms. Morgan Kaufmann, San Mateo, CA.]]
[31]
Lynch, N. and Tuttle, M. 1989. An introduction to input/output automata. CWI Quarterly 2, 3 (Sept.), 219--246.]]
[32]
Misra, J. 1986. Axioms for memory access in asynchronous hardware systems. ACM Trans. Prog. Lang. Syst. 8, 1, 142--153.]]
[33]
Owicki, S. and Gries, D. 1976. Verifying properties of parallel programs: An axiomatic approach. Commun. ACM 19, 5 (May), 279--285.]]
[34]
Park, S. and Dill, D. 1999. An executable specification and verifier for relaxed memory order. IEEE Trans. Comput. 48, 2 (Feb.), 227--235.]]
[35]
SPARC International, Inc. 1992. The SPARC Architecture Manual version 8. Prentice-Hall, Englewood Cliffs, NJ.]]
[36]
Sun Microsystems. 2004. http://www.sun.com/processors/whitepapers/us4_whitepaper.pdf.]]
[37]
Weaver, D. and Germond, T., Eds. 1994--2000. The SPARC Architecture Manual version 9. Prentice-Hall, Englewood Sliffs, NJ. http://developers.sun.com/solaris/articles/sparcv9.pdf.]]

Cited By

View all
  • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
  • (2023)Risotto: A Dynamic Binary Translator for Weak Memory Model ArchitecturesProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3567955.3567962(107-122)Online publication date: 25-Mar-2023
  • (2017)Automatically comparing memory consistency modelsACM SIGPLAN Notices10.1145/3093333.300983852:1(190-204)Online publication date: 1-Jan-2017
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computer Systems
ACM Transactions on Computer Systems  Volume 25, Issue 1
February 2007
106 pages
ISSN:0734-2071
EISSN:1557-7333
DOI:10.1145/1189736
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 February 2007
Published in TOCS Volume 25, Issue 1

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Memory consistency framework
  2. alpha
  3. coherence
  4. partial store order
  5. relaxed memory order
  6. sequential consistency
  7. sparc multiprocessors
  8. total store order
  9. write-buffer architectures

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)9
  • Downloads (Last 6 weeks)1
Reflects downloads up to 27 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2024)An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL LogicProceedings of the ACM on Programming Languages10.1145/36328638:POPL(604-637)Online publication date: 5-Jan-2024
  • (2023)Risotto: A Dynamic Binary Translator for Weak Memory Model ArchitecturesProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3567955.3567962(107-122)Online publication date: 25-Mar-2023
  • (2017)Automatically comparing memory consistency modelsACM SIGPLAN Notices10.1145/3093333.300983852:1(190-204)Online publication date: 1-Jan-2017
  • (2017)Automatically comparing memory consistency modelsProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009838(190-204)Online publication date: 1-Jan-2017
  • (2016)An operational semantics for C/C++11 concurrencyACM SIGPLAN Notices10.1145/3022671.298399751:10(111-128)Online publication date: 19-Oct-2016
  • (2016)An operational semantics for C/C++11 concurrencyProceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2983990.2983997(111-128)Online publication date: 19-Oct-2016
  • (2016)Pitfalls in Memory Consistency ModellingParallel Processing Letters10.1142/S012962641650008026:02(1650008)Online publication date: Jun-2016
  • (2014)Partition consistencyDistributed Computing10.1007/s00446-013-0205-027:5(363-389)Online publication date: 1-Oct-2014
  • (2011)Distributed collaboration models for social networks2011 International Conference on Computational Aspects of Social Networks (CASoN)10.1109/CASON.2011.6085917(48-53)Online publication date: Oct-2011
  • (2009)Interconnection of distributed memory modelsJournal of Parallel and Distributed Computing10.1016/j.jpdc.2008.11.00869:3(295-306)Online publication date: 1-Mar-2009
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media