Algunos de los fallos más peligrosos de los sistemas pueden detectarse antes de escribir el código, si el diseño mismo se trata como un sistema susceptible de análisis. Este es el eje de la presentación de Hillel Wayne, quien explica cómo los principios de los métodos formales ayudan a examinar sistemas futuros y detectar problemas de resiliencia, concurrencia y fallos antes de que se conviertan en errores operativos.
Wayne comienza con un ejemplo simplificado de lo que denomina «ejecutor de tareas»: el sistema comprueba si la tarea se ha completado, después marca la tarea como completada y, a continuación, ejecuta la tarea. La secuencia parece lógica, pero se desmorona cuando se produce un fallo durante la ejecución. El sistema puede volver a intentarlo después de registrar la tarea como completada, por lo que la tarea no llega a ejecutarse realmente. Al trasladar el registro de finalización a después de la ejecución aparece otro problema: dos ejecutores concurrentes pueden ejecutar la misma tarea dos veces antes de que cualquiera de ellos registre que se ha completado.
No se trata solo de un problema teórico; la presentación lo relaciona con ejemplos como los sistemas de envío de paquetes, que podrían enviar el pedido dos veces; los sistemas de programación, que podrían reservar la misma cita para dos personas; y los mecanismos de instalación de aplicaciones, que podrían adoptar un comportamiento destructivo al repetir la solicitud.
Empieza por definir qué significa «correcto»
Wayne propone formular los requisitos del sistema como propiedades binarias: o son verdaderas o son falsas. Entre los ejemplos se encuentra que la tarea no se ejecute más de una vez, una propiedad de seguridad que impide que ocurra algo malo, y que la tarea se ejecute al menos una vez, una propiedad de vivacidad que garantiza que ocurra algo deseado.
La presentación subraya que las propiedades no tienen todas la misma fuerza. Un sistema capaz de procesar 10.000 consultas por segundo cumple automáticamente la propiedad de procesar dos consultas por segundo, pero lo contrario no es cierto. Por ello, superar una propiedad fuerte puede ser una prueba de la corrección de un conjunto de propiedades más débiles, mientras que el fallo de una propiedad más débil ayuda a acotar el origen del problema. Wayne relaciona esta idea con la pirámide de pruebas: muchas pruebas unitarias pueden ser más útiles para diagnosticar el error que un número limitado de pruebas de extremo a extremo.
El modelo simplificado revela el problema fundamental
En lugar de representar el sistema con todos sus detalles, Wayne invita a construir un modelo abstracto que incluya el mínimo estado necesario: la fase actual del algoritmo, si la tarea está marcada como completada y el número de veces que se ha ejecutado. Esto permite explorar los estados posibles y las rutas que el sistema puede seguir, incluidos los estados de fallo y los reintentos.
En los métodos formales, este modelo y sus propiedades pueden codificarse mediante fórmulas lógicas y examinarse con herramientas como los comprobadores de modelos y los solucionadores SMT. Sin embargo, la idea práctica de la presentación no exige utilizar directamente estas herramientas; el ingeniero puede adoptar la misma forma de pensar siguiendo los estados y las transiciones posibles.
El factor «adversario» en la concurrencia y los fallos
Wayne propone imaginar cada fuente de indeterminismo, como la entrada del usuario, la concurrencia, la aleatoriedad, los tiempos de espera y las interrupciones de los servidores, como un «adversario» que siempre elige el peor resultado posible. Si el sistema puede reintentar indefinidamente, este adversario elegirá el fallo cada vez, lo que revela que la propiedad de vivacidad no está garantizada aunque el éxito sea teóricamente posible.
También explica que la existencia de dos ejecutores concurrentes exige representar algunas variables como locales para cada proceso y otras como compartidas entre el sistema y el mundo exterior. Al explorar las distintas secuencias de ejecución se puede llegar a un estado en el que la tarea se ejecuta dos veces, incluso cuando cada ejecutor parece correcto por separado.
Las suposiciones forman parte del diseño
La corrección del sistema no depende únicamente de sus propiedades, sino también de las suposiciones sobre el entorno en el que funciona. Un diseño puede requerir la suposición fuerte de que el proceso nunca falla, mientras que otro puede funcionar si el fallo ocurre un número limitado de veces. Wayne señala que reordenar los pasos puede reducir las suposiciones de vivacidad, pero aumentar los requisitos de seguridad, como la necesidad de garantizar que solo haya un ejecutor al mismo tiempo.
La situación también cambia cuando cambia el entorno operativo. Depender de una consistencia fuerte en una base de datos y después pasar a una consistencia eventual puede hacer que propiedades que antes eran ciertas dejen de estar garantizadas, aunque el código del sistema no cambie. Por ello, las suposiciones sobre el proveedor del servicio o la base de datos no deben considerarse detalles externos; son condiciones directas para la corrección del diseño.
¿Qué cambia en la práctica?
El valor práctico del enfoque no reside en sustituir las pruebas ni en recomendar el uso de herramientas formales en todos los proyectos, sino en hacer más rigurosas las preguntas de diseño: ¿cuáles son los estados posibles? ¿Cuál es la peor secuencia de acontecimientos? ¿Qué controlamos realmente? ¿Y qué suposiciones no puede garantizar el equipo? Cuanto más fuerte sea la propiedad requerida o menos predecible sea el entorno, más complejo deberá ser el diseño del sistema, o habrá que relajar la propiedad exigida, por ejemplo, transformando la condición de «procesar todos los mensajes» en «procesar los mensajes o enviarlos a una cola de mensajes muertos».
Wayne presenta estas ideas como herramientas de pensamiento derivadas de los métodos formales, no como un sustituto listo para usar del criterio de ingeniería. La pregunta abierta en cada sistema sigue siendo hasta qué punto son precisos el modelo y las suposiciones utilizadas; si se omite un estado o el equipo da por supuesto un comportamiento que el entorno no garantiza, el análisis puede demostrar la corrección de un modelo que no se parece al sistema real.