Data-Races and Static Analysis for Interrupt-Driven Kernels
We consider a class of interrupt-driven programs that model the kernel API libraries of some popular real-time embedded operating systems and the synchronization mechanisms they use. We define a natural notion of data races and a happens-before ordering for such programs. The key insight is the notion of disjoint blocks to define the synchronizes-with relation. This notion also suggests an efficient and effective lockset based analysis for race detection. It also enables us to define efficient ‘‘sync-CFG’’ based static analyses for such programs, which exploit data-race freedom. We use this theory to carry out static analysis on the FreeRTOS kernel library to detect races and to infer simple relational invariants on key kernel variables and data-structures.
Thu 11 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:30 | Program Analysis and Automated VerificationESOP at SUN II Chair(s): Stephanie Balzer Carnegie Mellon University | ||
10:30 30mTalk | Data-Races and Static Analysis for Interrupt-Driven Kernels ESOP Link to publication | ||
11:00 30mTalk | An abstract domain for trees with numeric relations ESOP Link to publication | ||
11:30 30mTalk | A static higher-order dependency pair framework ESOP Link to publication | ||
12:00 30mTalk | Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses ESOP Henning Basold CNRS & ENS Lyon, Ekaterina Komendantskaya Heriot-Watt University, UK, Yue Li Heriot-Watt University, UK Link to publication |