Synthèse automatique du code OS

Description

Cette séance de cours de l'instructeur aborde le thème de la synthèse 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. La séance de cours présente le projet Velosiraptor, qui vise à alléger le fardeau des développeurs OS en générant automatiquement un code correct à partir d'une spécification comportementale. La séance de cours traite du processus de synthèse, des techniques de réduction de l'espace de recherche et d'un langage de spécification spécialisé utilisé dans le projet. Il met également en lumière les résultats de performance et les travaux en cours pour optimiser le processus de synthèse et traiter les dépendances de configuration globale.

Connectez-vous pour regarder la vidéo

Source officielle

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

À 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 (102)

Concepts associés (217)

Address space

In computing, an address space defines a range of discrete addresses, each of which may correspond to a network host, peripheral device, disk sector, a memory cell or other logical or physical entity. For software programs to save and retrieve stored data, each datum must have an address where it can be located. The number of address spaces available depends on the underlying address structure, which is usually limited by the computer architecture being used.

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.

Adresse physique

In computing, a physical address (also real address, or binary address), is a memory address that is represented in the form of a binary number on the address bus circuitry in order to enable the data bus to access a particular storage cell of main memory, or a register of memory-mapped I/O device. In a computer supporting virtual memory, the term physical address is used mostly to differentiate from a virtual address.

Adresse MAC

Une adresse MAC (de l'anglais Media Access Control), parfois nommée adresse physique, est un identifiant physique stocké dans une carte réseau ou une interface réseau similaire. Elle est unique au monde. Toutes les cartes réseau ont une adresse MAC, même celles contenues dans les PC et autres appareils connectés (tablette tactile, smartphone, consoles de jeux, réfrigérateurs, montres). MAC constitue la partie inférieure de la couche de liaison (couche 2 du modèle OSI). Elle insère et traite ces adresses au sein des trames transmises.