pikos_popl2020
1.0.0
هذا هو قطعة أثرية البرمجيات التي تصاحب الورقة "حساب Fixpoint الحتمي" من تأليف سونغ كوك كيم ، أرنود ج. فينيت ، وأديتيا ف. ثاكور.
"حساب FixPoint الحتمي" 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},
}
وهو يتكون بشكل أساسي من مترجمنا التجريدي المتوازي ، 4330 معايير المستخدمة في التجارب ، والبرامج النصية لإعادة إنتاج النتائج في الورقة.
يعتمد Pikos على مترجم تجريدي متسلسل ، IKOS. تم تلخيص الملفات التي تم تغييرها في IKOS لتنفيذ pikos في CHANGES.md . بالنظر إلى برنامج كمدخلات ، يقوم كل من IKOS و PIKOS بحساب الثنائيات على كل نقطة برنامج وتشغيل الشيكات عليها. في الواقع ، يتم تنفيذ PIKOS كخيار تحليل لـ IKOS ، مما يسمح له بحساب الثبات بالتوازي باستخدام نوى وحدة المعالجة المركزية المتعددة. لذلك ، يتطلب 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: 3D99811735E0E357E7EEA90785323D1975AC6250939BA4F70E6695EBEDF5520
يمكن للمرء أيضًا بناء الصورة باستخدام 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/ الدليل. لا يتطلب الوصول إلى الجذر.
$ ./install.sh
سيقوم برنامج Script extract_benchmarks.sh بإجراء استخراج المعايير في ./benchmarks/ الدليل. لا يتطلب الوصول إلى الجذر. SHA256SUM للملف الذي تم تنزيله هو D4F35509713E1B32135D9FD530B33B02EA11536FD930C6FC3EE926F6B1C1.
$ ./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 كحد أقصى لعدد الخيوط. لتغيير هذا ، تعديل السطر 991 من ./pikos/analyzer/src/ikos_analyzer.cpp وتثبيته مرة أخرى.
استخدام المعلمة -cs يقيد حساسية السياق في PIKOS. هذا الرقم يتوافق مع العمق المسموح به للدخول الديناميكي في التحليل interprocedural. سيقوم الأمر التالي بتشغيل 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 المجال الفاصل ، وأجريت تجارب معها. إذا كنت ترغب في تجربة المجالات الأخرى ، فاستخدم المعلمة -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 مؤشرات ترابط. إذا اختلفت الثبات ، "Unfating !!" سيتم طباعتها وستُرجع العملية 42. جميع عمليات التشغيل باستخدام المجالات التجريدية أعلاه يجب أن يكون لها نفس الثوابات حسب التصميم.
$ ./run_pikos.sh -nt=104 ./benchmarks/test.c
تنقسم إعادة إنتاج النتائج إلى خطوات: (1) إعادة إنتاج البيانات و (2) توليد الجداول/الأرقام من البيانات. قد تستغرق الخطوة الأولى الكثير من الوقت إذا اخترت إعادة إنتاج جميع البيانات. قد يتم القيام بهذه الخطوة باستخدام AWS لإنهاء في الوقت المناسب. انظر aws/README.md لمزيد من المعلومات. الخطوة الثانية يجب ألا تستغرق الكثير من الوقت ويمكن القيام بها محليًا. لا يزال يتطلب تثبيت التبعيات محليًا. انظر install_dependencies.sh .
مرة أخرى ، يأتي تسريع Pikos من استخدام نوى وحدة المعالجة المركزية المتعددة. يتطلب 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 أو OSS.cs : حساسية السياق المستخدمة.walltime (s) : وقت التحليل في IKOSwalltime (s)-k : وقت التحليل في Pikos ، حيث K هو عدد المواضيع المسموح بها.speedup-k : Speedup of Pikosتجاهل التحذيرات حول عدم وجود PropertyFile ، والاستبدال المتغير ، واسم الملف يظهر مرتين عند تشغيل البرامج النصية.
يدير IKOS و Pikos <2> و Pikos <4> و Pikos <6> و Pikos <8> على جميع المعايير. إنه يخرج all.csv . 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 تكوينات فرعية ، 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
