Tình trạng ảm đạm của các thư viện kiểm thử dựa trên thuộc tính

 (stevana.github.io)
1 điểm bởi GN⁺ 2024-07-06 | 1 bình luận | Chia sẻ qua WhatsApp
  • Property-based testing đã lan rộng sang nhiều ngôn ngữ sau QuickCheck, nhưng tính đến tháng 7/2024, nhiều thư viện vẫn chưa cung cấp đầy đủ kiểm thử dựa trên trạng thái và kiểm thử song song, vốn đã được tổng kết từ năm 2009
  • Khoảng cách cốt lõi nằm ở khả năng dùng mô hình máy trạng thái để kiểm chứng các thay đổi trạng thái tuần tự, rồi tái sử dụng cùng mô hình đó cho kiểm tra khả năng tuyến tính hóa (linearisability) nhằm tìm race condition trong thực thi song song
  • Nhiều thư viện được khảo sát không có kiểm thử dựa trên trạng thái hoặc chỉ ở mức thử nghiệm; kiểm thử song song còn hiếm hơn, với các issue liên quan vẫn tồn tại nhiều năm trong FsCheck, Gopter, RapidCheck, SwiftCheck, jsverify, v.v.
  • Một bản triển khai Haskell khoảng 400 dòng tái hiện property-based testing dựa trên trạng thái và song song, đồng thời dùng triển khai tham chiếu dựa trên fake quen thuộc với lập trình viên làm mô hình thay cho đặc tả máy trạng thái truyền thống
  • Fake đã được kiểm thử hợp đồng có thể được tái sử dụng không chỉ để kiểm chứng một component đơn lẻ, mà còn cho kiểm thử tích hợp nhanh và tất định bằng cách tiêm vào thay cho dependency thật

Khoảng cách tính năng xuất hiện sau QuickCheck

  • Property-based testing lan rộng sang các cộng đồng ngôn ngữ lập trình khác nhau dưới khẩu hiệu “đừng viết test, hãy sinh test”
  • Trang Wikipedia của QuickCheck, thư viện Haskell gốc, liệt kê 57 bản triển khai lại cho các ngôn ngữ khác
  • Bài báo QuickCheck đầu tiên, QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs, được trình bày tại ICFP 2000; toàn bộ mã nguồn của bản triển khai đầu tiên chỉ khoảng 300 dòng trong phụ lục bài báo
  • QuickCheck ban đầu chỉ có thể kiểm thử hàm thuần, và đến năm 2002, Testing monadic code with QuickCheck đặt nền tảng để xử lý code có hiệu ứng như mutable state, file I/O và networking

Sự xuất hiện của kiểm thử dựa trên trạng thái và song song

  • Quviq AB được John Hughes và Thomas Arts thành lập năm 2006, và việc kiểm thử các dự án Erlang của Ericsson là một trong những use case ban đầu
  • Erlang không phải là ngôn ngữ hàm thuần và concurrency rất phổ biến, nên chỉ dùng QuickCheck monadic hiện có là chưa đủ tiện lợi
  • Erlang QuickCheck closed source của Quviq sau đó bao gồm hai tính năng vắng mặt trong nhiều bản triển khai open source
    • Property-based testing tuần tự dựa trên trạng thái dùng mô hình máy trạng thái
    • Kiểm thử song song tái sử dụng cùng mô hình máy trạng thái tuần tự để phát hiện race condition
  • Kiểm thử dựa trên trạng thái xuất hiện với hình thức hiện nay trong QuickCheck testing for fun and profit (2007)
  • Kiểm thử song song được trình bày chi tiết trong Finding Race Conditions in Erlang with QuickCheck and PULSE (ICFP 2009), lấy Linearizability: a correctness condition for concurrent objects (1990) của Herlihy và Wing làm kỹ thuật cốt lõi
  • Mã thư viện của Quviq QuickCheck không được chia sẻ trong các bài báo; những gì được công khai là API và các ví dụ test sử dụng API đó

Kết quả khảo sát thư viện năm 2024

  • State-of-the-art hiện nay là stateful testing dựa trên mô hình máy trạng thái và parallel testing kết hợp linearisability với cùng mô hình tuần tự đó
  • Khảo sát được tổng hợp dựa trên việc đọc tài liệu, issue tracker và một phần mã nguồn tính đến tháng 7/2024
  • Nhiều thư viện không cung cấp kiểm thử dựa trên trạng thái hoặc chỉ cung cấp ở mức hạn chế
    • QuickCheck(Haskell) có issue bổ sung kiểm thử dựa trên trạng thái mở từ năm 2016
    • SwiftCheck cũng có issue bổ sung kiểm thử dựa trên trạng thái mở từ năm 2016
    • jsverify vẫn còn issue bổ sung kiểm thử dựa trên trạng thái từ năm 2015
    • proptest(Rust) cần tham khảo gói riêng proptest-state-machine
  • Hỗ trợ kiểm thử song song còn hiếm hơn
    • Gopter ghi trong README rằng “No parallel commands … yet?” và có issue từ năm 2017
    • FsCheck có issue bổ sung parallel support mở từ năm 2016
    • RapidCheck có issue bổ sung parallel support mở từ năm 2015
    • propcheck có issue bổ sung parallel testing từ năm 2020
  • Các ví dụ open source hỗ trợ cả hai tính năng gồm PropEr, Hedgehog, qcheck-stm, quickcheck-state-machine, stateful-check, v.v.
  • Ngay cả khi có tính năng song song, vẫn có trường hợp bị hạn chế
    • Chú thích trong mã nguồn của QuickTheories ghi rằng kiểm thử song song của thư viện này khiến số end state khả dĩ tăng nhanh theo số lệnh, nên thường phải giới hạn command list ở mức 10 lệnh trở xuống
    • Các ví dụ LevelDB và Redis của ScalaCheck được trình bày là ví dụ tuần tự với threadCount = 1
    • Hỗ trợ race condition của fast-check có vẻ không tái sử dụng mô hình máy trạng thái tuần tự hoặc dùng linearisability như kiểm thử song song của Quviq QuickCheck
  • Không thấy ví dụ rõ ràng nào về việc tính năng song song được thêm vào sau; nếu không được phản ánh trong thiết kế API ngay từ đầu, có thể cần tái thiết kế đáng kể

Vì sao tính năng lan rộng chậm

  • John Hughes đưa ra ba lý do
    • Kiểm thử dựa trên trạng thái và song song không hữu ích bằng kiểm thử hàm thuần
    • Viết mô hình máy trạng thái đòi hỏi cách tư duy khác với test thông thường và cần đào tạo
    • Chỉ open source thì khó được ngành công nghiệp chấp nhận, còn sản phẩm closed source cùng đào tạo và tư vấn đã hỗ trợ việc áp dụng
  • Chỉ cần property-based testing cho các phần hàm thuần cũng đem lại nhiều hiệu quả, nhưng trong hệ thống công nghiệp có nhiều database, stateful protocol và concurrent data structure, nên kiểm thử dựa trên trạng thái và song song cũng gần như quan trọng tương đương
  • Đặc tả dựa trên trạng thái không phải lúc nào cũng khó hơn đặc tả bằng hàm thuần
    • Mô hình key-value store có thể đi khá xa chỉ với danh sách key-value pair
    • Trong trường hợp LevelDB, một mô hình đơn giản đã tìm ra counterexample rút gọn 17 bước chỉ trong vài phút; sau khi Google sửa, nó lại tìm ra counterexample 31 bước trong vài phút
    • Vấn đề thứ hai là lỗi trong background compaction process; compaction quan trọng cho việc cải thiện hiệu năng đọc và thu hồi disk space, nhưng không được đưa rõ vào mô hình
  • Closed source có thể đã giúp việc áp dụng trong công nghiệp, nhưng được đánh giá là không giúp ích cho việc áp dụng open source
  • Để tái hiện kết quả của các bài báo mà không có giấy phép Quviq QuickCheck, cần rất nhiều reverse engineering, nên gần như bất khả thi

Đề xuất: triển khai nhỏ, công khai và đặc tả dễ viết

  • Có hai hướng cải thiện
    • Cung cấp một bản triển khai open source ngắn cho property-based testing dựa trên trạng thái và song song, giống bản triển khai QuickCheck gốc khoảng 300 dòng
    • Giảm gánh nặng viết đặc tả bằng cách tái sử dụng các khái niệm mock và test double mà lập trình viên đã quen thuộc, thay vì máy trạng thái
  • Để kiểm chứng giả thuyết này, hai điều được trình bày
    • Triển khai property-based testing dựa trên trạng thái và song song bằng khoảng 400 dòng code
    • Dùng in-memory reference implementation, tức fake, làm mô hình thay cho state machine

Tóm tắt kiểm thử dựa trên thuộc tính thuần túy

  • Trong kiểm thử hàm thuần túy, ta sinh đầu vào và kiểm tra xem đầu ra của hàm có thỏa mãn một quan hệ nào đó với đầu vào hay không
  • Ví dụ, reverse có thể được kiểm thử bằng thuộc tính reverse (reverse xs) == xs với danh sách bất kỳ xs
  • QuickCheck mặc định sinh 100 ca kiểm thử; nếu thất bại, nó shrink đầu vào để đưa ra counterexample nhỏ nhất
  • Một thuộc tính sai như reverse xs == xs sẽ được thu nhỏ thành phản ví dụ tối thiểu như [0,1]
  • Các mẫu thuộc tính thường gặp gồm inverse, idempotency, associativity, các axiom của abstract data type, metamorphic property, v.v.
    • inverse: deserialise (serialise i) == i
    • idempotency: sort (sort xs) == sort xs
    • associativity: (i + j) + k == i + (j + k)

Kiểm thử dựa trên thuộc tính theo trạng thái

  • Các thành phần có trạng thái không phải lúc nào cũng tạo cùng một đầu ra từ cùng một đầu vào
    • Kết quả incr lần đầu và kết quả incr lần thứ hai của counter phụ thuộc vào trạng thái trước đó
    • database và file system cũng có lịch sử đầu vào trước đó ảnh hưởng đến đầu ra tiếp theo
  • Nếu kiểm thử hàm thuần túy xử lý một đầu vào đơn lẻ, thì kiểm thử theo trạng thái sinh chuỗi đầu vào để kiểm tra hệ thống thay đổi theo thời gian như thế nào
  • Model được biểu diễn dưới dạng fake có dạng m -> i -> (m, o)
    • Từ trạng thái model trước đó m và đầu vào i, tính model tiếp theo và đầu ra o
    • So sánh đầu ra của hệ thống thực với đầu ra của fake ở từng bước
    • Nếu không khớp, shrink chuỗi đầu vào để tìm counterexample nhỏ

  • Ví dụ Counter

    • Lấy một counter Haskell dùng biến mutable toàn cục làm đối tượng kiểm thử
    • incr tăng counter, còn get đọc giá trị hiện tại
    • Model chỉ cần một Counter Int; instance StateModel định nghĩa trạng thái ban đầu Counter 0, Incr, Get, Incr_ (), Get_ Int, runFake, runReal, và command generator
    • Nếu đưa vào lỗi như incr42Bug, trong đó counter không tăng khi giá trị là 42, QuickCheck tìm thấy thất bại sau 66 ca kiểm thử và shrink 29 lần để đưa ra phản ví dụ tối thiểu: increment 43 lần rồi Get
    • Nếu không reset counter toàn cục thực giữa các ca kiểm thử, model luôn bắt đầu từ 0 nhưng counter thực giữ trạng thái từ ca kiểm thử trước, dẫn đến mismatch

  • Giao diện thư viện theo trạng thái

    • Giao diện StateModel xem hệ thống cần kiểm thử như một black box, coi command là đầu vào và response là đầu ra
    • Các thành phần cốt lõi gồm Command state, Response state, initialState, runFake, runReal, generateCommand
    • Các thành phần tùy chọn như sau
      • Reference: dùng khi command sau cần tham chiếu đến tài nguyên do response trước tạo ra, chẳng hạn file handle
      • PreconditionFailure: biểu diễn lỗi precondition kiểu không cho phép read từ handle không phải file đang mở
      • CommandMonad: mặc định là IO, nhưng có thể dùng monad khác
      • monitoring, commandName: dùng cho coverage và thống kê
    • Khi sinh command, không thể tạo các giá trị như file handle thực, nên sinh symbolic reference dạng Var Int và thay thế bằng reference thực trong lúc chạy
    • Sau khi shrink, loại bỏ các command phá vỡ precondition hoặc dùng symbolic reference ngoài scope

  • Ví dụ circular buffer

    • Kiểm thử một circular queue viết bằng C thông qua Haskell FFI, còn model được viết dưới dạng queue đơn giản dựa trên danh sách
    • Phần triển khai C không kiểm tra lỗi, nên nếu get từ empty queue thì có thể trả về bộ nhớ chưa được khởi tạo
    • Triển khai thực hiệu quả nhờ circular index nhưng không hiển nhiên là correct, còn fake kém hiệu quả hơn nhưng chỉ dùng để kiểm thử nên không thành vấn đề
    • Vì new trả về queue reference, model quản lý nhiều queue bằng Map (Var Queue) FQueue
    • Ban đầu thiếu precondition cho việc put vào full queue, nên khi đưa 0, 1 vào queue kích thước 1 rồi get, model kỳ vọng 0 theo FIFO nhưng mã C trả về 1
    • Đây không phải lỗi triển khai mà là thiếu precondition trong model, nên được sửa bằng cách thêm precondition QueueIsFull
    • Việc command Size bị thiếu trong generator được phát hiện qua đầu ra coverage; sau khi thêm vào thì phát hiện lỗi tính kích thước queue
    • Với queue kích thước 1 chứa một item, Size có giá trị kỳ vọng là 1 nhưng giá trị thực là 0; bản sửa được đề xuất là đặt kích thước buffer nội bộ thành n + 1 trong new
    • Sau đó, abs(q->inp - q->outp) % q->size vượt qua với kích thước 1 nhưng lại thất bại với kích thước 2; bản sửa cuối cùng là (q->inp - q->outp + q->size) % q->size

  • Câu đố bình nước trong Die Hard 3

    • Giải câu đố tạo đúng 4L bằng bình nước 3L và 5L bằng kiểm thử theo trạng thái
    • Ngay cả khi không có triển khai thực và chỉ chạy model cùng fake, có thể làm bài kiểm thử thất bại khi đạt đến một trạng thái cụ thể để thu được action sequence đã được shrink
    • Sau 199 ca kiểm thử và 11 lần shrink, sequence được đưa ra có luồng như sau
      • Đổ đầy bình 5L
      • Rót từ bình 5L sang bình 3L
      • Đổ cạn bình 3L
      • Rót lại từ bình 5L sang bình 3L
      • Đổ đầy bình 5L
      • Rót từ bình 5L sang bình 3L
    • Trace hiển thị các trạng thái trung gian, cho phép xác nhận quá trình big jug đạt 4L

Kiểm thử dựa trên thuộc tính song song

  • Lỗi trong concurrent code rất khó tái hiện và xác minh việc sửa lỗi vì thread interleaving thay đổi qua mỗi lần chạy
  • Mục tiêu là cho phép người dùng thực hiện kiểm thử song song giống như kiểm thử dựa trên trạng thái tuần tự, mà không phải viết thêm nhiều mã kiểm thử
  • Trong ví dụ counter, nếu incr thực hiện readIORef rồi writeIORef theo cách không nguyên tử, hai thread có thể ghi đè increment của nhau và gây ra race condition
  • Kiểm thử song song thu thập thời điểm invocation và response của các command trong lúc chạy để tạo concurrent history, rồi kiểm tra history đó có thể được giải thích bằng một interleaving tuần tự nào hay không
  • Nếu có ít nhất một interleaving khớp với mô hình tuần tự, history được xem là linearise và được đánh giá là correct
  • Nếu không có interleaving tuần tự nào giải thích được response thực tế, kết quả được xử lý là non-linearisable

  • Sinh và shrink command song song

    • Chương trình song song được biểu diễn bằng ParallelCommands và nhiều Fork, trong đó các command bên trong mỗi Fork được chạy song song
    • Phần triển khai ví dụ xử lý việc thực thi một, hai và ba thread
    • Trong thực thi song song, trạng thái mô hình khả dĩ có thể thay đổi tùy theo interleaving, chẳng hạn Fork [Write "a" "foo", Write "a" "bar"]
    • Mô hình song song thực hiện sinh command và shrink dựa trên tập trạng thái, chứ không phải một state đơn lẻ
    • parallelSafe kiểm tra xem precondition có được duy trì trong mọi permutation của các command bên trong Fork hay không
    • Ví dụ, nếu Write "a" và Delete "a" nằm trong cùng một fork, một command có thể phá vỡ precondition của command kia
    • Trong quá trình shrink, chỉ giữ lại các command vẫn duy trì precondition và phạm vi symbolic reference

  • Thực thi song song và kiểm tra linearisability

    • Thực thi song song ghi lại event Invoke và Ok của mỗi command vào history
    • Nếu response chứa reference mới, môi trường được mở rộng bằng atomic counter để tránh xung đột số reference giữa các thread
    • Tất cả interleaving khả dĩ từ history được liệt kê dưới dạng cây Rose
    • linearisable kiểm tra xem có path nào trong cây này làm response khớp với mô hình tuần tự runFake hay không
    • Vì kiểm thử song song cuối cùng vẫn tái sử dụng mô hình tuần tự, người dùng chỉ cần viết mô hình tuần tự rồi thêm rất ít mã để có kiểm thử song song

  • Ví dụ Parallel counter

    • Mã được thêm để kích hoạt kiểm thử song song cho counter chỉ gồm instance ParallelModel Counter và property
    • Khi dùng incrRaceCondition không nguyên tử, kiểm thử tìm ra race condition
    • Ngay cả khi test case nhỏ hơn vẫn có race, nếu lỗi không tái hiện do một interleaving khác, QuickCheck có thể xem test case nhỏ hơn là pass và dừng shrink
    • Giải pháp đúng là deterministic thread scheduler, và bài báo về kiểm thử song song sử dụng cách này
    • Phần triển khai ví dụ dùng một workaround đơn giản hơn: chèn sleep ngắn quanh thao tác read/write trên shared memory để tăng khả năng xảy ra cùng một interleaving
    • Sleep không cần để tìm race, mà để làm cho counterexample của race đã tìm được trở nên nhỏ hơn
    • Sau khi thêm sleep, phản ví dụ tối thiểu được rút gọn thành ParallelCommands [Fork [Incr,Incr],Fork [Get]]

  • Ví dụ Process registry

    • Hệ thống ví dụ tương tự Erlang process registry: spawn thread, rồi register·lookup·unregister·kill ThreadId theo tên
    • Mô hình tuần tự theo dõi các thread id đã được tạo, các cặp name-thread đã đăng ký, và các thread id đã bị kill
    • Register và Unregister có thể thất bại, nên response dùng Either ErrorCall ()
    • Thông tin error location của triển khai thực được loại bỏ bằng abstractError để khớp với fake
    • monitoring hiển thị coverage cho RegisterFailed, RegisterSucceeded, UnregisterFailed, UnregisterSucceeded
    • Nếu cố ý đưa vào lỗi khiến register ghi đè registry hiện có, sẽ xuất hiện một phản ví dụ tuần tự trong đó không thể unregister "e" đã đăng ký trước đó
    • Trong kiểm thử song song, phản ví dụ dài hơn xuất hiện; khi dùng SleepyIORef, nó shrink về dạng Fork [Register "b" (Var 0), Register "c" (Var 0)]
    • Vấn đề là race trong khoảng giữa lúc kiểm tra bằng readRegistry và lúc gọi atomicModifyIORef, nơi một thread khác có thể chen vào
    • Sau khi áp dụng global lock cho register, unregister, kill, kiểm thử song song pass

Mô hình dựa trên fake và kiểm thử tích hợp

  • Thay vì state machine specification truyền thống với post-condition, dùng fake in-memory làm reference implementation
  • Bài viết năm 2019 của Edsko de Vries năm 2019 được giới thiệu là bài đầu tiên đề xuất cách triển khai fake trên đặc tả state machine dựa trên post-condition
  • fake tương tự mock, nên được trình bày như một cách tiếp cận dễ hơn cho các lập trình viên chưa quen với formal specification
  • fake cũng có lợi thế là có thể dùng thay cho component phụ thuộc trong kiểm thử tích hợp
    • Không cần khởi động hoặc enable dependency thật
    • Có thể xây dựng integration test nhanh hơn và deterministic hơn
  • Vấn đề fake có thể sai được xử lý bằng contract test
  • Vì kiểm thử property-based dựa trên trạng thái và song song xác minh sự khớp nhau giữa fake và triển khai thật, fake đóng vai trò như một dependency đã được contract-test

  • Tách kiểm thử và triển khai bằng Queue fake

    • Interface queue IQueue có iNew, iPut, iGet, iSize
    • Triển khai thật nối trực tiếp C queue wrapper
    • Triển khai fake lưu trạng thái mô hình trong IORef và cập nhật qua fNew, fPut, fGet, fSize
    • Component được viết theo interface IQueue q
    • Khi kiểm thử dùng instance fake, khi triển khai dùng instance real
    • Dùng kiểm thử property-based dựa trên trạng thái để đặt tiền đề rằng fake faithful với real

  • File system fake

    • Interface file system IFileSystem h có iMkDir, iOpen, iWrite, iClose, iRead
    • Triển khai thật dùng file system thực dưới /tmp/qc-test
    • fake được triển khai bằng FakeFS in-memory gồm directory set, file content map, open handle map và next handle
    • fOpen, fWrite, fClose, fRead mô hình hóa các precondition failure như busy file, directory không tồn tại, handle đã đóng
    • Nếu fake file system được kiểm thử là faithful với file system thật, các component phụ thuộc vào file system có thể integration test bằng fake và thay bằng real file system khi triển khai
    • Nếu phát sinh bug khi thay bằng real, cần điều tra mismatch giữa fake và real đã vượt qua kiểm thử property-based dựa trên trạng thái như thế nào

  • Hệ thống component lớn hơn

    • Hệ thống trong đó A phụ thuộc vào B và B phụ thuộc vào C cũng được mở rộng theo cùng cách
    • Đặt interface cho từng component
      • iC :: IO IC
      • iB :: IC -> IO IB
      • iA :: IB -> IO IA
    • Chiến lược kiểm thử như sau
      • Xác minh C bằng kiểm thử property-based dựa trên trạng thái và song song để thu được fake C đã contract-test
      • Trong integration test của B, dùng fake C
      • Trong kiểm thử A, dùng fake B sử dụng fake C
    • Cách này mở rộng theo cùng một pattern cho nhiều component hoặc service hơn

Kết luận

  • Kiểm thử property-based dựa trên trạng thái và song song có thể được triển khai bằng khoảng 400 dòng code, quy mô tương đương bản triển khai QuickCheck đầu tiên khoảng 300 dòng khi chưa có shrinking
  • Dùng fake làm mô hình giúp việc viết đặc tả cho kiểm thử dựa trên trạng thái và song song trở nên quen thuộc hơn, đồng thời có thể tái sử dụng để kiểm thử các hệ thống lớn hơn theo cách compositional
  • Nếu cộng đồng từng ngôn ngữ tiếp tục thử nghiệm, vẫn còn dư địa để cải thiện tình trạng của các thư viện property-based testing

Bài viết liên quan

1 bình luận

 
GN⁺ 2024-07-06
Ý kiến trên Hacker News

  • Fuzzing dựa trên coverage đã xuất hiện và Go cũng hỗ trợ khá tốt, nên tôi tò mò nếu không dùng thư viện kiểm thử dựa trên thuộc tính thì sẽ bỏ lỡ điều gì
    https://www.tedinski.com/2018/12/11/fuzzing-and-property-tes...
    Nhìn vào fuzz test bên dưới và phần kiểm tra bất biến tương ứng, tôi thấy về thực chất nó gần như giống kiểm thử thuộc tính
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...
    https://github.com/ncruces/aa/blob/505cbbf94973042cc7af4d6be...

    • Việc phân biệt giữa kiểm thử dựa trên thuộc tính và fuzzing phần lớn chỉ là cách gom nhóm khá thô theo cảm nhận
      Có khác biệt thực sự, nhưng ranh giới khá mờ, và việc phân định chính xác cái gì là fuzzing, cái gì là kiểm thử dựa trên thuộc tính không quá quan trọng
      Các bài test chạy nhanh với assertion chi tiết thì là kiểm thử dựa trên thuộc tính; chạy lâu và chỉ tìm crash thì là fuzzing; phần ở giữa thì mơ hồ
      https://hypothesis.works/articles/what-is-property-based-tes...
    • Hoàn toàn có thể kết hợp fuzzing dựa trên coverage với kiểm thử dựa trên thuộc tính
      Khi còn ở Google, có một công cụ nội bộ kết hợp hai thứ này rất tốt. Bạn viết kiểm thử dựa trên thuộc tính như bình thường; khi chạy, test framework sẽ biên dịch theo cách đặc biệt để thu được coverage và điều chỉnh input ngẫu nhiên nhằm tăng coverage. Tất nhiên nó chạy hoàn toàn tự động trên một cụm nhiều máy
      Kiểm thử dựa trên thuộc tính truyền thống thường chỉ được triển khai dưới dạng thư viện, nên không nhất thiết có thông tin coverage để dẫn hướng việc sinh input ngẫu nhiên
    • Vì đang assertion các thuộc tính, tôi xem nó theo định nghĩa là kiểm thử dựa trên thuộc tính, kiểu như “mọi node có level lớn hơn 1 đều có hai con”
      Tuy nhiên tùy thư viện, bạn có thể nhận được khá nhiều tiện ích. Một trong những thứ hữu ích là shrinking, có thể tham khảo mục “Shrinking” ở đây: https://tech.fpcomplete.com/blog/quickcheck-hedgehog-validit...
      Các combinator để kết hợp generator cũng rất tuyệt, và tùy thư viện còn có sẵn tập các giá trị “xấu” đã biết có thể gây ra hành vi ngoại lệ
    • Tôi không rõ fuzz test của Go khác nội dung trong bài được liên kết như thế nào, nhưng bài đó nói rằng một fuzzer đúng nghĩa cần chạy trong nhiều ngày hoặc nhiều tuần, và hầu như lúc nào cũng nên chọn kiểm thử dựa trên thuộc tính thay vì fuzzing
      Lùi lại một bước, tôi muốn đặt câu hỏi mang tính meta hơn về kiểm thử. Test thành công có đồng nghĩa với code thành công, và điều ngược lại có đúng không? Có phần nào trong hợp đồng của Go ghi rõ rằng cùng một input đưa vào cùng một code sẽ cho ra cùng một output không?
    • Từ góc nhìn API, thứ chủ yếu nhận được là một thư viện combinator để sinh các cấu trúc dữ liệu ngẫu nhiên theo ý muốn
      Khi làm việc với kiểu Arbitrary biểu diễn tập các đối tượng ngẫu nhiên, bạn có thể dễ dàng viết các hàm tái sử dụng để sinh input kiểm thử. Có vẻ những thư viện như vậy cũng có thể dùng chung khá dễ với framework fuzzing của Go
      Dù vậy, tôi thấy các combinator thông thường như map, filter, chain, oneOf có thể hơi gượng, nên đang viết một thư viện kiểm thử thuộc tính mới cho JavaScript. Mục tiêu là làm cho nó dễ dùng hơn, nhưng hiện vẫn mang tính thử nghiệm và chưa công khai

  • clojure.spec.alpha là một trải nghiệm tuyệt vời, dù có dùng cùng test.check hay không, nhưng khi thử hypothesis của Python thì thật sự rất tệ
    Hypothesis có vẻ như theo thiết kế không xử lý được các tập dữ liệu đơn giản nhưng “lớn”, mà “lớn” ở đây thực ra cũng không lớn đến vậy. [0] Quá đau khổ nên tôi đã gỡ hẳn Hypothesis và kiểm thử dựa trên sinh dữ liệu khỏi bộ kiểm thử Python ở công ty
    [0] https://github.com/HypothesisWorks/hypothesis/issues/3493

    • Trong trường hợp này, nghe có vẻ không phải Hypothesis không xử lý được tập dữ liệu lớn, mà là nó đã từ chối khá nhiều trường hợp đã được thu nhỏ
      Hypothesis cố thu nhỏ số nguyên được sinh ra về 0 để xem lỗi có tồn tại cả với 0 không, còn bài test thì từ chối thay vì fail vì có chứa 0. Với các trường hợp nhỏ thì chỉ là kém hiệu quả, nhưng với trường hợp lớn thì đến mức Hypothesis bỏ cuộc
      Trong thread đó có người đề xuất dùng một chiến lược sinh instance khác không thể sinh ra 0. Tức là thay vì sinh ra giá trị mà bộ shrinker của Hypothesis thích nhất rồi từ chối nó, thì ngay từ đầu đừng tạo ra nó. Không biết bạn đã thử chưa
      Tôi cũng tò mò clojure.spec.alpha xử lý việc này khác thế nào
      Bình luận của mjaniczek tại https://news.ycombinator.com/item?id=40876437 nêu trường hợp này như một nhược điểm của cách tiếp cận Hypothesis
      Đại ý là: “Vì generator giờ trở thành một parser danh sách byte có thể thất bại, nên sẽ có chút kém hiệu quả, và người dùng có thể tạo ra những generator kỳ lạ mà shrinker nội bộ không thể thu nhỏ hoàn hảo. Dù vậy, trong ba cách tiếp cận thì trải nghiệm developer vẫn là tốt nhất…”
      Tất nhiên có lẽ bạn sẽ không đồng ý rằng mình đã viết test theo cách “kỳ lạ”
    • Tôi thích spec của Clojure vì rất dễ xây dựng mọi thứ xung quanh nó, nhưng khi chuyển sang Elixir, muốn viết kiểu test đó thì phải xuống tận propEr, một thư viện Erlang cũ. Khá thất vọng
    • Ví dụ trong issue GitHub đang dùng filter theo cách tự gây ra vấn đề
      Nếu sinh ngẫu nhiên rồi lọc những thứ phù hợp với một thuộc tính nào đó, thì trong quá trình sinh dữ liệu về cơ bản là bạn đang cào vé số

  • Câu trả lời ngắn cho câu hỏi trong bài “Tại sao không có yêu cầu rằng nghiên cứu đã xuất bản phải có thể tái lập bằng công cụ mã nguồn mở, hoặc ít nhất là bằng công cụ được cung cấp miễn phí cho công chúng và các nhà nghiên cứu khác?” là hệ quả tức thì của yêu cầu đó sẽ là những bài báo không đáp ứng điều kiện này sẽ không được xuất bản
    Chẳng hạn, ngay cả những thứ có vẻ hữu ích cho tác giả và người khác như bài báo về Quviq QuickCheck cũng có thể đã không được xuất bản, và cộng đồng sẽ mất đi món quà thông tin đó

    • Sẽ tốt nếu một số nhà xuất bản yêu cầu khả năng tái lập, còn một số thì không
      Mọi yêu cầu đều có hiệu ứng loại trừ, và luôn có những trường hợp ranh giới là các bài báo vẫn hữu ích dù không đáp ứng yêu cầu
    • Đây rõ ràng không phải một câu hỏi có ranh giới rạch ròi, thậm chí có thể gọi là câu hỏi mang tính chính trị, nhưng lập luận bảo vệ này cũng không mấy thuyết phục
      Nếu coi lập luận này là hợp lệ, ta có thể dùng nó làm lá chắn để đi xa đến bất cứ đâu. Nếu bỏ khả năng tái lập khỏi yêu cầu, thì không cần giải thích bất cứ điều gì mình không muốn giải thích. Không cần cung cấp dữ liệu về mẫu, cũng không cần kiểm định ý nghĩa thống kê. Chỉ một abstract mơ hồ tuyên bố đã đạt được kết quả nào đó là đủ
      Thậm chí ghi chú nổi tiếng mà Fermat để lại ở lề bản sao cá nhân của Arithmetica cũng trở thành một bài nghiên cứu hoàn toàn hợp lệ. Vì hẳn ta không muốn mất thông tin quý giá rằng một nhà toán học nổi tiếng nghĩ mình có một chứng minh ngắn gọn và thanh nhã cho một định lý nào đó. Dĩ nhiên trên thực tế rất có thể ông không có
      Quan điểm của tôi về câu hỏi chính trị này là tiêu chuẩn hiện nay quá lỏng lẻo. Không ai bị ép buộc phải xuất bản điều gì. Trên đời có nhiều nghiên cứu không được xuất bản ở đâu cả vì những lý do như giá trị độc quyền, và các nghiên cứu đó sẽ không biến mất
      Nhưng nếu làm việc trong giới học thuật, hơn nữa còn nhận tài trợ nghiên cứu, và nói rằng mục tiêu là thúc đẩy tri thức khoa học của thế giới tiến lên, thì việc yêu cầu thực sự theo đuổi mục tiêu đó là công bằng. Không nên chỉ giả vờ theo đuổi mục tiêu ấy để leo nấc thang sự nghiệp học thuật
    • Có lẽ cũng có thể theo cách chỉ công khai mã nguồn cho người phản biện
      Cung cấp kèm cả những thứ cần thiết để chạy code. Có thể họ đã làm như vậy rồi
    • Vì khả năng tái lập là nền tảng của phương pháp khoa học
    • Bài báo được xuất bản vì các tác giả muốn tăng “chỉ số tầm quan trọng”, và điều này liên quan rất trực tiếp đến lương thưởng cũng như cơ hội sự nghiệp học thuật
      Việc có thêm yêu cầu cho mục đích đó khó có khả năng làm giảm số lượng bài báo được xuất bản
      Vấn đề nghiêm trọng hơn của các bài báo đã xuất bản là người ta thường cố tình bỏ qua sai sót để xuất bản càng nhiều càng nhanh càng tốt. Nếu việc kiểm chứng bài báo trở nên dễ hơn thì tình hình có thể cải thiện, nhưng tôi sẽ không kỳ vọng quá nhiều. Con người rất giỏi tìm đường tắt

  • Tôi khá thường xuyên viết kiểm thử thuộc tính có trạng thái bằng proptest của Rust, và thường thì tự code cũng khá đơn giản
    Một ví dụ không tầm thường đã tìm ra 6 lỗi nằm ở https://github.com/sunshowers-code/buf-list/blob/main/src/cu...
    Kiểm thử song song đôi khi có thể hữu ích, nhưng nhiều lúc chỉ cần chạy nhiều bài test song song lại dễ hơn

    • Tôi viết khá nhiều kiểm thử thuộc tính thủ công trong Rust, đại thể theo dạng này
      Ở tầng trên cùng dùng tính ngẫu nhiên thật, bên dưới đặt nhiều vòng lặp lồng nhau để đi từ các trường hợp độ phức tạp thấp lên các trường hợp độ phức tạp cao. Sau đó tạo và in ra seed để đưa vào bộ sinh số giả ngẫu nhiên tất định. Nếu test thất bại, chỉ cần copy-paste seed lỗi để tái hiện ca thất bại
      Tôi thấy kiểu kiểm thử thuộc tính thủ công này nhanh hơn, linh hoạt hơn và nhìn chung ít phiền phức hơn bất kỳ framework hay thư viện nào
      Tuy nhiên, với kiểm thử đồng thời thật sự chắc chắn, tôi rất khuyến nghị thư viện AWS Shuttle (https://github.com/awslabs/shuttle). Nó có thể tìm ra những race condition phức tạp đến khó tin. Tôi cũng đã viết một tutorial nhỏ: https://grantslatton.com/shuttle
      Ở AWS, chúng tôi đã dùng thư viện này để kiểm chứng hệ thống tệp tùy chỉnh viết để vận hành AWS S3

  • Tôi đã lướt nhanh bài báo “Testing Telecoms Software with Quviq QuickCheck” được liên kết, nhưng không thấy ngay câu trả lời cho câu hỏi “tại sao không tự tạo các thao tác có trạng thái này thì tốt hơn?”
    Bài gốc chỉ vào phần này bằng mô hình các cặp khóa-giá trị của một kho khóa-giá trị, nhưng tôi không hiểu vì sao không thể chỉ viết một state machine, hay vì sao cần framework. Tuần trước ở chỗ làm tôi đã làm đúng như vậy để test tương tác với hệ thống tệp, và cuối cùng nó quy về kiểu type Instruction = | Read of stuff | Write of stuff | Seek of stuff | …
    Khi đó thuộc tính sẽ là “với danh sách lệnh này, …”. Kiểu StateModel về cơ bản cũng yêu cầu làm cùng việc đó. Tôi khó thấy StateModel thực sự đóng góp phần đáng kể nào; có vẻ nó chỉ giúp giảm một lượng rất nhỏ mã kiểm thử trong thực tế, đổi lại phải thêm vào nhiều mã framework cần hiểu hơn rất nhiều

    • Có những bài test mà nhận định đó đúng, nhưng phần thu nhỏ ca thất bại thường khá khó
      Nếu muốn chỉ sinh các chuỗi chuyển trạng thái “hợp lệ”, thường bạn cần trạng thái mô hình để xác định bước test nào hợp lệ ở một trạng thái cụ thể. Ngoài ra, trong quá trình thu nhỏ, khi loại bỏ các bước test, phải tránh phá vỡ các tiền điều kiện đã được tuân thủ khi sinh từng bước ban đầu, nếu không sẽ tạo ra lỗi giả
      Nếu ở trạng thái nào thao tác nào cũng hợp lệ và bạn chỉ muốn một chuỗi thao tác tùy ý hoàn toàn ngẫu nhiên, framework proptest có trạng thái có thể là quá mức cần thiết. Nhưng nếu phải duy trì trạng thái mô hình và chỉ định tiền điều kiện cho nhiều thao tác, một framework chuyên dụng sẽ giúp bớt rất nhiều việc
      Năm ngoái tôi đã viết một bài blog về chủ đề này; nếu muốn xem ví dụ sâu hơn thì có thể tham khảo: https://readyset.io/blog/stateful-property-testing-in-rust
      Như những người khác đã nói, kiểm thử state machine song song cũng là một lợi ích hay mà framework chuyên dụng mang lại, nhưng đó không phải lợi ích duy nhất
    • Tôi nghĩ phần có trạng thái được kiểm thử dựa trên mô hình xử lý tốt hơn
      Có thể trộn các phong cách kiểm thử với nhau. Dù sao cũng là code của bạn
    • Theo tôi hiểu, QuickCheck song song kiểm tra rằng mọi interleaving có thể có trong chương trình đa luồng rốt cuộc có tạo ra một trạng thái cũng có thể đạt được khi gọi các lệnh tuần tự hay không
      Đó chính là lợi ích

  • Tác giả tập trung vào khía cạnh máy trạng thái và song song của kiểm thử dựa trên thuộc tính, nhưng cũng có những khía cạnh khác có thể mang lại hiệu quả lớn hơn
    Một là kiểm thử dựa trên thuộc tính được dẫn dắt bởi độ bao phủ, có thể xem bài của Dan Luu: https://danluu.com/testing/
    Một khía cạnh khác, nơi tôi có phần thiên vị, là tự động hóa việc thu nhỏ trong khi vẫn duy trì mọi bất biến đã được tạo ra khi sinh giá trị
    Tóm lại, các hàm thu nhỏ phái sinh kiểu QuickCheck hoạt động trên giá trị (shrink : a -> [a]) có các ràng buộc và vấn đề, khiến mọi người tắt luôn việc thu nhỏ thay vì xử lý vấn đề
    “Thu nhỏ tích hợp” bằng cây rose (ví dụ: Hedgehog) tuân theo các ràng buộc của generator, nhưng gặp vấn đề với monad bind, tức là trường hợp dùng kết quả của generator để rẽ nhánh sang generator khác
    Cách tiếp cận duy nhất trông như có phép màu “cứ thế mà chạy” là thu nhỏ nội bộ của Hypothesis. Nó dùng một tầng gián tiếp để rút gọn danh sách các lựa chọn ngẫu nhiên thay vì chính giá trị. Nhược điểm là generator giờ trở thành một parser danh sách byte có thể thất bại, gây ra một chút kém hiệu quả, và người dùng có thể tạo ra những generator kỳ lạ mà bộ thu nhỏ nội bộ không thể rút gọn hoàn hảo. Dù vậy, trong ba cách tiếp cận, đây là cách có trải nghiệm nhà phát triển tốt nhất; xét đến việc chỉ riêng chuyện mọi người chịu viết test đã là một phép màu nhỏ, với tư cách tác giả thư viện kiểm thử, tôi thấy đây là cách đáng xây dựng nhất

    • Phần nói rằng “thu nhỏ tích hợp” bằng cây rose (ví dụ: Hedgehog) tuân theo các ràng buộc của generator nhưng có vấn đề với monad bind, trong giới hạn hiểu biết nghiệp dư của tôi, là giới hạn căn bản của monad bind/generator
      Thay vào đó, để thu nhỏ tối ưu nên ưu tiên generator applicative: https://github.com/hedgehogqa/haskell-hedgehog/issues/473#is...
      Nói cách khác, generator applicative không “dùng kết quả của generator để rẽ nhánh sang generator khác”, và nhờ tính chất “song song” của applicative mà việc thu nhỏ được tối ưu hóa. Ở đây “song song” không mang nghĩa threading trong bài viết, mà theo nghĩa monadic. Vì applicative là “song song” nên các generator có thể được rút gọn độc lập. Ngược lại, generator monad là “tuần tự”, nên khi rút gọn một cái thì hành vi của generator theo sau nhất thiết sẽ thay đổi
      Nếu có bài trình bày công khai thì tôi muốn xem liên kết
    • Cá nhân tôi thấy Hypothesis còn lâu mới là kiểu “cứ thế mà chạy”
      Tôi không nghĩ nó thực sự sẵn sàng cho production, và điều đó có vẻ là do thiết kế.[0]
      Tôi đã dùng clojure.spec.alpha khá nhiều, cả cùng với test.check lẫn không, nên dù có khác biệt, tôi cũng không hoàn toàn xa lạ với ý tưởng chung
      [0] https://github.com/HypothesisWorks/hypothesis/issues/3493
    • Framework tôi thích là falsify, và nó cung cấp “thu nhỏ tích hợp nội bộ”
      Nó giống Hypothesis nhưng dùng cây generator thay vì chuỗi tuyến tính. Nó dựa trên selective functor, một giao diện tốt và cũng hữu ích cho những thứ như validator
      Theo https://hackage.haskell.org/package/falsify, thư viện này cung cấp kiểm thử dựa trên thuộc tính hỗ trợ thu nhỏ tích hợp nội bộ. “Tích hợp” theo nghĩa của Hedgehog, tức là không cần viết riêng shrinker và generator; và “nội bộ” theo nghĩa của Hypothesis, tức là vẫn hoạt động tốt xuyên suốt monad bind

  • Tôi từng thử dùng kiểm thử dựa trên thuộc tính nhưng luôn có cảm giác bị kẹt giữa hai chiếc ghế
    Nếu hiểu một thuộc tính đủ rõ để kiểm thử nghiêm ngặt, thường thì có thể đẩy nó vào hệ thống kiểu để nó đúng theo cấu trúc. Còn nếu chỉ muốn một bài smoke test đơn giản thì một input tùy ý sẽ dễ hơn

    • Tôi tò mò bạn đang nghĩ đến loại thuộc tính nào
      Ví dụ, thường có hai implementation: một bản ngây thơ chậm nhưng đơn giản và một bản đã tối ưu, rồi có thể so sánh output của chúng với input tùy ý. Đây là một thuộc tính đơn giản, dễ hiểu, nhưng nói chung khó đưa vào hệ thống kiểu
      Tương tự, có thể có các tính chất như thứ tự đưa input vào không được quan trọng, hoặc có cách chia dữ liệu sao cho max(giá trị lớn nhất của A, giá trị lớn nhất của B) = maximum(A union B). Làm sao encode những thứ như vậy vào hệ thống kiểu?
      Hoặc những điều như “với A và B bất kỳ, một nghiệm tối ưu tìm được trong A sẽ không tệ hơn một nghiệm tối ưu nào đó tìm được trong A union B”, hay tính lũy đẳng như f(f(A)) = f(A)
      Tất cả đều là những thuộc tính dễ hiểu, nhưng không dễ mô tả trong hầu hết các hệ thống kiểu
    • Nếu có thể thì rõ ràng ép ràng buộc ở thời điểm biên dịch sẽ tốt hơn
      Nhưng có nhiều ràng buộc mà các trình kiểm tra kiểu phổ biến không xử lý được. Kiểu phụ thuộc sẽ giúp rất nhiều, nhưng hiện có vẻ vẫn bị giới hạn trong các ngách như theorem prover

  • Tôi tự hỏi liệu danh sách có đang thiếu QuviQ Erlang QuickCheck gốc không
    Sản phẩm đầy đủ là độc quyền, nhưng họ cũng cung cấp bản miễn phí QuickCheck Mini: http://www.quviq.com/downloads/

  • Clojure giờ cũng có thư viện quickcheck có trạng thái: https://github.com/griffinbank/test.contract
    Kiểm thử song song thì thú vị, nhưng đến giờ vẫn chưa phải nguồn gây đau đầu lớn

  • Với các bài test C#/.NET, tôi đã dùng CsCheck[0] và khá hài lòng
    Nó dễ tiếp cận hơn nhiều so với Hedgehog hay FsCheck, và tốc độ cũng khá nhanh
    [0] https://github.com/AnthonyLloyd/CsCheck