Spunky #4: Kernel Timing
Martin is working at Genode Labs. He has been especially involved in the custom kernel, platform support, networking and testing. Furthermore, he is enthusiastic about Genode Labs' yearly Hack'n'Hike and the Microkernel Devroom at the FOSDEM.
In this article series I illustrate the development of an Ada kernel for Genode named Spunky. The approach is to first successively translate parts from the C++ base-hw kernel and temporarily integrate them with the remaining C++ parts. Once, the whole Kernel made it to Ada, Spunky can be further developed independently to benefit from the characteristics of Ada or even SPARK. This time, I talk about the translation of timeout scheduling and the underlying timer driver.
You can find the code behind this article on my Github branch. If you're interested in the discussion around Spunky, you may have a look at the Github issue. You also might want to read the former articles of this series:
