Cours de “Systèmes d’exploitation: principes et modélisation”
(2012–2013), L3 - 2ième semestre

Enseignants: Marc Pouzet et Louis Mandel
Cours: jeudi de 13h30 à 15h30, en salle R.
TPs: jeudi de 15h45 à 17h45, en salle INFO 4.

Pour toute question liée au cours, nous contacter par mail (Marc.Pouzet@ens.fr ou Louis.Mandel@ens.fr) ou passer nous voir (bureaux S13 et S14, passage Saumon du DI; équipe PARKAS).

Objectifs

Le cours présente les concepts fondamentaux des systèmes d’exploitation, leur utilisation et leur mise en oeuvre dans le système Unix. La première partie étudie le cas d’Unix: organisation de la mémoire, systèmes de fichiers, gestion des processus lourds et léger (“threads”), signaux, communication entre processus, sockets. La seconde partie étudie les problèmes classiques apparaissant dans les systèmes d’exploitation: interblocage et famine entre processus, courses critiques, prise en compte des temps de calcul, etc. Nous verrons comment modéliser certains de ces problèmes et comment les techniques de vérification formelle peuvent nous aider à définir des implémentations prouvées correctes.

Les notes de cours et les énoncés de TD/TP sont mis en ligne chaque semaine. Le corrigé de TD/TP est donné après la séance. Si vous n’avez pas eu le temps de finir le sujet en TP, vous devez l’avoir terminé avant la séance suivante. Cette année, le cours abordera les points suivants:

• système de fichiers;
• gestion des processus;
• mémoire virtuelle;
• communication et synchronisation entre processus concurrents (mémoire partagée, signaux, sémaphores, sockets);
• ordonnancement préemptif et non-préemptif; OS temps réel;
• interblocage, famine et courses critiques.
• langages de modélisation et techniques de “vérification par modèles” (Model-checking).
• cas des systèmes réactifs synchrones; modélisation et implémentation.

Les notions introduites seront illustrées par l’écriture d’applications, principalement en Ocaml, et utilisant la librairie Unix.

Plan du cours

Cours:

• Cours 1 (21/02/2013): Introduction; redirections; systèmes de fichiers. Introduction, Système de fichiers, code C et OCaml.
• Cours 2 (28/02/2013): Systèmes de fichiers (suite et fin); Gestion des processus, code C et OCaml, code OCaml et RML des deux peintres (installer ReactiveML)
• Cours 3 (7/03/2013): Gestion des processus et communication par signaux. code C et OCaml.
• Cours 4 (21/03/2013): processus légers et synchronisation. code C et OCaml.
• Cours 5 (28/03/2013): processus légers et synchronisation et code.
• Cours 6 (4/04/2013): Réseaux de processus et communication par buffers et code OCaml.
• Cours 7 (11/04/2013): Modélisation et vérification de systèmes concurrents avec l’outil Cubicle par Sylvain Conchon. Notes de cours par Sylvain Conchon.
• Cours 8 (18/04/2013): Modélisation de systèmes concurrents; Machines de Moore/Mealy, représentation explicite/implicite, composition parallèle. Notes de cours.
• Cours 9: Modélisation synchrone avec le langage Lustre (distribution).
• Cours 10: Modélisation de la communication par rendez-vous binaire, par diffusion (“broadcast”), par FIFOs, par tableau noir. Communication par échantillonnage périodique, voteurs.
• Examen (2012): sujet et correction.

TD/TPs:

• TP 01 (14/02/2013). Shell. shell, énoncé, correction.
• TP 02 (21/02/2013). Manipulations de fichiers. énoncé, code, correction.
• TP 03 (28/02/2013). Système de fichiers. énoncé, correction.
• TP 03-bis (14/03/2013). Système de fichiers (suite de la fiche précédente).
• TP 04. Mini-shell. énoncé, correction.
• TP5. Processus (implémentation de réseaux de Kahn). énoncé, code.
• TP6. Cubicle. énoncé, code.
• TP8 et TP9. Prises (sockets).
• TP10. Un jeu en réseau.

Trousse de survie Unix:

• Documentation de Christophe Blaess. Commandes Unix; Programmation shell; Administration Linux
• bash
• Un site sur la programmation système de bas niveau.

Articles à lire:

Une liste d’articles a lire, mise a jour progressivement.

• First Draft of a Report on the EDVAC, John Von Neumann, 1945.. L’ancêtre des ordinateurs.
• Solution of a Problem in Concurrent Programming Control, E. W. DIJKSTRA, 1965. Un des premiers articles sur les problèmes d’exclusion mutuelle.
• A New Solution of Dijkstra’s Concurrent Programming Problem, Leslie Lamport, 1974. La fameuse solution de Lamport au problème de Dijkstra.
• On micro-kernel Construction, Jochen Liedtke, 1995. La définition de la notion de micro-noyau.
• seL4: Formal Verification of an OS Kernel, Klein et al. 2010. La validation en utilisant un environnement de preuve formelle du micro-noyau proposé par Liedtke.
• “The semantics of a simple language for parallel programming”, Gilles Kahn, 1974 et “Coroutines and Networks of Parallel Processes”, Gilles Kahn et David MacQueen. Les articles sur la sémantique de systèmes de processus déterministes communicant par FIFO. Influence majeure sur la sémantique du parallélisme et le domaine des systèmes embarqués.
• Synchronous Modelling of Asynchronous Systems, Nicolas Halbwachs, 2002, EMSOFT’02. La modélisation dans le langage Lustre du parallélisme et de la communication asynchrones.
• Virtual Execution of AADL Models via a Translation into Synchronous Programs, Erwan Jahier, Nicolas Halbwachs Pascal Raymond, Xavier Nicollin, David Lesens. Modélisation synchrone de systèmes et d’architectures asynchrones.
• Synchronous modeling and validation of priority inheritance schedulers, Erwan Jahier, Nicolas Halbwachs, and Pascal Raymond, 2009. Modélisation d’ordonnanceurs temps reel.
• Deux articles intéressants et de culture générale donnant le point de vue d’Edward Lee sur les threads (The Problem with Threads) et la modélisation du temps physique (Computation Needs Time).

This document was translated from L^AT_EX by H^EV^EA.