{"id":"8346fc11-0589-4e0f-be07-42c0868b3e10","arxiv_id":"2501.07472","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A new litmus testing tool for Kotlin runs concurrency stress tests on JVM and Native and found unsafe publication bugs in Kotlin/Native.","lead":"LitmusKt is a new testing tool that runs small concurrent programs, called litmus tests, against Kotlin code compiled for JVM and Native. It found previously unknown unsafe-publication bugs in the Kotlin/Native compiler, which were fixed and later integrated into Kotlin's CI pipeline.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The UPUB garbage-value evidence strongly indicates a compiler bug, but the lack of a standalone reproducer leaves an unresolved risk that LitmusKt's state-reuse harness contributed to the FORBIDDEN outcomes.","rationale":"The paper's central claim is well supported by the fix commit and CI integration, and the garbage values (e.g., 71817408) are far outside any interleaving of the source-level writes, so the absence of a formal Kotlin memory model is not the main vulnerability. The weakest spot is the lack of a standalone reproducer that isolates the compiler from the LitmusKt runner. The runner's reuse of state objects and barrier synchronization is a plausible source of artifact if any index or timing bug exists, and the paper does not provide the test source or raw logs needed to rule this out. The external fix mitigates this risk substantially, but because the same group authored both the tool and the fix, independent verification remains valuable. The reader's conditional verdict is therefore appropriate; a full acceptance would be premature until the standalone reproducer confirms that the forbidden outcomes are independent of the harness.","tokens_in":7550,"tokens_out":9800,"duration_ms":100176,"concrete_test":"Run the released LitmusKt UPUB test on Kotlin/Native 1.9.0 on Apple M1 for at least 40.8 million iterations and record the exact FORBIDDEN values; then write a standalone Kotlin/Native program (without LitmusKt) that allocates an IntHolder and publishes it through a plain var h, while a second thread reads h?.x, using the same allocation pattern and no barriers, and check whether the same garbage integers appear. If the standalone program reproduces the FORBIDDEN values on 1.9.0 but not on 1.9.20, the harness-artifact concern is refuted.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim depends on the FORBIDDEN UPUB outcomes being attributable to Kotlin/Native code generation rather than to the LitmusKt runner. Section 2.2 describes a runner that allocates a large array of state objects and has threads iterate over them while periodically synchronizing on barriers. Because the state objects are reused across iterations, a reading thread could in principle observe a field value written by a previous iteration or a partially initialized newly allocated object that is not the object actually published in the current iteration. The paper reports only aggregate outcome counts (Table 3) and does not provide the UPUB test source, raw logs, a standalone minimal program, or a before/after comparison on the fixed compiler. If the harness's index/barrier logic, rather than Kotlin/Native's failure to zero-initialize object fields, produced the garbage, then the bug report and the d2e0361b fix would not support the claimed compiler defect. The external fix commit and CI integration are strong corroboration, but they do not by themselves rule out a harness-specific interaction, because the corroboration comes from within the same project group. This is a reproducibility/artifact gap, not a formal-model objection: even without a Kotlin memory model, the appearance of values never written to x would still indicate a memory-safety violation.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":7739,"tokens_out":7935,"duration_ms":77706,"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":[{"comment":"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":"Section 3, Table 3"},{"comment":"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.","section":"Section 2.2, Section 3"}],"minor_comments":[{"comment":"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.","section":"Section 2.2, Figure 2"},{"comment":"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":"Table 2"},{"comment":"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.","section":"Section 3"},{"comment":"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.","section":"Listing 1, Table 1"},{"comment":"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.","section":"References [7], [8]"}],"recommendation":"major_revision","confidential_remarks":"The tool is timely and the reported bug appears to be real, but because the corroborating fix and CI commit are authored within the same research group, the artifact gap matters more than it would for an independent reproduction. If the authors supply the UPUB source, raw logs, and a minimal reproducer with before/after behavior, I would view the paper as acceptable for a Companion venue. If a standalone reproducer cannot be supplied, the central bug-discovery claim should be weakened to 'LitmusKt reported suspicious outcomes that were subsequently acknowledged and fixed.'"},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","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.\n\nWhat'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.\n\nWhere 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.\n\nThe 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.\n\nBottom 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.","headline":"A solid tools paper that found and fixed real Kotlin/Native bugs; the formal-model gap is real but secondary.","tokens_in":8297,"tokens_out":1801,"would_cite":true,"duration_ms":17517,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["Kotlin","litmus testing","stress testing","concurrency","compiler design","memory model","unsafe publication","Kotlin/Native"],"falsifier":"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.","tokens_in":7320,"feed_emoji":"🧪","tokens_out":8494,"duration_ms":76708,"temperature":0.7,"pith_summary":"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.","feed_headline":"LitmusKt catches real Kotlin/Native concurrency bugs","feed_subtitle":"A single Kotlin DSL stress-tests two platforms and found unsafe object publication; the fix is now in Kotlin's CI.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Defines the litmus-test methodology and the stress techniques (barriers, repetition) that LitmusKt adapts for Kotlin.","marker":"[1]"},{"why":"The merged fix commit that removes the unsafe-publication bug reported in Section 3.","marker":"[7]"},{"why":"The merge that adds LitmusKt to the Kotlin continuous-integration pipeline.","marker":"[8]"},{"why":"The survey that supplies the standard litmus tests used in the evaluation table.","marker":"[11]"},{"why":"The Java stress-testing tool used as the execution backend for the Kotlin/JVM runner.","marker":"[13]"}],"fun_headline_variants":["First litmus tester for Kotlin uncovers compiler bugs","LitmusKt exposes Kotlin/Native memory-safety flaws","Kotlin compiler bugs found by single-DSL litmus testing","LitmusKt catches real Kotlin concurrency bugs in CI","Unsafe publication bugs in Kotlin/Native found by LitmusKt"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["First litmus tester for Kotlin uncovers compiler bugs","LitmusKt exposes Kotlin/Native memory-safety flaws","Kotlin compiler bugs found by single-DSL litmus testing","LitmusKt catches real Kotlin concurrency bugs in CI","Unsafe publication bugs in Kotlin/Native found by LitmusKt"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000646,"raw_usage":{"total_tokens":2926,"prompt_tokens":862,"completion_tokens":2064,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":478,"completion_tokens_details":{"reasoning_tokens":1973}},"tokens_in":478,"tokens_out":2064,"duration_ms":14291,"temperature":1.0,"reasoning_tokens":1973,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T20:40:11.803165+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The merged fix commit that removes the unsafe-publication bug reported in Section 3."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The merge that adds LitmusKt to the Kotlin continuous-integration pipeline."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The survey that supplies the standard litmus tests used in the evaluation table."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The Java stress-testing tool used as the execution backend for the Kotlin/JVM runner."}],"review_version":1}