This paper details the application of property-based testing (PBT) to find bugs in the OCaml 5 multicore runtime system, which underwent a major rewrite to support parallel execution. The author presents three case studies of increasing complexity, all utilizing a model-based state machine framework: testing the Array module, the non-deterministic weak hash sets, and the garbage collector (GC). The methodology involves generating random sequences of operations and comparing the system's behavior against a formal model, particularly in parallel scenarios designed to uncover race conditions. The paper evaluates the success of this approach by detailing the numerous critical bugs discovered—ranging from segmentation faults and race conditions to incorrect documentation and assertion failures—and discusses the practical challenges encountered during the process.
Uncovering Bugs in OCaml 5: A Property-Based Testing Approach
Sec. 1 - The Challenge of Multicore: The paper introduces Property-Based Testing (PBT) as a method to ensure the stability of OCaml 5's rewritten multicore runtime system. It uses a model-based state machine framework to test random sequences of function calls against a simplified model of their expected behavior, which is particularly useful for complex and concurrent systems.
Sec. 2 - Case Study 1: The Array Module: As a "warm-up," the Array module is tested. The framework generates commands (Get, Set, Sort), compares results to a list-based model, and runs tests both sequentially and in parallel.
Key Takeaway: This simple test successfully identified a segmentation fault on the PPC64 architecture related to its unique signal-based method for handling out-of-bounds indexing.
Sec. 3 - Case Study 2: Weak Hash Sets: This study tackles a more complex, non-deterministic data structure where elements can be garbage collected at any time. The model defines the "best case" behavior (no elements removed), while post-conditions are relaxed to accept valid non-deterministic outcomes (e.g., an element is not found).
Key Takeaway: Parallel testing revealed race conditions in the underlying functions for weak hash sets, which could cause the runtime to crash.
Sec. 4 - Main Case Study: The Garbage Collector (GC): The most complex test targets the OCaml 5 garbage collector. A comprehensive set of commands is defined to trigger memory allocations, explicit collection cycles (minor, major, compaction), and dynamic configuration changes. This test focuses on performing sanity checks and detecting crashes, hangs, or assertion failures rather than strict state agreement.
Sec. 5.1 - Key Bugs Discovered: The test suite proved highly effective, finding over 40 issues in total. The paper highlights 8 bugs from these three case studies alone, including:
A race condition where a terminating domain could corrupt the heap during GC compaction.
Segmentation faults from improper GC root registration.
An assertion failure in the debug runtime caused by incorrect stat updates during compaction.
Outdated and incorrect documentation for GC functions.
Sec. 5.3 - Testing Challenges: The author outlines several practical difficulties, including test runs that deadlock or enter infinite loops, runtime crashes that also take down the test runner (solved by forking test processes), and the challenge of reproducing rare, timing-sensitive race conditions, even after a failure is detected.
Sec. 7 - Conclusion: A Highly Effective Approach: The paper concludes that model-based PBT is an excellent technique for finding subtle, hard-to-reproduce bugs in complex systems, memorably described by a core developer as "manufacturing bad luck on an industrial scale." The complete test suite is open source.