Cours Systèmes d’exploitation:
principes, programmation et modélisation

L3: 2018, 2ième semestre
Enseignants: Marc Pouzet et Timothy Bourke
Cours: jeudi de 13h15 à 15h15, en salle U/V.
TPs: jeudi de 15h15 à 17h00, 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:

 Présentation du coursslides.
8-02-2018Cours 1Introduction, Principes du Shell, Un micro-noyau en OCaml, Code OCaml.
15-02-2018Cours 2Systèmes de fichiers: Systèmes de fichiers, code C et OCaml.
22-02-2018Cours 3Processus lourds; code C et OCaml,
1-03-2018Cours 3 (suite)communication par signaux code C et OCaml.
8-03-2018Cours 4Processus légers et synchronisation. Code C et OCaml. Peintres en ReactiveML.
15-03-2018Cours 5Micro-noyau et sa vérification formelle (seL4), par Timothy Bourke.
22-03-2018Cours 6 Communications et synchronisations code C. Communication par FIFOs
29-03-2018Cours 7Mémoire Virtuelle. code C; Code C de l’utilisation de mmap.
5-04-2018Cours 8Introduction au langage Lustre; modélisation et vérification. exemple.
12-04-2018Cours 9Sémantique et implémentation des processus communiquant par FIFOs.
vacances
3-05-2018 École inaccessible
10-05-2018Cours 10Algorithmes d’ordonnancement.
17-05-2018Cours invité.MirageOS par Thomas Gazagnaire (slides).
24-05-2018Soutenances de projets 
31-05-2018Examen2017 (corrigé). 2016 (corrigé), 2014 (corrigé) 2013

TD/TPs – Projet:

8-02-2018TP01Shell. Énoncé, correction.
15-02-2018TP02Manipulation du système de fichiers. Énoncé, code, correction.
22-02-2018TP03Manipulation et implantation de systèmes de fichiers. Énoncé, code, correction.
1-03-2018TP03b / TP04Mini-shell. Énoncé, code, correction.
8-03-2018TP04bContinuation du TP4.
15-03-2018TP05Micro-noyau seL4. Énoncé, code et correction. (Syscall dans assembleur)
22-03-2018TP06Processus (implémentation de réseaux de Kahn). Énoncé, code, correction.
29-03-2018TP06/ProjetSéance de travail (TPs ou projet).
5-04-2018TP07Client et proxy HTTP. Énoncé, code et correction.
12-04-2018TP08Un jeu en réseau. Énoncé, code, pong.byte (pong_sdl.byte) et correction.
vacances
3-05-2018 École inaccessible
10-05-2018 Jour férié
17-05-2018TP9TP invité (énoncé)
A rendreProjetÀ faire en binôme et à rendre par mail: Énoncé Kahn et Énoncé Rock’n’Roll. 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.