pikos_popl2020
1.0.0
이것은 Sung Kook Kim, Arnaud J. Venet 및 Aditya V. Thakur의 논문 "결정 론적 병렬 고정 점 계산"에 수반되는 소프트웨어 아티팩트입니다.
"결정 론적 병렬 고정 점 계산" 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},
}
주로 병렬 추상 통역사 Pikos, 실험에 사용 된 4330 벤치 마크 및 논문의 결과를 재현하기위한 스크립트로 구성됩니다.
Pikos는 순차적 인 초록 통역사 인 Ikos를 기반으로합니다. Pikos를 구현하기 위해 Ikos에서 변경된 파일은 CHANGES.md 에 요약되어 있습니다. 입력으로 프로그램이 주어지면 IKO와 Pikos는 각 프로그램 지점에서 불변량을 계산하고 실행 확인을 수행합니다. 실제로, Pikos는 IKO의 분석 옵션으로 구현되어 여러 CPU 코어를 사용하여 불변량을 병렬로 계산할 수 있습니다. 따라서 Pikos는 결과를 재현하기 위해 멀티 코어 머신이 필요합니다. 모든 결과를 재현하려면 최소 16 개의 코어가 필요합니다. Ikos는 기준선으로 선정되었습니다.
Pikos를 구축하고 설치 한 후 각 벤치 마크에서 Pikos를 실행하여 분석 보고서를 얻거나 Ikos와 Pikos가 계산 한 불변량을 비교하거나 Ikos와 Pikos 간의 속도를 측정 할 수 있습니다. 또한 종이에서 데이터를 재현하고 테이블과 그림을 생성 할 수 있습니다.
논문이 4330 벤치 마크에서 실험을 실행함에 따라 클라우드 컴퓨팅 환경은 결과를 적시에 재현하는 것이 좋습니다. 저자가 사용하는 세부 AWS 구성 및 스크립트는 aws/ 로 제공됩니다.
기준 환경은 Ubuntu 16.04 사용합니다.
Docker를 사용하는 경우 설치 섹션을 건너 뜁니다. docker 설치해야합니다. DockerHub 리포지토리 skkeem/pikos:dev 에서 이미지가 사용됩니다. 다음 명령은 이미지를 다운로드하고 interactivley를 실행합니다.
$ docker run --rm -v /sys/fs/cgroup:/sys/fs/cgroup:rw -w /pikos_popl2020 -it --privileged skkeem/pikos:dev
SHA256 : 3D99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
이 repo에서 dockerfile을 사용하여 이미지를 빌드 할 수도 있습니다.
$ docker build -t skkeem/pikos:dev .
script install_dependencies.sh 필요한 모든 종속성을 설치합니다. 루트 액세스가 필요합니다.
$ sudo ./install_dependencies.sh
$ sudo usermod -aG benchexec $USER
$ ./install_python_dependencies.sh
종속성 :
Python3.6 종속성 :
스크립트 install.sh ./build/ directory에서 pikos를 buid 및 설치합니다. 루트 액세스가 필요하지 않습니다.
$ ./install.sh
스크립트 extract_benchmarks.sh ./benchmarks/ directory에서 벤치 마크를 추출합니다. 루트 액세스가 필요하지 않습니다. 다운로드 된 파일의 SHA256SUM은 D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE926F6F6B1C1입니다.
$ ./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 매개 변수를 사용하면 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 의 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 , 정기 분석 대신 IKO와 Pikos의 비교가 수행됩니다. 예를 들어, -nt=104 통과하면 Ikos와 Pikos의 불변량을 최대 4 개의 스레드와 계산하고 비교합니다. 불변이 다르면 "타의 추종을 불허합니다!" 인쇄되고 프로세스는 42를 반환합니다. 위의 추상 도메인을 사용하여 모든 실행은 디자인 별 동일한 불일치를 가져야합니다.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
결과를 재현하는 단계는 다음 단계로 나뉩니다. (1) 데이터를 재현하고 (2) 데이터에서 테이블/그림을 생성합니다. 모든 데이터를 재현하려면 첫 번째 단계에 많은 시간이 걸릴 수 있습니다. 이 단계는 AWS를 사용하여 적시에 마무리 할 수 있습니다. 자세한 내용은 aws/README.md 참조하십시오. 두 번째 단계는 시간이 많이 걸리지 않아야하며 로컬로 수행 할 수 있습니다. 여전히 종속성을 로컬로 설치해야합니다. install_dependencies.sh 참조하십시오.
다시, Pikos의 속도는 여러 CPU 코어를 사용하여 비롯됩니다. Pikos는 결과를 재현하기 위해 멀티 코어 머신이 필요합니다. 모든 결과를 재현하려면 최소 16 개의 코어가 필요합니다. reproduce*.sh 이름이있는 스크립트의 경우 이름 끝에서 필요한 코어의 최소량을 지정합니다.
또한 install_dependencies.sh 에 설치된 메모리 할당자인 TCMalloc 의 사용은 결과를 재현해야합니다. 제대로 설치되어 있는지 확인하십시오. /usr/local/lib/libtcmalloc.so 가 있어야합니다.
단일 벤치 마크의 속도를 측정하기 위해 선택적인 스크립트 measure_speedup.sh 가 제공됩니다. run_pikos.sh 와 동일한 명령 줄 옵션이 필요합니다. Pikos의 Ikos / Running Time의 실행 시간으로 정의 된 속도를 단순히 출력합니다.
$ ./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) : Ikos의 분석 시간walltime (s)-k : pikos의 분석 시간, 여기서 k는 허용 된 스레드 수입니다.speedup-k : 피코의 스피드 업스크립트를 실행할 때 PropertyFile, 가변 교체 및 파일 이름에 대한 경고를 무시하십시오.
그것은 모든 벤치 마크에서 ikos, pikos <2>, pikos <4>, pikos <6> 및 pikos를 실행합니다. all.csv 출력합니다. 시간이 많이 걸립니다 (단일 시스템 만 사용하는 경우 약 48 일).
$ ./reproduce_all-8.sh
모든 벤치 마크에서 Ikos와 Pikos를 실행합니다. rq1.csv 출력합니다. 이것은 RQ1에 대답하는 데 사용될 수 있습니다. 시간이 많이 걸립니다 (단일 시스템 만 사용하는 경우 약 25 일).
$ ./reproduce_rq1-4.sh
표 3의 벤치 마크에서 Ikos와 Pikos를 실행합니다. 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.
표 3의 벤치 마크에서 ikos, pikos <4>, pikos <8>, pikos <12> 및 pikos <16>을 실행합니다. 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 열이 필요합니다. 4 개의 하위 포도, fig6-[0~3].png 출력합니다.
$ ./generate_fig6.py ./results-paper/all.csv
스크립트 generate_fig9.py 그림 7에서 Box 플롯과 바이올린 플롯을 생성합니다. 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 필요합니다. 표 2를 채우는 데 사용되는 tab2-speedup.csv 및 tab2-ikos.csv 출력합니다.
$ ./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
