LitmusKt: Concurrency Stress Testing for Kotlin

Anton Podkopaev; Denis Lochmelis; Evgenii Moiseenko; Yaroslav Golubev

REVIEW 2 major objections 5 minor 16 references

LitmusKt: Concurrency Stress Testing for Kotlin

T0 review · 2 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read LitmusKt, a Kotlin concurrency stress-testing tool, found previously unknown unsafe-publication bugs in Kotlin/Native, got them fixed, and joined Kotlin's CI pipeline.

desk verdict A solid tools paper that found and fixed real Kotlin/Native bugs; the formal-model gap is real but secondary. read the letter →

arxiv 2501.07472 v2 pith:FIMHVAGN submitted 2025-01-13 cs.PL cs.SE

Denis Lochmelis , Evgenii Moiseenko , Yaroslav Golubev , Anton Podkopaev This is my paper · ORCID

classification cs.PLcs.SE

keywords KotlinlitmustestingstressconcurrencycompilerdesignmemorymodelunsafepublicationKotlin/Native

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper claims that LitmusKt is the first tool that lets a programmer write a concurrency litmus test once in a Kotlin DSL and run it on both Kotlin/Native and Kotlin/JVM, and that the tool is good enough to find real compiler defects. The central evidence is the Unsafe Publication test: when one thread publishes an object while another reads one of its fields, Kotlin/Native 1.9.0 on an Arm processor returned garbage integers (e.g., 71817408) instead of null, a default value, or the value actually written; tests with reference fields could crash. The paper reports that the underlying bug was fixed, is absent from Kotlin 1.9.20 and later, and that LitmusKt was added to the Kotlin CI pipeline as a regression check. If this holds, LitmusKt demonstrates that useful stress testing is possible even for a language whose memory model is not formally specified.

What carries the argument

The carrying mechanism is the litmus test, i.e., a tiny concurrent program with a declared set of allowed outcomes, here written in a Kotlin DSL and executed many times by LitmusKt. The runner allocates a large array of independent test-state objects, lets each thread step across that array running its part of the test, and inserts periodic barriers so one thread cannot get too far ahead of the other; this amplifies rare weak interleavings into countable events. The DSL's spec classifies each observed outcome as acceptable, interesting, or forbidden, and the appearance of any forbidden outcome turns a run's status into FORBIDDEN. The unsafe-publication test then acts as the concrete probe: it arranges one thread to publish an object while another reads a field, and it is this probe that produced the garbage integers and crashes on Kotlin/Native.

What would settle it

Run the UPUB test as a standalone two-thread Kotlin/Native program without the tool's array-of-states runner; if millions of iterations on the same Arm hardware and Kotlin/Native 1.9.0 never show a garbage integer or crash, while the tool still shows FORBIDDEN outcomes, the runner becomes the suspect. If the standalone program reproduces the garbage values, the compiler is confirmed as the source.

Watch

Extended reading notes

Core claim

LitmusKt's discovery claim is that concurrent Kotlin code can violate the language's most basic memory-safety expectations. In the UPUB test, one thread publishes an IntHolder object while a second thread reads its field; on Kotlin/Native 1.9.0 for Arm the reader observed values like 71817408 and -1493360416, which no thread ever wrote, at frequencies around 12 in 40.8 million runs, and the analogous test with a class reference triggered segmentation faults. The paper classifies these as forbidden outcomes, argues they are compiler bugs rather than acceptable weak behaviors, reports a fix that landed by Kotlin 1.9.20, and states that LitmusKt is now part of Kotlin's continuous integration.

Load-bearing premise

The load-bearing premise is that Kotlin's unwritten memory-safety rules really do forbid the observed outgoing values, and that the stress-test tool's machinery for running the test many times does not itself create them.

Editorial extensions

If this is right

If the central claim holds, Kotlin/Native 1.9.0 on Arm violates basic memory safety under unsafe publication: a reader can observe integer values that were never written by any thread, and a reader of reference fields can crash.
Cross-platform litmus testing is viable from a single DSL, so the same concurrency expectations can be checked on both Kotlin/Native and Kotlin/JVM instead of maintaining separate harnesses.
The specific unsafe-publication bug is gone from Kotlin 1.9.20 onward, and LitmusKt's continued inclusion in Kotlin CI means regressions of that class have a chance of being caught automatically.
The null-from-non-null observation shows that even the type system's nullability guarantees can be violated at runtime under a data race, a consequence compiler engineers and language designers now have to account for.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural extension the paper does not pursue is to run the same UPUB pattern on Kotlin/JS and Kotlin/Wasm; the paper's own comparison logic implies divergences there would also signal implementation bugs.
The observed null from a non-nullable type points beyond the compiler bug: if data races can break type invariants, a future Kotlin memory model will have to say whether such outcomes are memory-model violations or type-system violations.
The JVM backend's wrapper-based approach suggests a reusable recipe: compile DSL tests to a common bytecode, then generate platform-specific harnesses, which could be applied to other multiplatform languages.
A concrete testable extension would be to rerun the UPUB and Array<Int> variants on current Kotlin/Native versions while toggling compiler optimization flags; if garbage values reappear, the fix is tied to optimizer behavior rather than to the source-level compiler.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: this is a legitimate engineering contribution. LitmusKt is the first litmus harness for Kotlin, and it caught an actual Kotlin/Native bug—unsafe publication producing genuinely garbage values—that was fixed and then integrated into Kotlin CI. That sequence of events, from test to bug to fix to pipeline, is the strongest possible evidence for a tools paper, and it should be credited.

What's new: the multiplatform angle. Writing one litmus test in a DSL and running on both Kotlin/Native and Kotlin/JVM is genuinely new, and the jcstress black-box integration is a reasonable way to get JVM coverage. The DSL is clean and follows jcstress conventions. The paper is honest about what it does not do: Kotlin has no formal memory model, so nothing here is a spec-conformance claim.

Where it's soft: the 'forbidden' classification depends on informal expectations about Kotlin memory safety. Garbage values like 71817408 are not plausibly the result of correct code generation, so the empirical inference is sound, but the paper leans on that intuition rather than a formal model. The runner's state-reuse and barrier scheme could in principle contaminate results, though the fix commit and CI adoption weigh heavily against that. The biggest practical gap is reproducibility: no raw logs, no standalone reproducer, no before/after on the fixed compiler. The referenced commit helps but is not a full artifact. Also, the fix was made by the same project group, so external confirmation is not fully independent—though it is still a real maintenance commit in the Kotlin repo.

The stress-test note worried that the harness, not the compiler, produced the garbage. I don't think that holds: the garbage values appear only on Kotlin/Native Arm, not on x86 or on JVM, and they could not have been written by the test itself. If the runner were broken, you'd expect platform-independent garbage. So I'd call that concern minor.

Bottom line: a well-scoped tools/experience paper with a real result. It deserved a serious referee and likely acceptance with minor revisions. A reader working on Kotlin concurrency or litmus methodology gets real value; others get a clean example of how litmus testing surfaces compiler bugs. My vote: send to peer review.

Referee Report

2 major / 5 minor

Summary. The manuscript presents LitmusKt, a litmus-testing framework and DSL for Kotlin, with backends for Kotlin/Native and Kotlin/JVM. It describes a custom native runner based on arrays of reusable test states and periodic barriers, and a JVM backend that delegates generated wrappers to jcstress. Using a collection of standard litmus tests, the authors report a central empirical finding: the UPUB test on an Arm machine with Kotlin/Native 1.9.0 produced 'garbage' integer outcomes such as 71817408 and -1493360416 that never appear as writes in the test program. The paper claims these FORBIDDEN outcomes correspond to a compiler bug in unsafe object publication, that a fix was merged into Kotlin, and that LitmusKt was integrated into Kotlin CI. The paper also discusses interesting outcomes of other tests and outlines future work on fuzzing and false-sharing avoidance.

Significance. LitmusKt, if the empirical claims hold, is a meaningful tool contribution: it is the first litmus-testing tool for Kotlin, it allows one DSL to drive two very different runtime backends, and it has already produced an acknowledged compiler fix and CI integration, both supported by commits referenced in the paper. The authors are candid about the absence of a formal Kotlin memory model, and the external fix lowers the circularity risk inherent in declaring outcomes 'forbidden' from the test author's own expectations. The main weakness is verification: the paper does not include the full UPUB test source, raw outcome logs, a standalone reproducer, or a before/after comparison on the fixed compiler, so the attribution of the garbage values to Kotlin/Native code generation, rather than to LitmusKt's state-reuse runner, is not fully checkable from the manuscript.

major comments (2)

[Section 3, Table 3] The FORBIDDEN outcomes in Table 3 are the load-bearing evidence for the paper's main claim, but the manuscript never states the precise semantic criterion by which values such as 71817408 are forbidden. Because Section 1 acknowledges that Kotlin has no formal memory model, the authors should make their implicit argument explicit: no instruction in the UPUB test ever writes a non-zero value to the field x of IntHolder, so any non-zero value read from x violates the constructor-initialization semantics regardless of weak-memory effects. Please state this or an equivalent invariant, and specify exactly which outcomes the spec section of the UPUB test marks as forbidden.
[Section 2.2, Section 3] The custom Kotlin/Native runner reuses a fixed array of state objects across iterations, but the paper does not specify whether each state is reinitialized before every iteration or how the per-thread state indices are chosen relative to the barrier. Without this information, a reader of the paper cannot rule out that the UPUB garbage values arose from stale or partially reused runner state rather than from an unsafely published IntHolder. The fix commit referenced as [7] is strong corroboration, but it is not analyzed in the paper. Please include the full LitmusKt source of UPUB, describe the state-reset and indexing protocol precisely, and provide raw logs or a standalone minimal Kotlin/Native program that reproduces a garbage value on 1.9.0 and does not reproduce it on 1.9.20.

minor comments (5)

[Section 2.2, Figure 2] The schematic shows 't1(state[i])' and 't2(state[j])' followed by 'sync', but the text does not explain whether the two threads access the same state index or different indices; please clarify the indexing scheme.
[Table 2] The test abbreviations ATOM, MP DRF, CoRR CSE, OOTA, and LB Deps are not defined; a legend or pointer to the corresponding tests in [11] would make the table self-contained.
[Section 3] The claim that the x86-only weak MP outcome 'can only be reasonably explained by aggressive compiler optimizations' is a hypothesis, not a demonstrated fact; please rephrase as a conjecture and mention that the table reports no confidence intervals or total run counts.
[Listing 1, Table 1] The DSL example would be easier to follow if the mapping from the state's r1 and r2 fields to the ordered outcome pair in the spec block were stated in the main text, not only in footnotes.
[References [7], [8]] References [7] and [8] are raw commit URLs; adding the commit titles or short descriptions would allow readers to understand what each commit changed without following the links.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the UPUB garbage-value result is an empirical anomaly, not an outcome forced by the tool's own outcome definitions, and the central bug claim is corroborated by the observed values and the subsequent Kotlin fix.

full rationale

The paper's central claim is empirical: running UPUB on Kotlin/Native 1.9.0 on Arm produced FORBIDDEN outcomes with integer values (e.g., 71817408, -1493360416) that are distinct from any value written by the test (the field should be either unread via null, or an initialized value 0). This is not a reduction of a 'prediction' to its inputs by construction: the test's expected outcomes are stated independently (null or 0), and the garbage values violate that expectation. The observed values are not fitted parameters or renamed outputs of the runner. The paper's outcome categories (acceptable/interesting/forbidden) are user-declared, but the bug conclusion rests on the external memory-safety judgment that a memory-safe language must not expose values never written or dangling references, not on a mathematical derivation from the DSL. Self-citations exist (the litmus-test survey [11], the fix commit [7], the CI integration commit [8], and the YouTrack issue [10]), but none is load-bearing: [11] is only a source of standard litmus tests, [7] and [8] post-date and corroborate the empirical findings, and [10] is a future-work suggestion. There is no imported uniqueness theorem or ansatz smuggled in via citation. The paper itself acknowledges the main limitation: Kotlin lacks a formally defined memory model (Section 1), so 'forbidden' is based on informal semantic expectations; additionally, the runner's state-reuse scheme (Section 2.2) and the absence of a standalone reproducer leave a residual alternative explanation for the garbage values. That is an empirical validity/reproducibility concern, not circularity: if the harness caused the values, the claimed compiler bug would be false, not tautological. Therefore, the derivation chain is not circular, and the evidence, including the external fix and CI integration, supports the paper's claims.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The central claims rest on informal semantic expectations about Kotlin and on the correctness of the harness; no numerical fitted parameters are used. The tool itself is a new artifact but not a theoretical entity.

assumptions (3)

domain assumption Kotlin/Native's intended semantics disallow reading uninitialized or garbage values from non-nullable object fields after publication.
Used in Section 3 to classify observed garbage values as forbidden and hence as a compiler bug; Kotlin has no formal memory model, so this is an informal semantic expectation.
domain assumption The LitmusKt harness does not itself introduce the observed corruption.
The Kotlin/Native runner in Section 2.2 reuses an array of states and synchronizes threads with barriers; if this machinery could cause unsafe memory reuse, the forbidden outcomes would not be attributable to the compiler.
domain assumption Standard litmus-test methodology is sound for exposing weak behaviors without falsely attributing races to specific instructions.
Section 2.2 relies on standard techniques from jcstress and litmus7; no model-checking or formal validation of the harness is supplied.

how reviews work

0 comments

Cite this review

Pith. "Pith review of LitmusKt: Concurrency Stress Testing for Kotlin." pith.science (2026). https://pith.science/paper/FIMHVAGN

@misc{pith2026250107472,
  author       = {Pith},
  title        = {Pith review of: LitmusKt: Concurrency Stress Testing for Kotlin},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FIMHVAGN}},
  note         = {Machine review of arXiv:2501.07472}
}

read the original abstract

We present LitmusKt - the first tool for litmus testing concurrent programs in Kotlin. The tool's novelty also lies in the fact that Kotlin is a multiplatform language, i.e., it compiles into multiple platforms, which means that the concurrency has to be tested on several of them. Our tool allows writing litmus tests in a single custom DSL, and these tests are then run in Kotlin/Native and Kotlin/JVM, two main platforms for concurrent programming in Kotlin. Using LitmusKt, we discovered novel bugs in the Kotlin compiler, which we then fixed and they are no longer present. Moreover, LitmusKt was integrated into the CI pipeline for Kotlin. LitmusKt is available on GitHub: https://github.com/JetBrains-Research/litmuskt. The demo is available on YouTube: https://youtu.be/oWCZp_Huwss.

Figures

Figures reproduced from arXiv: 2501.07472 by the authors.

**Figure 1.** Store Buffering litmus test, a sample program that demonstrates weak behavior. of instructions and out-of-order execution. Due to these processes, concurrent programs can exhibit counterintuitive behaviors that cannot be observed in the case of single-threaded programs. As a classic example, consider the Store Buffering program in Figure 1, where the program first initializes locations 𝑥, 𝑦, 𝑟1, and 𝑟2 to 0 and the… view at source ↗

**Figure 2.** A schematic of the LitmusKt test running process, using Store Buffering as an example. One gray rectangle represents a single test state. We allocate an array of them. Then, test threads sequentially execute their functions on this array of states. The threads also regularly synchronize on barriers. track record of uncovering concurrency bugs in various JVM implementations [15]. Therefore, we decided to support jc… view at source ↗

**Figure 3.** The Unsafe Publication (UPUB) test. Firstly, the Unsafe Publication test (UPUB for short) demonstrates forbidden outcomes. Its schematic description is shown in [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

16 extracted references · 11 canonical work pages

[7]

Denis Lochmelis. 2023. UPUB Fix Merged into Kotlin. https://github. com/JetBrains/kotlin/commit/d2e0361b4e6de7e804c6c079e7195354cd77ced9 (Ac- cessed on 2025-04-10)

work page 2023
[1]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Mod- elling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 1–74. https://doi.org/10.1145/2627752

doi:10.1145/2627752 2014
[2]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In POPL 2011. ACM, 55–66. https://doi.org/10. 1145/1925844.1926394

work page arXiv 2011
[3]

JetBrains. 2024. The Kotlin Programming Language. https://kotlinlang.org/ (Accessed on 2025-04-10)

work page 2024
[4]

JetBrains Research. 2024. LitmusKt README. https://github.com/JetBrains- Research/litmuskt/blob/main/README.md (Accessed on 2025-04-10)

work page 2024
[5]

Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (1979), 690–691. https://doi.org/10.1109/TC.1979.1675439

arXiv 1979
[6]

Shuyang Liu, John Bender, and Jens Palsberg. 2022. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). https://doi.org/10.4230/LIPIcs.ECOOP.2022.6

doi:10.4230/lipics.ecoop.2022.6 2022
[8]

Denis Lochmelis. 2024. LitmusKT Merged into Kotlin CI. https://github.com/ JetBrains/kotlin/commit/c409279a3833105caf9a4c18c479358c14293ad7 (Accessed on 2025-04-10)

work page 2024

Show all 16 references

[9]

Jeremy Manson, William Pugh, and Sarita V. Adve. 2005. The Java Memory Model. In POPL 2005. ACM, 378–391. https://doi.org/10.1145/1040305.1040336

2005
[10]

Evgenii Moiseenko. 2024. YouTrack Issue about @Contended Annota- tion. https://youtrack.jetbrains.com/issue/KT-68369/Consider-providing- Contended-annotation (Accessed on 2025-04-10)

2024
[11]

Evgenii Moiseenko, Anton Podkopaev, and Dmitry Koznov. 2021. A Survey of Programming Language Memory Models. Programming and Computer Software 47 (2021), 439–456. https://doi.org/10.1134/S0361768821060050

2021 doi
[12]

Jonas Oberhauser, Lilith Oberhauser, Antonio Paolillo, Diogo Behrens, Ming Fu, and Viktor Vafeiadis. 2021. Verifying and Optimizing the HMCS Lock for Arm Servers. In Networked Systems: 9th International Conference, NETYS 2021, Virtual Event, May 19–21, 2021, Proceedings . Spri...

2021
[13]

OpenJDK. 2024. Java Concurrency Stress Tests. https://openjdk.org/projects/ code-tools/jcstress/ (Accessed on 2025-04-10)

2024
[14]

Sergio Rajsbaum and Michel Raynal. 2018. Mastering Concurrent Comput- ing Through Sequential Thinking: A Half-Century Evolution. arXiv preprint arXiv:1812.06011 (2018). https://doi.org/10.48550/arXiv.1812.06011

2018 doi arXiv
[15]

Aleksey Shipilev. 2024. JCStress Workshop. https://shipilev.net/talks/hydraconf- June2021-jcstress-workshop.pdf (Accessed on 2025-04-10)

2024
[16]

Viktor Vafeiadis, Thibaut Balabonski, Soham Chakraborty, Robin Morisset, and Francesco Zappa Nardelli. 2015. Common Compiler Optimisations Are Invalid in the C11 Memory Model and What We Can Do About It. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Princip...

2015

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.

[1] [7]

Denis Lochmelis. 2023. UPUB Fix Merged into Kotlin. https://github. com/JetBrains/kotlin/commit/d2e0361b4e6de7e804c6c079e7195354cd77ced9 (Ac- cessed on 2025-04-10)

work page 2023

[2] [1]

Jade Alglave, Luc Maranget, and Michael Tautschnig. 2014. Herding Cats: Mod- elling, Simulation, Testing, and Data Mining for Weak Memory. ACM Trans. Program. Lang. Syst. 36, 2 (2014), 1–74. https://doi.org/10.1145/2627752

doi:10.1145/2627752 2014

[3] [2]

Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber. 2011. Mathematizing C++ Concurrency. In POPL 2011. ACM, 55–66. https://doi.org/10. 1145/1925844.1926394

work page arXiv 2011

[4] [3]

JetBrains. 2024. The Kotlin Programming Language. https://kotlinlang.org/ (Accessed on 2025-04-10)

work page 2024

[5] [4]

JetBrains Research. 2024. LitmusKt README. https://github.com/JetBrains- Research/litmuskt/blob/main/README.md (Accessed on 2025-04-10)

work page 2024

[6] [5]

Leslie Lamport. 1979. How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs. IEEE Trans. Computers 28, 9 (1979), 690–691. https://doi.org/10.1109/TC.1979.1675439

arXiv 1979

[7] [6]

Shuyang Liu, John Bender, and Jens Palsberg. 2022. Compiling Volatile Correctly in Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). https://doi.org/10.4230/LIPIcs.ECOOP.2022.6

doi:10.4230/lipics.ecoop.2022.6 2022

[8] [8]

Denis Lochmelis. 2024. LitmusKT Merged into Kotlin CI. https://github.com/ JetBrains/kotlin/commit/c409279a3833105caf9a4c18c479358c14293ad7 (Accessed on 2025-04-10)

work page 2024