Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

Parallelize symbolic execution of tests

Aperta
  • Qualcosa non va?
#2,009 2 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

  • #2065 di @nwatson22 — chiusa senza merge

Valutazione

Difficoltà
5/5
Tempo stimato
Più di una settimana
Idoneità per principianti
20/100
Tipo di issue
Funzionalità
Chiarezza
Abbastanza chiara
Stato di attività
Ferma
Stack tecnologico
python
Ambito
testing-qa

Direzione di ricerca

Inizia leggendo pyk.kore.pool.KoreServerPool, APRProver, KCFGExplore, APRPRover e kevm_prove, concentrandoti su come gestiscono lo stato della dimostrazione, le chiamate RPC e le scritture su disco. Confronta il design esistente di ThreadPoolExecutor con il ciclo di attività proposto a livello di processo; il lavoro è completato quando le dimostrazioni di esecuzione simbolica possono essere pianificate in parallelo, i risultati possono essere persistiti in modo sicuro e le risorse vengono arrestate correttamente.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

engagement enhancement

This allows better utilization in case the number of tests remaining is smaller than the number of workers. (In particular if there's a single test.)

Design constraints

  1. Although kore-rpc is able to handle requests in parallel, each proof will probably need its own KoreServer instance. This is because pyk.proof.reachability.APRProver calls add_dependencies_module in its initializer. This limitation need further investigation though, maybe there's a way to prevent interference between proofs on the same server.
  2. Due to the Global Interpreter Lock in CPython, we either need to ensure that Python code has minimal overhead, or use process-level parallelism instead of threads. This means that we need to ensure pickleability of objects that are sent between processes.

Draft

This is based on pyk.kore.pool.KoreServerPool (design constraint 1) that currently uses concurrent.futures.ThreadPoolExecutor internally. As mentioned, this will probably have be replaced by ProcessPoolExecutor (design constraint 2).

Main thread initializes the pool with some initial tasks, and then processes results as they become available in a loop. Processing a result involves:

  • Persisting proof results to disk: as this is handled by a single thread, the data model does not have to be thread-safe.
  • Submitting new tasks to the pool.
# pending is a collection of futures
while pending:
    # pick a done future to process
    current_future = next((future for future in pending if future.done()), None)

    # if there is none, sleep for a while then retry
    if current_future is None:
        time.sleep(0.1)
        continue

    # get the result - if an exception occurred in in the thread, it will be raised
    result = current_future.result()
    # update the corresponding proof on disk
    write_data_to_disk(result)

    # schedule new tasks
    next_tasks = get_next_tasks(result)
    for fn, args in next_tasks:
        next_future = pool.submit(fn, *args)
        pending.append(next_future)

    # this task is completed
    pending.remove(current_future)

Ideally, granularity of a task should be a single proof step (i.e. an RPC call and as much of the necessary pre- and post-processing as makes sense). This is the most challenging part of the issue: it requires countrparts of KCFGExplore, APRPRover, kevm_prove, etc. that 1) enable fine-grained control of the proof process 2) do not write to disk. This suggests a prover interface like:

class Prover:
    def advance_proof(self, proof_state: ProofState) -> ProofStep:
        # Does a single RPC call based on proof state and prover configuration. Does not write to disk.
        ...

Further considerations

Task scheduling

It would be good to have control on task scheduling. For example, in the simplest case, tests are assigned a unique priority, and each task inherits the priority of the test it belongs to. This means that a test with a lower priority can only run if tests with a higher priority don't have enough tasks scheduled to utilize all workers. In a good design, such scheduling strategies can be provided by the caller (e.g. in form of a callable that takes a task and returns its priority).

Unfortunately Executor implementations take tasks from Queue, so tasks are processed in FIFO order. But maybe there's a way to wrap the executor and use an additional PriorityQueue:

  • Keep track of executor utilization (use Future.add_done_callback).
  • Keep submitted tasks in a PrioirityQueue. Only submit to the executor if it has an empty queue.
Graceful shutdown

On an exception or user request, the prover should shut down gracefully. In particular:

  • Properly close all resources (the pool, servers, clients, etc).
  • Write data from all done tasks to disk.
Lingua principale
KCL
Stelle
594
Fork
157
Merge medio
4g 3h
PR unite (30g)
1

Preparare l'ambiente

Questo progetto non fornisce container di sviluppo, Dockerfile né guida per i contributori, quindi l'ambiente è a tuo carico: parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/evm-semantics

Tutte le issue di runtimeverification/evm-semantics

Issue simili

Altre issue su Testing & QA

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.