felix - osgi service

¿El problema de resolución en OSGi NP-Complete?

Question

El problema de resolución se describe en el capítulo de modularidad de la especificación del núcleo OSGi R4. Es un problema de satisfacción de restricciones y ciertamente un problema difícil de resolver de manera eficiente, es decir, no por la fuerza bruta. Las principales complicaciones son la restricción de usos, que tiene efectos no locales, y la libertad de abandonar las importaciones opcionales para obtener una resolución exitosa.

NP-Completeness se trata en elsewhere en StackOverflow.

Ya ha habido mucha especulación sobre la respuesta a esta pregunta, así que evite la especulación. Las buenas respuestas incluirán una prueba o, en su defecto, un argumento informal convincente.

La respuesta a esta pregunta será valiosa para aquellos proyectos que crean resolutores para OSGi, incluidos los proyectos de código abierto Eclipse Equinox y Apache Felix, así como para la comunidad OSGi en general.

Answer 1

De memoria, pensé que este documento contenía la demostración, perdón por no haberlo comprobado antes. Aquí hay otro enlace que quise copiar y estoy seguro que proporciona una demostración en la página 48: http://www.edos-project.org/bin/download/Main/Deliverables/edos%2Dwp2d1.pdf

Answer 2

Este documento proporciona una demostración: http://www.cse.ucsd.edu/~rjhala/papers/opium.html

Answer 3

Sí.

El enfoque adoptado por el artículo edos que Pascal citó se puede hacer para trabajar con OSGi. A continuación, le mostraré cómo reducir cualquier instancia 3-SAT a un problema de resolución de paquetes OSGi. Este sitio no parece admitir la notación matemática, por lo que usaré el tipo de notación que es familiar para los programadores.

Aquí hay una definición del problema 3-SAT que estamos tratando de reducir:

Primero defina A para que sea un conjunto de átomos proposicionales y sus negaciones A = {a (1), ..., a (k), na (1), ..., na (k)}. En un lenguaje más simple, cada a (i) es un booleano y definimos na (i) =! A (i)

Luego, las instancias 3-SAT S tienen la forma: S = C (1) &… & C (n)

donde C (i) = L (i, 1) | L (i, 2) | L (i, 3) y cada L (i, j) es un miembro de A

Resolver una instancia particular de 3-SAT implica encontrar un conjunto de valores, verdadero o falso para cada a (i) en A, de manera que S se evalúe como verdadero.

Ahora definamos los paquetes que usaremos para construir un problema de resolución equivalente. A continuación, todas las versiones de paquetes y paquetes son 0 y los rangos de versiones de importación no están restringidos, excepto donde se especifique.

• Toda la expresión S estará representada por Bundle BS
• Cada cláusula C (i) estará representada por un paquete BC (i)
• Cada átomo a (j) estará representado por un paquete BA (j) versión 1
• Cada átomo negado na (j) estará representado por un paquete BA (j) versión 2

Ahora para las restricciones, comenzando con los átomos:

BA (j) versión 1
-exportación del paquete PA (j) versión 1
-para cada cláusula C (i) que contiene el átomo a (j) exportar PM (i) y agregar PA (j) a la directiva de usos de PM (i)

BA (j) versión 2
-exportar paquete PA (j) versión 2
-para cada cláusula C (i) que contiene el átomo negado na (j) exportar PM (i) y agregar PA (j) a la directiva de usos de PM (i)

BC (i)
-exportación a PC (i)
-importar PM (i) y agregarlo a la directiva de usos de PC (i)
-para cada átomo a (j) en la cláusula C (i) opcionalmente importe PA (j) versión [1,1] y agregue PA (j) a la directiva de usos de la PC (i) exportación
-para cada átomo na (j) en la cláusula C (i) opcionalmente importe PA (j) versión [2,2] y agregue PA (j) a la directiva de usos de la PC (i) exportación

BS
-no exportaciones
-para cada cláusula C (i) importar PC (i)
-para cada átomo a (j) en una importación PA (j) [1,2]

Unas pocas palabras de explicación:

Las relaciones AND entre las cláusulas se implementan haciendo que BS importe desde cada BC (i) un paquete PC (i) que solo sea exportado por este paquete.

La relación OR funciona porque BC (i) importa el paquete PM (i) que solo es exportado por los paquetes que representan a sus miembros, por lo que al menos uno de ellos debe estar presente, y porque opcionalmente importa alguna versión de PA (j) x de cada uno paquete que representa a un miembro, un paquete exclusivo de ese paquete.

La relación NO entre la versión 1 de BA (j) y la versión 2 de BA (j) se impone mediante restricciones de uso . BS importa cada paquete PA (j) sin restricciones de versión, por lo que debe importar la versión 1 de PA (j) o la versión 2 de PA (j) para cada j. Además, las restricciones de uso aseguran que cualquier PA (j) importada por un paquete de cláusulas BC (i) actúe como una restricción implícita en el espacio de clase de BS, por lo que BS no puede resolverse si ambas versiones de PA (j) aparecen en su implícito restricciones Así que solo una versión de BA (j) puede estar en la solución.

Por cierto, hay una forma mucho más fácil de implementar la relación NOT: solo agregue la directiva singleton: = true a cada BA (j). No lo he hecho de esta manera porque la directiva singleton rara vez se usa, por lo que parece ser una trampa. Solo lo menciono porque, en la práctica, ningún marco OSGi que conozco implementa las restricciones de paquetes basados ​​adecuadamente en las importaciones opcionales, por lo que si realmente creara paquetes utilizando este método, probarlos podría ser una experiencia frustrante.

Otras observaciones:

Una reducción de 3-SAT que no usa importaciones opcionales también es posible, aunque esto es más largo. Básicamente, implica una capa adicional de paquetes para simular la opcionalidad utilizando versiones. Una reducción de 1 en 3 SAT es equivalente a una reducción a 3-SAT y parece más simple, aunque no lo he superado.

Aparte de las pruebas que usan singleton: = true, todas las pruebas que conozco dependen de la transitividad de las restricciones de uso. Tenga en cuenta que tanto singleton: = true como transitivo son restricciones no locales.

La prueba anterior en realidad muestra que el problema de resolución OSGi es NP-Completo o peor. Para demostrar que no es peor, debemos demostrar que cualquier solución al problema puede verificarse en tiempo polinomial. La mayoría de las cosas que deben verificarse son locales, por ejemplo, mirando cada importación no opcional y verificando que esté conectada a una exportación compatible. Verificando esto es O (num-local-restricciones). Restricciones basadas en singleton: = true deben ver todos los paquetes de singleton y verificar que no haya dos que tengan el mismo nombre simbólico. El número de comprobaciones es menor que los paquetes de números . La parte más complicada es verificar que se cumplan las restricciones de uso. Para cada paquete, esto implica recorrer el gráfico de usos para reunir todas las restricciones y luego verificar que ninguno de estos esté en conflicto con las importaciones del paquete. Cualquier algoritmo de caminata razonable volvería atrás cuando se encontrara con un cable o use una relación que había visto antes, por lo que el número máximo de pasos en la caminata es (num-wires-in-framework + num-uses-in framework). El costo máximo de verificar que una conexión o uso no se haya recorrido antes es menor que el registro de esto. Una vez que se han recopilado los paquetes restringidos, el costo de la verificación de consistencia para cada paquete es menor que num-imports-in-bundle num-exports-in-framework. Todo aquí es un polinomio o mejor.