Scholarlink

Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C/C++, particularly the code for memory management. As a result, GenMC does not work for C/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.

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

Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2025年

查看全文
  • Shigeyuki Sato,
  • Taiyo Mizuhashi,
  • Genki Kimura,
  • Kenjiro Taura

摘要

Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C/C++, particularly the code for memory management. As a result, GenMC does not work for C/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.