Hola
Los mappings en un sistema de este tipo son en gerenal parciales porque hay operaciones diferentes que actualizan el sistema y en particular los mappings.
En general, en un sistema informático dinámico (a diferencia de lo que pueden ser funciones puramente matemáticas), como una BD, el mapping clave-valor puede cambiar o no tener valor para determinada clave; hay operaciones de alta, baja y modificación asociadas. Luego, no todo el espacio de claves tendrá un valor en determinado momento.
Volviendo a nuestro sistema y la formalización que se pide, en general los mappings los modelamos como parciales ya que hay operaciones definidas que actualizan parcialmente distintas partes del sistema. Para las propiedades en general se puede demostrar algo si las modificaciones realizadas al sistema (operaciones ejecutadas) aseguran el comportamiento deseado, sobre estados válidos.
De paso les dejo a continuación algunos comentarios más sobre las acciones del modelo de virtualización que estamos considerando. Quizás ayude a entender mejor el sistema en su conjunto:
Una de las acciones relevantes en la plataforma es la hcall (llamada al hyper visor). Hay ciertas tareas que los SO comúnmente realizan, pero que no pueden hacer en una plataforma virtualizada, por ejecutar en modo usuario (por ejemp lo, modificar Page Tables, agregar entradas al mapping del hypervisor o cambios de contexto). Estas tareas deben ser realizadas por el hypervisor. Históricamente han habido dos formas de resolver este problema:
1. Full virtualization: El hardware genera una excepción (trap) cuando el SO guest quiere ejecutar una acción privilegiada, que el hypervisor captura, emulando luego el comportamiento de la instrucción.
2. Paravirtualization: Se modifica el código del SO guest para sustituir las instrucciones privilegiadas por llamadas al hypervisor.
Nuestro modelo sigue la segunda opción, ya que está basado en Xen, que es un producto principalmente basado en el paradigma de paravirtualization. Esto se puede ver en la lista de posibles hypercalls de un sistema: new, delete, pin, unpin y lswitch.
El resto de las acciones pueden clasificarse en:
Acciones internas de un SO (silent y lswitch), que o bien no modifican el estado observable, o sólo implican un cambio en la PT actual.
Acceso a páginas de memoria (read y write) de un SO o del hypervisor
Actualización de PT (new y delete) realizadas por el hypervisor para un SO untrusted que lo pidió
Cambios de modo de ejecución (chmod, ret ctrl) que modelan los cambios en el modo de ejecución del procesador y en el componente que está eje cutando (pasar de ejecutar el hypervisor a un SO, o viceversa)
Cambios en el mapping de memoria del hypervisor (pin y unpin), realizados por el hypervisor para un SO que lo pidió. Estas acciones modelan la asignación y liberación de recursos para un SO.
Estas acciones son consistentes con el comportamiento de plataformas de virtualización conocidas, en donde es el hypervisor el que realiza cambios sobre el estado de la memoria virtual (creación, modificación y bajas de PT y de entradas dentro de sus mappings) a pedido del SO. Los SO untrusted no sólo no tienen forma de modificar estos mappings, si no que ni siquiera son capaces de direccionar memoria física directamente (el hardware asegura que se aplique siempre el mapping). Esto implica que, si el hypervisor es capaz de mantener mappings adecuados (disjuntos), los SO sólo podrán acceder a memoria que les pertenece.