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

TL;DR

This paper evaluates large language models' ability to understand and verify concurrency issues in programs across different memory models, highlighting their strengths and limitations in handling complex relaxed memory scenarios.

Contribution

It provides a comprehensive assessment of leading LLMs' performance in analyzing concurrent programs under various memory models, including relaxed ones, which is a novel focus.

Findings

GPT-4 and similar models effectively identify concurrency issues under sequential consistency.

All models struggle to verify correctness under relaxed memory models.

Models show limitations in understanding memory ordering constraints in complex scenarios.

Abstract

As concurrent programming becomes increasingly prevalent, effectively identifying and addressing concurrency issues such as data races and deadlocks is critical. This study evaluates the performance of several leading large language models (LLMs), including GPT-3.5-turbo, GPT-4, GPT-4o, GPT-4o-mini, and Mistral-AI's Large2, in understanding and analyzing concurrency issues within software programs. Given that relaxed memory models, such as Total Store Order (TSO) and Partial Store Order (PSO), are widely implemented and adapted in modern systems, supported even by commodity architectures like ARM and x86, our evaluation focuses not only on sequentially consistent memory models but also on these relaxed memory models. Specifically, we assess two main aspects: the models' capacity to detect concurrency problems under a sequentially consistent memory model and their ability to verify the correctness conditions of concurrent programs across both sequentially consistent and relaxed memory models. 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. The experimental results reveal that GPT-4, GPT-4o, and Mistral-AI's Large2 demonstrate a robust understanding of concurrency issues, effectively identifying data races and deadlocks when assessed under a sequentially consistent memory model. However, despite its superior performance, all selected LLMs face significant challenges verifying program correctness under relaxed memory models. These LLMs exhibit limitations in accurately capturing memory ordering constraints, and their current capabilities fall short in verifying even small programs in these complex scenarios.