search

utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software
https://utwente.nl/vercors
Mozilla Public License 2.0
56 stars 26 forks source link

Test MatrixTransposeWithF is unstable #1246

Open bobismijnnaam opened 1 month ago

bobismijnnaam commented 1 month ago

Test MatrixTransposeWithF in suite SYCLFullProgramsSpec is unstable. It is disabeld for now until a solution is found.

OmerSakar commented 1 month ago

To give my two cents:

The problem seems to be that the example times out due to the parsing taking too long. The C++ grammar from ANTLR is inefficient with the way we are parsing things in VerCors.

I guess the problem would be fixed if we rewrite the C++ grammar to have a similar style to the grammar of the other languages.

superaxander commented 1 month ago

I think the parsing is not the problem for the CI because what times out is some assert which it then concludes can't be proven (probably because the CI is slower than your local machine) On my branches with changes to the C++ struct encoding things are a bit slower and that causes this example to always fail, even locally. So I think it might just be an example that is on the edge of failing locally and then fails on a slower machine more often. Maybe adding the extra set of curly braces such that the buffer is definitely accessible can help in some cases but I don't have a consistent solution that will always work.