Main page Research activities Publications Talks MSc thesis projects Mentoring Hobby and spare time Write me This site uses
Google Analytics
Last updated on
15 January 2019

Publication details

D. B. de Oliveira, T. Cucinotta, R. S. de Oliveira. "Modeling the Behavior of Threads in the PREEMPT_RT Linux Kernel Using Automata," in Proceedings of the International Workshop on Embedded Operating Systems (EWILI 2018), October 10th, 2018, Torino, Italy.

Abstract

This article proposes an automata-based model for describing and verifying the behavior of thread management code in the Linux PREEMPT_RT kernel, on a single-core system. The automata model defines the events that influence the timing behavior of the execution of threads, and the relations among them. This article also presents the extension of the Linux trace features that enable the trace of such events in a real system. Finally, one example is presented of how the presented model and tracing tool helped catching an inefficiency bug in the scheduler code and ultimately led to improving the kernel.

Download paper


Main page Research activities Publications Talks MSc thesis projects Mentoring Hobby and spare time Write me Last updated on