Returning SUT values

[nikolaushuber]

This PR adds support for testing functions which return a SUT value

[jmid]

I'm curious as to whether you've been able to try out

opam pin -y qcheck-stm https://github.com/ocaml-multicore/multicoretests.git#stm-cmd-list-dist

from https://github.com/ocaml-multicore/multicoretests/pull/472 and noticed any difference in test execution time before and after? (/usr/bin/time test-command should be fine and a couple of runs would be helpful to - hopefully - notice a general improvement trend)

Edited: I just corrected the opam pin command to include .git before the branch name...

[nikolaushuber]

So as a quick trial I ran

hyperfine -w 2 -r 10 'dune build @launchtests -f'

with the current qcheck-stm and with the new (pinned) version. The average time for one run went down from 13s to 340ms :)

[jmid]

qcheck-stm has now been released in version 0.4: https://github.com/ocaml-multicore/multicoretests/releases/tag/0.4 By requiring this as a lower bound, it should now be possible to reintroduce the array test again :smiley: :+1:

[n-osborne]

Maybe we can also try to remove commit abe4aee that was introduced to fix the same problem?

[nikolaushuber]

Yes I was thinking the same thing! I'll try and get to that today :)

[nikolaushuber]

Some quick sanity check: dune rebase -i --exec "dune runtest" main will fail on commits: ...

Now I know how to run these checks on all commits ;) Fixed!

The function does_return_sut is implemented twice

I realised that as well, but then apparently forgot to fix it. It's fixed now!

Also, this last function is used in conditional tests, followed by a careful match on the list of returned values. The positive answer to the conditional test guarantees that we can safely simple use List.hd. The places are:

• [ ... ] Ir_of_gospel.ret_next_state

Here I would argue that we need to pattern match either way, since we need to get the field of the Lnone variant.

• [ ... ] Stm_of_ir.postcond_case.rhs.invariants.suts

Fixed!

• [ ... ] Stm_of_ir.pp_ortac_cmd_case.lhs1.pat_ret

Fixed!

[ ... ] I'm not sure Stm_of_it.next_state_case.unmodified_map is the right name, IIUC those are the (sut, var)s where sut is also in modified_suts?

Very true, that was a bit of a poor naming. I renamed it to modified_sut_map which is closer to what it is!

In [ ... ] (Ir_of_gospel.val_desc), does ret_state needs to be appended at the end of the next_state association list? If not, ret_state could be an option and its optional content could be consed to next_state, sparing a list traversal.

It does in fact not depend on it! I adapted it to use an optional return value now :)

Same commit, Stm_of_ir line 1427, unnecessary newline.

I'm not sure I know which newline you are referring to?

In [ ... ], regarding the error message (Reserr.Missing_fields_in_ret_sut), it makes sense to have a different error message than for modified suts (Reserr.Ensures_not_found_for_next_state), but I suggest to adopt a closer phrasing. Also, it would be better to indicate that this is about the returned value in the error message.

I renamed the error and added the SUT value in the error message!

In [ ... ] Stm_of_ir.pp_ortac_cmd_case, are unsupported ret_tys not already filtered out? (This is more a note for a future PR as I'm really not sure they are but I think they should).

I think you are correct. I changed to an assert false and all tests are still running. I left a comment, just in case.

[ ... ] if we want to make init_sut optional in the configuration, we may well want to keep the Empty_cmd_type error. As it is removed in its own commit, it could easily be revert later too.

I was actually thinking about this case as well. But I believe we would need a different error in that case either way, cause if there is not a single init/create like function with a spec then that is a problem even if the other functions have valid specs. At least that was my line of reasoning.

[n-osborne]

Thanks!

I'm not sure I know which newline you are referring to?

The line in 1525 in the current final commit (maybe easier to find that way)

In [ ... ], regarding the error message (Reserr.Missing_fields_in_ret_sut), it makes sense to have a different error message than for modified suts (Reserr.Ensures_not_found_for_next_state), but I suggest to adopt a closer phrasing. Also, it would be better to indicate that this is about the returned value in the error message. I renamed the error and added the SUT value in the error message!

Could I suggest to reuse the part of the message from Ensures_not_found_for_next_state where the expected form of the Gospel clause is explained? This would bring even more consistency in the error message, and this is a way of writing post-conditions that is really specific to Ortac/QCheck-STM.

I think you are correct. I changed to an assert false and all tests are still running. I left a comment, just in case.

Just thinking about it now: Gospel will fail on these types anyway (so they are indeed already filtered out).

[nikolaushuber]

Could I suggest to reuse the part of the message from Ensures_not_found_for_next_state where the expected form of the Gospel clause is explained? This would bring even more consistency in the error message, and this is a way of writing post-conditions that is really specific to Ortac/QCheck-STM.

That's a good idea. I have adapted it so that they are similar now!

I don't now exactly how that happened, but apparently I fused the commits about returning SUTs and about skipping underspecified SUT returning functions ...

Is that ok, or should I try to separate them again? They are kind of a package deal either way ...

[n-osborne]

If it is not too much work and headache, it would be ideal. But I've already reviewed their content (I was then happy that they were separated :smile: ) and, as you say, their content is related. So I would say the "too much" is rather low.

And the message is very nice now, thanks!

[nikolaushuber]

It should be back now :)

[n-osborne]

Thanks! I'll wait for the CI to finish and I'll merge.