pikos_popl2020
1.0.0
これは、Sung Kook Kim、Arnaud J. Venet、およびAditya V. Thakurによる「決定論的並列固定点計算」に伴うソフトウェアアーティファクトです。
「決定論的な並列固定点計算」プレプリント：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},
}
主に、並行抽象通訳者Pikos、実験で使用される4330のベンチマーク、およびペーパーの結果を再現するためのスクリプトで構成されています。
Pikosは、連続した抽象的な通訳であるIkosに基づいています。 ikosで変更されたファイルは、pikosを実装するために変更されていますCHANGES.md 。入力としてのプログラムが与えられた場合、各プログラムポイントでIKOSとPIKOSの両方が不変剤を計算し、それらをチェックします。実際、PikosはIKOSの分析オプションとして実装されており、複数のCPUコアを使用して不変剤を並行して計算できるようにします。したがって、 Pikosは結果を再現するためにマルチコアマシンを必要とします。すべての結果を再現するには、少なくとも16個のコアが必要です。イコスはベースラインとして選ばれます。
Pikosを構築およびインストールした後、各ベンチマークでPikosを実行して分析レポートを取得したり、IkosとPikosによって計算された不変性を比較したり、IkosとPikosの間の速度を測定したりできます。また、データを再現し、論文内の表と数字を生成することができます。
このペーパーが4330ベンチマークで実験を実行すると、結果をタイムリーに再現するためにクラウドコンピューティング環境が推奨されます。著者が使用する詳細なAWS構成とスクリプトは、 aws/で提供されています。
参照環境ではUbuntu 16.04を使用しています。
Dockerを使用している場合は、インストールセクションをスキップします。 dockerがインストールされる必要があります。この画像は、dockerhubリポジトリskkeem/pikos:devで利用できます。次のコマンドでは、画像をダウンロードして、インタラクティブリーを実行します。
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256：3D99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
また、このリポジトリのDockerFileを使用して画像を作成することもできます。
$ docker build -t skkeem/pikos:dev .
スクリプトinstall_dependencies.sh 、必要なすべての依存関係をインストールします。ルートアクセスが必要です。
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
依存関係：
python3.6依存関係：
スクリプトinstall.sh 、pikos ./build/ build/ directoryにバイイドおよびインストールされます。ルートアクセスは必要ありません。
$ ./install.sh
スクリプトextract_benchmarks.sh ./benchmarks/ディレクトリでベンチマークを抽出します。ルートアクセスは必要ありません。ダウンロードされたファイルのSha256SumはD4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE926666B1B1C1です。
$ ./extract_benchmarks.sh
スクリプトrun_pikos.sh 、指定されたプログラムで分析を実行します。不変剤を計算し、チェックを実行します。このスクリプトは、Pikosが完全に機能している抽象的な通訳者であり、結果を再現する際に使用または必要はないことを説明するためだけです。
$ ./run_pikos.sh ./benchmarks/test.c
結果として次の出力が表示された場合、インストールが成功し、結果を再現できるようになりました。 Pikosは、8行目と9行でバッファオーバーフローの2つの発生を報告しています。
[*] 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は、Ikosのコマンドラインオプションを継承します。以下は、このアーティファクトで使用される関連オプションを強調しています。数値抽象ドメインの説明は、IKOSのドキュメントから取得されます。
-ntパラメーターを使用すると、PIKOSの許可されたスレッドの数が制限されます。次のコマンドは、最大4つのスレッドでpikosを実行します。
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4はデフォルトです。 -nt=0 TBBライブラリにスレッドの数を決定させます。著者は、任意のスレッドの最大数として99を選択しました。これを変更するには、 ./pikos/analyzer/src/ikos_analyzer.cpp pikos/analyzer/src/ikos_analyzer.cppの行991を変更して、再度インストールします。
-csパラメーターを使用すると、PIKOSのコンテキスト感度が制限されます。この数値は、我本間分析における動的インラインの許可された深さに対応しています。次のコマンドは、最大5の機能深度呼び出しでPikosを実行します。
$ ./run_pikos.sh -cs=5 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-cs=0はデフォルトであり、この制限を無効にします。この制限は、分析に4時間以上かかるベンチマークにのみ使用されます。詳細については、 benchmarks/README.mdを参照してください。
利用可能な（スレッドセーフ）数値抽象的なドメインのリストは次のとおりです。
-d=interval ：間隔ドメイン、CC77を参照してください。-d=congruence ：合同ドメイン、GRA89を参照してください。-d=interval-congruence ：間隔と合同の産物の減少。-d=dbm ：差異マトリックスドメイン、pado01を参照してください。-d=gauge ：ゲージドメイン、CAV12を参照してください。-d=gauge-interval-congruence ：ゲージ、間隔、合同の産物の減少。デフォルトでは、Pikosは間隔ドメインを使用し、実験を実施しました。他のドメインを試してみたい場合は、 -dパラメーターを使用します。
$ ./run_pikos.sh -nt=4 -d=dbm ./benchmarks/OSS/audit-2.8.4/ausearch.bc
--no-checks --no-fixpoint-cache 、バッファオーバーフロー分析、ゼロ分析による分割、ヌルポインター分析などのチェックを無効にするオプションを渡します。
$ ./run_pikos.sh -nt=4 -d=dbm --no-checks --no-fixpoint-cache ./benchmarks/OSS/audit-2.8.4/ausearch.bc
不変の計算時間のみを心配しているため、結果のタイミング時に渡されます。
99を超える-ntの場合、定期的な分析の代わりに、IkosとPikosの比較が実行されます。たとえば、Passing -nt=104 、最大4つのスレッドでIkosとPikosの不変性を計算して比較します。不変剤が異なる場合は、「無礼!!」印刷され、プロセスは42を返します。上記の抽象的なドメインを使用してすべての実行は、設計上、同じ不変式を持つ必要があります。
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
結果を再現することは、次の手順に分けられます。（1）データの再現と（2）データからテーブル/図を生成する。すべてのデータを再現することを選択した場合、最初のステップには多くの時間がかかる場合があります。このステップは、AWSを使用してタイムリーに完了することができます。詳細については、 aws/README.md参照してください。 2番目のステップは時間をかけてはならず、ローカルで行うことができます。それでも、依存関係をローカルにインストールする必要があります。 install_dependencies.sh参照してください。
繰り返しますが、Pikosのスピードアップは、複数のCPUコアを使用することから来ています。 Pikosは、結果を再現するためにマルチコアマシンを必要とします。すべての結果を再現するには、少なくとも16個のコアが必要です。 reproduce*.shという名前のスクリプトの場合、名前の最後に必要なコアの最小量を指定します。
また、 install_dependencies.shにインストールされたメモリアロケーターであるTcmallocの使用は、結果を再現する必要があります。適切にインストールされていることを確認してください。ライブラリ、 /usr/local/lib/libtcmalloc.so local/lib/libtcmalloc.soが必要です。
オプションのスクリプトであるmeasure_speedup.shが提供され、単一のベンチマークの速度を測定します。 run_pikos.shと同じコマンドラインオプションが必要です。 PikosのIKOS /実行時間の実行時間として定義されるスピードアップを単純に出力します。
$ ./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.
次のスクリプトは、CSVファイルにデータを生成します。次の列があります。
benchmark ：ベンチマークの名前。category ：ベンチマークのソース。 SVCまたはOSS。cs ：使用されるコンテキスト感度。walltime (s) ：イコスの分析時間walltime (s)-k ：PIKOSの分析時間。ここで、Kは許可されているスレッドの数です。speedup-k ：Pikosのスピードアップスクリプトを実行するときに2回表示されるプロパティファイル、可変交換、ファイル名についての警告を無視します。
Ikos、Pikos <2>、Pikos <4>、Pikos <6>、およびPikos <8>をすべてのベンチマークで実行します。 all.csvを出力します。これには多くの時間がかかります（単一のマシンのみを使用する場合は約48日）。
$ ./reproduce_all-8.sh
すべてのベンチマークでikosとpikos <4>を実行します。 rq1.csvを出力します。これは、RQ1に答えるために使用できます。これには多くの時間がかかります（単一のマシンのみを使用する場合、約25日）。
$ ./reproduce_rq1-4.sh
表3のベンチマークでikosとpikos <4>を実行しますtab2.csvを出力します。これを使用して表2を生成できます。単一のマシンのみを使用する場合、これには約36時間かかります。
$ ./reproduce_tab2-4.sh
または、表2の上部のみを実行することを選択できますtab2a.csvを出力します。単一のマシンのみを使用する場合、これには約8時間かかります。
$ ./reproduce_tab2a-4.sh
次のコマンドは、Pikos <4>で最高のスピードアップでベンチマークのスピードアップを測定します。このベンチマークの結果は、表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.
Ikos、Pikos <4>、Pikos <8>、Pikos <12>、およびPikos <16>を表3のベンチマークで実行しますtab3.csvを出力します。これを使用して表3を生成できます。単一のマシンのみを使用する場合、これには約12時間かかります。
$ ./reproduce_tab3-16.sh
次のコマンドは、ベンチマークのスピードアップを最も高いスケーラビリティで測定します./benchmarks/OSS/audit-2.8.4/aureport.bc/ 。このベンチマークの結果は、表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.
上記で作成されたCSVファイルを使用して、論文内の表と図を生成できます。著者が./results-paper/all.csvの著者が取得したデータを実証します。
スクリプトgenerate_fig5.py 、図5に散布図を生成します。また、評価セクションで説明されている平均も出力します。 CSVファイルには、列のwalltime (s) 、 walltime (s)-4 、およびspeedup-4が必要です。 fig5.pngを出力します。
$ ./generate_fig5.py ./results-paper/all.csv
スクリプトgenerate_fig6.py 、図6にヒストグラムを生成します。これは、csvファイルの列のwalltime (s) 、 walltime (s)-4 、およびspeedup-4が必要です。 fig6-[0~3].pngを出力します。
$ ./generate_fig6.py ./results-paper/all.csv
スクリプトgenerate_fig9.py 、図7にボックスプロットとバイオリンプロットを生成します。CSVファイルの列walltime (s) 、 speedup-2 、 speedup-4 、 speedup-6 、およびspeedup-8が必要です。 fig7-a.pngとfig7-b.pngを出力します。
$ ./generate_fig7.py ./results-paper/all.csv
スクリプトgenerate_fig8.py 、図8にスケーラビリティ係数プロットを生成します。CSVファイルの列walltime (s) 、 speedup-2 、 speedup-4 、 speedup-6 、およびspeedup-8が必要です。 fig8-a.pngとfig8-b.pngを出力します。
$ ./generate_fig8.py ./results-paper/all.csv
スクリプトgenerate_tab3.py 、表2のエントリを生成します。CSVファイルの列benchmark 、 category 、 walltime (s) 、 walltime (s)-4 、およびspeedup-4が必要です。 tab2-speedup.csvおよびtab2-ikos.csvを出力します。これらは、表2の記入に使用されます。
$ ./generate_tab2.py ./results-paper/all.csv
スクリプトgenerate_tab4.py 、スケーラビリティ係数に基づいて表3のベンチマークを選択します。 CSVファイルには、列benchmark 、 category 、 cs 、 walltime (s) 、 walltime (s)-4 、 speedup-2 、 speedup-4 、 speedup-6 、 speedup-8が必要です。 tab3-candidates.csvを出力します。これらのベンチマークでPikos <12>およびPikos <16>を実行するには、表3を完成させる必要があります。
$ ./generate_tab3.py ./results-paper/all.csv
