Buenas,
estamos teniendo problemas para resolver como el predicado va_mapped_to_ma.
No sabemos si debemos buscar en el estado (State) que se pasa como parametro con el vadd que nos pasan,y asi matchear con el madd que tambien se pasa como parametro.
Cualquier ayuda sirve,
Muchas gracias.
Miguel
Hola.
va_mapped_to_ma expresa que la dirección virtual va está mapeada en la memoria a una dirección de máquina ma para un OS en un estado dado.
Saludos, Carlos
Hola,
gracias por tu respuesta,
en si, comprendemos la semantica de dicho predicado, lo que no sabemos es si estamos haciendo bien la construccion del mismo.
Por un lado tenemos que siendo s:State podemos definir a el page_content de esta manera => ((s.(memory) ma).(page_content))
que puede ser de tipo RW, PT u Other.
En caso de que fuera PT ahi es donde tenemos el mappeo de vadd->madd, pero primero debemos "matchear" el tipo para que coincida con PT, o me equivoco?
Y por otro lado, en el foro, en años anteriores lei que se necesitaba tambien el curr_page que es de tipo padd, pero la direccion fisica para que serviria en este caso? Es para mappear primero de direcciones fisicas a direcciones de maquina, o no es necesario?
Muchas gracias y perdon por la pregunta tan larga.
No te equivocás; tenés que ver que es de tipo PT.
Lo que mencionás de la current page table sirve para definir el predicado. Esto es, ver que va está mapeada a ma en la current page table (que cada OS guarda en cierta dirección física) del OS en cuestión.
Aunque la de abajo puede variar según como cada quien modeló las cosas, analizar esta definición seguramente te ayude a entender mejor varias de las cosas que entiendo están relacionadas a tu pregunta (y al modelo de memoria en los estados representados). Esta ayudita no se volverá a repetir :) :
Definition va_mapped_to_ma (s : state) (osi : os_ident) (va: vadd) (ma : madd) : Prop :=
exists map_padd_madd,
Value _ map_padd_madd = map_apply os_ident_eq (hypervisor s) osi /\
exists os,
Value _ os = map_apply os_ident_eq (oss s) osi /\
exists madd,
Value _ madd = map_apply padd_eq map_padd_madd (curr_page os) /\
exists page,
Value _ page = map_apply madd_eq (memory s) madd /\
exists map_vadd_madd,
PT map_vadd_madd = (page_content page) /\
Value vadd ma = map_apply vadd_eq map_vadd_madd va.
Saludos, Carlos
Muchisimas gracias Carlos,
fue de mucha utilidad tu respuesta, y nos ayudo a pasar en limpio varias cosas que estabamos haciendo.
Te mando un saludo.
Miguel.
