A repro case for a bug found by model-testing Chamelon

[gasche]

@Armael and I looked at model-based testing for Chamelon during the Mirage retreat, and we found what looks like a bug (full self-contained file at the end):

let () = Lwt_main.run @@
  let* empty = empty () in
(* @02 *) let x1 = empty in
(* @03 *) let* () =
            set x1 ([ 0; 0 ], 2) (String.make 67 ' ') in
(* @04 *) let* () =
            set x1 ([ 0; 0 ], 0) (String.make 126 ' ') in
(* @05 *) let* () =
            set x1 ([ 0; 0 ], 0) "\001" in
(* @07 *) let* () =
            set x1 ([ 0; 0 ], 0) "\000" in
(* @09 *) let* (Some observed) = get x1 ([ 0; 0 ], 0) in
          Printf.printf "%S\n%!" observed;
          assert (String.equal observed "\000");
          Lwt.return ()
          (* candidate finds "\001" *)

The sizes of the writes on instructions @03 and @04 matter, using 66 or 126 makes the bug go away.

momo_repro.ml.txt

[gasche]

When I posted the issue above we were just out of an intense bug-hunting session with @Armael and @yomimono -- and in particular, I did not want to admit that my git history for our bug-hunting branch was in a horrible state.

I have now invoked the historical powers of jj and pushed a branch with our experiments, that is probably more pleasant to use than momo_repro.ml.txt above: https://github.com/gasche/chamelon/tree/monolith-testing

(I also wrote a blog/forum post about our work at https://discuss.ocaml.org/t/blog-post-using-model-based-testing-on-a-mirage-filesystem-implementation/16666 )

[yomimono]

Thanks again for this work! I did finally manage to fix this bug, along with another tricky one that momo discovered. I'm currently using your monolith-testing branch, but since you didn't PR it I haven't merged it into main.

[gasche]

In my mind monolith-testing was exploratory programming, and I wouldn't have submitted it for inclusion upstream as a finished product. But then the details have escaped my medium-term memory since then, so it was probably unwise to leave it at that. I think it would be useful to document things a bit more, in particular the separation between the parts that make sense long-term and the parts that we added in to reproduce a specific trace. (I don't know if the content in the latter category should be left around as an example, or just removed.) I am also not sure how best to integrate this into your existing testing strategy.

(One good news is that, after we did this, Monolith evolved to stop taking control and running forever, now we can provide an explicit timeout through the command-line so it has become (barely) usable in non-interactive settings.)

I can't spend a lot of time right now; I can "submit a PR" but then I don't know if this is of any use to you (I myself wouldn't merge it in its current state). My impression is that you are better-positioned to decide whether/how to integrate this testing approach in the upstream repository long-term.

[gasche]

Note: I don't want to suggest that monolith-testing was only a one-time experiment that should be left alone. In my experience working on the store library, a model-based testsuite is in fact an invaluable tool during development, because it is extremely efficient at finding bugs when the code evolves. (We use it very often interactively during development, which means that it is not so useful in the CI as we check our changes with it first -- the project is small and does not receive external contributions so far).