Bluemoon

This tool has been created as a proof of concept and is not maintained any longer.

Descripción

Bluemoon es una herramienta prototípica para la simulación eficiente de eventos raros a través de técnicas de importance splitting. Sus usuarios pueden estudiar comportamientos poco frecuentes de su sistema (raros) sobre un modelo del mismo, por ejemplo la aparición de bugs en un software de alta confiabilidad o tolerante a fallas.

Bluemoon puede trabajar con cualquier tipo de sistema modelado como una cadena markoviana de tiempo discreto o continuo. Está preparada para estudiar comportamientos transitorios (e.g. cual es la probabilidad de perder un paquete antes de haber enviado todo el bache) y de estado estacionario (e.g. con qué frecuencia pierde paquetes mi red). La herramienta realiza un cómputo estadístico de la probabilidad de observar la anomalía de interés, construyendo un intervalo de confianza según los requerimientos del usuario. Ha logrado estimar correcta y eficientemente probabilidades del orden de 10-15, para niveles de confianza entre 90% y 95% y precisiones de hasta ± 10-16.

Bluemoon fue implementado como un módulo del model-checker probabilístico PRISM desarrollado principalmente por Dave Parker. Los modelos a analizar son descriptos con la sintaxis de PRISM en un archivo de texto plano, interpretado por éste y luego alimentados a Bluemoon, donde se realizan las simulaciones y el análisis de probabilidades. Por el momento sólo corre sobre sistemas operativos Linux.

Bluemoon es software gratuito, libre y de código abierto, disponible con la licencia Pública General de GNU (GPL).

Fundamentos teóricos

La división por importancia o importance splitting es una técnica de simulación de eventos raros que reduce la varianza de los estimadores Montecarlo estándares. Dado un presupuesto de cómputo permite lograr mejores estimaciones de la propiedad bajo estudio, o equivalentemente alcanza los criterios de confianza requeridos usando menos recursos computacionales.

A diferencia de otras técnicas como importance sampling, la división por importancia no requiere un análisis probabilístico de las distribuciones del modelo estudiado. Esto permite aplicarla de forma menos restrictiva en descripciones generales de sistemas, por ejemplo DTMCs y CTMCs. Importance splitting depende sin embargo de una función de importancia, normalmente definida por el usuario, para lograr la mejora prometida en la estimación.

Bluemoon implementa RESTART, un método particular de divisón por importancia de bajo costo en memoria y probada efectividad. A su vez utiliza las técnicas de Adaptive Multilevel Splitting para la definición del entorno de simulación. Su mayor contribución sin embargo es la posibilidad de construir automáticamente la función de importancia, que guiará al proceso de simulación otorgándole la eficiencia al método.

Bibliografía

  1. C.E. Budde, P.R. D'Argenio, and H. Hermanns, "Rare Event Simulation with Fully Automated Importance Splitting", in Computer Performance Engineering - 12th European Workshop, EPEW 2015, Madrid, Spain, August 31 - September 1, 2015, Proceedings, vol. 9272, M. Beltrán, W.J. Knottenbelt, and J.T. Bradley. Springer, 2015, pp. 275-290. DOI

Tutorial

Veamos qué ofrece Bluemoon con un ejemplo sencillo: la tandem queue.

Modelo del sistema

Una cola tandem consiste en dos buffers conectados secuencialmente. Paquetes llegan a cierta tasa λ al primer buffer q1, donde son almacenados temporalmente hasta que un servidor los atiende a tasa μ1. De allí pasan al segundo buffer, q2, donde se da el mismo proceso a una tasa de atención μ2, tras lo cual el paquete sale y se pierde de vista.

En un archivo de texto plano, digamos tandem.prism, podemos representar este sistema como una cadena de Markov de tiempo continuo en la sintaxis de PRISM de la siguiente forma:

 0  ctmc
 1 
 2  const int c;              // Queues capacity
 3  const double lambda = 3;  // rate(--> q1           )
 4  const double    mu1 = 2;  // rate(    q1 --> q2    )
 5  const double    mu2 = 6;  // rate(           q2 -->)
 6  
 7  module ContinuousTandemQueue
 8  
 9      q1: [0..c-1] init 0;
10      q2: [0..c-1] init 1;
11      arr:  [0..2] init 0;  // Arrival: (0:none) (1:lost) (2:successfull)
12      lost: [0..1] init 0;  // Package loss in q2: (0:none) (1:lost)
13      
14      // {- Package arrival at first queue -}
15      [] q1<c-1 -> lambda: (arr'=2) & (lost'=0) & (q1'=q1+1);
16      [] q1=c-1 -> lambda: (arr'=1) & (lost'=0);
17      
18      // {- Passing from first to second queue -}
19      [] q1>0 & q2<c-1 -> mu1: (arr'=0) & (lost'=0) & (q1'=q1-1) & (q2'=q2+1);
20      [] q1>0 & q2=c-1 -> mu1: (arr'=0) & (lost'=1) & (q1'=q1-1);
21      
22      // {- Package departure from second queue -}
23      [] q2>0 -> mu2: (arr'=0) & (lost'=0) & (q2'=q2-1);
24  
25  endmodule

Usando la herramienta: Análisis transitorio

Notemos que ambos buffers son finitos. Para simplificar el ejemplo ambos tienen la misma capacidad 'c', elegida por el usuario al momento de invocar la herramienta. Lo mismo podría haberse hecho con las tasas 'lambda', 'mu1' y 'mu2'.

Si observamos la línea 20, veremos que se puede descartar o perder un paquete. Esto ocurre cuando el primer servidor saca uno del primer buffer para llevarlo al segundo, pero el segundo buffer está al máximo de su capacidad. Como no se lo puede recibir, en nuestra implementación decidimos descartar dicho paquete, tomando nota de lo ocurrido en la variable booleana lost.

Ese será nuestro hecho de interés: la pérdida de un paquete en el segundo buffer. Para indicarle a Bluemoon cual es el evento raro añadimos una línea a tandem.prism, definiendo una etiqueta de PRISM con la palabra clave goal:

label "goal" = lost=1;

Supongamos que en particular nos interesa la probabilidad de perder un paquete antes de que se vacíe el segundo buffer, el cual siempre comienza conteniendo un paquete. Estamos pues estudiando la ocurrencia del evento raro en un intervalo específico de la vida del sistema: desde sus comienzos hasta que ocurre un evento que marca el fin. Este es un tipo de propiedad transitoria y puede ser analizada con Bluemoon. Todo lo que tenemos que hacer es indicarle a la herramienta cual es el evento "fin del mundo", a través de una nueva línea en tandem.prism con una etiqueta con la palabra clave stop:

label "stop" = q2=0;

¡Ya todo está listo para que estimemos la probabilidad del evento raro! Bluemoon utiliza intervalos de confianza para brindar garantías sobre la estimación que computa. El usuario elije el coeficiente de confianza y la precisión deseadas, y las indica a través de la línea de comandos, o como constantes de punto flotante en el archivo del modelo:

const double confidence = 0.90;
const double precision  = 5.0E-5;

La precisión puede ser un número concreto o un valor relativo al estimador. La segunda opción nos permite especificarla por ejemplo como un diez por ciento de la probabilidad de perder un paquete antes de que se vacíe el segundo buffer.

La invocación de la herramienta se realiza por línea de comandos de la misma manera que PRISM, especificando que deseamos usar el motor de simulación de eventos raros a través del switch -rarevent. Si queremos correr una simulación Monte Carlo estándar (i.e. sin la maravillosa división por importancia) sobre buffers con capacidad para cinco paquetes, la línea sería:

~$ prism-bm tandem.prism -const c=5 -rarevent fhit nosplit

El nombre del comando es "prism-bm" haciendo referencia a que es una versión de PRISM construida con el módulo bluemoon integrado. Notemos las dos palabras clave luego del switch. Con 'fhit' le indicamos a Bluemoon que estamos realizando un análisis transitorio, y mediante 'nosplit' apagamos el splitting, es decir que no se realizará división por importancia y se utilizarán sólo simulaciones Monte Carlo comunes y silvestres. El resultado debería ser algo como ésto:

PRISM
=====
 . . .

[DEV] Rare event simulation chosen.
[DEV] Simulation type: FIRST_HIT
[DEV] Simulation strategy: MONTECARLO

Confidence parameters
 - Looking inside modulesFile for confidence level
 - Looking inside modulesFile for precision
 - Confidence level: 90.0%
 - Precision to achieve: 5.0E-5

Special specifications
 - Techlog: rarevent_FIRST_HIT_MONTECARLO.log
 - CI build strategy: wilson
 - Splits: 1

Building model...
Model constants: c=5

Computing reachable states...

Reachability (BFS): 6 iterations in 0.00 seconds (average 0.000000, setup 0.00)

Time for model construction: 0.015 seconds.

Type:        CTMC
States:      19 (1 initial)
Transitions: 47

Rate matrix: 128 nodes (4 terminal), 47 minterms, vars: 7r/7c

Building sparse matrix for rarevent, from Prism (symbolically) built model.
Identifying special states... done.
Building importance function... done.
Setting up RESTART simulation environment....
Estimating rare event probability    {14}{15}{36} done:
 - Confidence interval: [ 4.711E-4 , 5.211E-4 ]
 - Precision: 5E-5
 - Point estimate: 4.961E-4

Processing times information
 - Total elapsed time: 0.86 s
 - Setup time: 0.04 s
    > Initial setup: 0.02 s
    > Rare/Reference states identification: 0.01 s
    > Importance function building: 0 s
 - Simulation time: 0.82 s

[DEV] Skipping other model checks.

Precisión relativa

Supongamos ahora que nos interesa estudiar buffers con capacidad para ocho paquetes. Entonces invocamos la herramienta como lo hicimos antes pero para la constante 'c=8', lo que podría darnos el siguiente resultado:

· · ·
Estimating rare event probability {7}{8} done:
 - Confidence interval: [ -1.891E-5 , 3.109E-5 ]
 - Precision: 5E-5
 - Point estimate: 6.089E-6

Notemos que el intervalo de confianza tiene un límite inferior negativo. Esto no huele muy bien que digamos, pues el mismo sugiere valores posibles para la probabilidad de observar el evento raro, y las probabilidades existen en el intervalo real [0,1]. El problema radica en que dicha probabilidad es más chica que la precisión que pedimos para el intervalo de confianza. La pregunta es entonces ¿cómo saber qué precisión pedir, sin saber de antemano cual es la probabilidad de mi evento raro?

Para estos casos existe la opción de precisión relativa. La misma debe ser pasada por línea de comandos con el switch -rareconf, se especifica como un porcentaje y se interpreta dinámicamente sobre las estimaciones que la herramienta va computando para el evento raro.

Digamos que queremos un intervalo muy preciso, que no se desvíe más de un diez por ciento del valor estimado a izquierda y otro tanto a derecha. La precisión relativa deseada es entonces de un 20%, y le indicamos esto a la herramienta con el siguiente comando:

~$ prism-bm tandem.prism -const c=8 -rarevent fhit nosplit \
   -rareconf .90 20%

El primer valor luego de -rareconf es el nivel de confianza deseado, que mantuvimos en un 90%, y el segundo es la precisión relativa. El resultado en este caso es:

· · ·
Estimating rare event probability {7}{24} done:
 - Confidence interval: [ 5.713E-6 , 6.983E-6 ]
 - Precision: 1.27E-6
 - Point estimate: 6.348E-6

Notemos que el veinte por ciento de 6.348 x 10-6 es 1.27 x 10-6, tal como lo pedimos, y en esta ocasión obtuvimos un intervalo de confianza sin valores negativos. Mucho mejor.

Terminación temprana

Bluemoon fue preparado para un fácil manejo en los casos de presupuesto computacional acotado. Ante una interrupción soft, por ejemplo cuando el usuario presiona Ctr+C, el programa se cierra ordenadamente y reporta los valores estimados hasta el momento. Para el caso anterior el resultado podría ser por ejemplo:

 · · ·
Estimating rare event probability {7}{8}^C

[rarevent.RareventSimulatorEngine] Interrupted, shutting down
 - Point estimate: 4.408E-6
 - 90% confidence: precision = 3.322E-6
                    interval = [ 2.747E-6 , 6.068E-6 ]
 - 95% confidence: precision = 3.99E-6
                    interval = [ 2.413E-6 , 6.402E-6 ]
 - 99% confidence: precision = 5.344E-6
                    interval = [ 1.735E-6 , 7.08E-6 ]

Como el cómputo fue interrumpido arbitrariamente por el usuario antes de su finalización, no se alcanzó el criterio de confianza exigido. En estos casos la herramienta reporta la probabilidad estimada hasta el momento de la interrupción. Además construye y reporta intervalos para tres de los niveles de confianza más populares en la estimación estadística: 90%, 95% y 99%.

Simulaciones con importance splitting

Muy bien, muy bonito, pero ahora querríamos usar aquello para lo cual Bluemoon fue construido: simulación eficiente con técnicas de división por importancia. Sólo que hay un pequeño problema, y es que dichas técnicas requieren la definición de una función de importancia diseñada específicamente para el sistema bajo estudio.

Por fortuna ¡eso no es ningún problema! Bluemoon realiza un análisis estático sobre el modelo alimentado, construyendo automáticamente esta función que de otra manera debería haber sido provista por el usuario. Para seleccionar este modo operativo invocamos a la herramienta con la opción 'auto' en reemplazo de 'nosplit':

~$ prism-bm tandem.prism -const c=5 -rarevent fhit auto

La primer diferencia que notaremos es que el preámbulo ahora nos saludará con la siguiente leyenda:

[DEV] Rare event simulation chosen.
[DEV] Simulation type: FIRST_HIT
[DEV] Simulation strategy: RESTART_AUTO

La otra diferencia la notaremos en los tiempos de simulación. Mientras más raro sea el evento estudiado, más veloz será la simulación con división por importancia en comparación con la Monte Carlo estándar. Las diferencias pueden ser realmente considerables.

Bluemoon también le permite al usuario escoger su propia función de importancia ad hoc, donde la única restricción es que debe tener imagen en los enteros. Para especificarla se puede usar la línea de comandos, o escribirla directamente sobre el archivo del modelo como una fórmula de PRISM llamada 'importance'. Por ejemplo si escribimos

formula importance = q2;

en tandem.prism, estamos especificando que la importancia del estado actual del sistema está dado por el número de paquetes que contiene el segundo buffer. La invocación por línea de comandos en este caso debería ser:

~$ prism-bm tandem.prism -const c=5 -rarevent fhit adhoc

Usando la herramienta: Análisis de estado estacionario

Hasta ahora hemos estudiado propiedades del tipo transitorio, pero Bluemoon también permite analizar propiedades de estado estacionario como por ejemplo la frecuencia de observación de eventos raros. Supongamos que nos interesa saber cual es la proporción de paquetes perdidos de entre todos aquellos que ingresan al sistema. En particular también consideraremos aquellos paquetes que intentaron entrar en el primer buffer, pero fueron descartados al encontrarse éste lleno.

Este nuevo tipo de evento, llamado "de referencia" en la literatura, marca el paso del tiempo para la simulación. Nos interesa la proporción de paquetes perdidos en función de todos los que ingresaron. Para indicarle a Bluemoon como identificar dichos eventos añadimos una nueva línea a tandem.prism con una etiqueta con la palabra clave reference:

label "reference" = arr!=0;

Muchas veces en cambio nos interesa saber la frecuencia absoluta de la anomalía, y no en función de otro evento específico del sistema. Para ello utilizamos la palabra clave '_TIME_' a la hora de definir el evento de referencia, aclarando que todo pasaje de tiempo es relevante para nuestro análisis:

label "reference" = _TIME_;

Finalmente invocamos la herramienta escribiendo 'freq' en el lugar donde antes habíamos escrito 'fhit', indicando así que las simulaciones harán corridas largas para computar la frecuencia buscada:

~$ prism-bm tandem.prism -const c=5 -rarevent freq adhoc

Esa línea de comando producirá el siguiente preámbulo:

[DEV] Rare event simulation chosen.
[DEV] Simulation type: FREQUENCY
[DEV] Simulation strategy: RESTART_AD_HOC

y podría terminar en un resultado similar al siguiente:

· · ·
Building sparse matrix for rarevent, from Prism (symbolically) built model.
Identifying special states... done.
Building importance function... (is Ad hoc: q2) done.
Setting up RESTART simulation environment... done.
Estimating rare event probability    {30} done:
 - Confidence interval: [ 6.001E-4 , 6.501E-4 ]
 - Precision: 5E-5
 - Point estimate: 6.251E-4

Processing times information
 - Total elapsed time: 5.07 s
 - Setup time: 0.05 s
    > Initial setup: 0.02 s
    > Rare/Reference states identification: 0.02 s
    > Importance function building: 0.01 s
 - Simulation time: 5.03 s

Documentación

La invocación de la herramienta sigue el estilo del model checker PRISM en el que está inserta. La sintaxis es:

~$ prism-bm <modelfile> <consts>  -rarevent [<type> <strategy>]  \
                              [-rareconf <conf> <prec>[%]]    \
                              [-rareparams "<params>"]

donde:

  • prism-bm es el comando de ejecución de la herramienta,
  • <modelfile> es un path a un archivo de texto plano con el modelo del sistema,
  • <consts> es la lista de definición de valores de constantes de PRISM (ver prism-bm --help const),
  • <type> es 'fhit' o 'freq', y le indica a la herramienta si la propiedad estudiada es transitoria o de estado estacionario respectivamente (ver prism-bm --help rarevent),
  • <strategy> es 'auto', 'adhoc' o 'nosplit', y le indica a la herramienta cual estrategia de simulación usar para la estimación (ver prism-bm --help rarevent),
  • <conf> es un real en el intervalo (0,1) que especifica el coeficiente de confianza deseado (ver prism-bm --help rareconf),
  • <prec> especifica la precisión deseada para el intervalo de confianza, y puede ser cualquier real positivo o un valor porcentual terminado con el caracter % (ver prism-bm --help rareconf),
  • <params> es una lista de argumentos separados por coma que especifica opciones finas para la simulación, donde las opciones son techlog, ifun, effort, split, ci y timeout (ver prism-bm --help rareparams).

A continuación, detallamos las ayudas particulares para cada comando relacionado a Bluemoon:

  • Salida del comando prism-bm --help rarevent:
    Switch: -rarevent [<type> <strategy>]
    
        <type>: fhit*, freq.
    <strategy>: auto*, adhoc, nosplit.
    
    <type> is required for <strategy> specification.
    If neither <type> nor <strategy> are specified, default is "fhit auto".
    
  • Salida del comando prism-bm --help rareconf:
    Switch: -rareconf <conf> <prec>[%]
    
      <conf> gives the desired confidence coefficient ∈ (0.0, 1.0).
      <prec> gives the desired confidence interval length, aka precision.
             This can be any positive number, or alternatively some percentage,
             which will be applied to the average over the first thirty 
             estimations of the rare event probability.
    
    Examples:
     -rareconf 0.95 1E-7
     -rareconf 0.9 5%
    
  • Salida del comando prism-bm --help rareparams:
    Switch: -rareparams "<params>"
    
    <params> is a comma-separated list of parameters for the rare event
    simulation engine, specifying at least one of the following:
      techlog=<name>, where <name> is the name of the file
                       to be used for technical output;
      ifun=<expr>,    where <expr> is an integer typed expression
                       to be used as Ad hoc importance function;
      effort=<val>,   where <val> is a positive integer
                       to be used as each simulation maximum effort;
      split=<val>,    where <val> is an integer greater than 1
                       to be used as split value on threshold level-up;
      ci=<method>,    where <method> specifies the confidence interval
                       construction method to use, which should be
                       one of: "mean", "prop" or "wilson";
      timeout=<val>,  where <val> is a non-negative number of minutes
                       to be used as wall time limit. If 0 == <val>
                       then there is no timeout, and simulation stops
                       once the confidence criteria is met (default)
    
    Examples:
     -rareparams "ifun=q2"
     -rareparams "ifun=x1+x2,split=4"
     -rareparams "split=2,effort=256,ifun=q1+5*q2,ci=wilson"
    

Finalmente, reportamos diversos ejemplos de uso:

Si "tandem.prism" es un archivo de texto plano con el modelo a estudiar, donde las constantes 'c' y 'mu1' están libres, una corrida típica para una propiedad transitoria puede ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent -rareconf .9 40%

o equivalentemente

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent fhit auto \
   -rareconf .9 40%

donde se especificó un nivel de confianza del 90%, una precisión del cuarenta por ciento del valor estimado, y donde se simulará usando división por importancia con la función de importancia automáticamente construida por Bluemoon.

Si quisiéramos hacer lo mismo pero sin utilizar división por importancia, sino simulaciones Monte Carlo estándar, el comando sería:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent fhit nosplit \
   -rareconf .9 40%

Si en cambio deseamos estudiar una propiedad de estado estacionario, el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq auto \
   -rareconf .9 40%

Si además queremos usar una función de importancia definida ad hoc pornosotros, digamos q1 + 10 q2, donde q1 y q2 son variables del modelo que asumen valores enteros, el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq adhoc \
   -rareconf .9 40% -rareparams "ifun=q1+10*q2"

Por último, si deseáramos también indicar que el splitting por threshold debe ser igual a ocho y que los detalles técnicos sean escritos dentro de un archivo con nombre "run5.log", entonces el comando debería ser:

~$ prism-bm tandem.prism -const c=10,mu1=3.4 -rarevent freq adhoc \
   -rareconf .9 40% -rareparams "ifun=q1+10*q2,split=8,techlog=run5.log"

Descarga

Bluemoon es software gratuito, libre y de código abierto, disponible con la licencia Pública General de GNU (GPL).

La última versión disponible de la herramienta puede descargarse desde aquí.

Los archivos contienen el código fuente que deberá ser descargado y compilado en la máquina donde se la desee utilizar.

Bluemoon se implementó sobre la versión 4.3 de PRISM. Los requisitos para la compilación y la ejecución son en general los mismos que para PRISM (ver la sección "Building PRISM from source"). A esto se le suma el requisito de una versión del compilador de GNU igual o superior a gcc 4.8.0.

Luego de descargar y descomprimir el archivo, el código fuente de la herramienta se ubicará dentro del subdirectorio "bluemoon-1.0". Para compilar el código nos movemos a ese directorio y tipeamos "make prism-bm" en la línea de comandos. Una vez finalizada exitosamente la compilación veremos un link simbólico con el nombre prism-bm que apunta al ejecutable generado.

Modelos de ejemplo

  1. Cola tandem CTMC
  2. Cola tandem DTMC
  3. Redes de colas abiertas/cerradas
  4. Cola con productores defectuosos (ATM)
  5. Redes de colas con rupturas y reparaciones
  6. Base de datos