pikos_popl2020
1.0.0
นี่คือสิ่งประดิษฐ์ซอฟต์แวร์ที่มาพร้อมกับกระดาษ
"การคำนวณจุดแก้ไขแบบคู่ขนาน" 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 ไฟล์ที่เปลี่ยนแปลงใน IKOS เพื่อใช้ Pikos สรุปไว้ใน CHANGES.md MD ให้โปรแกรมเป็นอินพุตทั้ง IKOS และ Pikos คำนวณค่าคงที่ในแต่ละจุดโปรแกรมและเรียกใช้การตรวจสอบพวกเขา ในความเป็นจริง Pikos ถูกนำมาใช้เป็นตัวเลือกการวิเคราะห์ของ IKOS ทำให้สามารถคำนวณค่าคงที่ในแบบคู่ขนานโดยใช้คอร์ 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: 3d99811735E0E3577E7EEA90785323D1975AC6250939BA4F70E6695EBEBEDF5520
หนึ่งยังสามารถสร้างภาพโดยใช้ DockerFile ใน repo นี้
$ 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/ ไดเรกทอรี ไม่จำเป็นต้องมีการเข้าถึงรูท
$ ./install.sh
สคริปต์ extract_benchmarks.sh จะแยกเกณฑ์มาตรฐานใน ./benchmarks/ benchmarks/ ไดเรกทอรี ไม่จำเป็นต้องมีการเข้าถึงรูท sha256sum ของไฟล์ที่ดาวน์โหลดคือ D4F355097133E1B32135D9FD530B33B02EA11536FD930C6FC3EE9266F6B1B1C1
$ ./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 ด้านล่างเน้นตัวเลือกที่เกี่ยวข้องที่ใช้ในสิ่งประดิษฐ์นี้ คำอธิบายของโดเมนนามธรรมเชิงตัวเลขนำมาจากเอกสารของ IKOS
การใช้พารามิเตอร์ -nt จะ จำกัด จำนวนเธรดที่อนุญาตใน pikos คำสั่งต่อไปนี้จะเรียกใช้ pikos ด้วยเธรดสูงสุด 4 เธรด:
$ ./run_pikos.sh -nt=4 ./benchmarks/OSS/audit-2.8.4/ausearch.bc
-nt=4 เป็นค่าเริ่มต้น -nt=0 จะให้ไลบรารี TBB ตัดสินใจจำนวนเธรด ผู้เขียนเลือก 99 เป็นจำนวนเธรดสูงสุด หากต้องการเปลี่ยนสิ่งนี้ให้แก้ไข Line 991 จาก ./pikos/analyzer/src/ikos_analyzer.cpp และติดตั้งอีกครั้ง
การใช้พารามิเตอร์ -cs จะ จำกัด ความไวของบริบทใน Pikos หมายเลขนี้สอดคล้องกับความลึกที่อนุญาตของการอินไลน์แบบไดนามิกในการวิเคราะห์ระหว่างกระบวนการ คำสั่งต่อไปนี้จะเรียกใช้ pikos ด้วยความลึกสูงสุด 5 การโทร:
$ ./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 ใช้โดเมน Interval และทำการทดลองด้วย หากคุณต้องการลองใช้โดเมนอื่นให้ใช้พารามิเตอร์ -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
สิ่งเหล่านี้จะถูกส่งผ่านเมื่อกำหนดเวลาผลลัพธ์ เนื่องจากเรามีความกังวลเกี่ยวกับเวลาการคำนวณที่ไม่เปลี่ยนแปลงเท่านั้น
สำหรับ -nt สูงกว่า 99 การเปรียบเทียบระหว่าง IKOS และ PIKOS จะดำเนินการแทนการวิเคราะห์ปกติ ตัวอย่างเช่นการส่งผ่าน -nt=104 จะคำนวณและเปรียบเทียบค่าคงที่ของ IKOS และ Pikos กับเธรดสูงสุด 4 เธรด ถ้าค่าคงที่แตกต่างกัน "unmatch !!" จะถูกพิมพ์และกระบวนการจะกลับ 42 การทำงานทั้งหมดโดยใช้โดเมนนามธรรมข้างต้นควรมีค่าคงที่เดียวกันโดยการออกแบบ
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
การทำซ้ำผลลัพธ์จะถูกแบ่งออกเป็นขั้นตอน: (1) การทำซ้ำข้อมูลและ (2) การสร้างตาราง/ตัวเลขจากข้อมูล ขั้นตอนแรกอาจใช้เวลานานหากคุณเลือกที่จะทำซ้ำข้อมูลทั้งหมด ขั้นตอนนี้อาจทำได้โดยใช้ AWS ให้เสร็จในเวลาที่เหมาะสม ดู aws/README.md สำหรับข้อมูลเพิ่มเติม ขั้นตอนที่สองไม่ควรใช้เวลามากและสามารถทำได้ในท้องถิ่น มันยังคงต้องใช้การพึ่งพาที่จะติดตั้งในเครื่อง ดู install_dependencies.sh
อีกครั้งการเร่งความเร็วของ Pikos มาจากการใช้คอร์ CPU หลายตัว Pikos ต้องการเครื่องหลายคอร์เพื่อทำซ้ำผลลัพธ์ มันต้องใช้อย่างน้อย 16 คอร์ เพื่อทำซ้ำผลลัพธ์ทั้งหมด สำหรับสคริปต์ที่มีชื่อของ reproduce*.sh เราจะระบุจำนวนคอร์น้อยที่สุดที่ต้องการในตอนท้ายของชื่อ
นอกจากนี้การใช้ TCMALLOC ซึ่งเป็นหน่วยหน่วยความจำที่ติดตั้งใน install_dependencies.sh เป็นสิ่งที่ต้องทำในการทำซ้ำผลลัพธ์ โปรดตรวจสอบให้แน่ใจว่าติดตั้งอย่างถูกต้อง ควรมีห้องสมุด /usr/local/lib/libtcmalloc.so
สคริปต์เสริม measure_speedup.sh มีไว้เพื่อวัดการเร่งความเร็วของเกณฑ์มาตรฐานเดียว ต้องใช้ตัวเลือกบรรทัดคำสั่งเดียวกันกับ run_pikos.sh มันเพียงแค่ส่งออกการเร่งความเร็วซึ่งกำหนดเป็นเวลาทำงานของ IKOS / เวลาทำงานของ 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.
สคริปต์ต่อไปนี้สร้างข้อมูลในไฟล์ CSV มีคอลัมน์ต่อไปนี้:
benchmark : ชื่อของเกณฑ์มาตรฐานcategory : แหล่งที่มาของเกณฑ์มาตรฐาน SVC หรือ OSScs : ความไวของบริบทที่ใช้walltime (s) : เวลาวิเคราะห์ใน ikoswalltime (s)-k : เวลาวิเคราะห์ใน Pikos โดยที่ k คือจำนวนเธรดที่อนุญาตspeedup-k : การเร่งความเร็วของ pikosละเว้นคำเตือนเกี่ยวกับไม่มีคุณสมบัติการเปลี่ยนตัวแปรและชื่อไฟล์ปรากฏขึ้นสองครั้งเมื่อเรียกใช้สคริปต์
มันทำงาน 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
มันรัน ikos และ pikos <4> บนมาตรฐานในตารางที่ 3 มันส่งออก 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 นอกจากนี้ยังส่งออกวิธีการที่อธิบายไว้ในส่วนการประเมิน มันต้องใช้คอลัมน์ walltime (s) , walltime (s)-4 และ speedup-4 ในไฟล์ CSV มันส่งออก fig5.png
$ ./generate_fig5.py ./results-paper/all.csv
สคริปต์ generate_fig6.py สร้างฮิสโตแกรมในรูปที่ 6 มันต้องใช้คอลัมน์ walltime (s) , walltime (s)-4 และ speedup-4 ในไฟล์ CSV มันส่งออก 4 รูป subfigures, fig6-[0~3].png
$ ./generate_fig6.py ./results-paper/all.csv
สคริปต์ generate_fig9.py สร้างพล็อตบ็อกซ์และพล็อตไวโอลินในรูปที่ 7 มันต้องใช้คอลัมน์ walltime (s) , speedup-2 , speedup-4 , speedup-6 และ speedup-8 ในไฟล์ CSV มันส่งออก fig7-a.png และ fig7-b.png
$ ./generate_fig7.py ./results-paper/all.csv
สคริปต์ generate_fig8.py สร้างพล็อตค่าสัมประสิทธิ์ความสามารถในการปรับขนาดในรูปที่ 8 มันต้องใช้คอลัมน์ walltime (s) , speedup-2 , speedup-4 , speedup-6 และ speedup-8 ในไฟล์ CSV มันส่งออก fig8-a.png และ fig8-b.png
$ ./generate_fig8.py ./results-paper/all.csv
สคริปต์ generate_tab3.py สร้างรายการสำหรับตารางที่ 2 ต้องใช้ benchmark คอลัมน์ category walltime (s) walltime (s)-4 และ speedup-4 ในไฟล์ CSV มันส่งออก tab2-speedup.csv และ tab2-ikos.csv ซึ่งใช้ในการเติมตารางที่ 2
$ ./generate_tab2.py ./results-paper/all.csv
สคริปต์ generate_tab4.py เลือกมาตรฐานสำหรับตารางที่ 3 ตามค่าสัมประสิทธิ์ความสามารถในการปรับขนาด มันต้องใช้ benchmark คอลัมน์, category , cs , walltime (s) , walltime (s)-4 , speedup-2 , speedup-4 , speedup-6 และ speedup-8 ในไฟล์ CSV มันส่งออก tab3-candidates.csv หนึ่งต้องเรียกใช้ pikos <12> และ pikos <16> บนเกณฑ์มาตรฐานเหล่านี้เพิ่มเติมเพื่อให้ตารางที่ 3 เสร็จสมบูรณ์
$ ./generate_tab3.py ./results-paper/all.csv
