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
