{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T03:32:59Z","timestamp":1768879979459,"version":"3.49.0"},"reference-count":34,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Syst."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/1189736.1189737","type":"journal-article","created":{"date-parts":[[2007,4,5]],"date-time":"2007-04-05T19:20:08Z","timestamp":1175800808000},"page":"1","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Specifying memory consistency of write buffer multiprocessors"],"prefix":"10.1145","volume":"25","author":[{"given":"Lisa","family":"Higham","sequence":"first","affiliation":[{"name":"The University of Calgary, Calgary, AB, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lillanne","family":"Jackson","sequence":"additional","affiliation":[{"name":"The University of Calgary, Calgary, AB, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jalal","family":"Kawash","sequence":"additional","affiliation":[{"name":"American University of Sharjah"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/165231.165264"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784241"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/65979.65982"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794278396"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129778"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/181014.192323"},{"key":"e_1_2_1_8_1","volume-title":"The Alpha Architecture Handbook","author":"Compaq Computer Corporation 1998.","unstructured":"Compaq Computer Corporation 1998. The Alpha Architecture Handbook . Compaq Computer Corporation . Order number: EC-QD2KC-TE.]] Compaq Computer Corporation 1998. The Alpha Architecture Handbook. Compaq Computer Corporation. Order number: EC-QD2KC-TE.]]"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 13th International Symposium on Computer Architecture. ACM","author":"Dubois M.","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s004460050014"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/140901.141895"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/362670.362673"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_1_16_1","series-title":"Lecture Notes in Computer Science","volume-title":"Java: Memory consistency and process coordination (extended abstract). In Proceedings of the 12th International Symposium on Distributed Computing","author":"Higham L.","year":"1998","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 7th International Conference on High Performance Computing. Lecture Notes in Computer Science","volume":"1970","author":"Higham L.","unstructured":"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.]] 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.]]"},{"key":"e_1_2_1_18_1","unstructured":"Higham L. and Kawash J. 2005. Process coordination in the absence of sequential consistency. In Preparation.]]  Higham L. and Kawash J. 2005. Process coordination in the absence of sequential consistency. In Preparation.]]"},{"key":"e_1_2_1_19_1","volume-title":"Academic","author":"Hoare C. A. R.","unstructured":"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 .]] 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.]]"},{"key":"e_1_2_1_20_1","unstructured":"Intel Corporation 2002. Intel itanium architecture software developer's manual Volume 2: System architecture. http:\/\/www.intel.com\/.]]  Intel Corporation 2002. Intel itanium architecture software developer's manual Volume 2: System architecture. http:\/\/www.intel.com\/.]]"},{"key":"e_1_2_1_21_1","unstructured":"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.]]  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.]]"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICPP.1993.15"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/357062.357068"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/5383.5385"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01786227"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.599898"},{"key":"e_1_2_1_30_1","volume-title":"Distributed Algorithms. Morgan Kaufmann","author":"Lynch N.","unstructured":"Lynch , N. 1996. Distributed Algorithms. Morgan Kaufmann , San Mateo, CA .]] Lynch, N. 1996. Distributed Algorithms. Morgan Kaufmann, San Mateo, CA.]]"},{"key":"e_1_2_1_31_1","first-page":"3","article-title":"An introduction to input\/output automata","volume":"2","author":"Lynch N.","year":"1989","unstructured":"Lynch , N. and Tuttle , M. 1989 . An introduction to input\/output automata . CWI Quarterly 2 , 3 (Sept.), 219--246.]] Lynch, N. and Tuttle, M. 1989. An introduction to input\/output automata. CWI Quarterly 2, 3 (Sept.), 219--246.]]","journal-title":"CWI Quarterly"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/5001.5007"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.752664"},{"key":"e_1_2_1_35_1","unstructured":"SPARC International Inc. 1992. The SPARC Architecture Manual version 8. Prentice-Hall Englewood Cliffs NJ.]]   SPARC International Inc. 1992. The SPARC Architecture Manual version 8. Prentice-Hall Englewood Cliffs NJ.]]"},{"key":"e_1_2_1_36_1","unstructured":"Sun Microsystems. 2004. http:\/\/www.sun.com\/processors\/whitepapers\/us4_whitepaper.pdf.]]  Sun Microsystems. 2004. http:\/\/www.sun.com\/processors\/whitepapers\/us4_whitepaper.pdf.]]"},{"key":"e_1_2_1_37_1","volume-title":"1994--2000. The SPARC Architecture Manual version 9","author":"Weaver D.","unstructured":"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.]] 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.]]"}],"container-title":["ACM Transactions on Computer Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1189736.1189737","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1189736.1189737","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:22Z","timestamp":1750259182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1189736.1189737"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["10.1145\/1189736.1189737"],"URL":"https:\/\/doi.org\/10.1145\/1189736.1189737","relation":{},"ISSN":["0734-2071","1557-7333"],"issn-type":[{"value":"0734-2071","type":"print"},{"value":"1557-7333","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]},"assertion":[{"value":"2007-02-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}