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 条

[41] Weak Memory Models as LLVM-to-LLVM Transformations
Still, Vladimir
Rockai, Petr
Barnat, Jiri
MATHEMATICAL AND ENGINEERING METHODS IN COMPUTER SCIENCE, MEMICS 2015, 2016, 9548 : 144 - 155
[42] The SPINJA Model Checker
de Jonge, Marc
Ruys, Theo C.
MODEL CHECKING SOFTWARE, 2010, 6349 : 124 - 128
[43] Weak solvability of irregularized model of viscoelastisity with memory
Zvyagin, Victor
Orlov, Vladimir
INTERNATIONAL CONFERENCE ON ANALYSIS AND APPLIED MATHEMATICS (ICAAM 2016), 2016, 1759
[44] A Statistical Model Checker for Situation Calculus Based Multi-Agent Models
Kroiss, Christian
AAMAS'14: PROCEEDINGS OF THE 2014 INTERNATIONAL CONFERENCE ON AUTONOMOUS AGENTS & MULTIAGENT SYSTEMS, 2014, : 1567 - 1568
[45] Formal verification of a pipelined processor with new memory hierarchy using a commercial model checker
Nakamura, H
Arai, T
Fujita, M
2002 PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING, PROCEEDINGS, 2002, : 321 - 324
[46] Portability Analysis for Weak Memory Models PORTHOS: One Tool for all Models
Ponce-de-Leon, Hernan
Furbach, Florian
Heljanko, Keijo
Meyer, Roland
STATIC ANALYSIS (SAS 2017), 2017, 10422 : 299 - 320
[47] Prescient Memory: Exposing Weak Memory Model Behavior by Looking into the Future
Cao, Man
Roemer, Jake
Sengupta, Aritra
Bond, Michael D.
ACM SIGPLAN NOTICES, 2016, 51 (11) : 99 - 110
[48] Scheduling Constraint Based Abstraction Refinement for Weak Memory Models
Yin, Liangze
Dong, Wei
Liu, Wanwei
Wang, Ji
PROCEEDINGS OF THE 2018 33RD IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMTED SOFTWARE ENGINEERING (ASE' 18), 2018, : 645 - 655
[49] Formally verifying the distributed shared memory weak consistency models
Chennareddy, Venkateswarlu
Deka, Jatindra Kumar
2006 INTERNATIONAL CONFERENCE ON ADVANCED COMPUTING AND COMMUNICATIONS, VOLS 1 AND 2, 2007, : 443 - +
[50] Reasoning About Promises in Weak Memory Models with Event Structures
Wehrheim, Heike
Bargmann, Lara
Dongol, Brijesh
FORMAL METHODS, FM 2023, 2023, 14000 : 282 - 300

← 1 2 3 4 5 →