Describir: Verificación de la linealizabilidad en tiempo de ejecución