SCRATCH: a tool for automatic analysis of dma races
Abstract
We present the SCRATCH tool, which uses bounded model checking and k-induction to automatically analyse software for multicore processors such as the Cell BE, in order to detect DMA races.
Related papers
- A refinement hierarchy for free list memory allocators ISMM 2017
- Automatic Analysis of Scratch-Pad Memory Code for Heterogeneous Multicore Processors TACAS 2010
- DR.FIX: Automatically Fixing Data Races at Industry Scale PLDI 2025
- LOCKSMITH: Practical static race detection for C TOPLAS 2011
- Automated type-based analysis of data races and atomicity PPoPP 2005
- Automatic generation of library bindings using static analysis PLDI 2009
- Automatically classifying benign and harmful data racesallusing replay analysis PLDI 2007
- When threads meet events: efficient and precise static race detection with origins PLDI 2021