[Practico 7] - Ejercicio 5 - propiedad v

[Practico 7] - Ejercicio 5 - propiedad v

de Bruno Rolando Boz -
Número de respuestas: 3

Buenas,

Respecto a la propiedad en referencia:

1- ¿Debería verificar que el hipervisor este corriendo para el caso que la pagina actual pertenezca al hipervisor o predico solo para el caso que hay un os corriendo?

2- ¿Debo considerar el caso que la pagina actual no tenga dueño o es un caso de error para el cual el predicado no debería ser cierto?

Gracias.

En respuesta a Bruno Rolando Boz

Re: [Practico 7] - Ejercicio 5 - propiedad v

de Carlos Luna -

Hola

Sobre 1, no importa quien esté corriendo. Lo relevante es the "hypervisor maps an OS physical address to a machine address owned by that same OS. This mapping is also injective"

Sobre 2: no. Predicás sobre lo que querés que pase.

Para ayudar un poco, la propiedad v podría tener la siguiente pinta:

Definition valid_state_v (s : state) :=

  forall o : os_ident,

    exists (pa : padd) (ma : madd) (p : page) (map : padd -> option madd),

       hypervisor s o = Some map

    /\ map pa = Some ma

    /\ memory s ma = Some p

    /\ page_owned_by p = Os o

    /\ ... (** Inyectividad*)

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Practico 7] - Ejercicio 5 - propiedad v

de Bruno Rolando Boz -
Trabajando en el ejercicio 7 he vuelto a repensar esta función. ¿No debería pa estar cuantificado universalmente en vez de existencialmente? Es decir, yo quiero que para todo SO y para toda dirección física pa de ese SO exista una dirección de maquina ma tal que el hipervisor mapee pa en ma y que la pagina ubicada en ma pertenezca al SO.
En respuesta a Bruno Rolando Boz

Re: [Practico 7] - Ejercicio 5 - propiedad v

de Carlos Luna -

Hola.

En realidad se puede demostrar de ambas formas (existe y es única), asi que elegí. Es correcto cuantificar la deirección física universalmente.

Saludos, Carlos