{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T03:41:53Z","timestamp":1790480513512,"version":"4.1.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,10,10]]},"abstract":"<jats:p>Java's memory model was recently updated and expanded with new access modes. The accompanying documentation for these access modes is intended to make strong guarantees about program behavior that the Java compiler must enforce, yet the documentation is frequently unclear. This makes the intended program behavior ambiguous, impedes discussion of key design decisions, and makes it impossible to prove general properties about the semantics of the access modes.<\/jats:p>\n          <jats:p>In this paper we present the first formalization of Java's access modes. We have constructed an axiomatic model for all of the modes using the Herd modeling tool. This allows us to give precise answers to questions about the behavior of example programs, called litmus tests. We have validated our model using a large suite of litmus tests from existing research which helps to shed light on the relationship with other memory models. We have also modeled the semantics in Coq and proven several general theorems including a DRF guarantee, which says that if a program is properly synchronized then it will exhibit sequentially consistent behavior. Finally, we use our model to prove that the unusual design choice of a partial order among writes to the same location is unobservable in any program.<\/jats:p>","DOI":"10.1145\/3360568","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["A formalization of Java\u2019s concurrent access modes"],"prefix":"10.1145","volume":"3","author":[{"given":"John","family":"Bender","sequence":"first","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[{"name":"University of California at Los Angeles, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2010. Programming Languages-C++(final committee draft). C++ standards committee paper WG21\/N3092= J16\/10-0082.  2010. Programming Languages-C++(final committee draft). C++ standards committee paper WG21\/N3092= J16\/10-0082."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792233.1792237"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926394"},{"key":"e_1_2_2_6_1","unstructured":"Mark Batty and Peter Sewell. 2014. The Thin-air Problem. http:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/notes42.html . [Dec. 2018].  Mark Batty and Peter Sewell. 2014. The Thin-air Problem. http:\/\/www.cl.cam.ac.uk\/~pes20\/cpp\/notes42.html . [Dec. 2018]."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814318"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375591"},{"key":"e_1_2_2_9_1","unstructured":"Hans J Boehm Olivier Giroux and Viktor Vafeiades. 2018. P0982R1: Weaken Release Sequences. http:\/\/www.openstd.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p0982r1.html . [Aug. 2019].  Hans J Boehm Olivier Giroux and Viktor Vafeiades. 2018. P0982R1: Weaken Release Sequences. http:\/\/www.openstd.org\/jtc1\/sc22\/wg21\/docs\/papers\/2018\/p0982r1.html . [Aug. 2019]."},{"key":"e_1_2_2_10_1","unstructured":"Jon Corbet. 2012. ACCESS_ONCE(). https:\/\/lwn.net\/Articles\/508991\/ . [Dec 2018].  Jon Corbet. 2012. ACCESS_ONCE(). https:\/\/lwn.net\/Articles\/508991\/ . [Dec 2018]."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676984"},{"key":"e_1_2_2_12_1","first-page":"81","article-title":"The Java memory model: a formal explanation","volume":"7","author":"Huisman Marieke","year":"2007","journal-title":"VAMP"},{"key":"e_1_2_2_13_1","unstructured":"JDK9. 2017. VarHandle API Docs. https:\/\/docs.oracle.com\/javase\/9\/docs\/api\/java\/lang\/invoke\/VarHandle.html . [Mar. 2019].  JDK9. 2017. VarHandle API Docs. https:\/\/docs.oracle.com\/javase\/9\/docs\/api\/java\/lang\/invoke\/VarHandle.html . [Mar. 2019]."},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of POPL\u201917","author":"Kang Jeehoon","year":"2017"},{"key":"e_1_2_2_15_1","unstructured":"Ori Lahav. 2019. personal communication.  Ori Lahav. 2019. personal communication."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062352"},{"key":"e_1_2_2_17_1","unstructured":"Doug Lea. 2017. JEP 193. http:\/\/openjdk.java.net\/jeps\/193 . [Mar. 2019].  Doug Lea. 2017. JEP 193. http:\/\/openjdk.java.net\/jeps\/193 . [Mar. 2019]."},{"key":"e_1_2_2_18_1","unstructured":"Doug Lea. 2018. Using JDK 9 Memory Order Modes. http:\/\/gee.cs.oswego.edu\/dl\/html\/j9mm.html . [Online March 2019].  Doug Lea. 2018. Using JDK 9 Memory Order Modes. http:\/\/gee.cs.oswego.edu\/dl\/html\/j9mm.html . [Online March 2019]."},{"key":"e_1_2_2_19_1","unstructured":"Doug Lea. 2019. personal communication.  Doug Lea. 2019. personal communication."},{"key":"e_1_2_2_20_1","volume-title":"Proceedings of the 32Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201905)","author":"Manson Jeremy"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491967"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276506"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837616"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158107"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254102"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_3"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/42190.42277"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676995"},{"key":"e_1_2_2_31_1","volume-title":"Taming the complexities of the C11 and OpenCL memory models. arXiv preprint arXiv:1503.07073","author":"Wickerson John","year":"2015"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360568","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360568","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360568"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":30,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360568"],"URL":"https:\/\/doi.org\/10.1145\/3360568","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}