Salvato in:
Dettagli Bibliografici
Autore:PARRI, ANDREA
Titolo:Resource Reservation and Memory Ordering in the Linux Kernel
Pubblicazione:: Scuola Superiore Sant’Anna, 2018-03-19
Abstract: 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...sary 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.
Read more
Note:diritti: Copyright information available at source archive
application/pdf
Autori secondari:MARINONI, MAURO
LIPARI, GIUSEPPE
CUCINOTTA, TOMMASO
Classe MIUR:ING-INF/05
Risorsa digitale:Copia depositata in BNCF Repository di Ateneo
Copia depositata in BNCF Repository di Ateneo
Copia depositata in BNCF Repository di Ateneo
LEADER 03665nam a2200313 n 4500
001 TD20027333
005 20180330.0
049 |a TDMAGDIG 
100 |a 20190501d2018 --k--ita-50----ba  
101 1 |a it 
200 1 |a Resource Reservation and Memory Ordering in the Linux Kernel  |b Tesi di dottorato 
210 1 |c Scuola Superiore Sant’Anna  |d 2018-03-19 
300 |a diritti: info:eu-repo/semantics/embargoedAccess  |a diritti: Copyright information available at source archive 
328 0 |b tesi di dottorato  |c ING-INF/05  |e Scuola Superiore Sant’Anna 
330 |a 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.  
336 |a application/pdf 
689 0 |a ING-INF/05  |c TDR 
700 0 |a PARRI, ANDREA 
702 0 |a MARINONI, MAURO 
702 0 |a LIPARI, GIUSEPPE 
702 0 |a CUCINOTTA, TOMMASO 
801 3 |a IT  |b IT-FI0098 
856 4 |u http://memoria.depositolegale.it/*/http://dta.santannapisa.it/theses/available/etd-08312017-024701/  |2 http://dta.santannapisa.it/theses/available/etd-08312017-024701/ 
856 4 |u http://memoria.depositolegale.it/*/http://dta.santannapisa.it/theses/available/etd-08312017-024701/BNCaccess/DTA_thesis_Parri.pdf  |2 http://dta.santannapisa.it/theses/available/etd-08312017-024701/BNCaccess/DTA_thesis_Parri.pdf 
856 4 |u http://memoria.depositolegale.it/*/http://dta.santannapisa.it/theses/available/etd-08312017-024701/BNCaccess/frontespizio.pdf  |2 http://dta.santannapisa.it/theses/available/etd-08312017-024701/BNCaccess/frontespizio.pdf 
977 |a  CR 
997 |a CF 
FMT |a TD 
FOR |a TD 
Tesi di dottorato | Lingua: | Paese: | BID: TD20027333
Visualizza in formato Unimarc
Biblioteca Inventario Volume Collocazione Fruizione status