{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:14:22Z","timestamp":1725484462105},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540000297"},{"type":"electronic","value":"9783540361039"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36103-0_44","type":"book-chapter","created":{"date-parts":[[2007,5,15]],"date-time":"2007-05-15T23:15:07Z","timestamp":1179270907000},"page":"423-434","source":"Crossref","is-referenced-by-count":1,"title":["Formal Reasoning about Hardware and Software Memory Models"],"prefix":"10.1007","author":[{"given":"Abhik","family":"Roychoudhury","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,10,10]]},"reference":[{"key":"44_CR1","unstructured":"Java Specification Request (JSR) 133. Java Memory Model and Thread Specification revision. In http:\/\/jcp.org\/jsr\/detail\/133.jsp , 2001."},{"key":"44_CR2","doi-asserted-by":"crossref","unstructured":"S.V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. IEEE Computer, December 1996.","DOI":"10.21236\/ADA638015"},{"key":"44_CR3","doi-asserted-by":"crossref","unstructured":"A. Charlesworth. Starfire: Extending the SMP envelope. IEEE Micro, 1998.","DOI":"10.1109\/40.653032"},{"key":"44_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"44_CR5","unstructured":"D.E. Culler and J. Pal Singh. parallelComputerArchitecture:AHardware\/Software Approach. Morgan Kaufmann Publishers, 1998."},{"key":"44_CR6","unstructured":"D.L. Weaver and T. Germond, Prentice Hall Publishers. The SPARC Architecture Manual: Version 9, 1994."},{"key":"44_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Computer Aided Verification (CAV)","author":"D. L. Dill","year":"1996","unstructured":"D. L. Dill. The Mur\u03d5 verification system. In Computer Aided Verification (CAV), LNCS 1102, 1996."},{"key":"44_CR8","unstructured":"D.L. Dill, S. Park, and A. Nowatzyk. Formal specification of abstract memory models. In Symposium on Research on Integrated Systems. MIT Press, 1993."},{"key":"44_CR9","unstructured":"J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Chapter 17, Addison Wesley, 1996."},{"key":"44_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4302-1129-7","volume-title":"Taming Java Threads","author":"A. Holub","year":"2000","unstructured":"A. Holub. Taming Java Threads. Berkeley CA, APress, 2000."},{"key":"44_CR11","doi-asserted-by":"crossref","unstructured":"L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, 28(9), 1979.","DOI":"10.1109\/TC.1979.1675439"},{"key":"44_CR12","doi-asserted-by":"crossref","unstructured":"J. Maessen, Arvind, and X. Shen. Improving the Java Memory Model using CRF. In ACM OOPSLA, 2000.","DOI":"10.1145\/353171.353172"},{"key":"44_CR13","doi-asserted-by":"crossref","unstructured":"J. Manson and W. Pugh. Core semantics of multithreaded Java. In ACM Java Grande Conference, 2001.","DOI":"10.1145\/376656.376806"},{"key":"44_CR14","doi-asserted-by":"crossref","unstructured":"S. Park and D.L. Dill. An executable specification and verifier for relaxed memory order. IEEE Transactions on Computers, 48(2), 1999.","DOI":"10.1109\/12.752664"},{"key":"44_CR15","doi-asserted-by":"crossref","unstructured":"W. Pugh. Fixing the Java Memory Model. In ACM Java Grande Conference, 1999.","DOI":"10.1145\/304065.304106"},{"key":"44_CR16","doi-asserted-by":"crossref","unstructured":"A. Roychoudhury and T. Mitra. Specifying multithreaded Java semantics for program verification. In ACM S IG S OFT International Conference on Software Engineering (ICSE), 2002.","DOI":"10.1145\/581396.581399"},{"key":"44_CR17","unstructured":"D. Schmidt and T. Harrison. Double-checked locking: An optimization pattern for efficiently initializing and accessing thread-safe objects. In 3rd Annual Pattern Languages of Program Design conference, 1996."},{"key":"44_CR18","unstructured":"XSB. The XSB logic programming system v2.2, 2000. Available for downloading from http:\/\/xsb.sourceforge.net\/ ."},{"key":"44_CR19","unstructured":"Y. Yang, G. Gopalakrishnan, and G. Lindstrom. Formalizing the Java Memory Model for multithreaded program correctness and optimization. Technical Report UUCS-02-011, University of Utah, Department of Computer Science, 2002."}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36103-0_44","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T20:56:00Z","timestamp":1556398560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36103-0_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540000297","9783540361039"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-36103-0_44","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}