P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Juan Manuel Rivara De Leon -
Número de respuestas: 8

Buenas tardes.

Quería hacer una consulta sobre la forma de interpretar afirmaciones sobre mapas parciales en lo que refiere a la existencia de elementos.

En el práctico 7 hay algunas instancias de afirmaciones que hablan sobre propiedades de mapeos, pero no me termina de quedar claro si estas propiedades implican la existencia de las imágenes del mapeo.

Para plantearlo de forma abstracta, supongamos que tenemos las siguientes afirmaciones:

"P1. The map ABMap maps an element of A to an element of B that fulfills BProp"
"P2. The map BCMap maps an element of B that fulfills BProp to an element of C that fulfills CProp"

Y supongamos que tenemos el siguiente código de Coq:


Definition partial a b := a -> option b.
Notation "a ->> b" := (partial a b) (at level 51, right associativity).
Parameter A: Set.
Parameter B: Set.
Parameter C: Set.
Parameter ABMap: A ->> B.
Parameter BCMap: B ->> C.
Parameter BProp: B -> Prop.
Parameter CProp: C -> Prop.
Definition p1v1 := forall (a: A) (b: B), ABMap a = Some b -> BProp b.
Definition p1v2 := forall (a: A), exists (b: B), ABMap a = Some b /\ BProp b.
Definition p2v1 := forall (b: B) (c: C), BProp b -> BCMap b = Some c -> CProp c.
Definition p2v2 := forall (b: B), BProp b -> exists (c: C), BCMap b = Some c /\ CProp c.


Para la afirmación P1:

Tanto p1v1 como p1v2 son diferentes formas de intepretar la afirmación. La única diferencia real entre uno y otro es que p1v2 afirma que el mapeo ABmap está definido para todo elemento de A y (ABMap a) siempre cumple BProp, mientras que v1 solamente afirma que (ABMap a) cumple BProp en el caso de que el mapeo esté definido para a.

Para la afirmación P2:

El caso es similar, p2v1 no supone la existencia del mapeo y solamente afirma que se cumple la afirmación cuando el mapeo esté definido. Por otra parte, p2v2 afirma que (BCMap b) está definido por lo menos si b cumple BProp, y luego (BCMap b) cumple CProp.


Quería consultar entonces cuál de las dos interpretaciones sería la más correcta para este par de situaciones.


Saludos.

En respuesta a Juan Manuel Rivara De Leon

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Carlos Luna -

Hola!

Sobre mappings/funciones parciales:

Dado que en Coq las funciones son totales, una forma de trabajar con una función parcial de un tipo A a un tipo B, es mediante el uso del tipo option (totalizando la función):

Inductive option (T : Type) : Type := 

   Some : T -> option T | None : option T

Definition partial a b := a -> option b.

Notation "a ⇸ b" := (partial a b) (at level 51, right associativity).

Por ejemplo, la memoria sería una mapping parcial y para que vean la forma de trabajar con el tipo option copio abajo el ejemplo del update de la memoria:

  Definition system_memory := madd ⇸ page.

  Definition update mem addr page : system_memory :=

    fun addr' => if madd_eq addr' addr

                 then Some page

                 else mem addr'.

Esta es una forma de trabajar, pero no la única.

Sobre el uso de cuantificadores en las especificaciones que usan funciones parciales, un ejemplo lo di en un mensaje previo (precondición de la operación de lectura), usando un existencial. Esta es una forma conveniente y correcta de establecer condiciones sobre funciones parciales cuando se quiere predicar/raonar sobre valores definidos de la función.

Otro ejemplo (parcialmente):

  Definition va_mapped_to_ma (s : State) (va : vadd) (ma : madd) :=

    exists (curr_os : os)           (* SO actual *)        

           (ph_map : padd ⇸ madd)  (* mappings del HV para el SO actual *)

           (curr_pt_addr : madd)    (* dirección  de la PT del SO actual *)

           (pt : page)              (* PT del SO actual *)

           (vt_map : vadd ⇸ madd), (* mappings de la PT del SO actual *)

      oss s (active_os s) = Some curr_os /\ ...  /\ vt_map va = Some ma.


Saludos, Carlos

En respuesta a Carlos Luna

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Juan Manuel Rivara De Leon -
Hola, sobre el ejemplo de va_mapped_to_ma que mostraste, ¿no habría que considerar todos los sistemas operativos (es decir, todas las imágenes definidas de oss_map), y no solamente el actual?
Saludos.
En respuesta a Juan Manuel Rivara De Leon

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Carlos Luna -

Hola

No, es para el actual; alcanza con esto. 

Determina si una dirección virtual está mapeada a alguna direcicón de máquina para el sistema operativo actual.

Saludos, Carlos

En respuesta a Carlos Luna

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Juan Manuel Rivara De Leon -
Hola otra vez.
Revisando de nuevo el paper me encontré con esta frase: "note that a page might have been created without having been initialized, hence the use of option types." ¿Hace referencia al mapping system_memory: madd ⇸ page?
En caso afirmativo, ¿el mismo razonamiento aplica a todos los mappings parciales? Es decir ¿el valor None representa un resultado asignado pero no inicializado para todos los mappings parciales? En el mismo sentido, ¿esto quiere decir que todos los mappings parciales son eventualmente totalizados?
Saludos.
En respuesta a Juan Manuel Rivara De Leon

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Carlos Luna -

Hola.

La imagen None en un mapping parcial para un cierto valor del dominio indica que no está definido para éste (no quiere decir que está defindo pero no inicializado).

La división en los enteros es una funcion parcial; no está definida para divisor 0. Usando option daria None en este caso.

El tipo option permite en Coq trabajar con estas nociones, totalizando las funciones intrínsecamente parciales, ya que naturalmente el formalismo contempla funciones totales.

Saludos Carlos

En respuesta a Carlos Luna

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Juan Manuel Rivara De Leon -
Ok, entiendo el concepto de función parcial, lo que no me termina de cerrar entonces es el propósito del uso de mapas parciales para algunos casos (que a su vez me genera dudas sobre cuándo puedo afirmar la existencia de una imagen de función parcial en el modelado de propiedades).

Para el caso de mapeos entre memorias, en general entiendo que esto signifique que una dirección en un tipo de memoria (virtual, física, máquina) no tenga correspondencia en una dirección de otra.

Pero para casos como mapas parciales de os_ident me resulta menos claro. ¿Por qué existiría un identificador sin sistema operativo correspondiente (oss_map), o que no tenga un mapeo de su memoria física (hypervisor_map), sin perjuicio de que ese mapeo pueda no estar definido para ninguna dirección física?
En respuesta a Juan Manuel Rivara De Leon

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Juan Manuel Rivara De Leon -
Se me ocurre ahora que estoy considerando que los valores que pertenecen a los conjuntos parametrizados (os_ident, pero también vadd, padd, madd, Hyperv_call, etc) están limitados por los valores que defina el hipervisor. Si se supone que todos estos conjuntos sean en el fondo naturales no acotados (o por lo menos únicamente acotados por el tamaño de la variable donde se almacenan) entonces el mapeo parcial puede tener que ver con control de cotas de estos conjuntos.
En respuesta a Juan Manuel Rivara De Leon

Re: P7 - Consulta por aclaración sobre interpretación de existencia en mapas parciales

de Carlos Luna -

Hola

Los mappings en un sistema de este tipo son en gerenal parciales porque hay operaciones diferentes que actualizan el sistema y en particular los mappings. 

En general, en un sistema informático dinámico (a diferencia de lo que pueden ser funciones puramente matemáticas), como una BD, el mapping clave-valor puede cambiar o no tener valor para determinada clave; hay operaciones de alta, baja y modificación asociadas. Luego, no todo el espacio de claves tendrá un valor en determinado momento.

Volviendo a nuestro sistema y la formalización que se pide, en general los mappings los modelamos como parciales ya que hay operaciones definidas que actualizan parcialmente distintas partes del sistema. Para las propiedades en general se puede demostrar algo si las modificaciones realizadas al sistema (operaciones ejecutadas) aseguran el comportamiento deseado, sobre estados válidos. 

De paso les dejo a continuación algunos comentarios más sobre las acciones del modelo de virtualización que estamos considerando. Quizás ayude a entender mejor el sistema en su conjunto:

Una de las acciones relevantes en la plataforma es la hcall (llamada al hyper visor). Hay ciertas tareas que los SO comúnmente realizan, pero que no pueden hacer en una plataforma virtualizada, por ejecutar en modo usuario (por ejemp lo, modificar Page Tables, agregar entradas al mapping del hypervisor o cambios de contexto). Estas tareas deben ser realizadas por el hypervisor. Históricamente han habido dos formas de resolver este problema: 

1. Full virtualization: El hardware genera una excepción (trap) cuando el SO guest quiere ejecutar una acción privilegiada, que el hypervisor captura, emulando luego el comportamiento de la instrucción. 

2. Paravirtualization: Se modifica el código del SO guest para sustituir las instrucciones privilegiadas por llamadas al hypervisor. 

Nuestro modelo sigue la segunda opción, ya que está basado en Xen, que es un producto principalmente basado en el paradigma de paravirtualization. Esto se puede ver en la lista de posibles hypercalls de un sistema: new, delete, pin, unpin y lswitch. 

El resto de las acciones pueden clasificarse en: 

Acciones internas de un SO (silent y lswitch), que o bien no modifican el estado observable, o sólo implican un cambio en la PT actual. 

Acceso a páginas de memoria (read y write) de un SO o del hypervisor 

Actualización de PT (new y delete) realizadas por el hypervisor para un SO untrusted que lo pidió 

Cambios de modo de ejecución (chmod, ret ctrl) que modelan los cambios en el modo de ejecución del procesador y en el componente que está eje cutando (pasar de ejecutar el hypervisor a un SO, o viceversa) 

Cambios en el mapping de memoria del hypervisor (pin y unpin), realizados por el hypervisor para un SO que lo pidió. Estas acciones modelan la asignación y liberación de recursos para un SO. 

Estas acciones son consistentes con el comportamiento de plataformas de virtualización conocidas, en donde es el hypervisor el que realiza cambios sobre el estado de la memoria virtual (creación, modificación y bajas de PT y de entradas dentro de sus mappings) a pedido del SO. Los SO untrusted no sólo no tienen forma de modificar estos mappings, si no que ni siquiera son capaces de direccionar memoria física directamente (el hardware asegura que se aplique siempre el mapping). Esto implica que, si el hypervisor es capaz de mantener mappings adecuados (disjuntos), los SO sólo podrán acceder a memoria que les pertenece.