{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T04:03:30Z","timestamp":1746331410988,"version":"3.40.4"},"reference-count":61,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2014,6,10]],"date-time":"2014-06-10T00:00:00Z","timestamp":1402358400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Distrib. Comput."],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1007\/s00446-013-0205-0","type":"journal-article","created":{"date-parts":[[2014,6,10]],"date-time":"2014-06-10T18:30:58Z","timestamp":1402425058000},"page":"363-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Partition consistency"],"prefix":"10.1007","volume":"27","author":[{"given":"Steven","family":"Cheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lisa","family":"Higham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jalal","family":"Kawash","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,6,10]]},"reference":[{"key":"205_CR1","doi-asserted-by":"crossref","unstructured":"Aceto, L., Inglfsdttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge 8 (2007)","DOI":"10.1017\/CBO9780511814105"},{"issue":"5","key":"205_CR2","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1109\/TPDS.2003.1199067","volume":"14","author":"A. Adir","year":"2003","unstructured":"Adir A., Attiya H., Shurek G.: Information-flow models for shared memory with an application to the powerpc architecture. IEEE Trans. Parallel Distrib. Syst. 14(5), 502\u2013515 (2003)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"205_CR3","unstructured":"Adve, S.V.: Using Information from the Programmer to Implement System Optimizations without Violating Sequential Consistency. Technical Report ECE 9603, Department of Electrical and Computer Engineering, Rice University (March 1996)"},{"issue":"11","key":"205_CR4","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1145\/1839676.1839697","volume":"53","author":"S.V. Adve","year":"2010","unstructured":"Adve S.V.: Data races are evil with no exceptions: technical perspective. Commun. ACM 53(11), 84 (2010)","journal-title":"Commun. ACM"},{"key":"205_CR5","doi-asserted-by":"crossref","unstructured":"Agrawal, D., Choy, M., Leong, H.V., Singh, A.K.: Investigating weak memories using Maya. In: Proceedings of the 3rd International Symposium on High Performance, Distributed Computing, pp. 123\u2013130 (1994)","DOI":"10.1109\/HPDC.1994.340252"},{"key":"205_CR6","doi-asserted-by":"crossref","unstructured":"Ahamad, M., Bazzi, R., John, R., Kohli, P., Neiger, G.: The power of processor consistency. In: Proceedings of the 5th International Symposium on Parallel Algorithms and Architectures, pp. 251\u2013260. Technical Report GIT-CC-92\/34, College of Computing, Georgia Institute of Technology (June 1993)","DOI":"10.1145\/165231.165264"},{"key":"205_CR7","doi-asserted-by":"crossref","unstructured":"Aspinall, D., Sevc\u00edk, J.: Formalising Java\u2019s data race free guarantee. In: Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp. 22\u201337 (2007)","DOI":"10.1007\/978-3-540-74591-4_4"},{"key":"205_CR8","doi-asserted-by":"crossref","unstructured":"Attiya, H., Friedman, R.: Programming DEC-Alpha based multiprocessors the easy way. In: Proceedings of the 6th International Symposium on Parallel Algorithms and Architectures, pp. 157\u2013166. Technical Report LPCR 9411, Computer Science Department, Technion (1994)","DOI":"10.1145\/181014.192323"},{"issue":"2","key":"205_CR9","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/176575.176576","volume":"12","author":"H. Attiya","year":"1994","unstructured":"Attiya H., Welch J.: Sequential consistency versus linearizability. ACM Trans. Comput. Syst. 12(2), 91\u2013122 (1994)","journal-title":"ACM Trans. Comput. Syst."},{"key":"205_CR10","doi-asserted-by":"crossref","unstructured":"Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics. Wiley, New York (2004).","DOI":"10.1002\/0471478210"},{"key":"205_CR11","unstructured":"Backhouse, R.: Program Construction: Calculating Implementations from Specifications. Wiley, New York, NY (2003)"},{"key":"205_CR12","doi-asserted-by":"crossref","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing c++ concurrency. In: Ball, T., Sagiv, M. (eds.) POPL, pp. 55\u201366. ACM (2011)","DOI":"10.1145\/1925844.1926394"},{"issue":"6","key":"205_CR13","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/1379022.1375591","volume":"43","author":"H.-J. Boehm","year":"2008","unstructured":"Boehm H.-J., Adve S.V.: Foundations of the c++ concurrency memory model. SIGPLAN Not. 43(6), 68\u201378 (2008)","journal-title":"SIGPLAN Not."},{"issue":"1\u20133","key":"205_CR14","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","unstructured":"Brookes S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1\u20133), 227\u2013270 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"205_CR15","doi-asserted-by":"crossref","unstructured":"Brzezinski, J., Szychowiak, M.: Low cost coherence protocol for DSM systems with processor consistency. In: Yazici, A., Sener, C. (eds.) ISCIS, volume 2869 of Lecture Notes in Computer Science, pp. 916\u2013925. Springer, Berlin (2003)","DOI":"10.1007\/978-3-540-39737-3_114"},{"key":"205_CR16","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Alur, R., Martin, M.M.K.: CheckFence: checking consistency of concurrent data types on relaxed memory models. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 12\u201321. ACM (2007)","DOI":"10.1145\/1250734.1250737"},{"key":"205_CR17","doi-asserted-by":"crossref","unstructured":"Cholvi, V., Fern\u00e1ndez, A., Jim\u00e9nez, E., Raynal, M.: A methodological construction of an efficient sequential consistency protocol. In: Proceedings of the 3rd IEEE International Symposium on Network Computing and Applications, pp. 141\u2013148. IEEE Computer Society (2004)","DOI":"10.1109\/NCA.2004.1347771"},{"key":"205_CR18","unstructured":"Corella, F., Stone, J.M., Barton, C.: A Formal Specification of the PowerPC Shared Memory Architecture. Technical Report RC18638, IBM (1994)"},{"key":"205_CR19","unstructured":"Compaq Computer Corportaion: The Alpha Architecture Handbook (1998). Order number: EC-QD2KC-TE"},{"key":"205_CR20","doi-asserted-by":"crossref","unstructured":"Feijen, W.H.J., van Gasteren, A.J.M.: On a Method of Multiprogramming. Springer, New York (1999)","DOI":"10.1007\/978-1-4757-3126-2"},{"key":"205_CR21","unstructured":"Gharachorloo, K., Gupta, A., Hennessy, J.: Revision to Memory Consistency and Event Ordering in Scalable Shared-Memory Multiprocessors. Technical Report CSL-TR-93-568, Computer Systems Laboratory, Stanford University (April 1993)"},{"key":"205_CR22","doi-asserted-by":"crossref","unstructured":"Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P.B., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. In: Proceedings of the 17th International Symposium on Computer Architecture, pp. 15\u201326 (May 1990)","DOI":"10.1145\/325096.325102"},{"key":"205_CR23","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0304-3975(88)90124-7","volume":"61","author":"J.L. Gischer","year":"1988","unstructured":"Gischer J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61, 199\u2013224 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"205_CR24","unstructured":"Goodman, J.R.: Cache Consistency and Sequential Consistency. Technical Report 61, IEEE Scalable Coherence Interface Working, Group (March 1989)"},{"key":"205_CR25","unstructured":"Goodman, J.: Cache Consistency and Sequential Consistency. Technical Report 61, IEEE Scalable Coherent Interface Working Group (March 1989)"},{"issue":"3","key":"205_CR26","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M. Herlihy","year":"1990","unstructured":"Herlihy M., Wing J.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463\u2013492 (1990)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"205_CR27","doi-asserted-by":"crossref","unstructured":"Higham, L., Jackson, L.: Translating between Itanium and Sparc memory consistency models. In: Gibbons, P.B., Vishkin, U. (eds.) SPAA, pp. 170\u2013179. ACM (2006)","DOI":"10.1145\/1148109.1148138"},{"key":"205_CR28","doi-asserted-by":"crossref","unstructured":"Higham, L., Jackson, L., Kawash, J.: Capturing register and control dependence in memory consistency models with applications to the Itanium architecture. In: Proceedings of the 20th International Symposium on Distributed Computing (September 2006)","DOI":"10.1007\/11864219_12"},{"key":"205_CR29","doi-asserted-by":"crossref","unstructured":"Higham, L., Jackson, L., Kawash, J.: Programmer-centric conditions for Itanium memory consistency. In: Proceedings of the 8th International Conference on Distributed Computing and Networking (December 2006)","DOI":"10.1007\/11947950_7"},{"key":"205_CR30","doi-asserted-by":"crossref","unstructured":"Higham, L., Jackson, L., Kawash, J.: Specifying memory consistency of write buffer multiprocessors. ACM Trans. Comput. Syst. 25(1) (2007)","DOI":"10.1145\/1189736.1189737"},{"key":"205_CR31","unstructured":"Higham, L., Jackson, L., Kawash, J.: What is Itanium memory consistency from the programmer\u2019s point of view? Electr. Notes Theor. Comput. Sci. 174(9), 63\u201384 (2007)"},{"key":"205_CR32","doi-asserted-by":"crossref","unstructured":"Higham, L., Kawash, J.: Critical sections and producer\/consumer queues in weak memory systems. In: Proceedings of the 1997 International Symposium on Parallel Architectures, Algorithms and Networks, pp. 56\u201363 (December 1997)","DOI":"10.1109\/ISPAN.1997.645055"},{"key":"205_CR33","doi-asserted-by":"crossref","unstructured":"Higham, L., Kawash, J.: Java: memory consistency and process coordination (extended abstract). In: Proceeding of the 12th International Symposium on Distributed Computing. Lecture Notes in Computer Science, vol. 1499, pp. 201\u2013215 (1998)","DOI":"10.1007\/BFb0056484"},{"key":"205_CR34","unstructured":"Higham, L., Kawash, J.: Tight bounds for critical sections in processor consistent platforms. IEEE Trans. Parallel Distrib. Syst. 17(10), 1072\u20131083 (2006)"},{"key":"205_CR35","unstructured":"Higham, L., Kawash, J.: Implementing sequentially consistent programs on processor consistent platforms. J. Parallel Distrib. Comput. 68(4), 488\u2013500 (2008)"},{"key":"205_CR36","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes (Prentice-Hall International Series in Computer Science). Prentice Hall, Englewood Cliffs (1985)"},{"key":"205_CR37","unstructured":"Huseynov, J.: Distributed Shared Memory Home Pages. http:\/\/www.ics.uci.edu\/~javid\/dsm.html"},{"key":"205_CR38","unstructured":"Intel Corporation: Intel 64 Memory Ordering White Paper. Technical Report SKU:318147\u2013001, Intel Corporation (2007)"},{"key":"205_CR39","unstructured":"Intel Corporation: Intel 64 and IA-32 Architectures Software Developer\u2019s Manual, Volume 3A: System Programming Guide, Part 1, SKU:253668 (2008)"},{"key":"205_CR40","unstructured":"Intel Corporation: Intel Itanium Architecture Software Developer\u2019s Manual, Volume 2: System Architecture (Oct 2002). http:\/\/www.intel.com\/"},{"key":"205_CR41","unstructured":"Keleher, P.J., Cox, A.L., Dwarkadas, S., Zwaenepoel, W.: Treadmarks: Distributed shared memory on standard workstations and operating systems. In USENIX Winter, pp. 115\u2013132 (1994)"},{"key":"205_CR42","unstructured":"Kuperstein, M., Vechev, M.T., Yahav, E.: Automatic inference of memory fences. In: Bloem, R., Sharygina, N. (eds.) FMCAD, pp. 111\u2013119. IEEE (2010)"},{"key":"205_CR43","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (July 1978)","DOI":"10.1145\/359545.359563"},{"key":"205_CR44","doi-asserted-by":"crossref","unstructured":"Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. C-28(9), 690\u2013691 (1979)","DOI":"10.1109\/TC.1979.1675439"},{"key":"205_CR45","doi-asserted-by":"crossref","unstructured":"Lamport, L.: On interprocess communication (parts I and II). Distrib. Comput. 1(2), 77\u201385 and 86\u2013101 (1986)","DOI":"10.1007\/BF01786228"},{"key":"205_CR46","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Reading (2002)"},{"key":"205_CR47","unstructured":"Lipton, R.J., Sandberg, J.S.: PRAM: A Scalable Shared Memory. Technical Report 180-88, Department of Computer Science, Princeton University (September 1988)"},{"key":"205_CR48","unstructured":"Lynch, N.A.: Distributed Algorithms (The Morgan Kaufmann Series in Data Management Systems), 1st edn. Morgan Kaufmann, Los Altos (1997)"},{"key":"205_CR49","doi-asserted-by":"crossref","unstructured":"Manson, J., Pugh, W., Adve, S.: The Java memory model. In: Palsberg, J., Abadi, M. (eds.), POPL, pp. 378\u2013391. ACM (2005)","DOI":"10.1145\/1047659.1040336"},{"key":"205_CR50","unstructured":"Milner, R.: Communication and Concurrency (Prentice Hall International Series in Computer Science), 1st edn. Prentice Hall, Englewood Cliffs (1995)"},{"key":"205_CR51","doi-asserted-by":"crossref","unstructured":"M\u00fcller, O.: I\/O automata and beyond: temporal logic and abstraction in Isabelle. In: Grundy, J., Newey, M.C. (eds.) Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, volume 1479 of Lecture Notes in Computer Science, pp. 331\u2013348. Springer, Berlin (1998)","DOI":"10.1007\/BFb0055145"},{"key":"205_CR52","doi-asserted-by":"crossref","unstructured":"Owens, S., Sarkar, S., Sewell, P.: A better x86 memory model: x86-TSO. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, volume 5674 of Lecture Notes in Computer Science, pp. 391\u2013407. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"205_CR53","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Modeling concurrency with geometry. In: Proceedings of the 18th Annual ACM Symposium on Principles of Programming Languages, pp. 311\u2013322 (January 1991)","DOI":"10.1145\/99583.99625"},{"key":"205_CR54","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"205_CR55","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Alglave, J., Maranget, L., Williams, D.: Understanding POWER multiprocessors. In: Hall, M.W., Padua, D.A. (eds.) PLDI, pp. 175\u2013186. ACM (2011)","DOI":"10.1145\/1993316.1993520"},{"key":"205_CR56","doi-asserted-by":"crossref","unstructured":"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: Shao, Z., Pierce, B.C. (eds.), POPL, pp. 379\u2013391. ACM (2009)","DOI":"10.1145\/1594834.1480929"},{"issue":"7","key":"205_CR57","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/1785414.1785443","volume":"53","author":"P. Sewell","year":"2010","unstructured":"Sewell P., Sarkar S., Owens S., Nardelli F.Z., Myreen M.O.: x86-TSO: a rigorous and usable programmer\u2019s model for x86 multiprocessors. Commun. ACM 53(7), 89\u201397 (2010)","journal-title":"Commun. ACM"},{"issue":"2","key":"205_CR58","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/42190.42277","volume":"10","author":"D. Shasha","year":"1988","unstructured":"Shasha D., Snir M.: Efficient and correct execution of parallel programs that share memory. ACM Trans. Program. Lang. Syst. 10(2), 282\u2013312 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"5","key":"205_CR59","doi-asserted-by":"crossref","first-page":"800","DOI":"10.1145\/1017460.1017464","volume":"51","author":"R.C. Steinke","year":"2004","unstructured":"Steinke R.C., Nutt G.J.: A unified theory of shared memory consistency. J. ACM 51(5), 800\u2013849 (2004)","journal-title":"J. ACM"},{"key":"205_CR60","unstructured":"Verwaal, N.: Ambiguous Memory Consistency Models. Department of Computer Science, The University of Calgary, Master\u2019s thesis (1998)"},{"key":"205_CR61","unstructured":"Western Canada Research Grid. Westgrid website. http:\/\/www.westgrid.ca"}],"container-title":["Distributed Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-013-0205-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00446-013-0205-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00446-013-0205-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T09:09:15Z","timestamp":1746263355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00446-013-0205-0"}},"subtitle":["A case study in modeling systems with weak memory consistency and proving correctness of their implementations"],"short-title":[],"issued":{"date-parts":[[2014,6,10]]},"references-count":61,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2014,10]]}},"alternative-id":["205"],"URL":"https:\/\/doi.org\/10.1007\/s00446-013-0205-0","relation":{},"ISSN":["0178-2770","1432-0452"],"issn-type":[{"type":"print","value":"0178-2770"},{"type":"electronic","value":"1432-0452"}],"subject":[],"published":{"date-parts":[[2014,6,10]]}}}