DTA

Digital Theses Archive

 

Tesi etd-08312017-024701

Thesis type
Dottorato
Author
PARRI, ANDREA
URN
etd-08312017-024701
Title
Resource Reservation and Memory Ordering in the Linux Kernel
Scientific disciplinary sector
ING-INF/05
Corso di studi
INGEGNERIA - Ph.D. Programme in Emerging Digital Technologies (EDT)
Commissione
relatore MARINONI, MAURO
Presidente Prof. LIPARI, GIUSEPPE
Membro Prof. CUCINOTTA, TOMMASO
Parole chiave
  • concurrency
  • memory ordering
  • real-time scheduling
  • resource reservation
Data inizio appello
;
Disponibilità
parziale
Riassunto analitico
When integrating hard, soft and non-real-time tasks in general<br>purpose operating systems, it is necessary to provide temporal<br>isolation so that the timing properties of one task do not depend<br>on the behaviour of the others. Hierarchical scheduling is a promising<br>methodology for providing temporal isolation and for enabling<br>component-based design and analyis.<br><br>This thesis describes the implementation, within the Linux kernel,<br>of a multiprocessor bandwidth reservation mechanism for groups of<br>real-time tasks, based on the SCHED_DEADLINE scheduling class. It<br>then describes two reclaiming algorithms implementations for efficient<br>use of the computational resources in the presence of tasks with<br>variable workload.<br><br>Response time analysis (RTA) is one of the fundamental tools to<br>study the schedulability of real-time tasks on multiprocessors, and<br>several methods inspired by RTA have been successfully developed to address<br>more sophisticated execution platforms and application models. The major<br>issue with RTA is its time complexity, which is NP-hard.<br><br>This thesis presents polynomial and pseudo-polynomial time schedulability<br>tests, based on RTA, for determining whether a set of sporadic DAG-tasks<br>with arbitrary deadlines can be scheduled by G-EDF or G-DM on a platform<br>consisting of m identical processor. It also presents a new response time<br>upper bound for tasks scheduled by fixed priorities, and investigates its<br>tightness properties.<br><br>Concurrency can be a contentious topic when developing efficient, low-level<br>synchronisation primitives and scheduling algorithms in the Linux kernel.<br>The Linux kernel mailing list features numerous discussions related to<br>consistency models, including those of the more than 30 CPU architectures<br>supported by the kernel and that of the kernel itself.<br><br>A formal model can help address such issues, by allowing programmers to<br>experiment with the model and develop their intuition. This thesis offers<br>a model of Linux-kernel memory ordering written in the Cat language,<br>making it not only formal, but also executable by the Herd simulator.<br>It also formalises the fundamental law of the Read-Copy-Update<br>synchronisation mechanism.<br>
File