[Seq-Test] Spurious sequence testing failure

[dimecon]

Running cn seq-test cn-seq-test-gen/src/bst.pass.c in tests fails sometimes, yielding POST-CONDITION VIOLATION DETECTED.

[dc-mak]

A little bit more context, @echoumcp1 @ZippeyKeys12 sorry if you're already aware (but I've been hit this for like 7th time today so it's getting annoying).

I was looking at https://github.com/rems-project/cn/actions/metrics/performance and I noticed a few things.

1. The failure rate of the Spec Testing job is quite high (57%), much higher than (e.g.) proof (at most 20%).
2. The other is that the average time for the job is creeping up (I think?): the average over the last year is 11m but the average over the last month/3 months is 25-27m. https://github.com/rems-project/cn/actions/workflows/.github/workflows/spec-testing.yml is regularly hitting 40-45m.

I think the time is coming from Bennet, but the flakiness is coming from Seq-Test-Gen bst.pass.c; both are annoying, but the flakiness is probably worse since it blocks PRs. That being said I appreciate we are testing complex things so consider this a plea out of desperation rather than a criticism.

Can we parallelise these tests any more? Would investing in better runners help? Would splitting up the jobs help? Open to suggestions, am not keen on waiting around and kicking the failing jobs repeatedly until they go green and let me merge.

[echoumcp1]

There is possibly a non-post condition violation related issue that's getting misrecognized as one. Do you have the generated test sequence? (edit: the bug seems to be precondition ownership check fails are being registered as postcondition failures)

[echoumcp1]

Correct me if I'm wrong, but I don't see a way to differentiate between a precondition ownership check failure and a postcondition ownership check failure? The exit code seems to be 5 regardless.

[ZippeyKeys12]

1. The failure rate of the Spec Testing job is quite high (57%), much higher than (e.g.) proof (at most 20%).

#498

3. The other is that the average time for the job is creeping up (I think?): the average over the last year is 11m but the average over the last month/3 months is 25-27m. https://github.com/rems-project/cn/actions/workflows/.github/workflows/spec-testing.yml is regularly hitting 40-45m.>

It's about proportional to the development of testing. The issue is that smarter testing techniques are slower, so you still want the lighter option to work. Then you have both in CI.

I think the time is coming from Bennet, but the flakiness is coming from Seq-Test-Gen bst.pass.c; both are annoying, but the flakiness is probably worse since it blocks PRs. That being said I appreciate we are testing complex things so consider this a plea out of desperation rather than a criticism.

There's also some flakiness from Bennet too, it's not that common, but since I run CI a lot, I see it sometimes.

Can we parallelise these tests any more? Would investing in better runners help? Would splitting up the jobs help? Open to suggestions, am not keen on waiting around and kicking the failing jobs repeatedly until they go green and let me merge.

A little bit, which I've already done on another branch, was just busy with the OOPSLA deadline

[ZippeyKeys12]

Correct me if I'm wrong, but I don't see a way to differentiate between a precondition ownership check failure and a postcondition ownership check failure? The exit code seems to be 5 regardless.

Should use set_cn_failure_cb, in the generated C file, to set your own desired behavior. Otherwise the default behavior could be changed:

cn/runtime/libcn/src/cn-executable/utils.c

Line 72 in 408c032

spec_mode; // Might need to differentiate between failure modes via this exit code in the future