Scholarlink

Abstract <p>Optimization transformations performed by a compiler may violate memory consistency requirements for a multithreaded program. This leads to errors, when the program behavior will differ from expected. The memory consistency requirements for a particular programming language are called the memory model. An example of an error of this class may be an incorrect change in the order of execution of instructions, which does not affect the behavior of a single-threaded program, but leads to unpredictable results in the multithreaded case. Such errors are often difficult to detect, as they occur rarely and depend significantly on the hardware and the state of the computer system.</p> <p>Although there are formal methods for verifying the consistency of shared memory usage, their scalability for industrial software remains a major challenge. To verify multithreaded programs, the MCC tool was previously proposed, which used a simple type of static analysis. In this article, we present a modification of the MCC tool, which implements a model verification method to verify the correctness of memory access consistency.</p> <p>The proposed method combines the methods of generating test programs and the method of static program analysis. The OTK tool is used to generate test programs. For static analysis, a modified version of the MCC tool is used, which checks all possible execution options for the generated test program, regardless of the specifics of a particular hardware. The tool was tested on an ARK industrial virtual machine and successfully identified two real errors in compiler optimizations.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Software Model Checking for Memory Consistency Verification

  • 期刊论文

  • 发表日期：

    2025年9月22日

查看全文
  • P. S. Andrianov,
  • S. V. Zelenov,
  • V. S. Mutilin,
  • A. K. Petrenko

摘要

Abstract

Optimization transformations performed by a compiler may violate memory consistency requirements for a multithreaded program. This leads to errors, when the program behavior will differ from expected. The memory consistency requirements for a particular programming language are called the memory model. An example of an error of this class may be an incorrect change in the order of execution of instructions, which does not affect the behavior of a single-threaded program, but leads to unpredictable results in the multithreaded case. Such errors are often difficult to detect, as they occur rarely and depend significantly on the hardware and the state of the computer system.

Although there are formal methods for verifying the consistency of shared memory usage, their scalability for industrial software remains a major challenge. To verify multithreaded programs, the MCC tool was previously proposed, which used a simple type of static analysis. In this article, we present a modification of the MCC tool, which implements a model verification method to verify the correctness of memory access consistency.

The proposed method combines the methods of generating test programs and the method of static program analysis. The OTK tool is used to generate test programs. For static analysis, a modified version of the MCC tool is used, which checks all possible execution options for the generated test program, regardless of the specifics of a particular hardware. The tool was tested on an ARK industrial virtual machine and successfully identified two real errors in compiler optimizations.