Formal Verification: Release of Ortac 0.8.0 for Testing with Domains

We have recently released a new version, number 0.8.0, of the Ortac tool as part of the Gospel ecosystem for dynamic formal verification.

Gospel is a contract-based formal specification language for OCaml. It allows the user to define logical models for abstract data-types and describe the expected behaviour of functions with pre- and post-conditions. Specifications are type-checked with gospel check file.mli. In order to obtain some guarantees about your OCaml implementation with respect to the Gospel annotations, you need to use Ortac. The core idea behind ortac is to translate a subset of the Gospel specification language into OCaml code and use these translations to generate runtime checking.

For more context, you can explore our previous post discussing our involvement in the Gospel Project or check out our tutorial on how to use Ortac/QCheck-STM.

How Ortac Works: Modes

Ortac has a plugin architecture, including one to generate QCheck-STM tests and one to wrap original functions with runtime assertion checking. Those are respectively called the QCheck-STM mode (or Ortac/QCheck-STM) and the wrapper mode (or Ortac/Wrapper). We also propose a dune mode to help generate the necessary Dune boilerplate.

One other important piece of the architecture is the Ortac runtime. The code generated by the two first modes (QCheck-STM and Wrapper), depends on runtime functionalities. Among these functionalities is the trusted OCaml implementation of the Gospel logical library used to write the specifications. However, some parts of the generated code will be specific to each mode. Adding new functionalities can involve modifying or extending the runtime; it needs to be done carefully since it involves reasoning about the interaction between the generated code and the runtime.

The new release focusses on making Ortac/QCheck-STM take advantage of more features from the QCheck-STM test framework: namely testing in a parallel context and flexibility of the command generation. In this post, I will focus on testing with multiple domains using the latest version of Ortac.

Parallel Safety Testing and Ortac 0.8.0

Now, regarding testing in a parallel context, in the original QCheck-STM test framework, this feature is included 'for free' when we write an OCaml specification for a library. It is just a matter of instanciating the STM_domain.Make functor rather than the STM_sequential.Make one. So, why did we need a new release for Ortac to be able to generate a test suite for parallel safety with QCheck-STM?

There are two reasons:

1. The introduction of the bug report feature in version 0.2.0
2. Support for functions with multiple SUT arguments and SUT-returning functions since version 0.4.0

We'll start with how we've dealt with multiple SUT arguments and SUT-returning functions and then move on to the bug report feature.

Multiple SUTs and SUT-Returning Functions

As a reminder, SUT stands for System Under Test. It expresses the type of the OCaml value that is being tested against its model (called the state) in the QCheck-STM tests.

For example, if we have a library exposing a type 'a t and want to write some QCheck-STM tests for this library, we will declare a type sut = char t. We indeed have to instantiate the 'a type parameter in order to run tests.

QCheck-STM tests generate a program based on calls to functions from the library we want to test, run them and compare the traces of this run with a run of the same program on the model. You can read more about this in our blog post on property based tests for OCaml 5.

Now, since version 0.4.0, and thanks to Nikolaus Huber's internship, Ortac/QCheck-STM supports testing functions with multiple SUTs as arguments and SUT-returning functions. These functions are not easily tested when we write QCheck-STM tests by hand.

One example of a function with multiple SUTs as its argument is the comparison function. If you only have one SUT at hand, you can't really test the comparison function.

One example of a SUT-returning function is the copy function. The SUT being an abstract data-type, you can't really check postconditions about it. You'll need to wait until it appears as an argument to a later call, for example to a length or a get function.

In order to include these functions in the test coverage, the generated tests call a runtime that maintains a stack of SUTs. When the tests run a command, the SUTs arguments are popped from the stack. After the call the returned SUT value is pushed on the stack after the arguments have also been pushed back on the stack in an order-preserving way. You can read more on this topic here.

When adding support for testing with Domains, we had to be careful about parallel access to the arguments and decide what to do with newly created SUTs.

Regarding the SUT arguments, we had to make parallel access safe, but not too much so: we still wanted to be able to catch bugs from parallel accesses to individual SUTs, but we didn't want to catch bugs caused by race conditions on the stack of SUTs implemented in ortac-qcheck-stm-runtime. In other words, we needed to make access to the stack safe, but we didn't want to add safety to the element of the stack beyond the one provided by the library we were testing.

In the original implementation, the SUT arguments were popped from the stack. In a parallel setting when a stack is not made parallel-safe, anything can happen. First of all, we were relying on the scheduler to create a race condition on the stack of SUTs in order to test parallel access to the same SUT (parallel-safety is hard enough to test without adding one more layer of probability!). Then, once the same SUT had been selected by both domains, it would be pushed back twice.

               

We can't make the stack of SUTs completely parallel safe neither. Indeed, in this case we would end up never testing parallel access to the same SUT, completely defeating the point of targeting QCheck-STM+Domains tests.

The solution we've chosen is to modify the SUTs in place in the stack.

               

Now, regarding the newly created SUTs, do we want to push them to the stack or not?

In sequential testing, they are indeed pushed onto the stack. This it what allows us to test them: if a newly created SUT does not conform to its model (there is a bug in the function), then the behaviour of the rest of the program will most probably differ from the behaviour of the model.

When testing in a parallel context, the generated program is a triplet: a sequential prefix that allows us to put the SUT in a random state and two parallel tails that allows us to test the behaviour of the library in a parallel context. It is quite clear that we can still push the SUTs created in the sequential prefix on the stack: the behaviour is no different than when testing in a sequential context. But the stack of SUTs being shared, we can't push the ones created in the parallel tails onto it: this would allow a function from the other domain to access it, which is not the desired semantic.

More precisely, we need to enforce two new properties of how we handle SUTs in the runtime:

1. A call from one of the parallel tails should never pick as argument a SUT created in the other parallel tail
2. A call from one of the parallel tails should be able to pick as argument a shared SUT (created at initialisation or during the sequential prefix)

(1) is a behaviour that doesn't happen in a real run and (2) is precisely the behaviour we want to test.

One possibility would be to add two other stacks to the runtime: one for each of the parallel tails. Enforcing the first property is then relatively easy: a call from one of the parallel tails is not allowed to pick as an argument a SUT from the stack of SUTs on the other parallel tail.

Enforcing the second property would in contrast necessitate a bit more work. Indeed, we want to be able to pick SUTs from the stack attached to the parallel tail and from the one attached to the sequential prefix. This means replacing the current mechanism that just takes the arguments at the top of the stack by one that randomly chooses arguments from the two stacks (the sequential one and the correct parallel one).

The main concern here is not really the technical challenge (though, a more complex system means a greater possibility of bugs and we don't want bugs in our test frameworks). The main concern is that this implementation would reduce the probability that one SUT appears as argument of two parallel calls.

The solution we've chosen is to simply not push SUTs created in the parallel tails on the stack. This enforces the two properties above: SUTs from a parallel call are never taken as arguments of any call and every SUT argument is a shared SUT.

In order to differentiate between the different contexts at runtime, we simply add a flag to the generated commands to indicate whether they are meant to be run in a sequential context or in a parallel one. Then, the function that handles the stack of SUTs and the one that handles the stack of states look at this flag to decide whether to push the newly created SUT and corresponding state to the relevant stacks.

This way, SUT-returning functions are still fully tested thanks to the sequential prefix, and how the parallel tails are handled is not made more complex than necessary. In particular, no modification of the runtime was needed (which made reasoning about the modifications a lot easier).

The Bug Report Feature

Since version 0.2.0, tests generated by Ortac/QCheck-STM generate a bug report in case of test failure. This is a very nice feature that provides the user with:

1. The piece(s) of Gopsel specification that has been violated
2. The expected returned value (to be compared with the actual returned value) if it is computable from the Gospel specifications
3. A reproduction case in the form of a runnable OCaml program

These pieces of information need to be collected while checking the equivalence between the observed behaviour and the behaviour of the model.

In the original QCheck-STM test framework, a program is generated, then it runs and the observable behaviour is stored (for example the returned value of a length function). Finally, the observed behaviour is compared to the behaviour of running the equivalent program on a model, checking user-defined postconditions.

This comparison is done in STM.Internal.Make.check_disagree for the sequential run and in STM.Internal.Make.check_obs for the parallel one. Both are parameterised by the postcond predicate. In hand-written QCheck-STM tests, this postcond predicate is obviously hand-written and in Ortac-generated QCheck-STM tests, it is generated based on Gospel postcondition clauses and invariants.

Now, in order to build the bug report in case of test failure, we need the postcond function to not be a simple predicate anymore. We need it to return an optional report with the Gospel terms that were violated, the string representation of the call and, if possible, the expected result of the call.

The consequence of this change is that we have to reimplement the check_disagree and the check_obs functions. The former was reimplemented as part of the 0.2.0 release, the latter in the present one. But, as these are the pieces of code that actually do the testing, one has to be extra-careful when modifying them. We've adopted a step-by-step approach to make the preservation of the semantics scrutinasable with testing and reviewing.

The postcond function that the Ortac/QCheck-STM-generated code uses returns an option type rather than a boolean. The None case corresponds to true and the Some report one to false. The idea is to return an explanation in case of test failure.

The first step is to adapt the original function to deal with this postcond functional argument. On a technical level it is trivial, the main benefit is that the check_obs function is now in the ortac code base.

This function now looks like this:

let check_obs postcond =
  (* ignore the report for now *)
  let postcond c s r = Option.is_none @@ postcond c s r in
  let rec aux pref cs1 cs2 s =
    match pref with
    | (c, res) :: pref' ->
        let b = postcond c s res in
        b && aux pref' cs1 cs2 (Spec.next_state c s)
    | [] -> (
        match (cs1, cs2) with
        | [], [] -> true
        | [], (c2, res2) :: cs2' ->
            let b = postcond c2 s res2 in
            b && aux pref cs1 cs2' (Spec.next_state c2 s)
        | (c1, res1) :: cs1', [] ->
            let b = postcond c1 s res1 in
            b && aux pref cs1' cs2 (Spec.next_state c1 s)
        | (c1, res1) :: cs1', (c2, res2) :: cs2' ->
            (let b1 = postcond c1 s res1 in
             b1 && aux pref cs1' cs2 (Spec.next_state c1 s))
             ||
             let b2 = postcond c2 s res2 in
             b2 && aux pref cs1 cs2' (Spec.next_state c2 s))
  in
  aux

The general idea behind this check_obs function is to find a sequential explanation for the behaviour observed in the run involving parallelism. The sequential prefix is first checked against the state using the postcond function provided as an argument. Then, we explore all the possible sequential interleavings of the two parallel tails, using boolean operators short-circuits to stop when we found one interleaving that expains the observed behaviour.

The next step is to actually deal with the optional report postcond is returning. This means modifying the body of check_obs to make it return the report.

Moving from boolean to option type implies adding a lot of matches that could render the code harder to read. Adding to that, the translation is somewhat counter-intuitive: None is actually the max and Some the min of the boolean algebra. This makes the translation error-prone.

To establish trust in our modifications, we have chosen to try to make it as clear as possible on the syntactic level that the semantics are preserved.

We've done that by defining an infix operator corresponding to the equivalent of the conjunction and to the equivalent of the disjunction, using the lazy type to translate the boolean short-circuits.

By using these new infix operators in place of the boolean ones, we can clearly see in the diff between the two implementations that the semantic is preserved:

+  let ( &&& ) o1 o2 = match o1 with None -> Lazy.force o2 | _ -> o1
+  let ( ||| ) o1 o2 = match o1 with None -> None | Some _ -> Lazy.force o2
+
   let check_obs postcond =
-    (* ignore the report for now *)
-    let postcond c s r = Option.is_none @@ postcond c s r in
     let rec aux pref cs1 cs2 s =
       match pref with
       | (c, res) :: pref' ->
-          let b = postcond c s res in
-          b && aux pref' cs1 cs2 (Spec.next_state c s)
+          postcond c s res &&& lazy (aux pref' cs1 cs2 (Spec.next_state c s))
       | [] -> (
           match (cs1, cs2) with
-          | [], [] -> true
+          | [], [] -> None
           | [], (c2, res2) :: cs2' ->
-              let b = postcond c2 s res2 in
-              b && aux pref cs1 cs2' (Spec.next_state c2 s)
+              postcond c2 s res2
+              &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))
           | (c1, res1) :: cs1', [] ->
-              let b = postcond c1 s res1 in
-              b && aux pref cs1' cs2 (Spec.next_state c1 s)
+              postcond c1 s res1
+              &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))
           | (c1, res1) :: cs1', (c2, res2) :: cs2' ->
-              (let b1 = postcond c1 s res1 in
-               b1 && aux pref cs1' cs2 (Spec.next_state c1 s))
-              ||
-              let b2 = postcond c2 s res2 in
-              b2 && aux pref cs1 cs2' (Spec.next_state c2 s))
+              postcond c1 s res1
+              &&& lazy (aux pref cs1' cs2 (Spec.next_state c1 s))
+              ||| lazy
+                    (postcond c2 s res2
+                    &&& lazy (aux pref cs1 cs2' (Spec.next_state c2 s))))
     in
     aux

Obviously, this commit needs special attention in the review process, but it is made quite easy to review. In order to be able to display a runnable program leading to the reported postcondition violation, we need to collect the traces of calls. Adding this collection on top of the previous modifications doesn't change the structure and the logic of the function.

In conclusion, in order to get a bug report for Ortac/QCheck-STM+Domains, we had to reimplement the heart of the test framework, the check_obs function. As it should be, we have relied heavily on code review to make sure we implement the expected logic, and we tried to make the code review as easy as possible.

Funding

This work is partly funded by the research grant ANR-22-CE48-0013.

Until Next Time

You can connect with us on Bluesky, Mastodon, Threads, and LinkedIn or sign up for our mailing list to stay updated on our latest projects. We look forward to hearing from you!