Concurrent Incorrectness Separation Logic

被引：11

作者：

Raad, Azalea ^{[1
,2
]}

Berdine, Josh ^{[2
]}

Dreyer, Derek ^{[3
]}

O'Hearn, Peter W. ^{[2
,4
]}

机构：

[1] Imperial Coll London, London, England

[2] Meta, London, England

[3] MPI SWS, Saarbrucken, Germany

[4] UCL, London, England

来源：

PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2022年 / 6卷

基金：

欧洲研究理事会;

关键词：

Concurrency; program logics; separation logic; bug catching;

D O I：

10.1145/3498695

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Incorrectness separation logic (ISL) was recently introduced as a theory of under-approximate reasoning, with the goal of proving that compositional bug catchers find actual bugs. However, ISL only considers sequential programs. Here, we develop concurrent incorrectness separation logic (CISL), which extends ISL to account for bug catching in concurrent programs. Inspired by the work on Views, we design CISL as a parametric framework, which can be instantiated for a number of bug catching scenarios, including race detection, deadlock detection, and memory safety error detection. For each instance, the CISL meta-theory ensures the soundness of incorrectness reasoning for free, thereby guaranteeing that the bugs detected are true positives.

引用

页数：29

共 50 条

[1] Concurrent incorrectness separation logic
Raad, Azalea
Berdine, Josh
Dreyer, Derek
O'Hearn, Peter W.
Proceedings of the ACM on Programming Languages, 2022, 6 (POPL)
[2] Relative Completeness of Incorrectness Separation Logic
Lee, Yeonseok
Nakazawa, Koji
PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2024, 2025, 15194 : 264 - 282
[3] Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic
Raad, Azalea
Berdine, Josh
Dang, Hoang-Hai
Dreyer, Derek
O'Hearn, Peter
Villard, Jules
COMPUTER AIDED VERIFICATION, PT II, 2020, 12225 : 225 - 252
[4] Incorrectness Logic
O'Hearn, Peter W.
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2020, 4 (POPL):
[5] LOGIC AND SORTAL INCORRECTNESS
BERGMANN, M
REVIEW OF METAPHYSICS, 1977, 31 (01): : 61 - 79
[6] INDEPENDENCE AND CONCURRENT SEPARATION LOGIC
Hayman, Jonathan
Winskel, Glynn
LOGICAL METHODS IN COMPUTER SCIENCE, 2008, 4 (01)
[7] Granularity and Concurrent Separation Logic
Hayman, Jonathan
CONCUR 2011: CONCURRENCY THEORY, 2011, 6901 : 219 - 234
[8] A semantics for concurrent separation logic
Brookes, S
CONCUR 2004 - CONCURRENCY THEORY, PROCEEDINGS, 2004, 3170 : 16 - 34
[9] A semantics for concurrent separation logic
Brookes, Stephen
THEORETICAL COMPUTER SCIENCE, 2007, 375 (1-3) : 227 - 270
[10] Revisiting concurrent separation logic
Soares, Pedro
Ravara, Antonio
de Sousa, Simao Melo
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2017, 89 : 41 - 66

← 1 2 3 4 5 →