3 ms·

I had a quick look through the linked "Testing Telecoms Software with Quviq QuickCheck" paper, but couldn't immediately see anything to answer my question: "why

I had a quick look through the linked "Testing Telecoms Software with Quviq QuickCheck" paper, but couldn't immediately see anything to answer my question: "why is this stateful stuff not better rolled by hand?". The OP gestures at this with the key-value pair model of a key-value store, but why would one not just write a state machine; why does it require a framework? I literally did this last week at work to test a filesystem interaction; it boiled down to: type Instruction = | Read of stuff | Write of stuff | Seek of stuff | … And then the property is "given this list of instructions, blah". The `StateModel` formalism requires doing basically the same work! I really don't see that `StateModel` is pulling its weight: it's adding a bunch more framework code to understand, and the benefit is that it's getting rid of what is in my experience a very small amount of test code.

two_handfuls 2y ago
My understanding is that the parallel QuickCheck will check that in your multithreaded program, all possible interleavings result in a final state that can also be reached by a sequential invocation of the commands. That would be the benefit.
- Smaug123 2y ago
  Is it common to work in a runtime that lets the test harness control the order in which threads race to access mutable state? I wouldn't be surprised if Haskell could do it, but I think I'd have to write a custom interpreter of .NET or JVM bytecode, for example.
  - neonsunset 2y ago
    I believe Java has exactly that, but I couldn't recall the project name. In the case of .NET, there is https://github.com/microsoft/coyote https://github.com/microsoft/coyote which works by rewriting IL to inject hooks that control concurrent execution state. It would have been much more expensive to have a custom interpreter specifically for this task (CoreCLR never interprets IL). This approach somewhat reminds me of precise release-mode debugging and tracing framework for C++ a friend of mine was talking about, which relies on either manually adding the hooks to source files or doing so automatically with a tool.
    - Smaug123 2y ago
      Ah, now you mention it I did try Coyote once; it crashed out instantly on F#, which is why I forgot about it.
      - AlexErrant 2y ago
        I'm just here to commiserate with F# being the red-headed stepchild of dotnet. Everytime people say "dotnet" they really mean "C#".
        neonsunset 2y ago
        Given F# compiler outputs legal IL that is expected to execute in a particular way, and CoreCLR doesn't fail on importing it, and then executing it, it has probably more to do with either Coyote or other tooling that interacts with this setup. That is, if the issue persists. There's one that mentions F# submitted in 2020, but nothing else since: https://github.com/microsoft/coyote/issues/39 https://github.com/microsoft/coyote/issues/39 Edit: Whoops, meant to reference this one: https://stackoverflow.com/questions/61694051/how-to-use-microsoft-coyote-in-f-code-protected-nested-attribute-type-in-pare https://stackoverflow.com/questions/61694051/how-to-use-micr... I don't understand why there is less tolerance for having to make accommodations or take extra steps when working with F# than, let's say, when using Kotlin or Scala. Both follow a similar pattern where they can use pretty much every Java library by virtue of targeting JVM but can't use a huge amount of Java-only tooling that does meta-programming or instrumentation beyond what is provided by JVM bytecode specification, and yet it's not seen as such a huge ordeal from my surface impressions.
        Smaug123 2y ago
        Does that issue mention F#? I may be blind but I see no evidence that it does. In general the F# way is to write completely different stuff, right, either hiding away the underlying C# or completely replacing it. Witness the existence of the SAFE stack, Giraffe to hide the egregious ASP.NET, the totally different approaches with statically resolved type parameters in F# vs enormous hierarchies of interface types in C#, Myriad AST generation vs Roslyn stamping out strings, etc. I have no opinion on the languages hosted on the JVM, but there is a really nontrivial impedence mismatch between idiomatic C# and F#!
drewcoo 2y ago
I would say that stateful stuff is better covered by model-based testing. Feel free to mix test styles - it's your code!
NickM 2y ago
There are some tests where you’re right, but often the tricky part is shrinking failing cases. If you only want to generate sequences of state transitions that are considered “valid” then you typically have to have some sort of model state that dictates which test steps are valid for a given state, and you need to make sure that you don’t remove test steps during shrinking in a way that triggers a spurious failure by violating the preconditions that you followed to generate each step originally. If any operation is valid in any state and you just want a totally random sequence of arbitrary operations, then yeah a stateful proptest framework may be overkill. But if you need to maintain a model state and specify preconditions for different operations, having a dedicated framework saves a lot of work. I wrote a blog post about this stuff last year, if you’re interested in some more in-depth examples: https://readyset.io/blog/stateful-property-testing-in-rust https://readyset.io/blog/stateful-property-testing-in-rust Also, as others have mentioned, parallel state machine testing is another really cool benefit you can get from having a dedicated framework, but it’s not the only benefit.

two_handfuls 2y ago

My understanding is that the parallel QuickCheck will check that in your multithreaded program, all possible interleavings result in a final state that can also be reached by a sequential invocation of the commands. That would be the benefit.

Smaug123 2y ago
Is it common to work in a runtime that lets the test harness control the order in which threads race to access mutable state? I wouldn't be surprised if Haskell could do it, but I think I'd have to write a custom interpreter of .NET or JVM bytecode, for example.
- neonsunset 2y ago
  I believe Java has exactly that, but I couldn't recall the project name. In the case of .NET, there is https://github.com/microsoft/coyote https://github.com/microsoft/coyote which works by rewriting IL to inject hooks that control concurrent execution state. It would have been much more expensive to have a custom interpreter specifically for this task (CoreCLR never interprets IL). This approach somewhat reminds me of precise release-mode debugging and tracing framework for C++ a friend of mine was talking about, which relies on either manually adding the hooks to source files or doing so automatically with a tool.
  - Smaug123 2y ago
    Ah, now you mention it I did try Coyote once; it crashed out instantly on F#, which is why I forgot about it.
    - AlexErrant 2y ago
      I'm just here to commiserate with F# being the red-headed stepchild of dotnet. Everytime people say "dotnet" they really mean "C#".
      - neonsunset 2y ago
        Given F# compiler outputs legal IL that is expected to execute in a particular way, and CoreCLR doesn't fail on importing it, and then executing it, it has probably more to do with either Coyote or other tooling that interacts with this setup. That is, if the issue persists. There's one that mentions F# submitted in 2020, but nothing else since: https://github.com/microsoft/coyote/issues/39 https://github.com/microsoft/coyote/issues/39 Edit: Whoops, meant to reference this one: https://stackoverflow.com/questions/61694051/how-to-use-microsoft-coyote-in-f-code-protected-nested-attribute-type-in-pare https://stackoverflow.com/questions/61694051/how-to-use-micr... I don't understand why there is less tolerance for having to make accommodations or take extra steps when working with F# than, let's say, when using Kotlin or Scala. Both follow a similar pattern where they can use pretty much every Java library by virtue of targeting JVM but can't use a huge amount of Java-only tooling that does meta-programming or instrumentation beyond what is provided by JVM bytecode specification, and yet it's not seen as such a huge ordeal from my surface impressions.
        Smaug123 2y ago
        Does that issue mention F#? I may be blind but I see no evidence that it does. In general the F# way is to write completely different stuff, right, either hiding away the underlying C# or completely replacing it. Witness the existence of the SAFE stack, Giraffe to hide the egregious ASP.NET, the totally different approaches with statically resolved type parameters in F# vs enormous hierarchies of interface types in C#, Myriad AST generation vs Roslyn stamping out strings, etc. I have no opinion on the languages hosted on the JVM, but there is a really nontrivial impedence mismatch between idiomatic C# and F#!

drewcoo 2y ago

I would say that stateful stuff is better covered by model-based testing. Feel free to mix test styles - it's your code!

NickM 2y ago

There are some tests where you’re right, but often the tricky part is shrinking failing cases. If you only want to generate sequences of state transitions that are considered “valid” then you typically have to have some sort of model state that dictates which test steps are valid for a given state, and you need to make sure that you don’t remove test steps during shrinking in a way that triggers a spurious failure by violating the preconditions that you followed to generate each step originally. If any operation is valid in any state and you just want a totally random sequence of arbitrary operations, then yeah a stateful proptest framework may be overkill. But if you need to maintain a model state and specify preconditions for different operations, having a dedicated framework saves a lot of work. I wrote a blog post about this stuff last year, if you’re interested in some more in-depth examples: https://readyset.io/blog/stateful-property-testing-in-rust https://readyset.io/blog/stateful-property-testing-in-rust Also, as others have mentioned, parallel state machine testing is another really cool benefit you can get from having a dedicated framework, but it’s not the only benefit.