Dureza computacional de los programas informáticos "reales"

A menudo escuché decir que no se puede escribir un programa para detectar errores en un navegador web, procesador de texto o sistema operativo, debido al Teorema de Rice: cualquier propiedad semántica para un lenguaje completo de Turing es indecidible.

Sin embargo, no estoy seguro de hasta qué punto esto se aplica a los programas operativos del mundo real como los sistemas operativos. ¿Estos tipos de programas necesitan toda la fuerza de la integridad de Turing? ¿Existen modelos más simples de cómputo (como PR) en los que podrían escribirse estas aplicaciones? Si es así, ¿en qué medida esto permite la capacidad de decisión de la corrección del programa?

Ciertamente puede escribir programas que detectan errores: hay una comunidad grande y activa de personas que escriben programas para hacer exactamente eso. Sin embargo, lo que el teorema de Rice le impide hacer es escribir captadores de errores que sean sólidos y completos (es decir, atrapar todos los errores de una determinada clase sin falsos positivos).

Dicho esto, las restricciones ingenuas sobre el modelo de cómputo en realidad no te ayudan mucho a mejorar la practicidad del análisis del programa. La razón es que puede obtener programas que hacen "casi lo mismo" girando los bucles while

while P do 
   C

en bucles for con una gran constante de iteración:

for i = 0 to BIGNUM do 
  if P then 
    C
  else
    break

Ahora, este programa ni siquiera necesita toda la fuerza del recursivo primitivo (ya que el bucle for puede expandirse macro en una gran instrucción anidada if-then-else), pero en la mayoría de los casos prácticos se comportará igual que antes. Tenga en cuenta que, en teoría, ayuda a la capacidad de decisión: el programa es total, por lo que puede responder preguntas ejecutando el programa y viendo qué sucede. Esto no es lo que realmente queremos, que es obtener respuestas más rápido que ejecutar el programa: la terminación artificial introducida en realidad no ayuda al análisis del programa en la práctica, ya que los errores ocurren debido a errores en la lógica real del programa, y ​​no hemos ' No toqué eso en absoluto.

$\epsilon_0$

Dado que usted preguntó acerca de la corrección de los programas del mundo real, como los sistemas operativos, es posible que le interese el proyecto seL4 ( revista , pdf , conferencia ).

El equipo de NICTA tomó un microkernel de tercera generación de 8700 líneas de C y 600 líneas de ensamblador implementadas de acuerdo con una especificación abstracta en Haskell. Proporcionaron una prueba formal verificada a máquina (en Isabelle / HOL) de que la implementación sigue estrictamente la especificación. De este modo, se demuestra que su programa no tiene errores.

Entonces, al igual que el problema de detención, aunque no se puede resolver en general, se puede resolver en algunos casos específicos. En este caso, aunque no puede probar que el código C arbitrario esté libre de errores, podrían hacerlo en el caso del microkernel seL4.

Las preguntas que haces son en realidad bastante diferentes.

Sin embargo, no estoy seguro de hasta qué punto esto se aplica a los programas operativos del mundo real como los sistemas operativos. ¿Estos tipos de programas necesitan toda la fuerza de la integridad de Turing?

Se necesita muy poco para que un modelo de computación se complete en Turing. Por ejemplo, varios modelos con contadores pueden simular máquinas de Turing. Si cree que su software requiere más de dos contadores que puede manipular arbitrariamente, está utilizando un lenguaje completo de Turing. Aunque los enteros de la máquina están limitados a priori, las estructuras de datos asignadas al montón generalmente no lo están. Si su software necesita listas, árboles y otros datos asignados dinámicamente, está utilizando un lenguaje completo de Turing.

¿Existen modelos más simples de cómputo (como PR) en los que podrían escribirse estas aplicaciones? Si es así, ¿en qué medida esto permite la capacidad de decisión de la corrección del programa?

Es importante reconocer que no queremos verificar las propiedades arbitrarias de nuestro software. La comprobación de propiedades muy específicas y estrechas (sin desbordamientos de búfer, sin desreferencias de puntero nulo, sin bucles infinitos, etc.) mejora enormemente la calidad y la usabilidad del software. En teoría, tales problemas aún son indecidibles. En la práctica, enfocarnos en propiedades específicas nos permite descubrir estructuras en nuestros programas que a menudo podemos explotar para resolver el problema.

En particular, puede modificar su pregunta original para

¿Existe una abstracción de mi software que pueda analizar eficientemente en un modelo completo que no sea de Turing?

Una abstracción es un modelo que incluye el comportamiento del software original y posiblemente muchos comportamientos adicionales. Hay modelos como máquinas de un contador o sistemas pushdown que no están completos y que podemos analizar. El enfoque estándar en la verificación de programas con herramientas automatizadas es construir una abstracción en dicho modelo y verificarla algorítmicamente.

Hay aplicaciones en las que las personas se preocupan por las propiedades sofisticadas de su hardware o software. Las compañías de hardware quieren que sus chips implementen correctamente algoritmos aritméticos, las compañías automotrices y de aviónica quieren un software certificablemente correcto. Si es tan importante, es mejor usar un ser humano (entrenado).