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

Enseignants: Marc Pouzet et Timothy Bourke
Cours: jeudi de 13h30 à 15h30, en salle W.
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 Timothy.Bourke@ens.fr) ou passer nous voir (bureaux S12 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:

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

Plan du cours

Cours:

21-01-2015IntroPrésentation du cours: slides.
19-02-2015Cours 1Introduction; Micro-noyau en OCaml; Principes du shell: Introduction, Shell, Un micro-noyau en OCaml, Code OCaml.
5-03-2015Cours 2Systèmes de fichiers: Gestion des processus, code C et OCaml, code OCaml et RML des deux peintres (installer ReactiveML)
12-03-2015Cours 3Communication par signaux. code C et OCaml.
19-03-2015Cours 4Processus légers et synchronisation. Code C et OCaml.
26-03-2015Cours 5Processus légers et synchronisation. Code C.
2-04-2015Cours 6Mémoire Virtuelle
9-04-2015Cours 7Micro-noyau et sa vérification formelle (seL4), par Timothy Bourke.
16-04-2015Cours 8Modélisation de systèmes concurrents: modèle data-flow; systèmes de transition, composition parallèle, représentations explicites/implicites, propriétés de sûreté et de vivacié.
7-05-2015Cours 9Modélisation du temps. Parallélisme synchrone et asynchrone.Lustre. Machines de Moore/Mealy, représentation explicite/implicite, composition parallèle. Un exemple de modélisation et de vérification: le protocole du bit alterné.
21-05-2015Cours 10Semantic Patch Language (outil Coccinelle), par Julia Lawall (voir l’article de POPL 2009 pour la théorie sous-jacente).
28-05-2015Examen2h. Notes de cours et TDs autorisées. Sujet et corrigé.
  Examen (2013): sujet.
  Examen (2012): sujet et correction.

TD/TPs – Projet:

19-02-2015TP01Shell. Énoncé, correction.
26-02-2015TP02Manipulation du système de fichiers. Énoncé, code, correction.
5-03-2015TP03Manipulation et implantation de systèmes de fichiers.
12-03-2015TP04Mini-shell.
19-03-2015TP05Processus (implémentation de réseaux de Kahn).
26-03-2015TP06Achèvement des TDs précédents et projet.
2-04-2015TP07 
9-04-2015TP08Client et proxy HTTP.
16-05-2015TP09Micro-noyau seL4.
7-05-2015TP10Un jeu en réseau.
21-05-2015ProjetÀ faire en binôme et à rendre par mail: Énoncé. Deux suggestions d’application :

Trousse de survie Unix:

Articles à lire:

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


This document was translated from LATEX by HEVEA.