Resource Reservation and Memory Ordering in the Linux Kernel

When integrating hard, soft and non-real-time tasks in general purpose operating systems, it is necessary to provide temporal isolation so that the timing properties of one task do not depend on the behaviour of the others. Hierarchical scheduling is a promising methodology for providing temporal isolation and for enabling component-based design and analyis. This thesis describes the implementation, within the Linux kernel, of a multiprocessor bandwidth reservation mechanism for groups of real-time tasks, based on the SCHED_DEADLINE scheduling class. It then describes two reclaiming algorithms implementations for efficient use of the computational resources in the presence of tasks with variable workload. Response time analysis (RTA) is one of the fundamental tools to study the schedulability of real-time tasks on multiprocessors, and several methods inspired by RTA have been successfully developed to address more sophisticated execution platforms and application models. The major issue with RTA is its time complexity, which is NP-hard. This thesis presents polynomial and pseudo-polynomial time schedulability tests, based on RTA, for determining whether a set of sporadic DAG-tasks with arbitrary deadlines can be scheduled by G-EDF or G-DM on a platform consisting of m identical processor. It also presents a new response time upper bound for tasks scheduled by fixed priorities, and investigates its tightness properties. Concurrency can be a contentious topic when developing efficient, low-level synchronisation primitives and scheduling algorithms in the Linux kernel. The Linux kernel mailing list features numerous discussions related to consistency models, including those of the more than 30 CPU architectures supported by the kernel and that of the kernel itself. A formal model can help address such issues, by allowing programmers to experiment with the model and develop their intuition. This thesis offers a model of Linux-kernel memory ordering written in the Cat language, making it not only formal, but also executable by the Herd simulator. It also formalises the fundamental law of the Read-Copy-Update synchronisation mechanism.