pikos_popl2020
1.0.0
Dies ist das Software -Artefakt, das das Papier "Deterministische parallele Fixpoint -Berechnung" von Sung Kook Kim, Arnaud J. Venet und Aditya V. Thakur begleitet.
"Deterministische parallele Fixpoint -Berechnung" 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},
}
Es besteht hauptsächlich aus unserem parallelen abstrakten Dolmetscher Pikos, 4330 Benchmarks, die in den Experimenten verwendet werden, und Skripte, um die Ergebnisse in der Arbeit zu reproduzieren.
Pikos basiert auf einem sequentiellen abstrakten Interpreter, IKOS. Die in IKOs geänderten Dateien, um Pikos zu implementieren, sind in CHANGES.md zusammengefasst.md. Bei einem Programm als Eingabe berechnen sowohl IKOs als auch Pikos Invarianten für jeden Programmpunkt und führen Schecks aus. Tatsächlich wird Pikos als Analyseoption von IKOs implementiert, sodass es die Invarianten parallel unter Verwendung mehrerer CPU -Kerne berechnen können. Daher benötigen Pikos Multi-Core-Maschinen, um die Ergebnisse zu reproduzieren. Es erfordert mindestens 16 Kerne , um alle Ergebnisse zu reproduzieren. Ikos wird als Grundlinie ausgewählt.
Nach dem Erstellen und Installieren von Pikos kann man Pikos auf jedem Benchmark ausführen, um einen Analysebericht zu erhalten, die von IKOS und Pikos berechneten Invarianten zu vergleichen oder die Beschleunigung zwischen IKOS und Pikos zu messen. Außerdem kann man die Daten reproduzieren und Tabellen und Figuren im Papier generieren.
Während das Papier die Experimente mit 4330 Benchmarks ausführt, wird empfohlen, die Ergebnisse rechtzeitig zu reproduzieren. Detaillierte AWS -Konfigurationen und -Skripte, die von den Autoren verwendet werden, sind in aws/ bereitgestellt.
Die Referenzumgebung verwendet Ubuntu 16.04 .
Überspringen Sie den Installationsabschnitt, wenn Sie den Docker verwenden. Man braucht docker installiert. Das Bild ist im DockerHub -Repository skkeem/pikos:dev . Der folgende Befehl lädt das Bild herunter und führt es interaktiv aus:
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256: 3D99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
Man kann das Bild auch mit der Dockerfile in diesem Repo erstellen.
$ docker build -t skkeem/pikos:dev .
Das Skript install_dependencies.sh installiert alle erforderlichen Abhängigkeiten. Es erfordert Root -Zugriff.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
Abhängigkeiten:
Python3.6 Abhängigkeiten:
Das Skript install.sh wird Pikos in ./build/ verzeichnis buid und installieren. Es erfordert keinen Root -Zugriff.
$ ./install.sh
Das Skript extract_benchmarks.sh extrahiert Benchmarks in ./benchmarks/ Verzeichnis. Es erfordert keinen Root -Zugriff. Das SHA256SUM der heruntergeladenen Datei ist D4F35509713E1B32135D9FD530B33B02EA11536FD930C6FC3EE9266F6B1B1C1.
$ ./extract_benchmarks.sh
Das Skript run_pikos.sh führt die Analyse im angegebenen Programm aus. Es berechnet die Invarianten und führt Schecks aus. Dieses Skript ist nur zu veranschaulichen, dass Pikos voll funktionsfähiger abstrakter Interpreter ist und nicht verwendet oder bei der Reproduktion der Ergebnisse erforderlich ist.
$ ./run_pikos.sh ./benchmarks/test.c
Wenn Sie die folgende Ausgabe als Ergebnis sehen, war die Installation erfolgreich und Sie können nun die Ergebnisse reproduzieren. Pikos berichtet über zwei Vorkommen des Pufferüberlaufs in Zeile 8 und 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 erbt die Befehlszeilenoptionen von IKOS. Nachfolgend beleuchten die in diesem Artefakt verwendeten Optionen. Die Beschreibung der numerischen abstrakten Domänen stammt aus der Dokumentation von IKOs.
Wenn Sie den Parameter -nt -Parameter verwenden, wird die Anzahl der zulässigen Threads in Pikos eingeschränkt. Im folgenden Befehl werden Pikos mit maximalen 4 Threads ausgeführt:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 ist der Standard. -nt=0 lässt die TBB -Bibliothek die Anzahl der Threads entscheiden. Die Autoren für willkürliche Auswahl von 99 als maximale Anzahl von Threads. Um dies zu ändern, ändern Sie Zeile 991 von ./pikos/analyzer/src/ikos_analyzer.cpp und installieren Sie erneut.
Die Verwendung des Parameters -cs schränkt die Kontextempfindlichkeit in Pikos ein. Diese Zahl entspricht der zulässigen Tiefe der dynamischen Einbeziehung in der interprozeduralen Analyse. Im folgenden Befehl werden Pikos mit maximal 5 Tiefe der Funktionsanrufe ausgeführt:
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0 ist die Standardeinstellung und deaktiviert diese Einschränkung. Diese Einschränkung wird nur für die Benchmarks verwendet, deren Analyse länger als 4 Stunden dauert. Weitere Informationen finden Sie unter benchmarks/README.md .
Die Liste der verfügbaren numerischen abstrakten Domänen (Thread-Safe) lautet:
-d=interval : Die Intervalldomäne, siehe CC77.-d=congruence : Die Kongruenzdomäne, siehe GRA89.-d=interval-congruence : Das reduzierte Produkt von Intervall und Kongruenz.-d=dbm : Die differenzgebundene Matrizendomäne, siehe Pado01.-d=gauge : Die Messdomäne, siehe Cav12.-d=gauge-interval-congruence : Das reduzierte Produkt von Messgerät, Intervall und Kongruenz. Standardmäßig verwendet Pikos die Intervalldomäne und es wurden Experimente damit durchgeführt. Wenn Sie andere Domänen ausprobieren möchten, verwenden Sie den Parameter -d :
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Übergeben der Optionen, --no-checks --no-fixpoint-cache , deaktiviert die Überprüfungen-wie die Analyse des Pufferüberlaufs, Division nach Zero-Analyse, Null-Zeigeranalyse usw.-nach Berechnung der Invarianten:
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Diese werden beim Timing der Ergebnisse verabschiedet , da wir nur über die invariante Berechnungszeit besorgt sind.
Für -nt über 99 wird der Vergleich zwischen IKOS und Pikos anstelle der regulären Analyse durchgeführt. Zum Beispiel wird das Passieren -nt=104 die Invarianten von IKOs und Pikos mit maximalen 4 Threads berechnen und vergleichen. Wenn sich die Invarianten unterscheiden, "unerreicht !!" wird gedruckt und der Vorgang wird zurückgegeben. 42. Alle Läufe mit den obigen abstrakten Domänen sollten die gleichen Invarianten für das Design haben.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
Die Reproduktion der Ergebnisse ist in Schritte unterteilt: (1) Reproduktion der Daten und (2) Erzeugung von Tabellen/Zahlen aus den Daten. Der erste Schritt kann viel Zeit in Anspruch nehmen, wenn Sie alle Daten reproduzieren. Dieser Schritt kann mit AWS ausgeführt werden, um rechtzeitig zu beenden. Weitere Informationen finden Sie unter aws/README.md . Der zweite Schritt sollte nicht viel Zeit in Anspruch nehmen und kann lokal durchgeführt werden. Es müssen immer noch die Abhängigkeiten vor Ort installiert werden. Siehe install_dependencies.sh .
Auch hier kommt Pikos 'Geschwindigkeit aus der Verwendung mehrerer CPU -Kerne. Pikos benötigen Multi-Core-Maschinen, um die Ergebnisse zu reproduzieren. Es erfordert mindestens 16 Kerne , um alle Ergebnisse zu reproduzieren. Für die Skripte mit dem Namen reproduce*.sh geben wir die am wenigsten am Ende der Namen erforderliche Anzahl von Kernen an.
Außerdem ist die Verwendung von TCMALLOC , bei dem es sich um einen in install_dependencies.sh installierten Speicher Allocator handelt. Bitte stellen Sie sicher, dass es ordnungsgemäß installiert ist. Es sollte eine Bibliothek, /usr/local/lib/libtcmalloc.so geben.
Ein optionales Skript, measure_speedup.sh , wird bereitgestellt, um die Beschleunigung eines einzelnen Benchmarks zu messen. Die gleichen Befehlszeilenoptionen wie run_pikos.sh . Es gibt einfach die Geschwindigkeit aus, definiert als die Laufzeit von IKOs / Laufzeit von 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.
Die folgenden Skripte generieren Daten in einer CSV -Datei. Es hat die folgenden Spalten:
benchmark : Name des Benchmarks.category : Die Quelle des Benchmarks. SVC oder OSS.cs : Die verwendete Kontextempfindlichkeit.walltime (s) : Analysezeit in IKOswalltime (s)-k : Analysezeit in Pikos, wobei k die Anzahl der zulässigen Fäden ist.speedup-k : Geschwindigkeit von PikosIgnorieren Sie Warnungen über keine Property -Datei, variabler Austausch und Dateinamen, der beim Ausführen der Skripte zweimal angezeigt wird.
Es läuft auf allen Benchmarks Ikos, Pikos <2>, Pikos <4>, Pikos <6> und Pikos <8>. Es gibt all.csv aus. Dies dauert viel Zeit (ungefähr 48 Tage, wenn nur eine einzelne Maschine verwendet).
$ ./reproduce_all-8.sh
Es läuft auf allen Benchmarks Ikos und Pikos <4>. Es gibt rq1.csv aus. Dies kann zur Beantwortung von RQ1 verwendet werden. Dies dauert auch viel Zeit (ungefähr 25 Tage, wenn nur eine einzelne Maschine verwendet wird).
$ ./reproduce_rq1-4.sh
Es wird IKOS und Pikos <4> auf Benchmarks in Tabelle 3 ausgeführt. Es gibt tab2.csv aus. Dies kann verwendet werden, um Tabelle 2 zu erzeugen. Dies dauert ungefähr 36 Stunden, wenn nur eine einzelne Maschine verwendet wird.
$ ./reproduce_tab2-4.sh
Alternativ kann man nur den oberen Teil von Tabelle 2 ausführen. Es gibt tab2a.csv aus. Dies dauert ungefähr 8 Stunden, wenn nur eine einzelne Maschine verwendet wird.
$ ./reproduce_tab2a-4.sh
Der folgende Befehl misst die Beschleunigung für den Benchmark mit höchster Beschleunigung in Pikos <4>. Das Ergebnis für diesen Benchmark finden Sie im ersten Eintrag der Tabelle 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.
Es läuft IKOS, Pikos <4>, Pikos <8>, Pikos <12> und Pikos <16> auf Benchmarks in Tabelle 3. Es gibt tab3.csv aus. Dies kann verwendet werden, um Tabelle 3 zu erzeugen. Dies dauert ungefähr 12 Stunden, wenn nur eine einzelne Maschine verwendet wird.
$ ./reproduce_tab3-16.sh
Der folgende Befehl misst die Beschleunigungen für den Benchmark mit höchster Skalierbarkeit, ./benchmarks/OSS/audit-2.8.4/aureport.bc/ . Das Ergebnis für diesen Benchmark finden Sie im ersten Eintrag der Tabelle 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.
Die oben erstellte CSV -Datei kann verwendet werden, um Tabellen und Abbildungen im Papier zu erzeugen. Wir werden mit den Daten demonstrieren, die von den Autoren in ./results-paper/all.csv erhalten wurden und durch die Verwendung des in reproduzierten Skripts reproduziert werden können.
Das Skript generate_fig5.py generiert das Streudiagramm in Abb. 5. Es gibt auch die im Abschnitt bewerteten Bewertungsabschnitt aus. Es erfordert die Säulen walltime (s) , walltime (s)-4 und speedup-4 in der CSV-Datei. Es gibt fig5.png aus.
$ ./generate_fig5.py ./results-paper/all.csv
Das Skript generate_fig6.py erzeugt die Histogramme in Abb. 6. Es erfordert die Spalten walltime (s) , walltime (s)-4 und speedup-4 in der CSV-Datei. Es gibt 4 Unterfiguren aus, fig6-[0~3].png .
$ ./generate_fig6.py ./results-paper/all.csv
Das Skript generate_fig9.py erzeugt in Abb. 7 Box-Diagramm und Geigenplot. Es sind in der CSV-Datei die walltime (s) , speedup-2 , speedup-4 , speedup-6 und speedup-8 erforderlich. Es gibt fig7-a.png und fig7-b.png aus.
$ ./generate_fig7.py ./results-paper/all.csv
Das Skript generate_fig8.py erzeugt in Abb. 8 Skalierbarkeitskoeffizienten. Es erfordert die walltime (s) , speedup-2 , speedup-4 , speedup-6 und speedup-8 in der CSV-Datei. Es gibt fig8-a.png und fig8-b.png .
$ ./generate_fig8.py ./results-paper/all.csv
Das Skript generate_tab3.py generiert die Einträge für die Tabelle 2. Es erfordert die Spalten benchmark , die category , walltime (s) , walltime (s)-4 und speedup-4 in der CSV-Datei. Es gibt tab2-speedup.csv und tab2-ikos.csv aus, die zum Ausfüllen von Tabelle 2 verwendet werden.
$ ./generate_tab2.py ./results-paper/all.csv
Das Skript generate_tab4.py wählt die Benchmarks für Tabelle 3 basierend auf dem Skalierbarkeitskoeffizienten aus. Es erfordert die Säulen benchmark , category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 und speedup-8 in der CSV-Datei. Es gibt tab3-candidates.csv aus. Man muss Pikos <12> und Pikos <16> auf diesen Benchmarks zusätzlich ausführen, um die Tabelle 3 zu vervollständigen.
$ ./generate_tab3.py ./results-paper/all.csv
