Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
La virtualización es una técnica que se utiliza para correr múltiples sistemas operativos en una sola máquina física, pero creando la ilusión de que en realidad cada uno de estos sistemas operativos corre dentro de una Máquina Virtual diferente. El Monitor de Máquinas Virtuales es el encargado de a...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | |
| Formato: | bachelorThesis tesis de grado publishedVersion |
| Lenguaje: | Español |
| Publicado: |
Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
2013
|
| Materias: | |
| Acceso en línea: | http://hdl.handle.net/2133/2815 http://hdl.handle.net/2133/2815 |
| Aporte de: |
| Sumario: | La virtualización es una técnica que se utiliza para correr múltiples sistemas operativos en una sola máquina física, pero creando la ilusión de que en realidad cada uno de estos sistemas operativos corre dentro de una
Máquina Virtual diferente. El Monitor de Máquinas Virtuales es el encargado de administrar los recursos compartidos por los sistemas operativos que corren en las Maquinas Virtuales de manera que todos se puedan ejecutar adecuadamente. En particular, el acceso y uso de la Memoria Principal (i.e. Memoria RAM) es un aspecto crítico que el Monitor de Máquinas Virtuales debe controlar.
En este trabajo se presenta un modelo formal idealizado de un Monitor de Máquinas Virtuales, sobre el cual se demuestran propiedades que garantizan el uso correcto de las acciones provistas por dicho Monitor a los distintos sistemas operativos virtualizados y el correcto acceso y uso de la Memoria Principal por parte de estos sistemas operativos. Además, se utiliza el asistente de pruebas de Coq para las demostraciones y posterior extracción de una versión ejecutable del modelo. |
|---|