GENMC: A Model Checker for Weak Memory Models

被引：30

作者：

Kokologiannakis, Michalis ^{[1
]}

Vafeiadis, Viktor ^{[1
]}

机构：

[1] MPI SWS, Kaiserslautern, Germany

来源：

COMPUTER AIDED VERIFICATION (CAV 2021), PT I | 2021年 / 12759卷

基金：

欧洲研究理事会;

关键词：

CONSISTENCY; SYMMETRY;

D O I：

10.1007/978-3-030-81685-8_20

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

GENMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models. In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.

引用

页码：427 / 440

页数：14

共 50 条

[1] A memory model sensitive checker for C#
Huynh, Thuan Quang
Roychoudhury, Abhik
FM 2006: FORMAL METHODS, PROCEEDINGS, 2006, 4085 : 476 - 491
[2] PARAM: A Model Checker for Parametric Markov Models
Hahn, Ernst Moritz
Hermanns, Holger
Wachter, Bjoern
Zhang, Lijun
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 660 - +
[3] Benchmarking Weak Memory Models
Ritson, Carl G.
Owens, Scott
ACM SIGPLAN NOTICES, 2016, 51 (08) : 289 - 299
[4] Fences in Weak Memory Models
Alglave, Jade
Maranget, Luc
Sarkar, Susmit
Sewell, Peter
COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 258 - +
[5] Implementing and Evaluating a Model Checker for Transactional Memory Systems
Baek, Woongki
Bronson, Nathan
Kozyrakis, Christos
Olukotun, Kunle
2010 15TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS 2010), 2010, : 117 - 126
[6] Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)
Ponce-de-Leon, Hernan
Furbach, Florian
Heljanko, Keijo
Meyer, Roland
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 378 - 382
[7] On the Verification Problem for Weak Memory Models
Atig, Mohamed Faouzi
Bouajjani, Ahmed
Burckhardt, Sebastian
Musuvathi, Madanlal
ACM SIGPLAN NOTICES, 2010, 45 (01) : 7 - 18
[8] Linearizability on hardware weak memory models
Smith, Graeme
Winter, Kirsten
Colvin, Robert J.
FORMAL ASPECTS OF COMPUTING, 2020, 32 (01) : 1 - 32
[9] A formal hierarchy of weak memory models
Alglave, Jade
FORMAL METHODS IN SYSTEM DESIGN, 2012, 41 (02) : 178 - 210
[10] A formal hierarchy of weak memory models
Jade Alglave
Formal Methods in System Design, 2012, 41 : 178 - 210

← 1 2 3 4 5 →