AtomiS: Data-Centric Synchronization Made Practical
Authors: 
Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, 
António RavaraAuthors Info & Claims
Article No.: 226, Pages 116 - 145
Abstract
Data-Centric Synchronization (DCS) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCS is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters.
To overcome these limitations, in this paper we present AtomiS, a new DCS approach that requires only qualifying types of parameters and return values in interface definitions, and of fields in class definitions. The latter may also be abstracted away in type parameters, rendering class implementations virtually annotation-free. From this high level specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives that are responsible for ensuring the absence of data-races, atomicity-violations and deadlocks.
We provide a Java implementation and showcase the applicability of AtomiS in real-life code. For the benchmarks analysed, AtomiS requires fewer annotations than the original number of regions requiring locks, as well as fewer annotations than Atomic Sets (a reference DCS proposal).
References
[1]
Martín Abadi, Andrew Birrell, Tim Harris, and Michael Isard. 2011. Semantics of transactional memory and automatic mutual exclusion. ACM Trans. Program. Lang. Syst., 33, 1 (2011), 2:1–2:50. https://doi.org/10.1145/1889997.1889999
[2]
Cyrille Artho, Klaus Havelund, and Armin Biere. 2003. High-level data races. Softw. Test. Verification Reliab., 13, 4 (2003), 207–227. https://doi.org/10.1002/stvr.281
[3]
Sara Abbaspour Asadollah, Daniel Sundmark, Sigrid Eldh, and Hans Hansson. 2017. Concurrency bugs in open source software: a case study. J. Internet Serv. Appl., 8, 1 (2017), 4:1–4:15. https://doi.org/10.1186/s13174-017-0055-2
[4]
Chandrasekhar Boyapati, Robert Lee, and Martin C. Rinard. 2002. Ownership types for safe programming: preventing data races and deadlocks. In Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, Seattle, Washington, USA, November 4-8, 2002, Mamdouh Ibrahim and Satoshi Matsuoka (Eds.). ACM, 211–230. https://doi.org/10.1145/582419.582440
[5]
Elias Castegren and Tobias Wrigstad. 2019. OOlong: A Concurrent Object Calculus for Extensibility and Reuse. SIGAPP Appl. Comput. Rev., 18, 4 (2019), Jan., 47–60. issn:1559-6915 https://doi.org/10.1145/3307624.3307629
[6]
Luis Ceze, Pablo Montesinos, Christoph von Praun, and Josep Torrellas. 2007. Colorama: Architectural Support for Data-Centric Synchronization. In 13st International Conference on High-Performance Computer Architecture (HPCA-13 2007), 10-14 February 2007, Phoenix, Arizona, USA. IEEE Computer Society, 133–144. isbn:1-4244-0804-0 https://doi.org/10.1109/HPCA.2007.346192
[7]
Luis Ceze, Christoph von Praun, Calin Cascaval, Pablo Montesinos, and Josep Torrellas. 2008. Concurrency control with data coloring. In Proceedings of the 2008 ACM SIGPLAN workshop on Memory Systems Performance and Correctness: held in conjunction with the Thirteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’08), Seattle, Washington, USA, March 2, 2008, Emery D. Berger and Brad Chen (Eds.). ACM, 6–10. https://doi.org/10.1145/1353522.1353525
[8]
Sigmund Cherem, Trishul M. Chilimbi, and Sumit Gulwani. 2008. Inferring locks for atomic sections. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, Rajiv Gupta and Saman P. Amarasinghe (Eds.). ACM, 304–315. https://doi.org/10.1145/1375581.1375619
[9]
Brian Chin, Shane Markstrum, Todd D. Millstein, and Jens Palsberg. 2006. Inference of User-Defined Type Qualifiers and Qualifier Rules. In Programming Languages and Systems, 15th European Symposium on Programming, ESOP 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 27-28, 2006, Proceedings, Peter Sestoft (Ed.) (Lecture Notes in Computer Science, Vol. 3924). Springer, 264–278. https://doi.org/10.1007/11693024_18
[10]
Contemplate Ltd. 2014. ThreadSafe. http://www.contemplateltd.com/threadsafe Last visited in 4/2023
[11]
Weidong Cui, Xinyang Ge, Baris Kasikci, Ben Niu, Upamanyu Sharma, Ruoyu Wang, and Insu Yun. 2018. REPT: Reverse Debugging of Failures in Deployed Software. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8-10, 2018, Andrea C. Arpaci-Dusseau and Geoff Voelker (Eds.). USENIX Association, 17–32. https://www.usenix.org/conference/osdi18/presentation/weidong
[12]
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, C. R. Ramakrishnan and Jakob Rehof (Eds.) (Lecture Notes in Computer Science, Vol. 4963). Springer, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24
[13]
Peter Dinges, Minas Charalambides, and Gul Agha. 2013. Automated inference of atomic sets for safe concurrent execution. In ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE ’13, Seattle, WA, USA, June 20, 2013, Stephen N. Freund and Corina S. Pasareanu (Eds.). ACM, 1–8. isbn:978-1-4503-2128-0 https://doi.org/10.1145/2462029.2462030
[14]
Julian Dolby, Christian Hammer, Daniel Marino, Frank Tip, Mandana Vaziri, and Jan Vitek. 2012. A data-centric approach to synchronization. ACM Trans. Program. Lang. Syst., 34, 1 (2012), 4:1–4:48. https://doi.org/10.1145/2160910.2160913
[15]
Michael Emmi, Jeffrey S. Fischer, Ranjit Jhala, and Rupak Majumdar. 2007. Lock allocation. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, Martin Hofmann and Matthias Felleisen (Eds.). ACM, 291–296. isbn:1-59593-575-4 https://doi.org/10.1145/1190216.1190260
[16]
Dawson R. Engler and Ken Ashcraft. 2003. RacerX: effective, static detection of race conditions and deadlocks. In Proceedings of the 19th ACM Symposium on Operating Systems Principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, Michael L. Scott and Larry L. Peterson (Eds.). ACM, 237–252. https://doi.org/10.1145/945445.945468
[17]
Facebook Inc. 2013. A tool to detect bugs in Java and C/C++/Objective-C code before it ships. https://fbinfer.com/ Last visited in 4/2023
[18]
Cormac Flanagan and Stephen N. Freund. 2004. Atomizer: a dynamic atomicity checker for multithreaded programs. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, Neil D. Jones and Xavier Leroy (Eds.). ACM, 256–267. https://doi.org/10.1145/964001.964023
[19]
Jeffrey S. Foster, Manuel Fähndrich, and Alexander Aiken. 1999. A Theory of Type Qualifiers. In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, May 1-4, 1999, Barbara G. Ryder and Benjamin G. Zorn (Eds.). ACM, 192–203. https://doi.org/10.1145/301618.301665
[20]
Jeffrey S. Foster, Robert Johnson, John Kodumal, and Alex Aiken. 2006. Flow-insensitive type qualifiers. ACM Trans. Program. Lang. Syst., 28, 6 (2006), 1035–1087. https://doi.org/10.1145/1186632.1186635
[21]
David Greenfieldboyce and Jeffrey S. Foster. 2007. Type qualifier inference for java. In Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, Richard P. Gabriel, David F. Bacon, Cristina Videira Lopes, and Guy L. Steele Jr. (Eds.). ACM, 321–336. https://doi.org/10.1145/1297027.1297051
[22]
Michael Hicks, Jeffrey S Foster, and Polyvios Pratikakis. 2006. Lock inference for atomic sections. In Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing (TRANSACT ’06). ACM. http://www.cs.umd.edu/~polyvios/publications/transact06.pdf
[23]
Wei Huang and Ana Milanova. 2012. Inferring AJ Types for Concurrent Libraries. 19th International Workshop on Foundations of Object-Oriented Languages, FOOL 2012, Tucson, AZ, USA; October 22, 2012
[24]
2011. C++ 11 standard. https://www.iso.org/standard/50372.html Section 6.7.2.4 - Atomic type specifiers
[25]
Tim Kraska, Martin Hentschel, Gustavo Alonso, and Donald Kossmann. 2009. Consistency Rationing in the Cloud: Pay only when it matters. Proc. VLDB Endow., 2, 1 (2009), 253–264. https://doi.org/10.14778/1687627.1687657
[26]
Vivek Kumar, Julian Dolby, and Stephen M. Blackburn. 2016. Integrating Asynchronous Task Parallelism and Data-centric Atomicity. In Proceedings of the 13th International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, Lugano, Switzerland, August 29 - September 2, 2016, Walter Binder and Petr Tuma (Eds.). ACM, 7:1–7:10. https://doi.org/10.1145/2972206.2972214
[27]
Nancy G. Leveson and Clark Savage Turner. 1993. Investigation of the Therac-25 Accidents. Computer, 26, 7 (1993), 18–41. https://doi.org/10.1109/MC.1993.274940
[28]
Cheng Li, João Leitão, Allen Clement, Nuno M. Preguiça, Rodrigo Rodrigues, and Viktor Vafeiadis. 2014. Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference, USENIX ATC ’14, Philadelphia, PA, USA, June 19-20, 2014, Garth Gibson and Nickolai Zeldovich (Eds.). USENIX Association, 281–292. https://www.usenix.org/conference/atc14/technical-sessions/presentation/li_cheng_2
[29]
Shan Lu, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. 2008. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2008, Seattle, WA, USA, March 1-5, 2008, Susan J. Eggers and James R. Larus (Eds.). ACM, 329–339. https://doi.org/10.1145/1346281.1346323
[30]
Shan Lu, Joseph Tucek, Feng Qin, and Yuanyuan Zhou. 2006. AVIO: detecting atomicity violations via access interleaving invariants. In Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006, John Paul Shen and Margaret Martonosi (Eds.). ACM, 37–48. https://doi.org/10.1145/1168857.1168864
[31]
Daniel Marino, Christian Hammer, Julian Dolby, Mandana Vaziri, Frank Tip, and Jan Vitek. 2013. Detecting deadlock in programs with data-centric synchronization. In 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA, May 18-26, 2013, David Notkin, Betty H. C. Cheng, and Klaus Pohl (Eds.). IEEE Computer Society, 322–331. isbn:978-1-4673-3076-3 https://doi.org/10.1109/ICSE.2013.6606578
[32]
Bill McCloskey, Feng Zhou, David Gay, and Eric A. Brewer. 2006. Autolocker: synchronization inference for atomic sections. 346–358. isbn:1-59593-027-2 https://doi.org/10.1145/1111037.1111068
[33]
Scott Meyers. 2005. Effective C++: 55 Specific Ways to Improve Your Programs and Designs (3rd Edition). Addison-Wesley Professional. isbn:0321334876
[34]
2006. Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, J. Gregory Morrisett and Simon L. Peyton Jones (Eds.). ACM. isbn:1-59593-027-2 http://dl.acm.org/citation.cfm?id=1111037
[35]
David Neves and Hervé Paulino. 2022. Condition-based synchronization in data-centric concurrency control. In SAC ’22: The 37th ACM/SIGAPP Symposium on Applied Computing, Virtual Event, April 25 - 29, 2022, Jiman Hong, Miroslav Bures, Juw Won Park, and Tomás Cerný (Eds.). ACM, 1268–1275. https://doi.org/10.1145/3477314.3507120
[36]
OpenJDK. 2004. java.util.Collections. https://github.com/openjdk/jdk/blob/master/src/java.base/share/classes/java/util/Collections.java Last visited in 4/2023
[37]
Peter-Michael Osera. 2019. Constraint-based type-directed program synthesis. In Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2019, Berlin, Germany, August 18, 2019, David Darais and Jeremy Gibbons (Eds.). ACM, 64–76. isbn:978-1-4503-6815-5 https://doi.org/10.1145/3331554.3342608
[38]
Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, and António Ravara. 2023. Sound Atomicity Inference for Data-Centric Synchronization. CoRR, abs/2309.05483 (2023), https://doi.org/10.48550/arXiv.2309.05483 arXiv:2309.05483.
[39]
Hervé Paulino, Daniel Parreira, Nuno Delgado, António Ravara, and Ana Gualdina Almeida Matos. 2016. From atomic variables to data-centric concurrency control. In Proceedings of the 31st Annual ACM Symposium on Applied Computing. ACM, 1806–1811. https://doi.org/10.1145/2851613.2851734
[40]
Kevin Poulsen. 2004. Tracking the blackout bug. http://www.securityfocus.com/news/8412
[41]
Jake Roemer, Kaan Genç, and Michael D. Bond. 2020. SmartTrack: efficient predictive race detection. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 747–762. https://doi.org/10.1145/3385412.3385993
[42]
Ayesha Sadiq, Yuan-Fang Li, and Sea Ling. 2020. A survey on the use of access permission-based specifications for program verification. J. Syst. Softw., 159 (2020), https://doi.org/10.1016/j.jss.2019.110450
[43]
Florian T. Schneider, Vijay Menon, Tatiana Shpeisman, and Ali-Reza Adl-Tabatabai. 2008. Dynamic optimization for efficient strong atomicity. In Proceedings of the 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2008, October 19-23, 2008, Nashville, TN, USA, Gail E. Harris (Ed.). ACM, 181–194. https://doi.org/10.1145/1449764.1449779
[44]
Nir Shavit and Dan Touitou. 1995. Software Transactional Memory. In Proceedings of the Fourteenth Annual ACM Symposium on Principles of Distributed Computing, Ottawa, Ontario, Canada, August 20-23, 1995, James H. Anderson (Ed.). ACM, 204–213. isbn:0-89791-710-3 https://doi.org/10.1145/224964.224987
[45]
Herb Sutter and Andrei Alexandrescu. 2004. C++ Coding Standards: 101 Rules, Guidelines, and Best Practices (C++ in Depth Series). Addison-Wesley Professional. isbn:0321113586 https://www.oreilly.com/library/view/c-coding-standards/0321113586/
[46]
Mandana Vaziri, Frank Tip, and Julian Dolby. 2006. Associating synchronization constraints with data in an object-oriented language. 334–345. isbn:1-59593-027-2 https://doi.org/10.1145/1111037.1111067
[47]
Mandana Vaziri, Frank Tip, Julian Dolby, Christian Hammer, and Jan Vitek. 2010. A Type System for Data-Centric Synchronization. In ECOOP 2010 - Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21-25, 2010. Proceedings, Theo D’Hondt (Ed.) (Lecture Notes in Computer Science, Vol. 6183). Springer, 304–328. https://doi.org/10.1007/978-3-642-14107-2_15
[48]
Weiwei Xiong, Soyeon Park, Jiaqi Zhang, Yuanyuan Zhou, and Zhiqiang Ma. 2010. Ad Hoc Synchronization Considered Harmful. In 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings, Remzi H. Arpaci-Dusseau and Brad Chen (Eds.). USENIX Association, 163–176. http://www.usenix.org/events/osdi10/tech/full_papers/Xiong.pdf
[49]
Joshua Yanovski, Hoang-Hai Dang, Ralf Jung, and Derek Dreyer. 2021. GhostCell: separating permissions from data in Rust. Proc. ACM Program. Lang., 5, ICFP (2021), 1–30. https://doi.org/10.1145/3473597
[50]
Nosheen Zaza and Nathaniel Nystrom. 2016. Data-centric Consistency Policies: A Programming Model for Distributed Applications with Tunable Consistency. In First Workshop on Programming Models and Languages for Distributed Computing, PMLDC@ECOOP 2016, Rome, Italy, July 17, 2016. ACM, 3. https://doi.org/10.1145/2957319.2957377
[51]
Tong Zhang, Changhee Jung, and Dongyoon Lee. 2017. ProRace: Practical Data Race Detection for Production Use. In Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2017, Xi’an, China, April 8-12, 2017, Yunji Chen, Olivier Temam, and John Carter (Eds.). ACM, 149–162. https://doi.org/10.1145/3037697.3037708
Index Terms
- AtomiS: Data-Centric Synchronization Made Practical
Recommendations
A Transactional Correctness Tool for Abstract Data Types
Transactional memory simplifies multiprocessor programming by providing the guarantee that a sequential block of code in the form of a transaction will exhibit atomicity and isolation. Transactional data structures offer the same guarantee to concurrent ...
A data-centric approach to synchronization
Concurrency-related errors, such as data races, are frustratingly difficult to track down and eliminate in large object-oriented programs. Traditional approaches to preventing data races rely on protecting instruction sequences with synchronization ...
Associating synchronization constraints with data in an object-oriented language
POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesConcurrency-related bugs may happen when multiple threads access shared data and interleave in ways that do not correspond to any sequential execution. Their absence is not guaranteed by the traditional notion of "data race" freedom. We present a new ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2023
2250 pages
Copyright © 2023 Owner/Author.
This work is licensed under a Creative Commons Attribution 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 16 October 2023
Published in PACMPL Volume 7, Issue OOPSLA2
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 382Total Downloads
- Downloads (Last 12 months)344
- Downloads (Last 6 weeks)57
Reflects downloads up to 18 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in