The PREEMPT RT Thread Synchronization Model is the base for the work I’ve been developing during my Ph.D.. Giving its complexity, it followed the incremental development of workshop paper, followed by a conference paper and then the journal paper, which is finally online (you can access the accepted version here).

Looking back now, it was risky. Linux complexity is indeed high – and hard to justify and find the correct words to explain it, and I could put my Ph.D. at risk. I received some rejects along the way, but mostly because of concepts that took me a while to express in natural languages – the formal part was never indeed criticized.

But, it was a good bet, mainly because it is enabling the application of more sophisticated forms of reasoning on the kernel because it abstracts the code complexity. It opened the door for the exploration of the Efficient Runtime Verification for the Linux kernel, and other researches that will appear soon, mainly about the formalization of the metrics on Linux and the utilization of other runtime verification methods. But it is not only impacting my work, as other researchers are also using the model. For example, people at Oxford University used my method as motivation to create automatically generated models!

I am glad that this paper is finally online, but that is not the end of the line! More to come soon! And the next articles will potentially be more exciting than this.