JetBrains / lincheck

Framework for testing concurrent data structures
Mozilla Public License 2.0
576 stars 33 forks source link

Unclear exception result #207

Closed zuevmaxim closed 1 year ago

zuevmaxim commented 1 year ago

image Use this project to reproduce https://github.com/ndkoval/concurrent-programming-intensive-berlin

Two issues are here: 1) Minimisation did not drop the second operation. See this check for the cause

2) The cause of the lincheck failure is an invalid first operation, while the exception in the second operation is expected. However, this is unclear to the user. It would be nice to either state that exception is expected or highlight the concrete point that makes execution incorrect (where the linearisation fails)

ndkoval commented 1 year ago

I don't think we can find a good solution. I suggest using ChatGPT to generate an error explanation in IDEA. It may fix the issue.

eupp commented 1 year ago

The first point (1) "Minimisation did not drop the second operation." is actually easy to fix --- we need to patch minimizer so that it will not split single thread scenarios into init/parallel/post parts. As a byproduct of that, the minimizer will be able to further remove some actors from the scenario.

In the example attached to this issue, it would allow the minimizer to remove actor that raises exception.

ndkoval commented 1 year ago

We will allow removing all operations in the parallel part, which will fix the current issue: #215. As we do not have a better way to show exception results, I'm closing this issue.