{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:18Z","timestamp":1776305058530,"version":"3.50.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377051","type":"print"},{"value":"9783031377068","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T00:00:00Z","timestamp":1689552000000},"content-version":"vor","delay-in-days":197,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper presents , a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM).  provides a simple and declarative way to write concurrent tests: instead of describing <jats:italic>how<\/jats:italic> to perform the test, users specify <jats:italic>what to test<\/jats:italic> by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with  are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking,  provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation.<\/jats:p><jats:p>To the best of our knowledge,  is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated  in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java\u2019s standard  and a liveliness bug in Java\u2019s  framework, which is used in most of the synchronization primitives. We believe that  can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness.<\/jats:p>","DOI":"10.1007\/978-3-031-37706-8_8","type":"book-chapter","created":{"date-parts":[[2023,7,16]],"date-time":"2023-07-16T10:01:21Z","timestamp":1689501681000},"page":"156-169","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Lincheck: A Practical Framework for\u00a0Testing Concurrent Data Structures on\u00a0JVM"],"prefix":"10.1007","author":[{"given":"Nikita","family":"Koval","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Fedorov","sequence":"additional","affiliation":[]},{"given":"Maria","family":"Sokolova","sequence":"additional","affiliation":[]},{"given":"Dmitry","family":"Tsitelov","sequence":"additional","affiliation":[]},{"given":"Dan","family":"Alistarh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,7,17]]},"reference":[{"key":"8_CR1","unstructured":"Lincheck - A framework for testing concurrent data structures on JVM. https:\/\/github.com\/Kotlin\/kotlinx-lincheck"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"},{"key":"8_CR3","unstructured":"The Java Concurrency Stress tests. https:\/\/openjdk.java.net\/projects\/code-tools\/jcstress"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"444","DOI":"10.1007\/11562948_33","volume-title":"Automated Technology for Verification and Analysis","author":"G Lindstrom","year":"2005","unstructured":"Lindstrom, G., Mehlitz, P.C., Visser, W.: Model checking real time java using java pathfinder. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 444\u2013456. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11562948_33"},{"issue":"6","key":"8_CR5","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/1273442.1250785","volume":"42","author":"M Musuvathi","year":"2007","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. SIGPLAN Not. 42(6), 446\u2013455 (2007)","journal-title":"SIGPLAN Not."},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/978-3-030-81685-8_20","volume-title":"Computer Aided Verification","author":"M Kokologiannakis","year":"2021","unstructured":"Kokologiannakis, M., Vafeiadis, V.: GenMC: a model checker for weak memory models. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 427\u2013440. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_20"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Jung, R., et al.: Iris: monoids and invariants as an orthogonal basis for concurrent reasoning. In: Conference Record of the Annual ACM Symposium on Principles of Programming Languages 2015, pp. 637\u2013650 (2015)","DOI":"10.1145\/2775051.2676980"},{"key":"8_CR8","unstructured":"Coq - a formal proof management system. https:\/\/coq.inria.fr"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463\u2013492 (1990)","DOI":"10.1145\/78969.78972"},{"key":"8_CR10","unstructured":"Herlihy, M., Shavit, N., Luchangco, V., Spear, M.: The art of multiprocessor programming. Newnes (2020)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Kirsch, C.M., Payer, H., Sezgin, A., Sokolova, A.: Quantitative relaxation of concurrent data structures. In ACM SIGPLAN Notices, vol. 48, pp. 317\u2013328. ACM (2013)","DOI":"10.1145\/2480359.2429109"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-17653-1_29","volume-title":"Principles of Distributed Systems","author":"Y Afek","year":"2010","unstructured":"Afek, Y., Korland, G., Yanovsky, E.: Quasi-linearizability: relaxed consistency for improved concurrency. In: Lu, C., Masuzawa, T., Mosbah, M. (eds.) OPODIS 2010. LNCS, vol. 6490, pp. 395\u2013410. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17653-1_29"},{"key":"8_CR13","unstructured":"[JDK-8256833] ConcurrentLinkedDeque is non-linearizable. https:\/\/bugs.openjdk.java.net\/browse\/JDK-8256833"},{"key":"8_CR14","unstructured":"[JDK-8188900] ConcurrentLinkedDeque linearizability. https:\/\/bugs.openjdk.java.net\/browse\/JDK-8188900"},{"key":"8_CR15","unstructured":"[JDK-8189387] ConcurrentLinkedDeque linearizability continued. https:\/\/bugs.openjdk.java.net\/browse\/JDK-8189387"},{"key":"8_CR16","unstructured":"Kotlin Coroutines. https:\/\/github.com\/Kotlin\/kotlin-coroutines"},{"key":"8_CR17","unstructured":"JCTools - Java Concurrency Tools for the JVM. https:\/\/github.com\/JCTools\/JCTools"},{"key":"8_CR18","unstructured":"Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM. Zenodo (2023)"},{"key":"8_CR19","unstructured":"Race in NonBlockingHashMapLong in JCTools. https:\/\/github.com\/JCTools\/JCTools\/issues\/319"},{"key":"8_CR20","unstructured":"MutexLincheckTest.modelCheckingTest detects non lock-free execution path in Mutex #2590. https:\/\/github.com\/Kotlin\/kotlinx.coroutines\/issues\/2590"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Lu, S., Park, S., Seo, E., Zhou, Y.: 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, pp. 329\u2013339 (2008)","DOI":"10.1145\/1346281.1346323"},{"key":"8_CR22","unstructured":"Lincheck User Guide. https:\/\/kotlinlang.org\/docs\/lincheck-guide.html"},{"key":"8_CR23","unstructured":"ObjectWeb ASM. https:\/\/asm.ow2.io"},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"06","DOI":"10.1145\/2499370.2462162","volume":"48","author":"T Elmas","year":"2013","unstructured":"Elmas, T., Burnim, J., Necula, G., Sen, K.: Concurrit: a domain specific language for reproducing concurrency bugs. ACM SIGPLAN Not. 48, 06 (2013)","journal-title":"ACM SIGPLAN Not."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Raad, A., Vafeiadis, V.: Model checking for weakly consistent libraries. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 96\u2013110. Association for Computing Machinery, New York (2019)","DOI":"10.1145\/3314221.3314609"},{"issue":"1","key":"8_CR26","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0169-7552(96)00017-7","volume":"29","author":"J Tretmans","year":"1996","unstructured":"Tretmans, J.: Conformance testing with labelled transition systems: implementation relations and test generation. Comput. Netw. ISDN Syst. 29(1), 49\u201379 (1996)","journal-title":"Comput. Netw. ISDN Syst."},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Koval, N., Alistarh, D., Elizarov, R.: Scalable fifo channels for programming via communicating sequential processes. In European Conference on Parallel Processing. Springer, Heidelberg (2019). http:\/\/pub.ist.ac.at\/dalistar\/Scalable_FIFO_Channels_EuroPar.pdf","DOI":"10.1007\/978-3-030-29400-7_23"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"Scherer III, W.N., Scott, M.L.: Nonblocking concurrent objects with condition synchronization. In: Proceedings of the 18th International Symposium on Distributed Computing, pp. 2121\u20132128 (2004)","DOI":"10.1007\/978-3-540-30186-8_13"},{"key":"8_CR29","unstructured":"Concurrent Radix and Suffix Trees for Java. https:\/\/github.com\/npgall\/concurrent-trees"},{"key":"8_CR30","unstructured":"Race in ConcurrentSuffixTree in Concurrent-Trees library. https:\/\/github.com\/npgall\/concurrent-trees\/issues\/33"},{"issue":"5","key":"8_CR31","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/1837853.1693488","volume":"45","author":"NG Bronson","year":"2010","unstructured":"Bronson, N.G., Casper, J., Chafi, H., Olukotun, K.: A practical concurrent binary search tree. SIGPLAN Not. 45(5), 257\u2013268 (2010)","journal-title":"SIGPLAN Not."},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Drachsler, D., Vechev, M., Yahav, E.: Practical concurrent binary search trees via logical ordering. In: Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2014, pp. 343\u2013356. Association for Computing Machinery, New York (2014)","DOI":"10.1145\/2555243.2555269"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Sagonas, K., Winblad, K.: Contention adapting search trees. In: 2015 14th International Symposium on Parallel and Distributed Computing, pp. 215\u2013224 (2015)","DOI":"10.1109\/ISPDC.2015.32"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Aksenov, V., Gramoli, V., Kuznetsov, P., Malova, A., Ravi, S.: A concurrency-optimal binary search tree, pp. 580\u2013593 (2017)","DOI":"10.1007\/978-3-319-64203-1_42"},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Pradel, M., Gross, T.R.: Fully automatic and precise detection of thread safety violations. In: Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, pp. 521\u2013530 (2012)","DOI":"10.1145\/2254064.2254126"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 330\u2013340 (2010)","DOI":"10.1145\/1806596.1806634"},{"key":"8_CR37","doi-asserted-by":"crossref","unstructured":"Li, G., Lu, S., Musuvathi, M., Nath, S., Padhye, R.: Efficient scalable thread-safety-violation detection: finding thousands of concurrency bugs during testing. In: Proceedings of the 27th ACM Symposium on Operating Systems Principles, pp. 162\u2013180 (2019)","DOI":"10.1145\/3341301.3359638"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"O\u2019Callahan, R., Choi, J.D.: Hybrid dynamic data race detection. In: Proceedings of the Ninth ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2003, pp. 167\u2013178. Association for Computing Machinery, New York (2003)","DOI":"10.1145\/781498.781528"},{"key":"8_CR39","doi-asserted-by":"crossref","unstructured":"Naik, M., Aiken, A., Whaley, J.: Effective static race detection for java. In: Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2006, pp. 308\u2013319. Association for Computing Machinery, New York (2006)","DOI":"10.1145\/1133981.1134018"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Sen, K.: Race directed random testing of concurrent programs. In PLDI 2008 (2008)","DOI":"10.1145\/1375581.1375584"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Huang, J., O\u2019Neil Meredith, P., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not. 49(6), 337\u2013348 (2014)","DOI":"10.1145\/2666356.2594315"},{"key":"8_CR42","doi-asserted-by":"crossref","unstructured":"Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Proceedings of the 25th International Conference on Computer Aided Verification, vol. 8044, pp. 141\u2013157 (2013)","DOI":"10.1007\/978-3-642-39799-8_9"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Kokologiannakis, M., Lahav, O., Sagonas, K., Vafeiadis, V.: Effective stateless model checking for c\/c++ concurrency. Proc. ACM Program. Lang. 2(POPL) (2017)","DOI":"10.1145\/3158105"},{"key":"8_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/978-3-030-25543-5_30","volume-title":"Computer Aided Verification","author":"M Emmi","year":"2019","unstructured":"Emmi, M., Enea, C.: Violat: generating tests of observational refinement for concurrent objects. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 534\u2013546. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_30"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-37706-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T11:04:06Z","timestamp":1704452646000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37706-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377051","9783031377068"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37706-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"17 July 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}