pikos_popl2020
1.0.0
Este es el artefacto de software que acompaña al documento "Computación determinista de punto de fijación paralelo" de Sung Kook Kim, Arnaud J. Venet y Aditya V. Thakur.
"Preprint determinista paralelo de punto de fijación" : http://arxiv.org/abs/1909.05951.
@article{DBLP:conf/popl/KimVT20,
author = {Sung Kook Kim and
Arnaud J. Venet and
Aditya V. Thakur},
title = {Deterministic Parallel Fixpoint Computation},
journal = {{PACMPL}},
volume = {4},
number = {{POPL}},
pages = {14:1--14:33},
year = {2020},
note = {To appear},
url = {https://doi.org/10.1145/3371082},
doi = {10.1145/3371082},
}
@article{DBLP:journals/corr/abs-1909-05951,
author = {Sung Kook Kim and
Arnaud J. Venet and
Aditya V. Thakur},
title = {Deterministic Parallel Fixpoint Computation},
journal = {CoRR},
volume = {abs/1909.05951},
year = {2019},
url = {http://arxiv.org/abs/1909.05951},
archivePrefix = {arXiv},
eprint = {1909.05951},
}
Consiste principalmente en nuestros Pikos de intérprete abstracto paralelo, 4330 puntos de referencia utilizados en los experimentos y scripts para reproducir los resultados en el documento.
Pikos se basa en un intérprete abstracto secuencial, IKOS. Los archivos cambiados en IKOS para implementar Pikos se resumen en CHANGES.md . Dado un programa como entrada, tanto IKOS como Pikos calculan invariantes en cada punto de programa y ejecutan verificaciones en ellos. De hecho, Pikos se implementa como una opción de análisis de IKOS, lo que le permite calcular a los invariantes en paralelo utilizando múltiples núcleos de CPU. Por lo tanto, Pikos requiere máquinas de múltiples núcleos para reproducir los resultados. Requiere al menos 16 núcleos para reproducir todos los resultados. IKOS es elegido como la línea de base.
Después de construir e instalar Pikos, uno puede ejecutar Pikos en cada punto de referencia para obtener un informe de análisis, comparar los invariantes calculados por IKOS y Pikos, o medir la aceleración entre IKOS y Pikos. Además, se puede reproducir los datos y generar tablas y figuras en el documento.
A medida que el documento ejecuta los experimentos en 4330 puntos de referencia, se recomienda el entorno de computación en la nube para reproducir los resultados de manera oportuna. Las configuraciones y scripts de AWS detallados utilizados por los autores se proporcionan en aws/ .
El entorno de referencia utiliza Ubuntu 16.04 .
Omita la sección de instalación si está utilizando el Docker. Uno necesita instalado docker . La imagen está disponible en el repositorio de Dockerhub skkeem/pikos:dev . El siguiente comando descargará la imagen y la ejecutará Interactivley:
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256: 3D99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
También se puede construir la imagen utilizando DockerFile en este repositorio.
$ docker build -t skkeem/pikos:dev .
El script install_dependencies.sh instalará todas las dependencias requeridas. Requiere acceso a la raíz.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
Dependencias:
Python3.6 Dependencias:
El script install.sh buid e instalará pikos en ./build/ directorio. No requiere acceso a la raíz.
$ ./install.sh
El script extract_benchmarks.sh extraerá puntos de referencia en el directorio ./benchmarks/ . No requiere acceso a la raíz. El sha256sum del archivo descargado es D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE9266F6B1B1C1.
$ ./extract_benchmarks.sh
El script run_pikos.sh ejecuta el análisis en el programa dado. Calcula los invariantes y ejecuta los controles. Este script es solo para ilustrar que Pikos está funcionando totalmente de intérprete abstracto, y no se usa ni se requiere para reproducir los resultados.
$ ./run_pikos.sh ./benchmarks/test.c
Si ve la siguiente salida como resultado, la instalación fue exitosa y ahora puede reproducir los resultados. Pikos informa dos ocurrencias de desbordamiento del búfer en la línea 8 y 9.
[*] Compiling ./benchmarks/test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] (Concurrently) Analyzing entry point 'main'
[*] Checking properties for entry point 'main'
# Time stats:
clang : 0.056 sec
ikos-analyzer: 0.019 sec
ikos-pp : 0.011 sec
# Summary:
Total number of checks : 7
Total number of unreachable checks : 0
Total number of safe checks : 5
Total number of definite unsafe checks: 2
Total number of warnings : 0
The program is definitely UNSAFE
# Results
benchmarks/test.c: In function 'main':
benchmarks/test.c:8:10: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
a[i] = i;
^
benchmarks/test.c: In function 'main':
benchmarks/test.c:9:18: error: buffer overflow, trying to access index 10 of global variable 'a' of 10 elements
printf("%i", a[i]);
^
Pikos hereda las opciones de línea de comandos de IKOS. A continuación destaca las opciones relevantes utilizadas en este artefacto. La descripción de los dominios abstractos numéricos se toman de la documentación de IKOS.
El uso del parámetro -nt restringe el número de hilos permitidos en Pikos. El siguiente comando ejecutará Pikos con 4 hilos máximos:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 es el valor predeterminado. -nt=0 permitirá que la biblioteca TBB decida el número de hilos. Los autores arbitrarios eligieron 99 como el número máximo de hilos. Para cambiar esto, modifique la línea 991 de ./pikos/analyzer/src/ikos_analyzer.cpp e instale nuevamente.
El uso del parámetro -cs restringe la sensibilidad de contexto en Pikos. Este número corresponde a la profundidad permitida de la enlinición dinámica en el análisis interprocedural. El siguiente comando ejecutará Pikos con una máxima profundidad de las llamadas de función:
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0 es el valor predeterminado, y deshabilita esta restricción. Esta restricción se usa solo para los puntos de referencia que tardan más de 4 horas en analizarse. Consulte benchmarks/README.md para más detalles.
La lista de dominios abstractos numéricos disponibles (a prueba de hilos) es:
-d=interval : el dominio de intervalo, ver CC77.-d=congruence : el dominio de congruencia, ver Gra89.-d=interval-congruence : el producto reducido del intervalo y la congruencia.-d=dbm : el dominio de las matrices unidas a la diferencia, ver PADO01.-d=gauge : el dominio del calibre, ver cav12.-d=gauge-interval-congruence : el producto reducido del medidor, el intervalo y la congruencia. Por defecto, Pikos usa el dominio de intervalo , y los experimentos se realizaron con él. Si desea probar otros dominios, use el parámetro -d :
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Pasar las opciones, --no-checks --no-fixpoint-cache , deshabilita las verificaciones, como el análisis de desbordamiento de búfer, división por análisis cero, análisis de puntero nulo, etc.-después de calcular los invariantes:
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Estos se pasan al cronometrar los resultados , ya que solo estamos preocupados por el tiempo de cálculo invariante.
Para -nt por encima de 99, se realizará una comparación entre IKOS y Pikos en lugar del análisis regular. Por ejemplo, pasar -nt=104 calculará y comparará los invariantes de IKOS y Pikos con 4 hilos máximos. Si los invariantes difieren, "¡inigualable!" se imprimirá y el proceso regresará 42. Todas las ejecuciones utilizando los dominios abstractos anteriores deben tener los mismos invariantes por diseño.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
La reproducción de los resultados se divide en pasos: (1) reproducir los datos y (2) generar tablas/figuras a partir de los datos. El primer paso puede llevar mucho tiempo si elige reproducir todos los datos. Este paso se puede hacer usando AWS para terminar de manera oportuna. Consulte aws/README.md para obtener más información. El segundo paso no debería tomar mucho tiempo y se puede hacer localmente. Todavía requiere que las dependencias se instalen localmente. Consulte install_dependencies.sh .
Nuevamente, la aceleración de Pikos proviene de utilizar múltiples núcleos de CPU. Pikos requiere máquinas de múltiples núcleos para reproducir los resultados. Requiere al menos 16 núcleos para reproducir todos los resultados. Para los scripts con nombre de reproduce*.sh , especificaremos la menor cantidad de núcleos requeridos al final de los nombres.
Además, el uso de TCMALLOC , que es un asignador de memoria instalado en install_dependencies.sh , es imprescindible para reproducir los resultados. Asegúrese de que esté instalado correctamente. Debe haber una biblioteca, /usr/local/lib/libtcmalloc.so .
Se proporciona un script opcional, measure_speedup.sh , para medir la aceleración de un solo punto de referencia. Se necesitan las mismas opciones de línea de comando que run_pikos.sh . Simplemente genera la aceleración, definida como el tiempo de ejecución de IKOS / tiempo de ejecución de Pikos.
$ ./measure_speedup.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
>>> Running time of IKOS = 31.33911 seconds.
>>> Running time of PIKOS = 10.12769 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS) = 3.09x.
Los siguientes scripts generan datos en un archivo CSV. Tiene las siguientes columnas:
benchmark : Nombre del punto de referencia.category : la fuente del punto de referencia. SVC o OSS.cs : la sensibilidad de contexto utilizada.walltime (s) : Tiempo de análisis en IKOSwalltime (s)-k : Tiempo de análisis en Pikos, donde K es el número de hilos permitidos.speedup-k : Speedup of PikosIgnore las advertencias sobre No PropertyFile, reemplazo de variable y nombre de archivo que aparezca dos veces al ejecutar los scripts.
Ejecuta Ikos, Pikos <2>, Pikos <4>, Pikos <6> y Pikos <8> en todos los puntos de referencia. Emite all.csv . Esto lleva mucho tiempo (aproximadamente 48 días, si usa solo una máquina).
$ ./reproduce_all-8.sh
Ejecuta Ikos y Pikos <4> en todos los puntos de referencia. Emite rq1.csv . Esto se puede usar para responder RQ1. Esto también lleva mucho tiempo (aproximadamente 25 días, si usa solo una máquina).
$ ./reproduce_rq1-4.sh
Ejecuta IKOS y PIKOS <4> en puntos de referencia en la Tabla 3. Emite tab2.csv . Esto se puede usar para generar la Tabla 2. Esto lleva aproximadamente 36 horas, si usa solo una máquina.
$ ./reproduce_tab2-4.sh
Alternativamente, uno puede optar por ejecutar solo la parte superior de la Tabla 2. Emite tab2a.csv . Esto lleva aproximadamente 8 horas, si usa solo una máquina.
$ ./reproduce_tab2a-4.sh
El siguiente comando mide la aceleración para el punto de referencia con la mayor aceleración en Pikos <4>. El resultado de este punto de referencia se puede encontrar en la primera entrada de la Tabla 2.
$ ./measure_speedup.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/aureport.bc
>>> Running time of IKOS = 684.19316 seconds.
>>> Running time of PIKOS = 188.25443 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS) = 3.63x.
Ejecuta Ikos, Pikos <4>, Pikos <8>, Pikos <12> y Pikos <16> en puntos de referencia en la Tabla 3. Emite tab3.csv . Esto se puede usar para generar la Tabla 3. Esto lleva aproximadamente 12 horas, si solo usa una máquina.
$ ./reproduce_tab3-16.sh
El siguiente comando mide las aceleraciones para el punto de referencia con la más alta escalabilidad, ./benchmarks/OSS/audit-2.8.4/aureport.bc/ . El resultado de este punto de referencia se puede encontrar en la primera entrada de la Tabla 3.
$ ./measure_tab3-aureport.sh
>>> Running time of IKOS = 684.19316 seconds.
>>> Running time of PIKOS<4> = 188.25443 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<4>) = 3.63x.
>>> Running time of PIKOS<8> = 104.18474 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<8>) = 6.57x.
>>> Running time of PIKOS<12> = 75.86368 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<12>) = 9.02x.
>>> Running time of PIKOS<16> = 62.36445 seconds.
>>> Speedup (running time of IKOS / running time of PIKOS<16>) = 10.97x.
El archivo CSV producido anteriormente se puede usar para generar tablas y figuras en el documento. Demostraremos con los datos obtenidos por los autores en ./results-paper/all.csv , que se puede reproducir utilizando el script descrito en reproducir todos.
El script generate_fig5.py genera el gráfico de dispersión en la figura 5. También genera las medias descritas en la sección de evaluación. Requiere las columnas walltime (s) , walltime (s)-4 y speedup-4 en el archivo CSV. Emite fig5.png .
$ ./generate_fig5.py ./results-paper/all.csv
El script generate_fig6.py genera los histogramas en la figura 6. Requiere las columnas walltime (s) , walltime (s)-4 y speedup-4 en el archivo CSV. Emite 4 subfiguras, fig6-[0~3].png .
$ ./generate_fig6.py ./results-paper/all.csv
El script generate_fig9.py genera gráfico de caja y gráfico de violín en la figura 7. Requiere las columnas walltime (s) , speedup-2 , speedup-4 , speedup-6 y speedup-8 en el archivo CSV. Emite fig7-a.png y fig7-b.png .
$ ./generate_fig7.py ./results-paper/all.csv
El script generate_fig8.py genera gráfico de coeficiente de escalabilidad en la figura 8. Requiere las columnas walltime (s) , speedup-2 , speedup-4 , speedup-6 y speedup-8 en el archivo CSV. Emite fig8-a.png y fig8-b.png .
$ ./generate_fig8.py ./results-paper/all.csv
El script generate_tab3.py genera las entradas para la Tabla 2. Requiere el benchmark de columnas, category , walltime (s) , walltime (s)-4 y speedup-4 en el archivo CSV. Emite tab2-speedup.csv y tab2-ikos.csv , que se utilizan para llenar la Tabla 2.
$ ./generate_tab2.py ./results-paper/all.csv
El script generate_tab4.py elige los puntos de referencia para la Tabla 3 en función del coeficiente de escalabilidad. Requiere el benchmark de columnas, category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 y speedup-8 en el archivo CSV. Emite tab3-candidates.csv . Uno tiene que ejecutar Pikos <12> y Pikos <16> en estos puntos de referencia, además para completar la Tabla 3.
$ ./generate_tab3.py ./results-paper/all.csv
