Synthèse automatique du code OS

Description

Cette séance de cours explore le concept de synthétisation automatique du code OS, en mettant l'accent sur les défis auxquels sont confrontés les développeurs de systèmes d'exploitation dans la configuration manuelle du matériel de traduction. L'orateur, Reto Achermann de l'Université de la Colombie-Britannique, discute du processus fastidieux de lecture des manuels de matériel, de la complexité des unités de traduction et de la nécessité de vérifier l'exactitude. La séance de cours présente la chaîne d'outils Velosiraptor, qui construit automatiquement le code OS correct à partir d'une spécification, réduisant l'effort de développement et minimisant le risque d'erreurs.

Connectez-vous pour regarder la vidéo

Source officielle

https://mediaspace.epfl.ch/media/0_wcs2n8gy

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Séances de cours associées (61)

Concepts associés (173)

Table des pages

droite|vignette|Relations entre les pages adressée par les adresses virtuelles et les pages en mémoire physique. La mémoire physique peut contenir des pages appartenant à de nombreux processus. Les pages peuvent être conservées sur disque si elles sont rarement utilisées ou si la mémoire est pleine. Dans le diagramme ci-dessus, certaines pages ne sont pas dans la mémoire physique. La table des pages est la structure de données utilisée par un système de mémoire virtuelle dans un système d'exploitation pour stocker les correspondances entre adresses virtuelles et adresses physiques.

Unité de gestion de mémoire

Une unité de gestion mémoire (MMU pour memory management unit), parfois appelée unité de gestion de mémoire paginée (PMMU pour paged memory management unit), est un composant permettant de contrôler les accès qu'un processeur fait à la mémoire de l'ordinateur dans lequel il est placé. À l'époque des premiers microprocesseurs, il s'agissait d'un circuit intégré dédié. Puis le MMU a été intégré aux microprocesseurs, à partir du 80286 pour la gamme Intel x86, à partir du 68030 pour la gamme Motorola 680x0.

Mémoire virtuelle

thumb|Schéma de principe de la mémoire virtuelle. En informatique, le mécanisme de mémoire virtuelle a été mis au point dans les années 1960. Il repose sur l'utilisation de traduction à la volée des adresses (virtuelles) vues du logiciel, en adresses physiques de mémoire vive. La mémoire virtuelle permet : d'utiliser de la mémoire de masse comme extension de la mémoire vive ; d'augmenter le taux de multiprogrammation ; de mettre en place des mécanismes de protection de la mémoire ; de partager la mémoire entre processus.

Example-based machine translation

Example-based machine translation (EBMT) is a method of machine translation often characterized by its use of a bilingual corpus with parallel texts as its main knowledge base at run-time. It is essentially a translation by analogy and can be viewed as an implementation of a case-based reasoning approach to machine learning. At the foundation of example-based machine translation is the idea of translation by analogy.

Extension d'adresse physique

La technique d'extension d'adresse physique (EAP) ou Physical Address Extension (PAE) est une fonctionnalité des processeurs x86 qui permet d'adresser jusqu'à de mémoire physique sur des systèmes 32 bits (autrement limités à ), pourvu que le système d'exploitation le supporte. La PAE est fournie par les processeurs Intel Pentium Pro et suivants (incluant tous les processeurs de la série Pentium à l'exception des Pentium M disposant d'un bus ), ainsi que par des processeurs compatibles tels ceux d'AMD.