Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

Parallelize symbolic execution of tests

Đang mở
  • Có gì không ổn?
#2,009 2 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

  • #2065 của @nwatson22 — đã đóng, không merge

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
20/100
Loại issue
Tính năng
Độ rõ ràng
Khá rõ ràng
Mức độ hoạt động
Đình trệ
Công nghệ
python
Lĩnh vực
testing-qa

Hướng nghiên cứu

Bắt đầu bằng cách đọc pyk.kore.pool.KoreServerPool, APRProver, KCFGExplore, APRPRover và kevm_prove, tập trung vào cách chúng quản lý trạng thái chứng minh, các lệnh gọi RPC và việc ghi vào đĩa. So sánh thiết kế ThreadPoolExecutor hiện có với vòng lặp tác vụ ở cấp tiến trình được đề xuất; công việc được xem là hoàn tất khi các phép chứng minh thực thi tượng trưng có thể được lập lịch song song, các kết quả được lưu bền vững một cách an toàn và các tài nguyên được tắt sạch sẽ.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

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.
Ngôn ngữ chính
KCL
Star
592
Fork
156
Merge trung bình
2 giờ 19 phút
Pull request đã merge (30 ngày)
1

Chuẩn bị môi trường

Chúng tôi chưa kiểm tra các tệp thiết lập môi trường của dự án này. Hãy bắt đầu từ README và xem hướng dẫn đóng góp lần đầu của chúng tôi để biết các bước chung.

Bắt đầu từ đâu

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. 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.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của runtimeverification/evm-semantics

Tất cả issue của runtimeverification/evm-semantics

Issue tương tự

Thêm issue về Testing & QA

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.