Tesi etd-08312017-024701
Link copiato negli appunti
Tipo di tesi
Dottorato
Autore
PARRI, ANDREA
URN
etd-08312017-024701
Titolo
Resource Reservation and Memory Ordering in the Linux Kernel
Settore scientifico disciplinare
ING-INF/05
Corso di studi
INGEGNERIA - Ph.D. Programme in Emerging Digital Technologies (EDT)
Commissione
relatore MARINONI, MAURO
Membro Prof. CUCINOTTA, TOMMASO
Presidente Prof. LIPARI, GIUSEPPE
Membro Prof. CUCINOTTA, TOMMASO
Presidente Prof. LIPARI, GIUSEPPE
Parole chiave
- concurrency
- memory ordering
- real-time scheduling
- resource reservation
Data inizio appello
15/03/2018;
Disponibilità
completa
Riassunto analitico
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.
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.
File
| Nome file | Dimensione |
|---|---|
| DTA_thesis_Parri.pdf | 1.25 Mb |
Contatta l'autore |
|