Hola,
Tenemos una duda sobre este predicado. Cual es exactamente la función del mismo? No debería depender del state? Sino como se chequea si es accesible o no?
Muchas gracias
Saludos.
Hola.
Como se indica en el paper, hay direcciones virtuales que son accesibles por los sistemas operativos y otras que están reservadas para uso por parte del hypervisor.
En el archivo State.v esto está contemplado en el Record context: ctxt_vadd_accessible: vadd -> bool. Esta función no varía para cada OS ni depende del estado del sistema.
Luego, las direcciones virtuales accesibles por los OSs es global. En tal sentido, el predicado va_accesible del paper refiere a si va es accesible por "algún" OS. La idea en la precondición del read (con dicho predicado) es decir que un OS no puede leer direcciones de memoria que están reservadas para el hypervisor.
Saludos, Carlos
Hola,
Entonces deberiamos de pasarle el context al predicado? o se define como parameter?
Muchas gracias.
Saludos
Podés definir:
Parameter ctxt : context.
Saludos, Carlos