Cómo probar correctamente estructuras de datos concurrentes

 (matklad.github.io)
2 puntos por GN⁺ 2024-07-07 | 1 comentarios | Compartir por WhatsApp
  • Usando como ejemplo un contador concurrente roto en Rust, muestra problemas que las pruebas comunes de carga con hilos no detectan mediante un control del orden de ejecución reproducible y minimizable
  • Un wrapper de AtomicU32 para pruebas inserta pause(), y un managed thread se detiene antes y después de las operaciones atómicas para luego continuar en el orden elegido por la prueba
  • Una prueba simple puede hacer que 100 hilos incrementen 100 veces cada uno y producir fallas como 9598 en lugar del valor esperado 10000, pero depende del timing, por lo que es difícil de reproducir, depurar y reducir
  • Una prueba basada en propiedades con arbtest reproduce el mismo interleaving con la misma seed y minimiza el caso fallido hasta 0: increment, 1: increment, 0: unpause, 1: unpause
  • Extendiendo la misma estructura con exhaustigen, se pueden enumerar todos los interleavings hasta 5 incrementos, y después de corregirlo con fetch_add, pasan 81133 interleavings

Contador concurrente no atómico

  • El ejemplo usa AtomicU32 de Rust, pero increment() hace load seguido de store(value + 1), así que la operación de incremento en sí no es atómica
  • La estructura Counter es simple
    • value: AtomicU32
    • increment() lee el valor con SeqCst, le suma 1 y lo vuelve a guardar
    • get() lee el valor actual con SeqCst
  • Dos hilos pueden leer el mismo valor y luego guardar el mismo resultado incrementado, haciendo que se pierda una actualización

Por qué las pruebas normales con hilos no alcanzan

  • La verificación más simple consiste en hacer que varios hilos incrementen repetidamente el mismo contador y revisar el valor final
    • thread_count = 100
    • increment_count = 100
    • El valor esperado es 10000
  • Una ejecución de ejemplo falla con left: 9598, right: 10000
  • Este enfoque depende mucho del timing del scheduler
    • Es difícil reproducir de forma determinista la misma falla
    • Es difícil de depurar
    • Si se reduce el número de hilos o de incrementos, puede pasar por suerte, así que cuesta minimizar el caso fallido

Manejo de interleavings con pruebas basadas en propiedades

  • Las pruebas basadas en propiedades (PBT) encajan bien con pruebas de máquinas de estado
    • Es fácil generar entradas arbitrarias
    • Se puede definir como propiedad que el resultado concurrente debe ser igual al del modelo secuencial
    • También encaja con la necesidad de minimizar entradas fallidas
  • La dificultad está en que no es fácil avanzar hilos reales del sistema operativo paso a paso justo cuando uno quiere
  • La solución es una estructura que en cada iteración elige un hilo al azar y lo avanza un paso
    • Tiene que poder insertar otro hilo entre el load y el store de un mismo hilo
    • Para eso se construye una API de managed thread que permite controlar directamente los hilos

AtomicU32 para pruebas e inserción de pause

  • En builds de prueba se usa un managed_thread::AtomicU32 propio en lugar de std::sync::atomic::AtomicU32
    • #[cfg(test)] use managed_thread::AtomicU32
    • #[cfg(not(test))] use std::sync::atomic::AtomicU32
  • El wrapper AtomicU32 llama a pause() antes y después de load() y store()
    • load: pause() → load real → pause()
    • store: pause() → store real → pause()
  • Gracias a estos puntos de inserción, la prueba puede detener y reanudar hilos alrededor de operaciones atómicas para controlar el orden de ejecución

Forma de la API de managed thread

  • La prueba crea dos managed threads dentro de std::thread::scope
    • Como usa scoped threads, puede tomar prestados datos locales del stack
    • Se pasa el estado como referencia al contador, por ejemplo spawn(scope, &counter)
  • Un managed thread no ejecuta una función main fija desde el inicio, sino closures enviadas por el hilo de control con submit()
    • t.submit(|c| c.increment())
    • El hilo ejecuta la closure sobre su estado T
  • El loop de prueba realiza acciones aleatorias sobre cada hilo mientras quede entropía
    • Si el hilo está detenido, hace unpause()
    • Si no está detenido, ejecuta increment() con submit()
    • El modelo secuencial counter_model también se incrementa el mismo número de veces
  • Al final, hace join() de todos los hilos y compara counter_model con el valor real de counter.get()

Implementación de pause y unpause

  • pause() usa thread_local! para encontrar el contexto del managed thread actual sin cambiar la API de Counter bajo prueba
    • El contexto se comparte como Arc<SharedContext>
    • SharedContext tiene Mutex<State> y Condvar
  • Los estados se dividen en Ready, Running y Paused
    • Ready: esperando la siguiente closure
    • Running: el managed thread está ejecutándose
    • Paused: detenido en un punto de pause()
  • Cuando el managed thread llega a pause(), cambia el estado de Running a Paused y notifica al hilo de control mediante la condition variable
  • unpause() cambia el estado de Paused a Running, despierta al managed thread y luego espera hasta que deje de estar en Running
    • Así se evita que el hilo de control y el managed thread sigan ejecutándose al mismo tiempo
    • Hace que en cualquier momento solo uno de los dos esté ejecutándose, reduciendo la no determinación

Reproducción y minimización de fallas

  • Una ejecución con arbtest encuentra una falla en el contador roto
    • Un ejemplo de falla da valor del modelo 4 y valor real 3
    • La seed fallida es 0x4fd7ddff00000020
  • Si se usa la misma seed, se obtiene el mismo interleaving otra vez, lo que facilita reproducir la falla
  • Con .minimize(), el caso fallido se reduce a una ejecución más corta
    • La seed mínima final es 0x9c2a13a600000001
    • El trace mínimo tiene cuatro pasos
      • 0: increment
      • 1: increment
      • 0: unpause
      • 1: unpause
  • En este caso mínimo, el valor esperado es 2 pero el valor real es 1, dejando en evidencia el defecto del incremento basado en load/store

Extensión a la enumeración de todos los interleavings

  • La misma estructura puede cambiarse de interleavings aleatorios a una estrategia basada en enumeración
  • Usando exhaustigen, se escribe una prueba que explora todos los interleavings hasta 5 incrementos
    • La prueba evita iteraciones dummy y está construida para siempre hacer unpause o enviar increment
  • La implementación rota encuentra el mismo bug
    • Un ejemplo de falla es left: 2, right: 1
  • Si Counter::increment() se corrige a fetch_add(1, SeqCst), la prueba pasa
    • Al wrapper AtomicU32 también se le agrega pause() antes y después de fetch_add()
    • El resultado de ejecución es all 81133 interleavings are fine!
    • El tiempo de ejecución es real 8.65s, CPU 8.16s, RSS 63.91mb

Extensión a modelos de memoria débiles y model checking

  • La implementación actual de juguete de AtomicU32 delega en atomics reales
  • Una idea de extensión es mantener, para cada atomic, el conjunto de valores escritos y devolver en cada lectura un valor arbitrario consistente con un modelo de memoria débil
  • La exploración de interleavings también puede hacerse de forma más inteligente que al azar
    • Con un enfoque de model checking se puede verificar si ya se consideraron todos los interleavings significativamente distintos
    • También se pueden enumerar todos los interleavings en rangos pequeños al estilo de Generate All The Things

Por qué se puede minimizar sin shrinking

  • El arbtest usado se parece a una interfaz PRNG familiar, pero usa un PRNG finito
    • Si se siguen pidiendo valores aleatorios, en algún momento devuelve Err(OutOfEntropy)
    • Por eso en el código de prueba aparecen ? y while !rng.is_empty()
  • Cuando la prueba consume toda la entropía, termina antes, así que si se reduce la entropía disponible, la ejecución de la prueba también se acorta
  • Su implementación interna conceptualmente se parece a &mut &[u8]
    • Cada vez que se pide un número aleatorio, el slice de bytes se acorta
    • Cuanto más corto sea el slice inicial, más simple será la prueba
  • Gracias a este enfoque, los casos fallidos pueden hacerse más cortos sin implementar lógica de shrinking por separado
  • El código fuente de ejemplo está en properly-concurrent

Lecturas relacionadas

1 comentarios

 
GN⁺ 2024-07-07
Opiniones en Hacker News

  • En Rust, estoy creando una biblioteca llamada Temper con un enfoque similar: https://github.com/reitzensteinm/temper/tree/main
    Sin embargo, para modelar las implicaciones extrañas que produce todo el modelo de memoria de Rust, hay que ir mucho más lejos: se necesita una especie de libro mayor que rastree qué escrituras ha percibido cada thread. Según el orden de memoria atómica, las fences de lectura/escritura, etc., pueden surgir garantías del tipo: si se percibe la escritura X, entonces necesariamente también se debe percibir la escritura Y
    Creo que es una de las colecciones más completas de casos de prueba para los modelos de memoria de C++/Rust, y reuní casi todo lo que se puede encontrar en libros, el estándar de C++, Stack Overflow, blogs, etc. Por ejemplo, el archivo para Rust Atomics and Locks de Mara Bos está aquí: https://github.com/reitzensteinm/temper/blob/main/memlog/tes...
    Loom, mencionado en el artículo, es una biblioteca parecida pero mucho más completa, que permite probar exhaustivamente componentes de más alto nivel como mutexes o colas: https://github.com/tokio-rs/loom Sin embargo, no modela el propio modelo de memoria con tanto detalle como Temper, y estaba considerando migrar los casos de prueba a Loom
    Me inspiró la presentación de Will Wilson sobre las pruebas de FoundationDB, y ahora él está trabajando en Antithesis en una solución basada en hipervisor para aplicar este tipo de pruebas a contenedores Docker arbitrarios: https://www.youtube.com/watch?v=4fFDFbi3toc, https://antithesis.com/
    Creo firmemente que esta área crecerá mucho durante los próximos 10 años. WebAssembly está en un punto ideal: es lo bastante completo como para compilar software arbitrario, pero lo bastante simple como para que crear algo como Antithesis no tenga que ser un proyecto de 5 años para un equipo de élite que ya haya lanzado una base de datos

  • Implementé un snapshot atómico de memoria compartida en Rust y también me tomé las pruebas automatizadas con la mayor seriedad posible: https://github.com/kaymanb/todc/tree/main/todc-mem
    Al principio usé Loom, que aparece en el artículo, pero después cambié a shuttle: https://github.com/tokio-rs/loom, https://github.com/awslabs/shuttle
    shuttle usa un enfoque aleatorizado en vez de una búsqueda exhaustiva como Loom, pero el scheduler aun así ofrece garantías probabilísticas para encontrar bugs. En mi experiencia, shuttle fue más rápido y escaló a escenarios de prueba más complejos
    De forma similar al enfoque del artículo, cuando un schedule específico provoca una falla en una prueba, se puede guardar la semilla aleatoria. La capacidad de reproducir rápidamente una prueba fallida es muy importante y permite escribir casos de prueba explícitos para bugs que ya se encontraron y corrigieron: https://github.com/kaymanb/todc/blob/0e2874a70ec8beed8fae773...

  • En el mundo de Kotlin/Java, Lincheck de JetBrains es una buena biblioteca para este tipo de trabajo: https://github.com/JetBrains/lincheck
    En particular, me gusta que sea declarativa y la forma en que muestra los resultados de linealizabilidad

  • Me pregunto si en C++ existe alguna biblioteca como Loom. Tengo algunas estructuras de datos lock-free que quiero probar

  • Si entendí bien, este enfoque tiene limitaciones relacionadas con las garantías débiles de progreso.
    El cálculo del texto no es del todo trivial, pero en hardware real y con un scheduler real se puede pensar en un bucle cmpxchg que tiene una probabilidad extremadamente baja de detenerse en una CPU específica. Si la cantidad de CPU es n, en el peor caso la probabilidad de avanzar es 1/n, pero con este método de prueba pasa a ser 1/t^p. Aquí t es la cantidad de tareas, que puede ser mucho mayor que la cantidad de CPU, y p es la cantidad de pausas dentro del cuerpo del bucle, que fácilmente llega a 3 o más. Eso basta para hacer que un algoritmo que en la práctica funciona parezca roto.
    Por el contrario, incluso si se quisiera detectar el progreso débil como un bug y por eso exigir progreso fuerte, este método no parece ofrecer una herramienta útil.
    Aun así, claramente es útil para muchos problemas de concurrencia.

    • 1/t^p no me parece correcto; lo veo simplemente como 1/t. Al final, después de un tiempo t, alguna tarea necesariamente habrá avanzado, y si hay t tareas, la probabilidad de que sea la mía es 1/t.
      La confusión clave parece estar en que detenerse no significa necesariamente perder en CAS.

  • Sobre la parte que dice: “Para ser honestos, aquí hay algo de conocimiento previo. Salvo que hagas algo muy maldito con ensamblador inline, no parece posible evitar crear hilos reales. Si algo llama a la función pause() y queremos que quede detenido hasta nuevo aviso, eso tiene que ocurrir dentro de un hilo que mantenga una pila separada de la pila de la prueba”, me pregunto si no se podría usar algún tipo de runtime asíncrono.
    Parece como si instrumentaran operaciones atómicas para lograr multitarea cooperativa. Quizá necesito más café, pero hacerlo sin hilos parece más simple.

    • Usar async sería cómodo, pero otro requisito es no querer cambiar la API observada externamente del software bajo prueba. Async es “contagioso”, así que para una API síncrona hay que usar una implementación síncrona.

  • Una desventaja de este enfoque es que hay que modificar el propio código bajo prueba para adaptarlo al código de prueba.
    Creo que se podría hacer lo mismo levantando dos hilos y ejecutándolos paso a paso con ptrace, intercalando la ejecución de instrucciones “al azar”. Algo como el modo chaos de rr.
    Sin embargo, algunas instrucciones podrían no ser atómicas, así que haría falta una forma de ejecutar paso a paso a nivel de “microcódigo atómico”, si es que eso siquiera es posible sin emulación.

    • Suena como el hipervisor de Antithesis.

  • Parece que para usar Loom hace falta compilación condicional, y aunque está bien cuando se prueba una biblioteca, es bastante invasivo.
    #[cfg(loom)]
    pub(crate) use loom::sync::atomic::AtomicUsize;
    #[cfg(not(loom))]
    pub(crate) use std::sync::atomic::AtomicUsize;
    Me pregunto si hay algún lenguaje que permita usar mejor un scheduler propio.

  • Si uno quisiera ser realmente exhaustivo, podría ejecutar las pruebas con ptrace y avanzar los hilos paso a paso para generar distintos interleavings a nivel de instrucción. Me pregunto si alguien ha visto algo así en la práctica.
    Cuando no se puede instrumentar el código como aquí, ¿hay alguna alternativa para pruebas de caja negra?

    • He usado un enfoque así para probar manejadores de señales asíncronas, pero en ese caso la cantidad de combinaciones es mucho más favorable. Si el hilo principal ejecuta n instrucciones, solo hacen falta n ejecuciones, ejecutando de 0 a n instrucciones antes de insertar la señal; después, el manejador de la señal corre hasta terminar y luego el hilo principal también corre hasta terminar. El tiempo total es O(n^2).
      Pero si hay t hilos que ejecutan n instrucciones cada uno, y pueden interrumpirse entre sí en todos los límites, con valores realistas de n el enfoque se vuelve difícil de abordar. Parece que habría que reducirlo eligiendo y simulando solo las operaciones que tienen comportamiento interesante.

  • Se ve bastante bueno, así que tendré que probarlo. Aunque no va a detectar todos los tipos de errores. ¿No podría ocurrir que cada llamada a pause() introduzca sincronización entre hilos y oculte algunos problemas de carreras de datos? Quizá en Rust eso no sea un problema.