POPL 2017 (series) / VMCAI 2017 (series) / VMCAI /
Detecting All High-Level Dataraces in an RTOS Kernel.
A high-level datarace occurs when an execution interleaves instructions corresponding to user-annotated critical accesses to shared memory structures. Such races are good indicators of atomicity violations. We propose a technique for detecting all high-level dataraces in a system library like the kernel API of a real-time operating system (RTOS) that relies on flag-based scheduling and synchronization. Our methodology is based on model-checking, but relies on a meta-argument to bound the number of task processes needed to orchestrate a race. We describe our approach in the context of FreeRTOS, a popular RTOS in the embedded domain.
Tue 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 17 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 16:30 Talk | Using Abstract Interpretation to Correct Synchronization Faults VMCAI Pietro FerraraIBM Research, Omer TrippIBM Thomas J. Watson Research Center, Peng LiuPurdue University, Eric KoskinenYale University | ||
16:30 - 17:00 Talk | Detecting All High-Level Dataraces in an RTOS Kernel. VMCAI | ||
17:00 - 17:30 Talk | Precise Thread-Modular Abstract Interpretation of Concurrent Programs using Relational Interference Abstractions VMCAI |