Cách kiểm thử đúng các cấu trúc dữ liệu đồng thời

 (matklad.github.io)
2 điểm bởi GN⁺ 2024-07-07 | 1 bình luận | Chia sẻ qua WhatsApp
  • Dùng một bộ đếm đồng thời Rust bị lỗi làm ví dụ để phơi bày những vấn đề mà các bài test tải bằng luồng thông thường bỏ sót, bằng điều khiển thứ tự thực thi có thể tái lập và tối giản được
  • Bộ bao AtomicU32 dành cho kiểm thử chèn pause(), và managed thread sẽ dừng trước/sau các phép toán nguyên tử rồi tiếp tục lại theo thứ tự do bài test chọn
  • Bài test đơn giản có thể cho 100 luồng tăng mỗi luồng 100 lần, tạo ra lỗi kiểu 9598 thay vì giá trị kỳ vọng 10000, nhưng vì phụ thuộc thời điểm nên khó tái lập, gỡ lỗi và rút gọn
  • Kiểm thử dựa trên thuộc tính với arbtest có thể tái lập cùng interleaving với cùng seed, và tối giản ca lỗi xuống còn 0: increment, 1: increment, 0: unpause, 1: unpause
  • Mở rộng cùng cấu trúc với exhaustigen cho phép liệt kê mọi interleaving đến tối đa 5 lần tăng, và sau khi sửa bằng fetch_add, 81133 interleaving đều vượt qua

Bộ đếm đồng thời không có tính nguyên tử

  • Ví dụ dùng AtomicU32 của Rust, nhưng increment() thực hiện load rồi store(value + 1), nên bản thân phép tăng không phải là nguyên tử
  • Cấu trúc Counter rất đơn giản
    • value: AtomicU32
    • increment() đọc giá trị bằng SeqCst, cộng thêm 1 vào giá trị đã đọc rồi lưu lại
    • get() đọc giá trị hiện tại bằng SeqCst
  • Hai luồng có thể đọc cùng một giá trị rồi lưu cùng một kết quả sau khi tăng, khiến một lần cập nhật bị mất

Vì sao test luồng thông thường là chưa đủ

  • Cách kiểm tra đơn giản nhất là cho nhiều luồng lặp đi lặp lại việc tăng cùng một bộ đếm rồi kiểm tra giá trị cuối cùng
    • thread_count = 100
    • increment_count = 100
    • Giá trị kỳ vọng là 10000
  • Một lần chạy ví dụ thất bại với left: 9598, right: 10000
  • Cách này phụ thuộc rất mạnh vào thời điểm lập lịch
    • Khó tái lập chính xác cùng một lỗi theo cách tất định
    • Khó gỡ lỗi
    • Nếu giảm số luồng hoặc số lần tăng, bài test có thể vô tình vượt qua nên khó tối giản ca lỗi

Xử lý interleaving bằng kiểm thử dựa trên thuộc tính

  • Kiểm thử dựa trên thuộc tính (PBT) rất hợp với kiểm thử state machine
    • Dễ tạo dữ liệu vào ngẫu nhiên
    • Có thể đặt thuộc tính rằng kết quả chạy đồng thời phải giống mô hình chạy tuần tự
    • Cũng phù hợp với yêu cầu muốn tối giản dữ liệu gây lỗi
  • Điểm khó là không dễ ép các OS thread thật sự chạy từng bước một đúng vào thời điểm mong muốn
  • Cách giải quyết là ở mỗi vòng lặp, chọn ngẫu nhiên một luồng để cho tiến thêm một bước
    • Cần có khả năng chen một luồng khác vào giữa load và store của một luồng
    • Để làm vậy, tác giả xây dựng API managed thread có thể điều khiển trực tiếp luồng

AtomicU32 cho kiểm thử và việc chèn pause

  • Trong bản build kiểm thử, thay vì std::sync::atomic::AtomicU32 sẽ dùng managed_thread::AtomicU32 tự cài đặt
    • #[cfg(test)] use managed_thread::AtomicU32
    • #[cfg(not(test))] use std::sync::atomic::AtomicU32
  • Bộ bao AtomicU32 gọi pause() trước và sau load() cũng như store()
    • load: pause() → load thật sự → pause()
    • store: pause() → store thật sự → pause()
  • Nhờ các điểm chèn này, bài test có thể dừng và cho chạy lại luồng ở quanh các phép toán nguyên tử để điều khiển thứ tự thực thi

Hình dạng của API managed thread

  • Bài test tạo hai managed thread bên trong std::thread::scope
    • Vì dùng scoped thread nên có thể mượn dữ liệu cục bộ trên stack
    • Trạng thái như tham chiếu bộ đếm được truyền vào theo kiểu spawn(scope, &counter)
  • Managed thread không chạy một hàm main cố định ngay từ đầu, mà thực thi closure do luồng điều khiển gửi qua submit()
    • t.submit(|c| c.increment())
    • Luồng sẽ chạy closure trên trạng thái T của chính nó
  • Vòng lặp test sẽ hành động ngẫu nhiên trên từng luồng chừng nào vẫn còn entropy
    • Nếu luồng đang dừng thì gọi unpause()
    • Nếu chưa dừng thì dùng submit() để chạy increment()
    • Mô hình tuần tự counter_model cũng được tăng với cùng số lần tương ứng
  • Cuối cùng, tất cả các luồng được join() rồi so sánh counter_model với counter.get() thật sự

Cách cài đặt pause và unpause

  • pause() tìm context của managed thread hiện tại bằng thread_local! để không phải thay đổi API Counter đang được kiểm thử
    • Context được chia sẻ dưới dạng Arc<SharedContext>
    • SharedContext chứa Mutex<State> và Condvar
  • Trạng thái được chia thành Ready, Running, Paused
    • Ready: đang chờ closure tiếp theo
    • Running: managed thread đang chạy
    • Paused: đang dừng tại điểm pause()
  • Khi managed thread chạm tới pause(), nó đổi trạng thái từ Running sang Paused và báo cho luồng điều khiển qua condition variable
  • unpause() đổi trạng thái từ Paused sang Running, đánh thức managed thread rồi tiếp tục đợi cho tới khi nó không còn ở trạng thái Running nữa
    • Điều này ngăn luồng điều khiển và managed thread tiếp tục chạy song song cùng lúc
    • Tại mọi thời điểm chỉ có một trong hai bên chạy, giúp giảm tính không tất định

Tái lập và tối giản lỗi

  • Chạy arbtest sẽ tìm ra lỗi trong bộ đếm bị hỏng
    • Một lỗi ví dụ có giá trị mô hình là 4, giá trị thực là 3
    • Seed gây lỗi là 0x4fd7ddff00000020
  • Chỉ định lại cùng seed sẽ cho lại đúng interleaving đó, nên rất dễ tái lập lỗi
  • Dùng .minimize() có thể rút ngắn ca lỗi thành một lần thực thi ngắn hơn
    • Seed tối giản cuối cùng là 0x9c2a13a600000001
    • Trace tối thiểu gồm bốn bước
      • 0: increment
      • 1: increment
      • 0: unpause
      • 1: unpause
  • Trong ca tối thiểu này, giá trị kỳ vọng là 2 nhưng giá trị thực là 1, bộc lộ khiếm khuyết của phép tăng dựa trên load/store

Mở rộng sang liệt kê mọi interleaving

  • Cùng cấu trúc đó có thể được đổi từ interleaving ngẫu nhiên sang cách tiếp cận dựa trên liệt kê
  • Dùng exhaustigen để viết bài test duyệt mọi interleaving cho tối đa 5 lần tăng
    • Bài test được tổ chức để tránh các vòng lặp giả và luôn hoặc unpause luồng, hoặc gửi increment
  • Cách cài đặt bị lỗi sẽ tìm ra cùng một bug
    • Một lỗi ví dụ là left: 2, right: 1
  • Nếu sửa Counter::increment() thành fetch_add(1, SeqCst) thì bài test sẽ vượt qua
    • Bộ bao AtomicU32 cũng thêm pause() trước và sau fetch_add()
    • Kết quả chạy là all 81133 interleavings are fine!
    • Thời gian chạy là real 8.65s, CPU là 8.16s, RSS là 63.91mb

Mở rộng sang mô hình bộ nhớ yếu và model checking

  • Ở bản đồ chơi hiện tại, AtomicU32 chỉ ủy quyền cho atomic thật sự
  • Một ý tưởng mở rộng là giữ tập các giá trị đã được ghi cho từng atomic, rồi khi đọc thì trả về một giá trị ngẫu nhiên phù hợp với mô hình bộ nhớ yếu
  • Việc duyệt interleaving cũng có thể được làm thông minh hơn thay vì chỉ ngẫu nhiên
    • Với cách tiếp cận model checking, có thể kiểm tra xem đã xét hết mọi interleaving khác biệt có ý nghĩa hay chưa
    • Hoặc có thể liệt kê mọi interleaving trong phạm vi nhỏ như cách trong Generate All The Things

Vì sao có thể tối giản mà không cần shrinking

  • arbtest được dùng trông giống giao diện PRNG quen thuộc, nhưng thực ra dùng PRNG hữu hạn
    • Nếu tiếp tục yêu cầu giá trị ngẫu nhiên, tới một lúc nào đó nó sẽ trả về Err(OutOfEntropy)
    • Vì vậy trong mã test mới có ? và while !rng.is_empty()
  • Khi bài test dùng hết entropy thì nó kết thúc sớm, nên nếu giảm lượng entropy khả dụng thì quá trình chạy test cũng ngắn hơn
  • Phần cài đặt bên trong về mặt khái niệm gần với &mut &[u8]
    • Mỗi lần yêu cầu số ngẫu nhiên thì lát cắt byte sẽ ngắn đi
    • Lát cắt ban đầu càng ngắn thì bài test càng đơn giản
  • Nhờ cách này, ca lỗi có thể được rút ngắn mà không cần tự cài logic shrinking riêng
  • Mã nguồn ví dụ có trong properly-concurrent

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-07-07
Các ý kiến trên Hacker News

  • Trong Rust, có người đang xây dựng một thư viện tên là Temper theo cách tiếp cận tương tự: https://github.com/reitzensteinm/temper/tree/main
    Tuy nhiên, để mô hình hóa những hệ quả kỳ lạ do toàn bộ mô hình bộ nhớ của Rust tạo ra thì cần đi xa hơn nhiều, cần một sổ cái theo dõi mỗi luồng đã nhận biết những lần ghi nào. Tùy theo thứ tự bộ nhớ nguyên tử, read/write fence, v.v., có thể có các bảo đảm kiểu như nếu đã nhận biết lần ghi X thì cũng nhất thiết phải nhận biết lần ghi Y
    Tôi nghĩ đây là một trong những bộ sưu tập nhiều test case nhất cho mô hình bộ nhớ C++/Rust, gần như đã gom hết những gì có thể tìm thấy trong sách, chuẩn C++, Stack Overflow, blog, v.v. Ví dụ, tệp dành cho Rust Atomics and Locks của Mara Bos nằm ở đây: https://github.com/reitzensteinm/temper/blob/main/memlog/tes...
    Loom được nhắc đến trong bài là một thư viện tương tự nhưng hoàn thiện hơn nhiều, cho phép kiểm thử kỹ lưỡng các thành phần cấp cao hơn như mutex hay queue: https://github.com/tokio-rs/loom Tuy nhiên, bản thân mô hình bộ nhớ không được mô hình hóa dày đặc như Temper, và tôi từng nghĩ đến việc chuyển các test case sang Loom
    Tôi lấy cảm hứng từ bài thuyết trình về kiểm thử FoundationDB của Will Wilson; hiện ông ấy đang làm tại Antithesis một giải pháp dựa trên hypervisor để thực hiện kiểu kiểm thử này trên các Docker container tùy ý: https://www.youtube.com/watch?v=4fFDFbi3toc, https://antithesis.com/
    Tôi tin chắc rằng lĩnh vực này sẽ lớn hơn rất nhiều trong 10 năm tới. WebAssembly nằm ở một điểm cân bằng tinh tế: đủ hoàn chỉnh để biên dịch phần mềm tùy ý, nhưng cũng đủ đơn giản để việc xây dựng thứ như Antithesis không trở thành một dự án 5 năm của một đội tinh nhuệ từng phát hành cơ sở dữ liệu

  • Tôi đã triển khai snapshot nguyên tử trên bộ nhớ chia sẻ bằng Rust và cũng xử lý kiểm thử tự động nghiêm túc nhất có thể: https://github.com/kaymanb/todc/tree/main/todc-mem
    Ban đầu tôi dùng Loom được nhắc trong bài, nhưng sau đó chuyển sang shuttle: https://github.com/tokio-rs/loom, https://github.com/awslabs/shuttle
    shuttle dùng cách tiếp cận ngẫu nhiên hóa thay vì vét cạn như Loom, nhưng scheduler vẫn cung cấp bảo đảm xác suất cho việc phát hiện lỗi. Qua sử dụng, shuttle nhanh hơn và mở rộng được tới các kịch bản kiểm thử phức tạp hơn
    Tương tự cách trong bài, nếu một lịch trình cụ thể làm test thất bại thì có thể lưu seed ngẫu nhiên. Khả năng tái hiện nhanh test thất bại là cực kỳ quan trọng, và cho phép viết các test case rõ ràng cho những lỗi đã từng bắt được và sửa: https://github.com/kaymanb/todc/blob/0e2874a70ec8beed8fae773...

  • Ở phía Kotlin/Java, Lincheck của JetBrains là một thư viện tốt cho loại việc này: https://github.com/JetBrains/lincheck
    Tôi đặc biệt thích tính khai báo của nó và cách nó xuất ra kết quả về khả năng tuyến tính hóa

  • Không biết trong C++ có thư viện nào giống Loom không. Tôi có vài cấu trúc dữ liệu lock-free muốn kiểm thử

  • Nếu hiểu đúng, cách tiếp cận này có hạn chế liên quan đến bảo đảm tiến triển yếu
    Phần tính toán trong bài không hẳn là quá tầm thường, nhưng trên phần cứng thực tế và scheduler thực tế, có thể nghĩ đến một vòng lặp cmpxchg mà khả năng bị dừng trên một CPU cụ thể là cực kỳ thấp. Nếu số CPU là n, trong trường hợp xấu nhất xác suất tiến triển là 1/n, còn với phương pháp kiểm thử này thì thành 1/t^p. Ở đây t là số tác vụ, có thể lớn hơn nhiều so với số CPU, và p là số lần tạm dừng trong thân vòng lặp đó, dễ dàng từ 3 trở lên. Chừng đó là đủ để khiến một thuật toán thực tế vẫn chạy được trông như bị hỏng
    Ngược lại, ngay cả khi muốn bắt tiến triển yếu như một lỗi và yêu cầu tiến triển mạnh, cách này cũng không có vẻ cung cấp công cụ hữu ích
    Dù vậy, với nhiều vấn đề đồng thời thì rõ ràng là hữu ích

    • Tôi nghĩ 1/t^p không đúng, mà chỉ nên xem là 1/t. Rốt cuộc sau thời gian t, chắc chắn một tác vụ nào đó đã tiến triển, và nếu có t tác vụ thì xác suất đó là tác vụ của mình là 1/t
      Điểm nhầm lẫn chính có vẻ là việc bị dừng không nhất thiết có nghĩa là sẽ thua ở CAS

  • Về đoạn “Nói thật thì ở đây có một chút kiến thức nền. Trừ khi làm một trò cực kỳ bị nguyền rủa bằng inline assembly, có vẻ không thể tránh việc tạo thread thật. Nếu có thứ gì đó gọi hàm pause() và ta muốn khiến nó dừng lại cho đến khi có chỉ thị sau này, việc đó phải xảy ra bên trong một thread duy trì stack riêng với stack của bài test”, tôi tự hỏi liệu có thể dùng một loại async runtime nào đó không
    Trông giống như đang instrument các phép toán nguyên tử để đạt cooperative multitasking. Có lẽ tôi cần uống thêm cà phê, nhưng làm mà không dùng thread có vẻ đơn giản hơn

    • Dùng async thì tiện, nhưng một yêu cầu khác là không muốn thay đổi API quan sát được từ bên ngoài của phần mềm đang được kiểm thử. Async có tính “lây lan”, nên với API đồng bộ thì phải dùng triển khai đồng bộ

  • Một nhược điểm của cách tiếp cận này là phải sửa chính mã được kiểm thử cho phù hợp với mã kiểm thử
    Có vẻ cũng có thể làm điều tương tự bằng cách tạo hai thread rồi dùng ptrace để chạy từng bước, “ngẫu nhiên” xen kẽ việc thực thi lệnh. Kiểu như chế độ chaos của rr
    Tuy nhiên một số lệnh có thể không phải là nguyên tử, nên nếu không dùng emulation mà vẫn làm được, có lẽ cần một cách chạy từng bước ở đơn vị “microcode nguyên tử”

    • Nghe giống hypervisor của Antithesis

  • Muốn dùng Loom có vẻ cần conditional compilation, và khi kiểm thử một thư viện thì cũng ổn, nhưng khá xâm lấn
    #[cfg(loom)]
    pub(crate) use loom::sync::atomic::AtomicUsize;
    #[cfg(not(loom))]
    pub(crate) use std::sync::atomic::AtomicUsize;
    Tôi tự hỏi có ngôn ngữ nào cho phép dùng scheduler riêng tốt hơn không

  • Nếu muốn thật sự triệt để, có vẻ có thể chạy test bằng ptrace rồi cho các thread chạy từng bước để tạo các interleaving khác nhau ở cấp lệnh. Tôi tò mò không biết đã có ai thực sự thấy cách như vậy chưa
    Khi không thể instrument mã như ở đây, có lựa chọn thay thế nào cho kiểm thử black-box không?

    • Tôi từng dùng cách đó để kiểm thử async signal handler, nhưng phía đó có số tổ hợp thuận lợi hơn nhiều. Nếu thread chính thực thi n lệnh, chỉ cần n lần chạy, trong đó chạy từ 0 đến n lệnh trước khi chèn tín hiệu, rồi sau đó signal handler chạy đến hết và thread chính cũng chạy đến hết. Tổng thời gian là O(n^2)
      Nhưng nếu có t thread, mỗi thread thực thi n lệnh, và có thể dừng nhau ở mọi ranh giới, thì với giá trị n thực tế sẽ rất khó tiếp cận. Có lẽ phải giảm bớt bằng cách chỉ chọn và mô phỏng các thao tác có hành vi thú vị

  • Trông khá hay nên tôi sẽ thử dùng. Tuy nhiên nó sẽ không bắt được mọi loại lỗi. Mỗi lần gọi pause() lại tạo ra đồng bộ hóa giữa các thread, liệu có che khuất một số vấn đề data race không? Có thể trong Rust thì đây không phải là vấn đề