# ConcurrencyPaper **Repository Path**: lapulatos/ConcurrencyPaper ## Basic Information - **Project Name**: ConcurrencyPaper - **Description**: No description available - **Primary Language**: Unknown - **License**: Not specified - **Default Branch**: master - **Homepage**: None - **GVP Project**: No ## Statistics - **Stars**: 1 - **Forks**: 0 - **Created**: 2025-08-14 - **Last Updated**: 2025-11-20 ## Categories & Tags **Categories**: Uncategorized **Tags**: None ## README # Papers ------------------- - Mark Meaning - **A**: Theoretical foundations or core technologies, recommended to read them first; - **B**: Derived theories or extended techniques, recommended to understand the theoretical foundation before reading; - **C**: Peripheral supporting techniques or tools, etc., just read briefly. - **1 -> 3**: Reading difficulty (the larger the number, the harder it is to read or understand). ------------------- - 01 **Survey/Review** - A1 [Verifying Concurrent Programs (Tutorial) (Slides)](https://www.cs.utexas.edu/~hunt/fmcad/fmcad11/slides/tutorial-e.pdf) - [When Memory Corruption Met Concurrency: Vulnerabilities in Concurrent Programs (Access 2023)](https://ieeexplore.ieee.org/document/10114930) - [Understanding Concurrency Vulnerabilities in Linux Lernel (2022)](https://arxiv.org/abs/2212.05438) - [Understanding Real-World Concurrency Bugs in Go (ASPLOS 2019)](https://songlh.github.io/paper/go-study.pdf) - [A systematic survey on automated concurrency bug detection, exposing, avoidance, and fixing techniques (SQJ 2018)](https://dl.acm.org/doi/10.1007/s11219-017-9385-3) - [Surveying concurrency bug detectors based on types of detected bugs (2017)](http://scis.scichina.com/en/2017/031101.pdf) - [A survey of race bug detection techniques for multithreaded programmes (2014)](https://onlinelibrary.wiley.com/doi/abs/10.1002/stvr.1564) - [Learning from Mistates: A Comprehensive Study on Real World Concurrency Bug Characteristics (ASPLOS 2008)](https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/concurrency-bugs.pdf) - [Understanding, Detecting and Exposing Concurrency Bugs (2003)](https://core.ac.uk/download/pdf/4820747.pdf) - [Notes on concurrency bugs](https://danluu.com/concurrency-bugs/) - [Slides: Dynamic Data Race Prediction](http://www.google.com/url?q=http%3A%2F%2Fumathur3.web.engr.illinois.edu%2Frace-prediction-tutorial.pdf&sa=D&sntz=1&usg=AOvVaw3nx81XoaU9iI1acBc876rk) - [Slides: CS636: Testing Concurrent Programs - CSE-IITK - IIT Kanpur](https://www.cse.iitk.ac.in/users/swarnendu/courses/spring2019-cs636/Testing%20Concurrent%20Programs.pdf) - 02 **Thesis** - [Finding and Tolerating Concurrency Bugs (by Jie Yu)](https://deepblue.lib.umich.edu/bitstream/handle/2027.42/99765/jieyu_1.pdf) - [A Pragmatic Verification Approach for Concurrent Programs (by Truc Lam Nguyen)](https://eprints.soton.ac.uk/413593/1/thesis.pdf) - [Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs (2017)](https://www.academia.edu/download/42896968/MultiRace_efficient_on-the-fly_data_race20160221-25597-1qyz9lv.pdf) - 03 **Maximal Causality Reduction** - [Speeding Up Maximal Causality Reduction with Static Dependency Analysis (ECOOP 2017)](https://huangshiyou.github.io/files/Huang-ECOOP-2017-16.pdf) - [Maximal Causality Reduction for TSO and PSO (OOPSLA 2016)](https://huangshiyou.github.io/files/mcr_relax-huang.pdf) - [Stateless Model Checking Concurrent Programs with Maximal Causality Reduction (PLDI 2015)](https://dl.acm.org/doi/pdf/10.1145/2813885.2737975) - [Maximal Sound Predictive Race Detection with Control Flow Abstraction (PLDI 2014)](http://fsl.cs.illinois.edu/FSL/papers/2014/huang-meredith-rosu-2014-pldi/huang-meredith-rosu-2014-pldi-public.pdf) - 04 **Stateless Model Checking** - C1 [GenMC: A Model Checker for Weak Memory Models (CAV 2021)](http://plv.mpi-sws.org/genmc/cav21-paper.pdf) -[[Slide]](soundandcomplete.org/papers/PLDI2019/GenMC-Talk.pdf), [[Tool: GenMC]](plv.mpi-sws.org/genmc) - [Parallel graph-based stateless model checking (ATVA 2020)](https://link.springer.com/chapter/10.1007/978-3-030-59152-6_21) - [Effective lock handling in stateless model checking (OOPSLA 2019)](https://dl.acm.org/doi/abs/10.1145/3360599) - [Optimal stateless model checking under the release-acquire semantics (OOPSLA 2018)](https://dl.acm.org/doi/abs/10.1145/3276505) - [Effective Stateless Model Checking for C/C++ Concurrency (POPL 2017)](https://plv.mpi-sws.org/rcmc/paper.pdf) -[[Tool: RCMC]](https://plv.mpi-sws.org/rcmc) - [Stateless Model Checking with Data-Race Preemption Points (OOPSLA 2016)](https://dl.acm.org/doi/abs/10.1145/2983990.2984036) - [Maximally stateless model checking for concurrent bugs under relaxed memory models (ICSE 2016)](https://dl.acm.org/doi/abs/10.1145/2889160.2891042) - [Stateless model checking for TSO and PSO (2016)](https://link.springer.com/article/10.1007/s00236-016-0275-0) -[[Tool: Nidhugg]](https://github.com/nidhugg/nidhugg) - [Stateless model checking for POWER (CAV 2016)](https://link.springer.com/chapter/10.1007/978-3-319-41540-6_8) - [SATCheck: SAT-directed stateless model checking for SC and TSO (2015)](https://dl.acm.org/doi/abs/10.1145/2858965.2814297) - [Fair stateless model checking (PLDI 2008)](https://dl.acm.org/doi/abs/10.1145/1379022.1375625) - [Stateless model checking of event-driven applications (OOPSLA 2015)](https://dl.acm.org/doi/abs/10.1145/2858965.2814282) - [CDSchecker: checking concurrent data structures written with C/C++ atomics (OOPSLA 2013)](http://plrg.eecs.uci.edu/publications/c11modelcheck.pdf) -[[Tool: CDSchecker]](plrg.eecs.uci.edu/software_page/42-2) - [Model Checking for Programming Languages using VeriSoft (POPL 1997)](http://web.eecs.umich.edu/~bchandra/courses/papers/Godefroid_Verisoft.pdf) -[[Slide]](http://pdfs.semanticscholar.org/a7c6/4af76f99dacb2e99a2edb384cb9d5947f583.pdf) - 05 **Partial-Order Reduction** - 01 **Mazurkiewivz Equivalence** - A2 [Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem (PhD Thesis 1996)](https://link.springer.com/content/pdf/10.1007/3-540-60761-7_31.pdf) - A2 [Dynamic Partial-Order Reduction for Model Checking Software (POPL 2005)](https://dl.acm.org/doi/abs/10.1145/1047659.1040315) - B2 [Partial Orders for Efficient Bounded Model Checking of Concurrent Software (CAV 2013)](https://link.springer.com/chapter/10.1007/978-3-642-39799-8_9) - [Dynamic Partial Order Reduction for Relaxed Memory Models (PLDI 2015)](https://dl.acm.org/doi/abs/10.1145/2737924.2737956) - B3 [Optimal Dynamic Partial Order Reduction (POPL 2014)](https://dl.acm.org/doi/abs/10.1145/2578855.2535845) - [Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction (POPL 2017)](https://dl.acm.org/doi/abs/10.1145/3073408) - B2 [Constrained Dynamic Partial Order Reduction (CAV 2018)](https://link.springer.com/chapter/10.1007/978-3-319-96142-2_24) - B1 [Prioritized Constraint-Aided Dynamic Partial-Order Reduction (ASE 2022)](https://dl.acm.org/doi/abs/10.1145/3551349.3561159) -[[Tool: PC-DPOR]](https://figshare.com/ndownloader/files/35039164) - 02 **Reads-From/Observation Equivalence** - A3 [Data-Centric Dynamic Partial Order Reduction (POPL 2017)](https://dl.acm.org/doi/abs/10.1145/3158119) -[[Tool: DC-DPOR]](https://github.com/nidhugg/nidhugg) -[[Slide]](https://cs.au.dk/~pavlogiannis/publications/presentations/popl18a_PR.pdf) - [Optimal Stateless Model Checking for Reads-From Equivalence Under Sequential Consistency (OOPSLA 2019)](https://dl.acm.org/doi/abs/10.1145/3360576) -[[Tool: NIDHUGG/rfsc]](https://zenodo.org/records/3384856) - B2 [Truly Stateless, Optimal Dynamic Partial Order Reduction (POPL 2022)](https://plv.mpi-sws.org/genmc/popl2022-trust-full.pdf) -[[Tool: TruSt]](https://doi.org/10.5281/zenodo.5550765) - B2 [Unblocking Dynamic Partial Order Reduction (CAV 2023)](https://people.mpi-sws.org/~viktor/papers/cav2023-unblocking.pdf) -[[Tool: AWAMOCHE]](https://doi.org/10.5281/zenodo.7868370) - [Optimal Reads-From Consistency Checking for C11-Style Memory Models (PLDI 2023)](https://dl.acm.org/doi/abs/10.1145/3591251) -[[Tool: Minimal Coherence]](https://zenodo.org/records/7816526) - [Data-Centric Dynamic Partial Order Reduction (POPL 2017)](https://dl.acm.org/doi/abs/10.1145/3158119) -[[Tool: DC-DPOR]](https://github.com/nidhugg/nidhugg) - 03 **Value-Centric Equivalence** - [Value-Centric Dynamic Partial Order Reduction (OOPSLA 2019)](https://cs.au.dk/~pavlogiannis/publications/papers/oopsla19.pdf) -[[Slides: VC-DPOR]](https://cs.au.dk/~pavlogiannis/publications/presentations/oopsla19_PR.pdf) -[[Video: VC-DPOR]](https://www.youtube.com/watch?v=-egu9p4SjBM) - 06 **Event Order Graph (SMT-based)** - A1 [On Scheduling Constraint Abstraction for Multi-Threaded Program Verification (TSE 2020)](https://ieeexplore.ieee.org/abstract/document/8428438) -[[Tool: Yogar-CBMC]](https://github.com/yinliangze/yogar-cbmc) - C1 [Parallel Refinement for Multi-Threaded Program Verification (ICSE 2019)](https://ieeexplore.ieee.org/abstract/document/8812136) - B1 [Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification (PLDI 2021)](https://dl.acm.org/doi/abs/10.1145/3453483.3454108) - B1 [Consistency-Preserving Propagation For SMT Solving of Concurrent Program Verification (OOPSLA 2022)](https://dl.acm.org/doi/abs/10.1145/3563321) -[[Tool: Deagle]](https://github.com/thufv/Deagle) - B1 [Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models (TOPLAS 2023)](https://dl.acm.org/doi/full/10.1145/3579835) -[[Tool: ZORD]](https://thufv.github.io/research/zord.html) - 07 **Weak Memory Model** - 01 **Semantics** - A2 [Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory (TOPLAS 2014)](https://dl.acm.org/doi/abs/10.1145/2627752) - C2 [Syntax and Semantics of the Weak Consistency Model Specification Language Cat (aRxiv 2016)](https://arxiv.org/pdf/1608.07531) - A3 [CAAT: Consistency as a Theory (OOPSLA 2022)](https://dl.acm.org/doi/abs/10.1145/3563292) - 02 **Consistency Checking** - B3 [BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings (CAV 2019)](https://link.springer.com/chapter/10.1007/978-3-030-25540-4_19) - [BMC with Memory Models as Modules (FMCAD 2018)](https://ieeexplore.ieee.org/abstract/document/8603021) - [GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency (CAV 2025)](https://cs.au.dk/~pavlogiannis/publications/papers/cav25.pdf) - 08 **Symmetry Reduction** - [Symmetry Reductions in Model Checking (CAV 2025)](https://link.springer.com/chapter/10.1007/bfb0028741) - [From Asymmetry to Full Symmetry - New Techniques for Symmetry Reduction in Model Checking (CHARME 1999)](https://link.springer.com/chapter/10.1007/3-540-48153-2_12) - [Symmetry and Reduced Symmetry in Model Checking (TOPLAS 2004)](https://dl.acm.org/doi/abs/10.1145/1011508.1011511) - [SPORE: Combining Symmetry and Partial Order Reduction (PLDI 2024)](https://plv.mpi-sws.org/genmc/pldi2024-spore-full.pdf) -[[Tool: SPORE]](https://zenodo.org/doi/10.5281/zenodo.10798179) - 09 **Static Analysis** - [HIPPODROME: Data Race Repair using Static Analysis Summaries (TOSEM 2023)](https://abhikrc.com/pdf/TOSEM23.pdf) - [Peahen: Fast and Precise Static Deadlock Detection via Context Reduction (FSE 2022)](https://2022.esec-fse.org/details/fse-2022-research-papers/32/Peahen-Fast-and-Precise-Static-Deadlock-Detection-via-Context-Reduction) - [Automatically Detecting and Fixing Concurrency Bugs in Go Software Systems (ASPLOS 2021)](https://asplos-conference.org/2021/abstracts/asplos21-paper1170-extended_abstract.pdf) - [PASAN: Detecting Peripheral Access Concurrency Bugs within Bare-Metal Embedded Applications (Usenix Sec 2021)](https://www.usenix.org/conference/usenixsecurity21/presentation/kim) - [Thread-Modular Analysis of Release-Acquire Concurrency (SAS 2021)](https://link.springer.com/chapter/10.1007/978-3-030-88806-0_19) - [When Threads Meet Events: Efficient and Precise Static Race Detection with Origins (PLDI 2021)](https://o2lab.github.io/p/o2.pdf) -[[Tool: coderrect]](https://coderrect.com/) - [Canary: Practical Static Detection of Inter-Thread Value-Flow Bugs (PLDI 2021)](https://pldi21.sigplan.org/details/pldi-2021-papers/74/Canary-Practical-Static-Detection-of-Inter-Thread-Value-Flow-Bugs) - [OpenRace: An Open Source Framework for Statically Detecting Data Races (SC 2021)](https://april1989.github.io/files/openrace.pdf) -[[Tool: OpenRace]](https://github.com/coderrect-inc/OpenRace) - [LLOV: A Fast Static Data-Race Checker for OpenMP Programs (TACO 2020)](https://sbjoshi.github.io/publication/llov-taco20/) -[[Slide]](https://llvm.org/devmtg/2020-02-23/slides/Utpal-LLOV.pdf), [[Tool: LLOV]](https://github.com/utpalbora/LLOV) - [Detection of Concurrency Errors in Multithreaded Applications Based on Static Source Code Analysis (Access 2021)](https://ieeexplore.ieee.org/document/9406024) - [OMPRacer: A Scalable and Precise Static RaceDetector for OpenMP Programs (SC 2020)](https://o2lab.github.io/p/ompracer.pdf) -[[Tool: OMPRacer]](https://github.com/parasol-aser/OMPRacer) - [Understanding Memory and Thread Safety Practices and Issues in Real-World Rust Programs (PLDI 2020)](https://pldi20.sigplan.org/details/pldi-2020-papers/76/Understanding-Memory-and-Thread-Safety-Practices-and-Issues-in-Real-World-Rust-Progra) - [SmartTrack: Efficient Predictive Race Detection (PLDI 2020)](https://arxiv.org/pdf/1905.00494.pdf) - [A True Positives Theorem for a Static Race Detector Extended Version (POPL 2019)](https://arxiv.org/pdf/1811.03503.pdf) - [Effective Static Analysis of Concurrency Use-After-Free Bugs in Linux Device Drivers (Usenix Sec 2019)](https://www.usenix.org/system/files/atc19-bai.pdf) - [Towards incremental static race detection in OpenMP programs (Correctness 2018)](https://ieeexplore.ieee.org/abstract/document/8638357/) -[[Slide]](https://correctness-workshop.github.io/2018/papers/swain.pdf) - [RacerD: Compositional Static Race Detection (OOPSLA 2018)](https://ilyasergey.net/papers/racerd-oopsla18-preprint.pdf) - [Using Polyhedral Analysis to Verify OpenMP Applications are Data Race Free (Correctness 2018)](https://www.osti.gov/servlets/purl/1570102) - [Static race detection for device drivers: the Goblint approach (ASE 2016)](https://dl.acm.org/doi/10.1145/2970276.2970337) -[[Tool]](http://goblint.in.tum.de/downloads) - [Polyhedral Optimizations of Explicitly Parallel Programs (PACT 2015)](https://wiki.rice.edu/confluence/download/attachments/4425835/Prasanth-PACT-Camera-ready.pdf) - [Locksmith: Practical Static Race Detection for C. (TOPLAS 2011)](http://www.cs.umd.edu/projects/PL/locksmith/toplas11.pdf) - [RELAY: Static Race Detection on Millions of Lines of Code (FSE 2007)](https://cseweb.ucsd.edu//~jvoung/race/fse2007.pdf) -[[Tool]](https://cseweb.ucsd.edu//~jvoung/race/) - 10 **Dynamic Analysis/Predictive Analysis** - [Tolerate Control-Flow Changes for Sound Data Race Prediction (ICSE 2023)] - [Deadlock Prediction via Generalized Dependency (ISSTA 2022)](https://conf.researchr.org/details/issta-2022/issta-2022-technical-papers/16/Deadlock-Prediction-via-Generalized-Dependency) - [Optimal Prediction of Synchronization-Preserving Races (POPL 2021)](http://umathur3.web.engr.illinois.edu/papers/sync-preserving-race-popl2021.pdf) - [Snowboard: Finding Kernel Concurrency Bugs through Systematic Inter-thread Communication Analysis (SOSP 2021)](https://www.cs.purdue.edu/homes/sishuai/pdf/sosp21-snowboard.pdf) - [Detecting Concurrency Vulnerabilities Based on Partial Orders of Memory and Thread Events (ESEC/FSE 2021)](https://dl.acm.org/doi/abs/10.1145/3468264.3468572) - [Sound and Efficient Concurrency Bug Prediction (ESEC/FSE 2021)](https://dl.acm.org/doi/10.1145/3468264.3468549) - [KARD: Lightweight Data Race Detection with Per-Thread Memory Protection (ASPLOS 2021)](https://asplos-conference.org/abstracts/asplos21-paper442-extended_abstract.pdf) - [ExpRace: Exploiting Kernel Races through Raising Interrupts (Usenix Sec 2021)](https://lifeasageek.github.io/papers/yoochan-exprace.pdf) - [Fast, sound, and effectively complete dynamic race prediction (POPL 2020)](https://dl.acm.org/doi/10.1145/3371085) - [The Complexity of Dynamic Data Race Prediction (LICS 2020)](http://umathur3.web.engr.illinois.edu/papers/race-complexity-lics2020.pdf) - [Atomicity Checking in Linear Time using Vector Clocks (ASPLOS 2020)](https://dl.acm.org/doi/pdf/10.1145/3373376.3378475) - [Dynamic Analysis Method for Concurrency Bugs in Multi-process/Multi-thread Environments (IJPP 2020)](https://www.x-mol.com/paperRedirect/1265038487945584640) - [Low-overhead deadlock prediction (ICSE 2020)](https://dl.acm.org/doi/10.1145/3377811.3380367) - [Detecting Concurrency Memory Corruption Vulnerabilities (ESEC/FSE 2019)](http://www.is.cas.cn/ztzl2016/2020xsnh/2020nhhbzs/202009/W020200908636552224883.pdf) - [UFO: Predictive Concurrency Use-After-Free Detection (ICSE 2018)](http://acm.mementodepot.org/pubs/proceedings/acmconferences_3180155/3180155/3180155.3180225/3180155.3180225.pdf) - [ConPredictor: Concurrency Defect Prediction in Real-World Applications (TSE 2018)](https://arxiv.org/pdf/1804.03589.pdf) - [High-coverage, unbounded sound predictive race detection (ACM SIGPLAN Notices 2018)](https://dl.acm.org/doi/10.1145/3296979.3192385) - [What Happens-After the First Race? Enhancing the Predictive Power of Happens-Before Based Dynamic Race Detection (OOPSLA 2018)](http://umathur3.web.engr.illinois.edu/papers/shb-oopsla2018.pdf) - [Dynamic Race Prediction in Linear Time (PLDI 2017)](https://dl.acm.org/doi/10.1145/3062341.3062374) - [A dynamic predictive race detector for C/C++ programs (2017)](https://link.springer.com/content/pdf/10.1007/s11227-017-1996-8.pdf) - [Dynamic Race Detection for C++11 (2017)](https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf) - [An Efficient Algorithm for On-the-Fly Data Race Detection Using an Epoch-Based Technique (2015)](http://dx.doi.org/10.1155/2015/205827) - [Efficient Data Race Detection for C/C++ Programs Using Dynamic Granularity (2014)](https://ieeexplore.ieee.org/document/6877300) - [Finding Complex Concurrency Bugs in Large Multi-Threaded Applications (EuroSys 2011)](https://www.gsd.inesc-id.pt/~rodrigo/pike_eurosys11.pdf) - [ThreadSanitizer – data race detection in practice (2009)](https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/35604.pdf) - 11 **Fuzzing** - [Context-Sensitive and Directional Concurrency Fuzzing for Data-Race Detection (NDSS 2022)](https://www-users.cse.umn.edu/~kjlu/papers/conzzer.pdf) - [Fuzzing Channel-Based Concurrency Runtimes using Types and Effects (OOPSLA 2020)](https://2020.splashcon.org/details/splash-2020-oopsla/62/Fuzzing-Channel-Based-Concurrency-Runtimes-using-Types-and-Effects) - [Muzz: Thread-aware Grey-box Fuzzing for Effective Bug Hunting in Multithreaded Programs (Usenix Sec 2020)](https://www.usenix.org/system/files/sec20-chen-hongxu.pdf) - [Krace: Data Race Fuzzing for Kernel File Systems (S&P 2020)](https://www.cc.gatech.edu/~mxu80/pubs/xu:krace.pdf) - [Finding race conditions in Kernels: from fuzzing to symbolic exection (2020)](#finding-race-conditions-in-kernels-from-fuzzing-to-symbolic-exection-2020) - [ConFuzz—A Concurrency Fuzzer (2019)](https://wcventure.github.io/FuzzingPaper/Paper/AISC19_ConFuzz.pdf) - [Razzer: Finding Kernel Race Bugs through Fuzzing (S&P 2019)](https://lifeasageek.github.io/papers/jeong-razzer.pdf) - [A Heuristic Framework to Detect Concurrency Vulnerabilities (ACSAC 2018)](https://dl.acm.org/doi/pdf/10.1145/3274694.3274718?download=true) - [OWL: Understanding and Detecting Concurrency Attacks (DSN 2018)](http://www.cs.columbia.edu/~junfeng/papers/owl-dsn18.pdf) - 12 **Dynamic Testing/Systematic Testing** - [Waffle: Exposing Memory Ordering Bugs Efficiently with Active Delay Injection (EuroSys 2023)](https://www.microsoft.com/en-us/research/uploads/prod/2022/12/EuroSys23_camera_ready__WAFFLE_Exposing_Memory_Ordering_Bugs_Efficiently_with_Active_Delay_Injection.pdf) - [Efficiently Detecting Concurrency Bugs in Persistent Memory Programs (ASPLOS 2022)](https://csyhua.github.io/csyhua/hua-asplos22.pdf) - [Controlled Concurrency Testing via Periodical Scheduling (ICSE 2022)](https://sites.google.com/view/period-cct) - [C4: the C compiler concurrency checker (ISSTA 2021)](https://dl.acm.org/doi/abs/10.1145/3460319.3469079) - [Nekara: Generalized Concurrency Testing (ASE 2021)](https://www.microsoft.com/en-us/research/uploads/prod/2021/09/nekara-ase2021.pdf) -[[Artifact]](https://github.com/pdeligia/nekara-artifact)，[[Tool]](https://github.com/microsoft/coyote-scheduler)，[[Slides]](https://www.dropbox.com/s/lq79dwhcbsbdwbv/Nekara%20-%20ASE%202021%20presentation.pdf?dl=0)， [[Video]](https://www.youtube.com/watch?v=UTWaUjsqV8s) - [Snowboard: Finding Kernel Concurrency Bugs through Systematic Inter-thread Communication Analysis (SOSP 2021)](https://dl.acm.org/doi/abs/10.1145/3477132.3483549) - [C11Tester: A Race Detector for C/C++ Atomics (ASPLOS 2021)](https://dl.acm.org/doi/pdf/10.1145/3445814.3446711) - [Language-agnostic systematic concurrency testing (2021)](https://microsoft.github.io/coyote/#overview/publications/) - [Learning-Based Controlled Concurrency Testing (OOPSLA 2020)](https://dl.acm.org/doi/pdf/10.1145/3428298) - [Symbolic Partial-Order Execution for Testing Multi-Threaded Programs (CAV 2020)](https://arxiv.org/abs/2005.06688) - [Timeless Timing Attacks: Exploiting Concurrency to Leak Secrets over Remote Connections (Usenix Sec 2020)](https://www.usenix.org/conference/usenixsecurity20/presentation/van-goethem) - [Exploiting Kernel Races through Taming Thread Interleaving (BlackHat USA 2020)](https://lifeasageek.github.io/papers/yoochan-exprace-bh.pdf) - [Sparse record and replay with controlled scheduling (PLDI 2019)](https://dl.acm.org/doi/10.1145/3314221.3314635) - [Efficient Transaction-Based Deterministic Replay for Multi-threaded Programs (ASE 2019)](https://www.cs.cityu.edu.hk/~wkchan/papers/ase19-pobee+mei+chan.pdf) - [Efficient Scalable Thread-Safety-Violation Detection (SOSP 2019)](https://www.microsoft.com/en-us/research/uploads/prod/2019/09/sosp19-final193.pdf) - [Adaptive Randomized Scheduling for Concurrency Bug Detection (ICECCS 2019) (JAVA)](https://tjusail.github.io/paper/liu/2019/ICECCS19.pdf) - [Partial Order Aware Concurrency Sampling (CAV 2018)](https://link.springer.com/chapter/10.1007%2F978-3-319-96142-2_20) - [Promoting Secondary Orders of Event Pairs in Randomized Scheduling using a Randomized Stride (ASE 2017)](https://ieeexplore.ieee.org/document/8115685) - [Efficient Detection of Thread Safety Violations via Coverage-Guided Generation of Concurrent Tests (ICSE 2017) (JAVA)](https://www.software-lab.org/publications/icse2017-covcon.pdf) - [ProRace: Practical Data Race Detection for Production Use (ASPLOS 2017)](https://www3.cs.stonybrook.edu/~dongyoon/papers/ASPLOS-17-ProRace.pdf) -[[Tool: ProRace]](https://github.com/lzto/ProRace) - [Radius Aware Probabilistic Testing of Deadlocks with Guarantees (ASE 2016)](https://ieeexplore.ieee.org/document/7582772) - [SKI: Exposing Kernel Concurrency Bugs through Systematic Schedule Exploration (OSDI 2014)](https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-fonseca.pdf) - [Concurrency Testing Using Schedule Bounding: an Empirical Study (SCTBench) (PPoPP 2014)](https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/PPoPP.pdf) - [Efficient Concurrency-Bug Detection Across Inputs (OOPSLA 2013)](https://dl.acm.org/doi/10.1145/2544173.2509539) - [Multicore Acceleration of Priority-Based Schedulers for Concurrency Bug Detection (PLDI 2012)](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/pldi12_needlepoint.pdf) -[[Slides]](https://www.cs.rutgers.edu/~santosh.nagarakatte/papers/PLDI2012-needlepoint-web.pdf) - [A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs (ASPLOS 2010)](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-83.pdf) - [CalFuzzer: An Extensible Active Testing Framework for Concurrent Programs (CAV 2009)](https://www.seas.upenn.edu/~mhnaik/papers/cav09.pdf) - [Finding and Reproducing Heisenbugs in Concurrent Programs (OSDI 2008)](https://www.usenix.org/legacy/events/osdi08/tech/full_papers/musuvathi/musuvathi.pdf) -[[Slides]](https://nebelwelt.net/teaching/15-510-SE/slides/16-testing3-chess.pdf) - [ConMem: Detecting Severe Concurrency Bugs through an Effect-Oriented Approach](http://pages.cs.wisc.edu/~shanlu/paper/asplos184-zhang.pdf) - [Effective Testing for Concurrency Bugs (Thesis)](https://www.mpi-sws.org/tr/2015-004.pdf) - [Concurrency: Testing isn’t good enough](http://www.contemplateltd.com/threadsafe/concurrency-testing-isnt-good-enough) - [Maple: a coverage-driven testing tool for multithreaded programs (OOPSLA 2012)](https://dl.acm.org/doi/10.1145/2384616.2384651) - [Stable Deterministic Multithreading through Schedule Memoization (OSDI 2010)](https://www.cs.columbia.edu/~junfeng/11sp-w4118/lectures/tern.pdf) - [Race Directed Random Testing of Concurrent Programs (PLDI 2008)](https://www.cs.columbia.edu/~junfeng/10fa-e6998/papers/racefuzz.pdf) - 13 **Other Verification Techniques** - [Dynamic verification of c/c++ 11 concurrency over multi copy atomics (2021)](https://arxiv.org/pdf/2103.01553.pdf) - [Bounded Verification of Multi-threaded Programs via Lazy Sequentialization (TOPLAS 2021)](https://dl.acm.org/doi/full/10.1145/3478536) - [Compositional Non-Interference for Fine-Grained Concurrent Programs (S&P 2021)](https://arxiv.org/abs/1910.00905) - [Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs (POPL 2021)](http://ramanathan.ts.gitlab.io/html-webpage/publications/POPL2021withAppendix.pdf) - [On Algebraic Abstractions for Concurrent Separation Logics (POPL 2021)](https://software.imdea.org/~aleks/popl21/popl21.pdf) - [Satisfiability Modulo Ordering Consistency Theory for Multi-threaded Program Verification (PLDI 2021)](https://pldi21.sigplan.org/details/pldi-2021-papers/83/Satisfiability-Modulo-Ordering-Consistency-Theory-for-Multi-threaded-Program-Verifica) - [Verifying Concurrent Search Structure Templates (PLDI 2020)](https://pldi20.sigplan.org/details/pldi-2020-papers/69/Verifying-Concurrent-Search-Structure-Templates) - [Armada: Low-Effort Verification of High-Performance Concurrent Programs (PLDI 2020)](https://www.microsoft.com/en-us/research/uploads/prod/2020/06/armada.pdf) - [The Anchor Verifier for Blocking and Non-blocking Concurrent Software (OOPSLA 2020)](https://2020.splashcon.org/details/splash-2020-oopsla/32/The-Anchor-Verifier-for-Blocking-and-Non-blocking-Concurrent-Software) - [Towards Generating Thread-Safe Classes Automatically (ASE 2020)](https://conf.researchr.org/details/ase-2020/ase-2020-papers/70/Towards-Generating-Thread-Safe-Classes-Automatically) - [Parallel Refinement for Multi-Threaded Program Verification (ICSE 2019)](https://2019.icse-conferences.org/details/icse-2019-Technical-Papers/44/Parallel-Refinement-for-Multi-Threaded-Program-Verification) - [Finding rare concurrent programming bugs: An automatic, symbolic, randomized, and parallelizable approach (ICTAC2018)](https://eprints.soton.ac.uk/425836/) - [A Runtime Verification Tool for Detecting Concurrency Bugs in FreeRTOS Embedded Software (ISPDC 2018)](http://www.es.mdh.se/pdf_publications/5186.pdf) - [Parallel Bug-finding in Concurrent Programs via Reduced Interleaving Instances (ASE 2017)](https://eprints.soton.ac.uk/413917/1/swarm_ASE2017.pdf) - [Inductive Data FLow Graph (POPL 2013)](https://www.cs.princeton.edu/~zkincaid/pub/popl13.pdf) - [Inspect: A Runtime Model Checker For Mulithreaded C Programs (2008)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.6260) - 14 **Energy Accounting** - [Calm Energy Accounting for Multithreaded Java Applications (ESEC/FSE 2020)](http://www.cs.binghamton.edu/~davidl/papers/FSE20Preprint.pdf) - 15 **Reproducing/Dubugging** - [Sparse record and replay with controlled scheduling (PLDI 2019)](https://dl.acm.org/doi/10.1145/3314221.3314635) - [AggrePlay: efficient record and replay of multi-threaded programs (ESEC/FSE 2019)](https://www.cs.cityu.edu.hk/~wkchan/papers/fse2019-pobee+chan.pdf) - [D4: Fast Concurrency Debugging with Parallel Differential Analysis (PLDI 2018)](https://parasol.tamu.edu/people/jeff/academic/d4.pdf) - [DESCRY: Reproducing System-Level Concurrency Failures (ESEC/FSE 2017)](https://par.nsf.gov/servlets/purl/10075449) - [CONCURRIT: A Domain Specific Language for Reproducing Concurrency Bugs (PLDI 2013)](https://people.eecs.berkeley.edu/~ksen/papers/concurrit.pdf) -[[Source]](https://code.google.com/archive/p/concurrit/) - [Using_SCHED_DEADLINE](https://elinux.org/images/f/fe/Using_SCHED_DEADLINE.pdf) - 16 **Theory** - [A Concurrent Program Logic with a Future and History (OOPSLA 2022)](https://arxiv.org/pdf/2207.02355.pdf) - [Concurrent Size (OOPSLA 2022)](https://arxiv.org/abs/2209.07100) - 17 **Empirical Study/Benchmarking** - [An Empirical Study on Concurrency Bugs in Interrupt-driven Embedded Software](https://2023.issta.org/details/issta-2023-technical-papers/99/An-Empirical-Study-on-Concurrency-Bugs-in-Interrupt-driven-Embedded-Software) - [Gobench: A benchmark suite of real-world go concurrency bugs (CGO 2021)](https://ieeexplore.ieee.org/abstract/document/9370317) - [Actor Concurrency Bugs: A Comprehensive Study on Symptoms, Root Causes, API Usages, and Differences (OOPSLA 2021)](https://mbagherz.bitbucket.io/lab-correct-software/papers/akka-actor-bugs.pdf) - [Concurrency testing using controlled schedulers: An empirical study (TOPC 2016)](https://dl.acm.org/doi/pdf/10.1145/2858651?casa_token=k7L1hBjlQeUAAAAA:6ZqKKosLEax0SKgNvKUiDLWRPO3e2ExV4FakJs9s5ohhIMXxtgyOMce17A-KUh3cHrcRe2UXl_Is) -[[Source]](https://github.com/mc-imperial/sctbench) - [RADBench: A Concurrency Bug Benchmark Suite (USENIX HotPar 2011)](https://www.usenix.org/legacy/event/hotpar11/tech/final_files/Jalbert.pdf) - [Bugbench: Benchmarks for Evaluating Bug Detection Tools](http://pages.cs.wisc.edu/~shanlu/paper/63-lu.pdf) -[[Source1]](https://github.com/lihebi/bugbench-orig),[[Source2]](https://github.com/lihebi/bugbench) - [A Case for an Interleaving Constrained Shared-Memory Multi-Processor](http://web.eecs.umich.edu/~nsatish/papers/ISCA-09-CPC.pdf) -[[Source]](https://github.com/jieyu/concurrency-bugs) - [The PARSEC benchmark suite: characterization and architectural implications (2008)](https://dl.acm.org/doi/pdf/10.1145/1454115.1454128) -[[Source]](https://parsec.cs.princeton.edu/index.htm) - [Experience with a Concurrency Bugs Benchmark (2008) (JAVA)](https://personal.cis.strath.ac.uk/marc.roper/TESTBENCH08/Papers/tzoref.pdf) - 18 **Large Language Model** - [Assessing Large Language Models in Comprehending and Verifying Concurrent Programs across Memory Models (arXiv 2025)](https://arxiv.org/abs/2501.14326) - 19 **Applications** - 01 **Data Race Detection** - [The Complexity of Dynamic Data Race Prediction (LICS 2020)](https://cs.au.dk/~pavlogiannis/publications/papers/lics20.pdf) [[Slides]](https://cs.au.dk/~pavlogiannis/publications/presentations/lics20_PR.pdf)