Hola, ¿Hay que considerar los casos de error? Es decir cuando al aplicar el mapping nos da error. O sea que el índice no esté en el mapping.
Saludos,
Jairo.
En respuesta a Jairo Yamil Bonanata Silva
Re: [Práctico 7] Ej5 - Regla v - casos de error
de Carlos Luna -
Hola.
Al escribir la propiedad predicás, en realidad, sobre casos válidos (que no dan error).
Saludos, Carlos
En respuesta a Carlos Luna
Re: [Práctico 7] Ej5 - Regla v - casos de error
Hola.
Me quedó la duda en esta regla si tenemos que para toda dirección física del SO podemos exigir que siempre esté mapeado a una dirección de máquina que le pertenece. Yo lo implementé de esta forma. Es decir, exijo que para toda dirección física del so exista siempre una dirección de máquina que se mapea por el hipervisor para esa dirección física. ¿Es correcto esto?
Saludos,
Jairo.
En respuesta a Jairo Yamil Bonanata Silva
Re: [Práctico 7] Ej5 - Regla v - casos de error
de Carlos Luna -
Si, es correcto.
Saludos, Carlos
En respuesta a Carlos Luna
Re: [Práctico 7] Ej5 - Regla v - casos de error
Hola.
No me queda del todo claro lo que se pide en la propiedad v de valid_state y me estoy mareando con los cuantificadores a usar.
El paper dice:
"the hypervisor maps an OS physical address to a machine address owned by that same OS. This mapping is also injective"
esto quiere decir que:
para cualquier osi os_ident
para cualesquiera pa dirección física, ma dirección de máquina, pa_to_ma mapeo de direciones físicas a direcciones de máquina, pg página
si tengo un mapeo pa => ma => pg entonces
pg tiene que ser de osi
o
para cualquier osi os_ident
para cualesquiera pa dirección física
si existe pa_to_ma mapeo de direciones físicas a direcciones de máquina
Y
existe una ma dirección de máquina, tal que pa=>ma
Y
existe una pg página, tal que ma=>pg
entonces
pg tiene que ser de osi
¿o ninguna de estas opciones? ¿o las opciones son equivalentes? (primero me pareció que sí, después que no).
Soy conciente de que la primera opción no usa el existencial en ma que menciona Jairo, pero tal vez por las restricciones que se le imponen luego igual es correcto.
Muchas gracias y pido disculpas si es demasiado explícita la pregunta.
Saludos
En respuesta a Romina Diana Romero Riva
Re: [Práctico 7] Ej5 - Regla v - casos de error
de Carlos Luna -
Hola.
La primera opción podría ser; supongo que el mapeo pa_to_ma involucra al osi que aparece al final.
Entiendo que hay otras formas de expresar esto (en particular si se establece que la ma en el mapeo del hipervisor debería existir). Vamos a ser flexibles con las distintas variantes; más teniendo en cuenta que falta un día para la entrega y la mitad ya entregó el caso de estudio.
Saludos, Carlos
En respuesta a Carlos Luna
Re: [Práctico 7] Ej5 - Regla v - casos de error
Muchas gracias.
Sí, pa_to_ma involucra a osi.
Saludos.