[Práctico 7] Ejericio 7

[Práctico 7] Ejericio 7

de Andres Fulloni Papaleo -
Número de respuestas: 4
Buenas, estamos teniendo un problema con la prueba.

Leímos que se sugiere utilizar las propiedades V y VI de valid state pero creemos que tenemos algo mal en la definición de la propiedad V, ya que al quererla utilizar en la prueba, no podemos porque no tenemos ninguna variable de tipo padd.

La propiedad V la definimos razonando lo siguiente: para todo OS y para toda dir fisica, existe una dir máquina, un mapeo y una página tal que la dir física está mapeada a la dir máquina y en la dir máquina se encuentra dicha página la cual tiene page_owned_by = OS.

Está bien ese razonamiento?

Gracias.




En respuesta a Andres Fulloni Papaleo

Re: [Práctico 7] Ejericio 7

de Carlos Luna -
Hola.


En la prueba de Read Isolation la idea puede ser en una parte usar V para concluir que el OS activo es dueño de la page table. Recordar que en el estado hay un mapping que a cada identificador de OS asigna la información dinámica de este. Por ejemplo:

Record os : Set :=

  OpSys

  {

    (* Page table actual *)

    curr_page : padd;

    (* Si tiene una hypercall pendiente *)

    hcall : option Hyperv_call

  }.


Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 7] Ejericio 7

de Andres Fulloni Papaleo -

Gracias por la respuesta Carlos. Entendemos lo que decis. Pudimos probarlo sólo con la propiedad VI pero formulándola de la siguiente manera:

para todo vadd, osi y madd: si la vadd es accesible entonces

         existe un mapping vadd-madd tal que la vadd esta mapeada con la ma y

             existe pagina ....

Lo que no nos queda claro es si está bien decir que "para todo madd", o si debería ser "existe madd".

Por otro lado, intentamos obtener el record OpSys al que te referiste pero no vemos como tratar el caso en que el map_apply de error:

Definition obtener_os (s1: State): os :=
                                     match map_apply os_ident_eq (oss s1) (active_os s1) with
                                      | Value _ o => o
                                      | Error _ _ => ??
                                     end.

Qué se podría poner ahí?

Gracias.

En respuesta a Andres Fulloni Papaleo

Re: [Práctico 7] Ejericio 7

de Carlos Luna -

Hola.

Lo primero está bien, ya que si bien madd está cuantificada universalmente, aparece en un implica y tiene que cumplir un predicado sobre una mappíng (mapping vadd-madd) cuantificado existencialmente.

Sobre lo segundo, no usaría la función obtener_os ya que deberías estar en un contexto en el cual el caso de error no aplica. De todas maneras, si lo probaste con lo primero entonces ya está!

Saludos, Carlos