Making our Own Luck: A Language for Writing Random Generators

QuickCheck-style property-based random testing requires efficient generators for well-distributed random data satisfying complex logical predicates.  Writing such generators by hand can be difficult and error prone.

We propose a domain-specific language, Luck, in which generators are expressed by decorating predicates with lightweight annotations controlling both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated.  Generators in
Luck are compact, readable, and maintainable, with efficiency close to custom handwritten generators.

We give a precise denotational semantics for Luck, reminiscent of those of probabilistic programming languages, and prove key theorems about its behavior, including the soundness and completeness of random generation with respect to a straightforward predicate semantics.  We evaluate Luck on a collection of common examples from the random testing literature and on two significant case studies showing how Luck can be used for complex bug-finding tasks with comparable effectiveness and an order of magnitude reduction in testing code size, compared to handwritten generators.

Extended Abstract: Making Our Own Luck

Slides: LuckSlides

by Leonidas Lampropoulos, Benjamin C. Pierce, Cătălin Hriţcu, John Hughes, Zoe Paraskevopoulou and Li-yao Xia

This entry was posted in Uncategorized. Bookmark the permalink.

2 Responses to Making our Own Luck: A Language for Writing Random Generators

  1. It seems a worthwhile project to take the random generators that have been found useful for testing and express them as a useful-for-testing probabilistic program or a family of useful-for-testing probabilistic programs. At least the program could just recapitulate the random generator implementation; at most the program could make use of conditioning or observation constructs in an elegant way.

    • I would love to see (and help from the testing side in) a project that encodes a lambda calculus typechecker as a probabilistic program that can find the same (shallow) bugs in GHC 6.12 as http://www.cse.chalmers.se/~palka/testingcompiler/. If, during this process, we can establish some sort of methodology for using probabilistic programs as test input generators in a more principled manner even better! I can use it afterwards for all the other projects we developed Luck for :)

Leave a Reply