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

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Chimento, Jesús Mauricio M.
Otros Autores: Luna, Carlos D.
Formato: bachelorThesis tesis de grado publishedVersion
Lenguaje:Español
Publicado: Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario 2013
Materias:
Virtualización
Máquina Virtual
Monitor de Máquinas Virtuales
Hypercall
Modelo Idealizado
Acceso en línea:http://hdl.handle.net/2133/2815
http://hdl.handle.net/2133/2815
Aporte de:
Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR) de Universidad Nacional de Rosario
id I15-R121-2133-2815
record_format dspace
institution Universidad Nacional de Rosario
institution_str I-15
repository_str R-121
collection Repositorio Hipermedial de la Universidad Nacional de Rosario (UNR)
language Español
orig_language_str_mv spa
topic Virtualización
Máquina Virtual
Monitor de Máquinas Virtuales
Hypercall
Modelo Idealizado
spellingShingle Virtualización
Máquina Virtual
Monitor de Máquinas Virtuales
Hypercall
Modelo Idealizado
Chimento, Jesús Mauricio M.
Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
topic_facet Virtualización
Máquina Virtual
Monitor de Máquinas Virtuales
Hypercall
Modelo Idealizado
description 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.
author2 Luna, Carlos D.
author_facet Luna, Carlos D.
Chimento, Jesús Mauricio M.
format bachelorThesis
tesis de grado
publishedVersion
author Chimento, Jesús Mauricio M.
author_sort Chimento, Jesús Mauricio M.
title Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
title_short Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
title_full Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
title_fullStr Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
title_full_unstemmed Análisis de modelos de memoria en plataformas de virtualización. Formalización de un prototipo funcional de plataforma con Cache y Tlb
title_sort análisis de modelos de memoria en plataformas de virtualización. formalización de un prototipo funcional de plataforma con cache y tlb
publisher Facultad de Ciencias Exactas, Ingeniería y Agrimensura. Universidad Nacional de Rosario
publishDate 2013
url http://hdl.handle.net/2133/2815
http://hdl.handle.net/2133/2815
work_keys_str_mv AT chimentojesusmauriciom analisisdemodelosdememoriaenplataformasdevirtualizacionformalizaciondeunprototipofuncionaldeplataformaconcacheytlb
bdutipo_str Repositorios
_version_ 1764820413697753091

Ejemplares similares