Understanding the `bmc-depth` bottleneck
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 4/5
- Thời gian dự kiến
- 3-5 ngày
- Mức phù hợp với người mới
- 35/100
- Loại issue
- Lỗi
- Độ rõ ràng
- Khá rõ ràng
- Mức độ hoạt động
- Đình trệ
- Công nghệ
- python
- Lĩnh vực
- performance
Hướng nghiên cứu
Start in pyk/src/pyk/proof/reachability.py at the linked shortest_path and same_loop locations, and reproduce bmc-depth on a proof with 1000+ nodes and parallel threads. Profile the Python and kore-rpc-booster processes while comparing runs with and without bmc-depth. Done means identifying which computation causes the slowdown and documenting measured evidence for the bottleneck.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
In real-world proofs that use bmc-depth and are sufficiently large (1000+ nodes), there is a massive slowdown introduced by the associated computations, to the point that a Kontrol proof that passes without bmc-depth in ~1h45m does not finish after more than a day with bmc-depth activated. The manifestation of this, at least on my machine and with 6 parallel threads, is a python process that is constantly at 100% and a kore-rpc-booster process that is way below its maximal throughput. The reasons for this could be:
- the computation of
shortest_pathwhen understanding the next steps, which needs to traverse the KCFG and does not appear to rely on dynamic programming and may be forcing thread synchronisation: https://github.com/runtimeverification/k/blob/76c534f16df17febd4560e9b492cfa024d82e9b0/pyk/src/pyk/proof/reachability.py#L182 - the computation of
same_loop, which extracts and examines cells in aCTerm, which could be costly: https://github.com/runtimeverification/k/blob/76c534f16df17febd4560e9b492cfa024d82e9b0/pyk/src/pyk/proof/reachability.py#L793
- Ngôn ngữ chính
- Python
- Star
- 591
- Fork
- 163
- Chỉ số merge pull request
- Không có pull request nào được merge trong 30 ngày
Chuẩn bị môi trường
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của runtimeverification/k
-
Introduce composable symbolic execution interface in pyxCó thể làm lại được @Stevengre đã nhận 98 ngày trước và không có pull request nào đang mở. Đang mở
runtimeverification/k#4939 · 1 người được giao ·
-
Concolic ExplorerĐang mở
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 32/100
runtimeverification/k#4937 ·
-
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 30/100
runtimeverification/k#4936 ·
-
Accelerating all-path reachability proofs with one-path reachability proofsCó thể làm lại được @Stevengre đã nhận 104 ngày trước và không có pull request nào đang mở. Đang mởtype:epic
runtimeverification/k#4934 · 4 bình luận · 1 người được giao ·
-
Support progressive depth halving as a generic policy in `Prover.advance_proof`Có thể làm lại được @Stevengre đã nhận 124 ngày trước và không có pull request nào đang mở. Đang mở
runtimeverification/k#4924 · 1 người được giao ·
Tất cả issue của runtimeverification/k
Issue tương tự
-
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 72/100
letsencrypt/cp-cps#353 ·
-
Marble Madness II is missingĐang mở
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 84/100
PedestrianDynamics/pyFDS-Evac#394 ·
Maintainer thường phản hồi trong vòng 1 ngày
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100
DOI-USGS/pywatershed#421 ·
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 78/100
python-pillow/Pillow#10087 · 1 bình luận ·
Maintainer thường phản hồi trong vòng 1 ngày