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 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.