
Marco de pruebas de corrección transaccional basado en Jepsen para DuckDB, detectando anomalías de aislamiento como violaciones G2-item y SSI mediante cargas de trabajo aleatorias y el verificador Elle.
Pruebas Jepsen para la base de datos DucKDB. Se ejecuta localmente, en lugar de en un clúster remoto. La prueba genera una colección de procesos locales que abren un archivo DuckDB localmente e interactúa con ellos a través de STDIN/STDOUT.
Este es un prototipo temprano. Se enciende, ejecuta transacciones, verifica su corrección e informa errores, pero no estoy seguro de si esos errores son reales.
Necesitarás un JDK (21+), Git, Gnuplot, Graphviz, además de Leiningen. A diferencia de la mayoría de las pruebas Jepsen, esto se ejecuta completamente en local; no necesitas un clúster de máquinas, claves SSH, etc.
sudo apt install openjdk leiningen gnuplot graphviz
brew install openjdk leiningen gnuplot graphviz
Para ejecutar una prueba, intenta:
lein run test
DuckDB proporciona (sospecho) Strong SI por defecto, y eso es lo que la prueba verifica. Sin embargo, sí permite G2-item, lo que viola Repeatable Read. Para demostrarlo, intenta:
lein run test --time-limit 10 --expected-consistency-model serializable --max-writes-per-key 8
Estamos pidiendo probar durante diez segundos, para buscar violaciones de Serializabilidad, y (para generar ejemplos pequeños y legibles), escribir solo 8 elementos por clave. Los ejemplos de G2-item deberían estar disponibles en store/latest/elle/G2-item.
Hay varias opciones de ajuste disponibles. La ayuda para las distintas opciones está disponible mediante lein run test --help.
Los resultados de las pruebas se escriben en store/<test-name>/<date>/, y se enlazan simbólicamente como store/latest. Cada uno de estos directorios de prueba es autocontenido; puedes copiarlo, comprimirlo, analizarlo más tarde, eliminarlo, etc. También puedes ejecutar un servidor web para explorar los resultados.
lein run serve
Hay un REPL disponible; consulta lein repl.
El entorno de pruebas reside en este directorio; su archivo de proyecto es project.clj, su código fuente está en src/, etc.
El entorno de pruebas ejecuta un programa separado, el "nodo local", que incrusta la biblioteca DuckDB y realiza transacciones contra ella. El entorno de pruebas genera transacciones aleatorias para una carga de trabajo determinada, las envía por HTTP al nodo local y registra los resultados de esas transacciones, verificando al final varias anomalías transaccionales. Buscamos Strong Snapshot Isolation, utilizando el verificador Elle (https://github.com/jepsen-io/elle).
El nodo local tiene un pequeño servidor HTTP que recibe transacciones abstractas (por ejemplo, "leer clave x, luego establecer y en 5") del entorno de pruebas, y las traduce en transacciones ejecutadas contra el controlador JDBC de DuckDB.
Podemos inyectar un tipo de fallo: la muerte de procesos.
Tenemos dos cargas de trabajo.
La primera, append (anexar), ejecuta transacciones que agregan enteros únicos a listas y lee el contenido de esas listas. Cada lista reside en una sola fila, distribuida en varias tablas. Las listas se identifican por clave primaria o una clave secundaria no indexada. Las listas se codifican como campos de texto o como listas DuckDB INTEGER{]. La mutación se realiza con INSERT ON CONFLICT UPDATE o MERGE INTO.
La segunda, fkey-register (registro de clave foránea), realiza lecturas y escrituras de registros enteros. En DuckDB, almacenamos esos registros en dos tablas. Una tabla lógica asigna claves a ID físicos, con una clave foránea. Una tabla física asigna IDs físicos a valores. Usamos un JOIN directo entre ambas para leer. Las escrituras se realizan actualizando la fila física, o creando una nueva fila física y alterando el puntero lógico hacia ella. Recién hoy logré que esta carga de trabajo se active; funciona, pero aún no está pulida.
Copyright © 2026 Jepens, LLC
Este programa y los materiales adjuntos se ponen a disposición bajo los términos de la Eclipse Public License 2.0, disponible en https://www.eclipse.org/legal/epl-2.0.
Este Código Fuente también puede ponerse a disposición bajo las siguientes Licencias Secundarias cuando se cumplan las condiciones para dicha disponibilidad establecidas en la Eclipse Public License, v. 2.0: GNU General Public License publicada por la Free Software Foundation, ya sea la versión 2 de la Licencia, o (a su elección) cualquier versión posterior, con la Excepción GNU Classpath disponible en https://www.gnu.org/software/classpath/license.html.