Concurrent incorrectness separation logic
File(s)3498695.pdf (864.05 KB)
Published version
OA Location
Author(s)
Raad, Azalea
Berdine, Josh
Dreyer, Derek
O'Hearn, Peter W
Type
Journal Article
Abstract
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.
Date Issued
2022-01-16
Date Acceptance
2022-01-01
Citation
Proceedings of the ACM on Programming Languages, 2022, 6 (POPL), pp.1-29
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
29
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
6
Issue
POPL
Copyright Statement
© 2022 Copyright held by the owner/author(s).
License URL
Sponsor
UK Research and Innovation
Identifier
https://dl.acm.org/doi/10.1145/3498695
Grant Number
MR/V024299/1
Publication Status
Published
Date Publish Online
2022-01-16