El equipo de dqlite en Canonical, formado por Marco Manino y Alberto Carretero, ha analizado un error de larga duración presente en el motor de base de datos SQLite desde 2010, cuya corrección se publicó en la versión 3.51.3. El fallo reside en la fase de checkpoint del modo Write Ahead Log (WAL) y, en determinadas condiciones, puede provocar la corrupción de la base de datos. Aunque su impacto en entornos reales es muy bajo, el equipo destaca que el defecto permaneció oculto durante 16 años y resulta extremadamente difícil de reproducir, lo que lo convierte en un caso de estudio sobre la complejidad de los sistemas de almacenamiento.
Para investigar el problema, los autores recurren a TLA+, un lenguaje de especificación formal que permite modelar el comportamiento concurrente de SQLite. En el artículo se explica la anatomía del WAL y de los checkpoints, describiendo las dos cerraduras implicadas (CKPT_LOCK y WRITE_LOCK) y los campos clave de la memoria compartida, como walSalt, mxFrame y nBackfill. A partir de ese modelo, el equipo reproduce la traza que desencadena la corrupción y, en una segunda fase, construye un modelo específico del uso que dqlite hace de SQLite para determinar si la biblioteca distribuida puede verse afectada por el mismo escenario. El trabajo ilustra cómo la verificación formal con TLA+ sirve para diagnosticar bugs casi imposibles de detectar mediante pruebas tradicionales, ofreciendo una metodología aplicable a otros proyectos de almacenamiento y replicación.