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},
}
它主要由我們的平行抽象解釋器長矛，實驗中使用的4330個基準和用於復制論文結果的腳本。
Pikos基於一個順序的抽象解釋器IKO。更改中的IKO中的文件更改以實現CHANGES.md 。給定一個程序作為輸入，IKOS和PIKOS都在每個程序點上計算不變性，並對它們進行檢查。實際上，Pikos是IKO的分析選項實現的，允許它使用多個CPU內核並行計算不變性。因此， Pikos需要多核機器來再現結果。它需要至少16個核心重現所有結果。 IKO被選為基線。
構建和安裝Pikos後，可以在每個基準測試上運行Pikos以獲取分析報告，比較Ikos和Pikos計算的不變性，或者測量IKOS和PIKOS之間的加速。另外，可以重現數據並在論文中生成表格和數字。
由於本文在4330個基准上運行實驗時，建議使用雲計算環境來及時再現結果。作者使用的詳細AWS配置和腳本以aws/提供。
參考環境使用Ubuntu 16.04 。
如果您使用的是Docker，則跳過安裝部分。一個需要安裝的docker 。該圖像在Dockerhub存儲庫skkeem/pikos:dev 。以下命令將下載圖像並運行It Interactivley：
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256：3D99811735E0E3577EEEA7EEA9078532323D1975AC6250939BA4BA4F70E6695EBEDF55520
一個人還可以在此存儲庫中使用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將在./build/ Directory中buid並安裝Pikos。它不需要根訪問。
$ ./install.sh
Script extract_benchmarks.sh將在./benchmarks/目錄中提取基準測試。它不需要根訪問。下載文件的SHA256SUM是D4F355097133E1B32135D9FD533B33B02EA11536FD930C6FC3EE9266F6B1B1B1B1C1。
$ ./extract_benchmarks.sh
腳本run_pikos.sh在給定程序上運行分析。它計算不變性並運行檢查。該腳本只是為了說明pikos正在充分發揮抽象解釋器的功能，並且在重現結果時沒有使用或不需要。
$ ./run_pikos.sh ./benchmarks/test.c
如果將以下輸出視為結果，則安裝成功，現在可以復制結果。 Pikos報告了第8和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繼承了IKOS的命令行選項。下面突出顯示了此工件中使用的相關選項。數值抽象域的描述取自IKO的文檔。
使用-nt參數限制匹克中允許線的數量。以下命令將運行具有最大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的991行並再次安裝。
使用-cs參數限制了皮科斯中的上下文靈敏度。該數字對應於概要分析中允許的動態內部內部允許的深度。以下命令將運行具有最大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 ，將進行IKO和PIKOS之間的比較，而不是常規分析。例如，傳遞-nt=104將計算並比較具有最大4個線程的IKO和PIKO的不變性。如果不變的人有所不同，則“不對！”將被打印，該過程將返回42。使用上述抽象域的所有運行都應通過設計具有相同的不變性。
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
再現結果分為步驟：（1）重現數據，（2）從數據中生成表/數字。如果您選擇複製所有數據，第一步可能需要大量時間。可以使用AWS及時完成此步驟。有關更多信息，請參見aws/README.md 。第二步不應該花費太多時間，可以在本地完成。它仍然需要在本地安裝依賴項。請參閱install_dependencies.sh 。
同樣，Pikos的加速來自利用多個CPU內核。長芯需要多核機器來再現結果。它需要至少16個核心重現所有結果。對於帶有reproduce*.sh名稱的腳本，我們將指定名稱末尾所需的最少核心。
另外，使用TCMALLOC （是安裝install_dependencies.sh中安裝的內存分配器）。 SH，必須重現結果。請確保其安裝正確。應該有一個庫， /usr/local/lib/libtcmalloc.so 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) ：IKO中的分析時間walltime (s)-k ：pikos中的分析時間，其中k是允許的線數。speedup-k ：pikos的加速忽略關於未屬性文件，可變替換和文件名在運行腳本時出現兩次的警告。
它在所有基准上運行IKOS，Pikos <2>，Pikos <4>，Pikos <6>和Pikos <8>。它輸出all.csv 。這需要大量時間（如果只使用一台計算機，大約48天）。
$ ./reproduce_all-8.sh
它在所有基準標准上運行IKO和PIKOS <4>。它輸出rq1.csv 。這可以用來回答RQ1。這也需要很多時間（大約25天，如果只使用一台機器）。
$ ./reproduce_rq1-4.sh
它在表3的基准上運行IKO和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/ /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 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 。它輸出了4個亞圖， fig6-[0~3].png 。
$ ./generate_fig6.py ./results-paper/all.csv
腳本generate_fig9.py在圖7中生成盒子圖和小提琴圖。它需要CSV文件中的walltime (s) ， speedup-2 ， speedup-4 ，SPEEDUP-4，SPEDUP-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-4， speedup-6和speedup-8 。它輸出tab3-candidates.csv 。除了完成表3，必須在這些基準測試上運行Pikos <12>和Pikos <16>。
$ ./generate_tab3.py ./results-paper/all.csv
