Add support for running tests in separate processes with a timeout #259

nikolaushuber · 2024-09-26T09:49:29Z

This fixes #254

When a test causes a segmentation fault this results in the overall test suite process to crash. With this PR, the runtime looks for the presence of an environment variable, in which case it runs all tests in separate processes with a timeout. This allows to get traces both from crashing and non-terminating tests.

This also adapts the dune plugin to accept a new command-line flag with which the timeout can be set.

This is a bit of a WIP, since I could not find a good way of testing this feature. As far as I know the CI expects all tests to run without error, so I don't know how to make it accept an expected error.

nikolaushuber · 2024-10-02T09:27:49Z

Rebased

n-osborne

Thank you! This looks very good!

I just have two small questions:

dd2f255 what happen when ORTAC_QCHECK_STM_TIMEOUT is set to a negative value?
c916ec7 maybe we don't need to be that specific on the cause of the crashes?

nikolaushuber · 2024-10-02T13:45:18Z

dd2f255 what happen when ORTAC_QCHECK_STM_TIMEOUT is set to a negative value?

That is indeed an interesting question. I just looked, under the hood it uses Unix.alarm, and the manpage for alarm does not state anything about what happens when you give it a negative value as argument ... If you try it, at least on my system it immediately returns with a non-zero return value.

Should we adapt the code to in case of negative values also just use the default 10 seconds?

c916ec7 maybe we don't need to be that specific on the cause of the crashes?

I can remove the first part about how segmentation faults can happen! I just thought it might be interesting for some people, especially since OCaml (if used without tricks 😅) promises to be a memory-safe language.

n-osborne · 2024-10-02T14:18:35Z

Should we adapt the code to in case of negative values also just use the default 10 seconds?

As a user, I think I would prefer it to fail rather than choosing a default value for me.

I can remove the first part about how segmentation faults can happen! I just thought it might be interesting for some people, especially since OCaml (if used without tricks 😅) promises to be a memory-safe language.

I had in mind the fact that the fork_prop_with_timeout was first added for crashing tests due to bugs in the OCaml runtime. Though I believe it was when tests with Domains, which we don't (yet) do.

I believe an OCaml program could crash when interfaced with bad C code?

Maybe you can keep the Obj.magic related information as a side note, as example of crashing programs. I also like the idea of poping your third paragraph on top of the section, as it is a really good explanation of the problem the feature solves.

nikolaushuber · 2024-10-02T16:13:56Z

As a user, I think I would prefer it to fail rather than choosing a default value for me.

I made it so that anything that cannot be converted to a positive integer raises a failure now!

Maybe you can keep the Obj.magic related information as a side note, as example of crashing programs. I also like the idea of poping your third paragraph on top of the section, as it is a really good explanation of the problem the feature solves.

I adapted it accordingly 😃

jmid · 2024-10-02T16:17:34Z

plugins/qcheck-stm/doc/index.mld

+   ORTAC_QCHECK_STM_TIMEOUT
+   10
+    (run %{test} --verbose)))
+]}


One can also set environment variables on the command line and have them be visible in dune:

$ ORTAC_QCHECK_STM_TIMEOUT=10 dune test ...

I think that offers a reasonable workflow when one hits an unexpected segfault - just rerun the last command in the console with a small addition 🙂

Indeed! Maybe we should distinguish between the CLI workflow and the CI workflow?

When I updated the documentation I was actually considering if I should mention other ways of setting environment variables, or if the standard user would already know about those. But I will add some additional comments about that!

n-osborne · 2024-10-03T13:52:34Z

Thanks!

Regarding how to fail when the timeout is not a positive integer (fcead56), maybe we can do something cleaner than failwith.
I was thinking something along the way of printf followed by an exit with some error code (1 being the catch-all could be enough)

When a test causes a segmentation fault, ortac/qcheck-stm can not report the (simplified) trace which lead to that fault. This is due to the fact, that the test runs in the same process as the ortac runtime. In order to get more output, the runtime is adapted to allow forking tests in a separate process. This also solves problems regarding non-terminating programs.

This adds a new command-line flag to specify an option timeout for each test.

The generated file from the qcheck-stm plugin ends with `_stm_tests.ml`

n-osborne · 2024-10-04T07:37:58Z

Excellent. Thanks! Merging.

This release brings a number of new features and improvements: - New features: + [ocaml#247](ocaml-gospel/ortac#247): Generated tests cover now functions with multiple SUT arguments + [ocaml#253](ocaml-gospel/ortac#253): Generated tests cover now functions returning SUT values + [ocaml#259](ocaml-gospel/ortac#259): Generated tests can be run in a separated process with a timeout - Improvements: + [ocaml#245](ocaml-gospel/ortac#245): Fix the analysis of function signature to explicitly not support SUTs inside another type + [ocaml#251](ocaml-gospel/ortac#251): Fix the display of the runnable scenario for value returned by a function that could have raised an exception

nikolaushuber force-pushed the fork-prop-env branch from 77e5ed8 to 2fe0312 Compare October 2, 2024 09:26

n-osborne approved these changes Oct 2, 2024

View reviewed changes

nikolaushuber force-pushed the fork-prop-env branch from 2fe0312 to d20263b Compare October 2, 2024 16:11

jmid reviewed Oct 2, 2024

View reviewed changes

nikolaushuber force-pushed the fork-prop-env branch from d20263b to 311390a Compare October 2, 2024 17:33

nikolaushuber added 7 commits October 3, 2024 18:29

Update documentation

4df2266

Update dune plugin

b2d7f3e

This adds a new command-line flag to specify an option timeout for each test.

Add test for --timeout flag

c7f9aae

Update dune plugin documentation

33dcb21

Fix dune plugin documentation

6aa0d3a

The generated file from the qcheck-stm plugin ends with `_stm_tests.ml`

Update changelog

7dffa7b

nikolaushuber force-pushed the fork-prop-env branch from 311390a to 7dffa7b Compare October 3, 2024 16:30

n-osborne merged commit aa86804 into ocaml-gospel:main Oct 4, 2024
3 checks passed

n-osborne mentioned this pull request Oct 8, 2024

Prepare release of version 0.4.0 #263

Merged

n-osborne mentioned this pull request Oct 8, 2024

[new release] Five Ortac packages 0.4.0 ocaml/opam-repository#26691

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for running tests in separate processes with a timeout #259

Add support for running tests in separate processes with a timeout #259

nikolaushuber commented Sep 26, 2024

nikolaushuber commented Oct 2, 2024

n-osborne left a comment

nikolaushuber commented Oct 2, 2024

n-osborne commented Oct 2, 2024

nikolaushuber commented Oct 2, 2024

jmid Oct 2, 2024

n-osborne Oct 2, 2024

nikolaushuber Oct 2, 2024

n-osborne commented Oct 3, 2024 •

edited

Loading

n-osborne commented Oct 4, 2024

Add support for running tests in separate processes with a timeout #259

Add support for running tests in separate processes with a timeout #259

Conversation

nikolaushuber commented Sep 26, 2024

nikolaushuber commented Oct 2, 2024

n-osborne left a comment

Choose a reason for hiding this comment

nikolaushuber commented Oct 2, 2024

n-osborne commented Oct 2, 2024

nikolaushuber commented Oct 2, 2024

jmid Oct 2, 2024

Choose a reason for hiding this comment

n-osborne Oct 2, 2024

Choose a reason for hiding this comment

nikolaushuber Oct 2, 2024

Choose a reason for hiding this comment

n-osborne commented Oct 3, 2024 • edited Loading

n-osborne commented Oct 4, 2024

n-osborne commented Oct 3, 2024 •

edited

Loading