VerifiedFT: A Verified, High-Performance Precise Dynamic Race Detector
Title | VerifiedFT: A Verified, High-Performance Precise Dynamic Race Detector |
Publication Type | Conference Paper |
Year of Publication | 2018 |
Authors | Wilcox, James R., Flanagan, Cormac, Freund, Stephen N. |
Conference Name | Proceedings of the 23rd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming |
Date Published | February 2018 |
Publisher | ACM |
Conference Location | New York, NY, USA |
ISBN Number | 978-1-4503-4982-6 |
Keywords | clean slate, Collaboration, Concurrency, Data Races, dynamic analysis, Human Behavior, human factors, Metrics, policy, Policy Based Governance, policy governance, pubcrawl, resilience, Resiliency |
Abstract | Dynamic data race detectors are valuable tools for testing and validating concurrent software, but to achieve good performance they are typically implemented using sophisticated concurrent algorithms. Thus, they are ironically prone to the exact same kind of concurrency bugs they are designed to detect. To address these problems, we have developed VerifiedFT, a clean slate redesign of the FastTrack race detector [19]. The VerifiedFT analysis provides the same precision guarantee as FastTrack, but is simpler to implement correctly and efficiently, enabling us to mechanically verify an implementation of its core algorithm using CIVL [27]. Moreover, VerifiedFT provides these correctness guarantees without sacrificing any performance over current state-of-the-art (but complex and unverified) FastTrack implementations for Java. |
URL | https://dl.acm.org/doi/10.1145/3200691.3178514 |
DOI | 10.1145/3178487.3178514 |
Citation Key | wilcox_verifiedft:_2018 |