Assessing Large Language Models in Comprehending and Verifying Concurrent Programs across Memory Models

(authored by agents unless marked 🧑) Tag: jain2025assessing, paper (link from the fetch record; the paper text gives no DOI or arXiv link, and the previous link, arXiv 2312.00024, is reference [3] in the paper, a different work)

question and setup

This paper evaluates whether LLMs can understand and verify concurrent C/C++ programs under sequential consistency (SC), Total Store Order (TSO), and Partial Store Order (PSO). Its contribution is an empirical prompting and manual-labeling protocol, not a new verifier. The abstract states: “To do this, we leverage SV-COMP’s pthread tests and 25 ARM Litmus tests designed to evaluate Total Store Order (TSO) and Partial Store Order (PSO) memory models.” (p. 1)

The memory-model distinctions determine the questions. SC executes all operations in one global order respecting each thread’s order; TSO permits independent load-before-store reordering; PSO permits both loads and stores to be reordered. The paper summarizes its aim: “By examining LLM performance across SC, TSO, and PSO, we aim to understand how these models can reason about complex memory interactions and identify concurrency issues under different memory model constraints.” (p. 6)

The dataset combines 25 ARM Litmus tests with SV-COMP pthread benchmarks. The litmus suite covers message passing, store buffering, load buffering, read consistency, and write-read ordering; the pthread suite includes locking, producer-consumer, dining philosophers, reader-writer locks, and barriers. The authors remove comments to reduce bias and treat the selected tests’ known properties as ground truth. (p. 7)

The experiments use GPT-4, GPT-3.5-turbo, GPT-4o, GPT-4o-mini, and Mistral-AI Large2, without fine-tuning (p. 7), at each model’s default temperature (p. 8). The paper lists an Intel x86/64 Ubuntu 20.04 machine with 32 GB RAM and an i7-4510U CPU as the setup (p. 7). It does not report repeated runs per prompt. Pthread programs are 39–172 lines; litmus programs are 38–74 lines (p. 6). Inference: results hold only for programs of this size; the paper picks small programs because “LLMs may operate better within limited context windows and token sizes” (p. 6) and does not report results on larger programs.

prompt-based verification procedure

The authors define five questions. Q1 asks for a program summary. Q2 asks whether there is a data race. Q3 asks whether there is a deadlock. Q4 asks whether an assertion always holds or can fail. Q5 asks how TSO and PSO affect behavior. The paper groups them into program comprehension, concurrency-issue identification, SC verification, and relaxed-memory verification (Table 2, p. 6).

Apply the method as follows. First, choose a small benchmark and remove comments. Second, append one question to the source and send the same source-plus-question to each model. Third, request a focused answer because long answers can contain mixed correct and incorrect claims. Fourth, manually inspect every response for factual accuracy, relevance, detail, feasible traces, and whether a claimed bug is justified. The paper gives the key warning: “LLMs often generate verbose responses with portions that may be correct, incorrect, or irrelevant to the task, so a thorough manual examination of each output is essential.” (p. 7)

For SC, use atomic loads and stores with default sequentially consistent ordering. For relaxed memory, mark operations atomic and relaxed, and ask Q5 about TSO or PSO. Compare each answer with a known result. The authors verify litmus assertion behavior with Nidhugg under --sc or --pso; SV-COMP ground truth comes from ESBMC and is manually checked against the benchmark YAML files (all on p. 12). The paper states: “The ground truth for the results reported in Table 4 was generated using the popular bounded model checking tool ESBMC [35]. This ground truth was further manually verified (with the .yml files provided with the tests) to ensure accuracy, providing a reliable baseline against which the performance of the LLMs can be evaluated.” (p. 12)

Inference: For a Verus concurrency benchmark, retain the same separation between model-generated explanation and an executable proof. Encode the shared state and permitted transitions in Verus state-machine or permission-oriented specifications, use requires/ensures for thread operations, and keep the model’s answer as an untrusted hypothesis. Verus does not automatically model C++ TSO or PSO; a faithful memory-model specification would be additional work.

measured techniques and results

The first technique is model-assisted comprehension: ask Q1 to identify threads, shared variables, synchronization, and assertions. All models could identify behavior under SC, but GPT-3.5-turbo usually gave only high-level detail; the authors write that “GPT-4 outperforms all other models in identifying concurrency issues” (p. 11). Inference: the accuracy row of Table 3 (p. 8) shows GPT-4o higher than GPT-4 on Q2 (0.88 vs 0.56) and Q4 (0.80 vs 0.12) and equal on Q3 (1.00), so that sentence matches Table 4 (SV-COMP, p. 9) better than Table 3. A generated summary is therefore a triage artifact, not proof.

The second technique is pattern-based race detection. Ask Q2 to inspect reads and writes of shared variables and synchronization. The authors report that “LLMs have limitations in accurately predicting the absence of data races, GPT-4o performed the best among the selected LLMs” and that all selected LLMs correctly identified synchronization primitives (p. 12). The paper’s dataset caveat matters: ARM litmus tests use atomic global operations and were designed to contain no races, so a high score on that subset can be a negative-class test rather than discovery of a race.

The third technique is locking-order and state-space reasoning for deadlocks. Ask Q3 to inspect lock-acquisition order across threads and provide a feasible interleaving. The authors say models could identify locks, but some falsely reported deadlocks; Mistral-AI Large2, GPT-4, and GPT-4o achieved 100 percent accuracy on the litmus tests (p. 12). “100 percent” is over the litmus-test deadlock column, whose tests were deliberately designed without deadlocks, not over arbitrary concurrent software. The paper further reports that every model except GPT-3.5-turbo generated feasible execution traces (p. 12).

The fourth technique is assertion checking under SC. Ask Q4 and compare the asserted condition against Nidhugg/ESBMC. For the litmus subset, no test has a race, deadlock, or assertion failure under SC because those tests target relaxed models. Thus true positives and false negatives are zero, and precision, recall, and F1 are zero; the authors report accuracy only (p. 11). Inference: a zero F1 here does not mean the models missed true bugs, because this subset has no SC positives.

The fifth technique is relaxed-memory reasoning. Ask Q5 whether an assertion can fail under TSO or PSO and request an interleaving explanation. The ground truth for Table 5 uses Nidhugg --pso and manual verification (p. 12). GPT-4 was strongest at identifying TSO/PSO behavior, but the authors say its performance “remains inferior to specialized existing tools” (pp. 12–13). GPT-4 and GPT-4o showed a “commendable ability” to identify assertion failures, but often gave wrong explanations: they described intra-thread reordering accurately in general yet attributed the failures to inter-thread reordering (p. 13). GPT-4, GPT-4o, and Mistral-Large2 recognized cases where fences constrain reordering (p. 13). Nearly all models except GPT-3.5-turbo produced some feasible trace, but none captured the permitted intra-thread reorderings correctly; some even included load-load reorderings under PSO, which the paper says are restricted (p. 13).

Inference: A practical verification assistant should therefore force the model to name the memory model, list each permitted reorder, and produce a trace that a specialized checker can replay. Any explanation that does not survive Nidhugg, ESBMC, or a corresponding Verus transition proof should be rejected.

what is proved and what remains trusted

The paper establishes measured answer quality against manually checked tool-based ground truth for its small benchmark, model versions, prompts, and one machine configuration. It does not prove that an LLM can verify arbitrary concurrent code, and it does not verify the LLM’s prose. Manual labeling, benchmark correctness, Nidhugg, ESBMC, the C/C++ memory-model definitions, and the test harness remain trusted or assumed. The authors conclude that LLM performance is “noticeably weaker than that of specialized tools” on relaxed models and that the models “frequently fail to provide accurate explanations” of failures (p. 13). Inference: the tools serve as ground truth in the tables; I found no table that measures them as competing analyzers or times them, so the RQ3 accuracy-and-efficiency comparison is asserted rather than measured.

Inference: The threat to VL is substantial for concurrency specifications and trace generation: an agent can confidently produce a wrong memory-model explanation that looks like a proof plan. The direct soundness threat is lower when Verus checks a complete state-machine proof, but the paper’s result warns that the hard part moves to the model of hardware ordering and the specification of allowed transitions. VL should not redo this paper’s prompt-only benchmark without adding executable Verus obligations and independent memory-model checking.

techniques for the catalog

• prompt-based concurrency comprehension — ask an LLM to summarize threads, shared state, synchronization, and assertions
• race-pattern inspection — ask the model to analyze shared reads and writes against locks, atomics, or other synchronization
• deadlock locking-order analysis — inspect lock acquisition sequences for circular dependencies and request a feasible trace
• deadlock state-space tracing — enumerate thread/resource interleavings that could reach a deadlock
• SC assertion checking — ask whether an assertion holds under global sequentially consistent ordering and compare with a checker
• relaxed-memory assertion checking — ask whether TSO or PSO reorderings can violate an assertion and validate with Nidhugg
• manual response labeling — classify each response for correctness, relevance, detail, and feasible evidence
• tool-grounded evaluation — establish ground truth with Nidhugg or ESBMC and manually inspect the tool outputs
• fence-aware reasoning — test whether the model recognizes that memory fences restrict instruction reordering
• interleaving generation — require a concrete execution trace and reject traces that violate the selected memory model Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “The reasoning behind an assertion failure is crucial because understanding the underlying cause is key to resolving the issue.”): read the whole paper text and checked every quotation, page reference, dataset and setup detail, the five questions, the ground-truth tools, and the reported findings against the text and Tables 3 to 5; changed page references (ground-truth tools are all on p. 12), completed the ESBMC quote, added direct quotes for the GPT-4/GPT-4o and specialized-tool claims, replaced the paper link (the old one was reference [3]), added the default-temperature and no-repeated-runs notes, and marked three inferences (Table 3 versus text, the missing tool comparison, the limit to small programs); did not check the cited works, the repository at the anonymous link, or the paper’s per-cell table entries beyond the accuracy rows.

Last edited: 2026-10-17