pikos_popl2020
1.0.0
Ini adalah artefak perangkat lunak yang menyertai kertas "perhitungan fixpoint paralel deterministik" oleh Sung Kook Kim, Arnaud J. Venet, dan Aditya V. Thakur.
"Perhitungan FixPoint Paralel Deterministik" 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},
}
Ini terutama terdiri dari pikos interpreter abstrak paralel kami, 4330 tolok ukur yang digunakan dalam percobaan, dan skrip untuk mereproduksi hasil dalam makalah.
Pikos didasarkan pada interpreter abstrak berurutan, IKOS. File berubah di IKOS untuk mengimplementasikan pikos dirangkum dalam CHANGES.md . Diberikan program sebagai input, baik IKOS dan Pikos menghitung invarian pada setiap titik program dan menjalankan pemeriksaan pada mereka. Faktanya, Pikos diimplementasikan sebagai opsi analisis IKO, yang memungkinkannya menghitung invarian secara paralel menggunakan beberapa core CPU. Oleh karena itu, pikos membutuhkan mesin multi-core untuk mereproduksi hasilnya. Ini membutuhkan setidaknya 16 core untuk mereproduksi semua hasil. IKOS dipilih sebagai garis dasar.
Setelah membangun dan memasang pikos, seseorang dapat menjalankan pikos pada setiap tolok ukur untuk mendapatkan laporan analisis, membandingkan invarian yang dihitung oleh IKOS dan Pikos, atau mengukur speedup antara IKO dan Pikos. Juga, seseorang dapat mereproduksi data dan menghasilkan tabel dan angka di koran.
Saat kertas menjalankan percobaan pada 4330 tolok ukur, lingkungan komputasi awan disarankan untuk mereproduksi hasilnya secara tepat waktu. Konfigurasi dan skrip AWS terperinci yang digunakan oleh penulis disediakan dalam aws/ .
Lingkungan referensi menggunakan Ubuntu 16.04 .
Lewati bagian instalasi jika Anda menggunakan Docker. Seseorang perlu docker terpasang. Gambar tersedia di repositori Dockerhub skkeem/pikos:dev . Perintah berikut akan mengunduh gambar dan menjalankannya Interactivley:
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256: 3D99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
Seseorang juga dapat membangun gambar menggunakan DockerFile dalam repo ini.
$ docker build -t skkeem/pikos:dev .
Script install_dependencies.sh akan menginstal semua dependensi yang diperlukan. Itu membutuhkan akses root.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
Ketergantungan:
Python3.6 Ketergantungan:
Script install.sh akan mendapatkan dan menginstal pikos di ./build/ direktori. Itu tidak memerlukan akses root.
$ ./install.sh
extract_benchmarks.sh skrip akan mengekstraksi tolok ukur di ./benchmarks/ direktori. Itu tidak memerlukan akses root. SHA256SUM dari file yang diunduh adalah D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE9266F6B1B1C1.
$ ./extract_benchmarks.sh
Skrip run_pikos.sh menjalankan analisis pada program yang diberikan. Itu menghitung invarian dan menjalankan cek di atasnya. Script ini hanya untuk menggambarkan bahwa pikos adalah interpreter abstrak yang berfungsi penuh, dan tidak digunakan atau diperlukan dalam mereproduksi hasil.
$ ./run_pikos.sh ./benchmarks/test.c
Jika Anda melihat output berikut sebagai hasilnya, instalasi berhasil, dan sekarang Anda dapat mereproduksi hasilnya. Pikos melaporkan dua kemunculan buffer overflow di baris 8 dan 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 mewarisi opsi baris perintah IKOS. Di bawah ini menyoroti opsi relevan yang digunakan dalam artefak ini. Deskripsi domain abstrak numerik diambil dari dokumentasi IKOS.
Menggunakan parameter -nt membatasi jumlah utas yang diizinkan di pikos. Perintah berikut akan menjalankan pikos dengan maksimum 4 utas:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 adalah default. -nt=0 akan membiarkan perpustakaan TBB memutuskan jumlah utas. Penulis sewenang -wenang memilih 99 sebagai jumlah maksimum utas. Untuk mengubah ini, ubah baris 991 dari ./pikos/analyzer/src/ikos_analyzer.cpp dan instal lagi.
Menggunakan parameter -cs membatasi sensitivitas konteks di piko. Jumlah ini sesuai dengan kedalaman inlining dinamis yang diizinkan dalam analisis interprocedural. Perintah berikut akan menjalankan pikos dengan maksimum 5 panggilan fungsi:
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0 adalah default, dan menonaktifkan pembatasan ini. Pembatasan ini hanya digunakan untuk tolok ukur yang membutuhkan waktu lebih dari 4 jam untuk dianalisis. Lihat benchmarks/README.md untuk lebih jelasnya.
Daftar domain abstrak numerik (utas-aman) yang tersedia adalah:
-d=interval : Domain interval, lihat CC77.-d=congruence : domain kongruensi, lihat GRA89.-d=interval-congruence : Pengurangan produk interval dan kongruensi.-d=dbm : Domain matriks-terikat-bound, lihat PADO01.-d=gauge : domain pengukur, lihat Cav12.-d=gauge-interval-congruence : Produk pengukur, interval, dan kongruensi. Secara default, Pikos menggunakan domain interval , dan percobaan dilakukan dengannya. Jika Anda ingin mencoba domain lain, gunakan parameter -d :
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Melewati opsi, --no-checks --no-fixpoint-cache , menonaktifkan cek-seperti analisis buffer overflow, divisi dengan analisis nol, analisis pointer nol, dll-setelah menghitung invarian:
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
Ini diteruskan saat mengatur waktu hasilnya , karena kami hanya khawatir tentang waktu perhitungan invarian.
Untuk -nt di atas 99, perbandingan antara IKOS dan Pikos akan dilakukan alih -alih analisis reguler. Misalnya, passing -nt=104 akan menghitung dan membandingkan invarian IKOS dan Pikos dengan maksimum 4 utas. Jika invarian berbeda, "Unmatch !!" akan dicetak dan prosesnya akan mengembalikan 42. Semua berjalan menggunakan domain abstrak di atas harus memiliki invarian yang sama berdasarkan desain.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
Mereproduksi hasilnya dibagi menjadi langkah -langkah: (1) mereproduksi data dan (2) menghasilkan tabel/angka dari data. Langkah pertama mungkin membutuhkan banyak waktu jika Anda memilih untuk mereproduksi semua data. Langkah ini dapat dilakukan dengan menggunakan AWS untuk menyelesaikan tepat waktu. Lihat aws/README.md untuk informasi lebih lanjut. Langkah kedua seharusnya tidak membutuhkan banyak waktu dan dapat dilakukan secara lokal. Itu masih membutuhkan dependensi untuk dipasang secara lokal. Lihat install_dependencies.sh .
Sekali lagi, speedup Pikos berasal dari memanfaatkan beberapa inti CPU. Pikos membutuhkan mesin multi-core untuk mereproduksi hasilnya. Ini membutuhkan setidaknya 16 core untuk mereproduksi semua hasil. Untuk skrip dengan nama reproduce*.sh , kami akan menentukan jumlah core yang diperlukan di akhir nama.
Juga, penggunaan tcmalloc , yang merupakan pengalokasi memori yang diinstal di install_dependencies.sh , adalah suatu keharusan dalam mereproduksi hasilnya. Pastikan diinstal dengan benar. Harus ada perpustakaan, /usr/local/lib/libtcmalloc.so .
Skrip opsional, measure_speedup.sh , disediakan untuk mengukur speedup dari satu tolok ukur. Dibutuhkan opsi baris perintah yang sama dengan run_pikos.sh . Ini hanya menghasilkan speedup, didefinisikan sebagai waktu berjalan IKOS / waktu berjalan 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.
Script berikut menghasilkan data dalam file CSV. Ini memiliki kolom berikut:
benchmark : Nama Benchmark.category : Sumber tolok ukur. SVC atau OSS.cs : Sensitivitas konteks yang digunakan.walltime (s) : Waktu analisis di IKOSwalltime (s)-k : Waktu analisis di pikos, di mana k adalah jumlah benang yang diizinkan.speedup-k : Speedup of PikosAbaikan peringatan tentang tidak ada propertyfile, penggantian variabel, dan nama file muncul dua kali saat menjalankan skrip.
Ini menjalankan IKOS, Pikos <2>, Pikos <4>, Pikos <6>, dan Pikos <8> pada semua tolok ukur. Itu menghasilkan all.csv . Ini membutuhkan banyak waktu (kira -kira 48 hari, jika hanya menggunakan satu mesin).
$ ./reproduce_all-8.sh
Ini menjalankan Ikos dan Pikos <4> pada semua tolok ukur. Ini output rq1.csv . Ini dapat digunakan untuk menjawab RQ1. Ini membutuhkan banyak waktu juga (kira -kira 25 hari, jika hanya menggunakan satu mesin).
$ ./reproduce_rq1-4.sh
Ini menjalankan IKOS dan Pikos <4> pada tolok ukur pada Tabel 3. Outputnya tab2.csv . Ini dapat digunakan untuk menghasilkan Tabel 2. Ini membutuhkan waktu sekitar 36 jam, jika hanya menggunakan satu mesin.
$ ./reproduce_tab2-4.sh
Atau, seseorang dapat memilih untuk menjalankan hanya bagian atas Tabel 2. Outputnya tab2a.csv . Ini membutuhkan waktu sekitar 8 jam, jika hanya menggunakan satu mesin.
$ ./reproduce_tab2a-4.sh
Perintah berikut mengukur speedup untuk tolok ukur dengan speedup tertinggi di Pikos <4>. Hasil untuk tolok ukur ini dapat ditemukan di entri pertama Tabel 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.
Ini menjalankan IKOS, Pikos <4>, Pikos <8>, Pikos <12>, dan Pikos <6> pada tolok ukur pada Tabel 3. IT output tab3.csv . Ini dapat digunakan untuk menghasilkan Tabel 3. Ini membutuhkan waktu sekitar 12 jam, jika hanya menggunakan satu mesin.
$ ./reproduce_tab3-16.sh
Perintah berikut mengukur speedup untuk tolok ukur dengan skalabilitas tertinggi, ./benchmarks/OSS/audit-2.8.4/aureport.bc/ . Hasil untuk tolok ukur ini dapat ditemukan di entri pertama Tabel 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.
File CSV yang diproduksi di atas dapat digunakan untuk menghasilkan tabel dan angka di koran. Kami akan menunjukkan dengan data yang diperoleh oleh penulis di ./results-paper/all.csv , yang dapat direproduksi dengan menggunakan skrip yang dijelaskan dalam reproduksi semua.
Script generate_fig5.py menghasilkan plot sebar pada Gambar. 5. Ini juga menghasilkan cara yang dijelaskan di bagian evaluasi. Dibutuhkan kolom walltime (s) , walltime (s)-4 , dan speedup-4 dalam file CSV. Itu output fig5.png .
$ ./generate_fig5.py ./results-paper/all.csv
Script generate_fig6.py menghasilkan histogram pada Gambar. 6. Ini membutuhkan kolom walltime (s) , walltime (s)-4 , dan speedup-4 dalam file CSV. Ini output 4 subfigures, fig6-[0~3].png .
$ ./generate_fig6.py ./results-paper/all.csv
Script generate_fig9.py menghasilkan plot kotak dan plot biola pada Gambar. 7. Ini membutuhkan kolom walltime (s) , speedup-2 , speedup-4 , speedup-6 , dan speedup-8 dalam file CSV. Ini output fig7-a.png dan fig7-b.png .
$ ./generate_fig7.py ./results-paper/all.csv
Script generate_fig8.py menghasilkan plot koefisien skalabilitas pada Gambar. 8. Ini membutuhkan kolom walltime (s) , speedup-2 , speedup-4 , speedup-6 , dan speedup-8 dalam file CSV. Ini output fig8-a.png dan fig8-b.png .
$ ./generate_fig8.py ./results-paper/all.csv
Script generate_tab3.py menghasilkan entri untuk Tabel 2. Ini membutuhkan benchmark kolom, category , walltime (s) , walltime (s)-4 , dan speedup-4 dalam file CSV. Output itu tab2-speedup.csv dan tab2-ikos.csv , yang digunakan untuk mengisi Tabel 2.
$ ./generate_tab2.py ./results-paper/all.csv
Script generate_tab4.py memilih tolok ukur untuk Tabel 3 berdasarkan koefisien skalabilitas. Ini membutuhkan benchmark kolom, category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 , dan speedup-8 dalam file CSV. Ini output tab3-candidates.csv . Seseorang harus menjalankan Pikos <11> dan Pikos <6> pada tolok ukur ini juga untuk menyelesaikan Tabel 3.
$ ./generate_tab3.py ./results-paper/all.csv
