Understanding the `bmc-depth` bottleneck
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 4/5
- Tiempo estimado
- 3-5 días
- Aptitud para principiantes
- 35/100
- Tipo de issue
- Error
- Claridad
- Bastante claro
- Estado de actividad
- Estancado
- Stack tecnológico
- python
- Área
- performance
Línea de trabajo
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.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
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
- Lenguaje dominante
- Python
- Estrellas
- 596
- Forks
- 164
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Sin plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/k
-
bug
Dificultad 3/5 Medio día Aptitud para principiantes 75/100
runtimeverification/k#4941 ·
-
Introduce composable symbolic execution interface in pyxQuizá libre de nuevo @Stevengre la tomó hace 120 días y no hay ningún pull request abierto. Abierto
runtimeverification/k#4939 · 1 asignado ·
-
Concolic ExplorerAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 32/100
runtimeverification/k#4937 ·
-
Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100
runtimeverification/k#4936 ·
-
Accelerating all-path reachability proofs with one-path reachability proofsQuizá libre de nuevo @Stevengre la tomó hace 126 días y no hay ningún pull request abierto. Abiertotype:epic
runtimeverification/k#4934 · 4 comentarios · 1 asignado ·
Todos los issues de runtimeverification/k
Issues similares
-
[Bug]: IndexHandler.post crashes with HTTP 500 on malformed payloads, missing credentials, or when login is disabledPosiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 78/100
Los mantenedores suelen responder en 6 días
-
Bump zizmor to 1.31.1+Abiertogithub_actions
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100
collective/icalendar#2003 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 79/100
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
openzim/python-scraperlib#360 ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
volcengine/OpenViking#6445 ·
Los mantenedores suelen responder en 1 día