As concurrent programming becomes more widespread, identifying issues like data races and deadlocks is increasingly vital. This study evaluates the ability of several leading large language models (LLMs), including GPT variants, o1 models, Mistral-AI’s Large2, and DeepSeek-r1-70B, to analyze concurrency issues in software. Recognizing that modern architectures such as ARM and x86 support relaxed memory models such as Total Store Order (TSO) and Partial Store Order (PSO), we assess the models under both sequential consistency and relaxed memory semantics. Using SV-COMP’s \textit{pthread} benchmarks and 25 ARM Litmus tests, we examine each model’s ability to detect concurrency bugs and verify correctness conditions.

Our results show that GPT-5 performs best in sequential consistency, effectively detecting concurrency bugs, followed by o1. However, all evaluated models struggle with relaxed memory models (RMMs), failing to reliably capture memory reordering behaviors. While the recent OpenAI’s o1 outperforms others in identifying program behavior under RMMs, it still falls short of achieving 100% accuracy in our experiments. These findings highlight the significant limitations of current LLMs in verifying concurrent programs under relaxed memory, underscoring the need for further research in this area.