pikos_popl2020
1.0.0
Il s'agit de l'artefact logiciel qui accompagne l'article "Calcul de correction parallèle déterministe" par Sung Kook Kim, Arnaud J. Venet et Aditya V. Thakur.
"Calcul de correction parallèle déterministe" " Preprint: 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},
}
Il se compose principalement de nos pikos d'interprète abstrait parallèle, de 4330 repères utilisés dans les expériences et des scripts pour reproduire les résultats du papier.
Pikos est basé sur un interprète abstrait séquentiel, IKOS. Les fichiers modifiés dans IKOS pour implémenter des pikos sont résumés en CHANGES.md . Compte tenu d'un programme en entrée, IKOS et PIKOS calculent les invariants sur chaque point de programme et les vérifient. En fait, Pikos est mis en œuvre comme une option d'analyse des IKOS, lui permettant de calculer les invariants en parallèle en utilisant plusieurs noyaux de processeur. Par conséquent, les pikos nécessitent des machines multi-cœurs pour reproduire les résultats. Il nécessite au moins 16 cœurs pour reproduire tous les résultats. IKOS est choisi comme base de référence.
Après avoir construit et installé des pikos, on peut exécuter des pikos sur chaque référence pour obtenir un rapport d'analyse, comparer les invariants calculés par IKOS et Pikos, ou mesurer l'accélération entre IKOS et Pikos. De plus, on peut reproduire les données et générer des tables et des chiffres dans le papier.
Au fur et à mesure que le papier exécute les expériences sur 4330 repères, un environnement de cloud computing est recommandé pour reproduire les résultats en temps opportun. Des configurations AWS détaillées et des scripts utilisés par les auteurs sont fournis dans aws/ .
L'environnement de référence utilise Ubuntu 16.04 .
Évitez la section d'installation si vous utilisez le Docker. Il faut installer docker . L'image est disponible dans le référentiel Dockerhub skkeem/pikos:dev . La commande suivante téléchargera l'image et l'exécutera Interactivley:
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256: 3d99811735e0e3577e7eea90785323d1975ac6250939ba4f70e6695ebedf5520
On peut également construire l'image à l'aide du dockerfile dans ce dépôt.
$ docker build -t skkeem/pikos:dev .
Le script install_dependencies.sh installera toutes les dépendances requises. Il nécessite un accès racine.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
Dépendances:
Python3.6 Dépendances:
Le script install.sh BUID et installera des pikos dans ./build/ Directory. Il ne nécessite pas d'accès racine.
$ ./install.sh
Le script extract_benchmarks.sh extrait des repères dans ./benchmarks/ répertoire. Il ne nécessite pas d'accès racine. Le SHA256SUM du fichier téléchargé est D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE9266F6B1B1C1.
$ ./extract_benchmarks.sh
Le script run_pikos.sh exécute l'analyse du programme donné. Il calcule les invariants et les vérifie. Ce script est juste pour illustrer que Pikos fonctionne pleinement sur l'interprète abstrait, et il n'est pas utilisé ou requis pour reproduire les résultats.
$ ./run_pikos.sh ./benchmarks/test.c
Si vous voyez la sortie suivante en conséquence, l'installation a été réussie et vous pouvez maintenant reproduire les résultats. Pikos rapporte deux occurrences de débordement de tampon aux lignes 8 et 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 hérite des options de ligne de commande d'Ikos. Ci-dessous met en évidence les options pertinentes utilisées dans cet artefact. La description des domaines abstraits numériques est tirée de la documentation des IKOS.
L'utilisation du paramètre -nt restreint le nombre de threads autorisés dans les pikos. La commande suivante exécutera des pikos avec un maximum de 4 threads:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 est la valeur par défaut. -nt=0 Laissera la bibliothèque TBB décider du nombre de threads. Les auteurs arbitraires ont choisi 99 comme nombre maximum de threads. Pour changer cela, modifiez la ligne 991 de ./pikos/analyzer/src/ikos_analyzer.cpp et remettez à nouveau.
L'utilisation du paramètre -cs restreint la sensibilité au contexte dans les pikos. Ce nombre correspond à la profondeur autorisée de l'inclinaison dynamique dans l'analyse interprocédurale. La commande suivante exécutera des pikos avec des appels de fonction de 5 profondeurs maximum:
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0 est la valeur par défaut, et il désactive cette restriction. Cette restriction est utilisée uniquement pour les repères qui prennent plus de 4 heures à analyser. Voir benchmarks/README.md pour plus de détails.
La liste des domaines abstraits numériques disponibles (en filetage) est:
-d=interval : le domaine d'intervalle, voir CC77.-d=congruence : le domaine de congruence, voir GRA89.-d=interval-congruence : le produit réduit de l'intervalle et de la congruence.-d=dbm : Le domaine des matrices liés à la différence, voir PADO01.-d=gauge : le domaine de la jauge, voir cav12.-d=gauge-interval-congruence : le produit réduit de la jauge, de l'intervalle et de la congruence. Par défaut, Pikos utilise le domaine d'intervalle et des expériences ont été menées avec elle. Si vous souhaitez essayer d'autres domaines, utilisez le paramètre -d :
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Passer les options, --no-checks --no-fixpoint-cache , désactive les vérifications - telles que l'analyse de débordement de tampon, la division par analyse zéro, l'analyse du pointeur nul, etc. - après avoir calculé les invariants:
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Ceux-ci sont passés lors du moment des résultats , car nous ne sommes préoccupés que par le temps de calcul invariant.
Pour -nt au-dessus de 99, la comparaison entre IKOS et PIKOS sera effectuée au lieu de l'analyse régulière. Par exemple, Passing -nt=104 calculera et comparera les invariants d'Ikos et de Pikos avec un maximum 4 threads. Si les invariants diffèrent, "sans renforcement !!" sera imprimé et le processus retournera 42. Toutes les exécutions en utilisant les domaines abstraits ci-dessus devraient avoir les mêmes invariants par conception.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
La reproduction des résultats est divisée en étapes: (1) reproduire les données et (2) générer des tables / chiffres à partir des données. La première étape peut prendre beaucoup de temps si vous choisissez de reproduire toutes les données. Cette étape peut être effectuée en utilisant AWS pour terminer en temps opportun. Voir aws/README.md pour plus d'informations. La deuxième étape ne devrait pas prendre beaucoup de temps et peut être fait localement. Il faut toujours installer les dépendances localement. Voir install_dependencies.sh .
Encore une fois, l'accélération de Pikos provient de l'utilisation de plusieurs cœurs de processeur. Pikos nécessite des machines multicœurs pour reproduire les résultats. Il nécessite au moins 16 cœurs pour reproduire tous les résultats. Pour les scripts avec nom de reproduce*.sh , nous spécifierons le moins de cœurs requis à la fin des noms.
De plus, l'utilisation de TCMALLOC , qui est un allocateur de mémoire installé dans install_dependencies.sh , est un incontournable pour reproduire les résultats. Veuillez vous assurer qu'il est installé correctement. Il devrait y avoir une bibliothèque, /usr/local/lib/libtcmalloc.so .
Un script facultatif, measure_speedup.sh , est fourni pour mesurer l'accélération d'une seule référence. Il faut les mêmes options de ligne de commande que run_pikos.sh . Il étend simplement l'accélération, définie comme le temps d'exécution de l'ikos / temps d'exécution des 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.
Les scripts suivants génèrent des données dans un fichier CSV. Il a les colonnes suivantes:
benchmark : Nom de la référence.category : la source de la référence. SVC ou OSS.cs : La sensibilité au contexte utilisée.walltime (s) : temps d'analyse dans IKOSwalltime (s)-k : Temps d'analyse dans les pikos, où K est le nombre de fils autorisés.speedup-k : accélération des pikosIgnorez les avertissements concernant aucun fichier de propriétés, remplacement de variable et nom de fichier apparaissant deux fois lors de l'exécution des scripts.
Il exécute Ikos, Pikos <2>, Pikos <4>, Pikos <6> et Pikos <8> sur tous les repères. Il produit all.csv . Cela prend beaucoup de temps (environ 48 jours, si vous n'utilisez qu'une seule machine).
$ ./reproduce_all-8.sh
Il exécute Ikos et Pikos <4> sur tous les repères. Il produit rq1.csv . Cela peut être utilisé pour répondre à RQ1. Cela prend aussi beaucoup de temps (environ 25 jours, si vous n'utilisez qu'une seule machine).
$ ./reproduce_rq1-4.sh
Il exécute IKOS et PIKOS <4> sur les repères dans le tableau 3. Il sortira tab2.csv . Cela peut être utilisé pour générer le tableau 2. Cela prend environ 36 heures, si vous n'utilisez qu'une seule machine.
$ ./reproduce_tab2-4.sh
Alternativement, on peut choisir d'exécuter uniquement la partie supérieure du tableau 2. Il sortira tab2a.csv . Cela prend environ 8 heures, si vous n'utilisez qu'une seule machine.
$ ./reproduce_tab2a-4.sh
La commande suivante mesure l'accélération de la référence avec une accélération la plus élevée en pikos <4>. Le résultat de cette référence se trouve dans la première entrée du tableau 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.
Il exécute Ikos, Pikos <4>, Pikos <8>, Pikos <12> et Pikos <16> sur les repères dans le tableau 3. Il publie tab3.csv . Cela peut être utilisé pour générer le tableau 3. Cela prend environ 12 heures, si vous n'utilisez qu'une seule machine.
$ ./reproduce_tab3-16.sh
La commande suivante mesure les accélérations de la référence avec une évolutivité la plus élevée, ./benchmarks/OSS/audit-2.8.4/aureport.bc/ . Le résultat de cette référence se trouve dans la première entrée du tableau 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.
Le fichier CSV produit ci-dessus peut être utilisé pour générer des tables et des chiffres dans le papier. Nous démontrerons avec les données obtenues par les auteurs dans ./results-paper/all.csv , qui peuvent être reproduites en utilisant le script décrit dans Reproduire All.
Le script generate_fig5.py génère le tracé de diffusion sur la figure 5. Il émet également les moyennes décrites dans la section d'évaluation. Il nécessite les colonnes walltime (s) , walltime (s)-4 et speedup-4 dans le fichier CSV. Il sort fig5.png .
$ ./generate_fig5.py ./results-paper/all.csv
Le script generate_fig6.py génère les histogrammes de la figure 6. Il nécessite les colonnes walltime (s) , walltime (s)-4 et speedup-4 dans le fichier CSV. Il produit 4 sous-figures, fig6-[0~3].png .
$ ./generate_fig6.py ./results-paper/all.csv
Le script generate_fig9.py génère un tracé de boîte et un tracé de violon sur la figure 7. Il nécessite les colonnes walltime (s) , speedup-2 , speedup-4 , speedup-6 et speedup-8 dans le fichier CSV. Il sort fig7-a.png et fig7-b.png .
$ ./generate_fig7.py ./results-paper/all.csv
Le script generate_fig8.py génère un tracé du coefficient d'évolutivité sur la figure 8. Il nécessite les colonnes walltime (s) , speedup-2 , speedup-4 , speedup-6 et speedup-8 dans le fichier CSV. Il sort fig8-a.png et fig8-b.png .
$ ./generate_fig8.py ./results-paper/all.csv
Le script generate_tab3.py génère les entrées du tableau 2. Il nécessite le benchmark des colonnes, category , walltime (s) , walltime (s)-4 et speedup-4 dans le fichier CSV. Il sort tab2-speedup.csv et tab2-ikos.csv , qui sont utilisés pour remplir le tableau 2.
$ ./generate_tab2.py ./results-paper/all.csv
Le script generate_tab4.py choisit les repères pour le tableau 3 en fonction du coefficient d'évolutivité. Il nécessite la benchmark des colonnes, category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 et speedup-8 dans le fichier CSV. Il publie tab3-candidates.csv . Il faut exécuter des pikos <12> et des pikos <16> sur ces repères en plus pour terminer le tableau 3.
$ ./generate_tab3.py ./results-paper/all.csv
