Klever

1. Do not use any rule specification intended for checking using the Linux kernel API when you are checking environment model specification and generation since they may have errors, may be changed at any time or even withdrawn. Either define your own model state if required at all and use ldv_assert() directly or introduce some test harness intended specially for this sort of tests. The latter can be actually done by introducing a special "rule specification".
2. Fix the coding style to correspond to the Linux kernel one, e.g. remove C++ comments, replace "if(cond){" with "if (cond) {" and so on.
3. Remove unused headers. Tests are very small and likely don't require the most of included headers.
4. If I understand properly, some tests are based on the real Linux kernel modules. In accordance with the license, you have to point this out. This can be very hard. So I recommend to develop your own "modules" for testing. Nevertheless you likely can leave original header files as is. Although it also will be better to drop them off.
5. Use the common way to introduce nondeterminism, e.g. use ldv_undef_int() rather than undefined ldv_function().
6. Reduce the job size by placing arrays and dictionaries with one element at one line like in the rule specification testing job.
7. Although it can be very hard, but it would be better to rearrange test cases and corresponding module names. For instance, it would be great to have a group of tests (e.g. init_and_exit) for module without initialization and exit functions (e.g. no_init_and_no_exit.ko), with the only initialization function (e.g. init_and_no_exit.ko), with the only exit function (e.g. no_init_and_exit.ko), with both initialization and exit functions (e.g. init_and_exit.ko). All test cases defining an initialization function can have two variants where one returns a proper value and another returns improper value - this can help to understand that EMG properly process these cases as well. The same can be done for all generic requirements. Other test cases can be intended for special interfaces (specifications) or reproduce very non-trivial cases, e.g. very hard syntax constructions, very large number of callbacks, etc.

Besides this issue is irrelevant since it doesn't reflect any bounds. #6764 is much better. I will reject it as other similar issues when you will complete #6764.

Generally I agree with you, but:
1) Tests have been developed for 32_7a rule of ldv-tools and almost all have specific logic to check correctness of callback sequences, so it will need huge refactoring to do that, not just replace locks by asserts. But anyway it is a work worth doing.
2) Agree I will try to do it with an automatic formatter.
3) Will not do that until the issue #7239 will be solved, since it will require many test runs and will take a lot of time too.
4) Hm, I have thrown out several, but I will do it for all of them.
5) Completely agree.
6) I generated the list of sub-jobs automatically (and names too, since they all were like 'ldv_test.c') but the list is sorted by names of interface categories. I am not sure how I can rearrange them differently, since a sub-job with several modules should have a single verdict for all of them, but tests on a common interface category can have different verdicts. Also my tests check callback order (have order in names) or check a specific function model or a couple of models and I avoided to put names of functions as test names to keep them short. I think this is better to do with the rest refactoring.

The test suit in its current state definitely can help me now in a development of new specifications but I agree that it has many problems. Rewriting 150 tests for 33 interface categories to meet all requirements will take a considerable amount of time, so does it make sense to do it before merge to Master and postpone the other issues?

Evgeny Novikov wrote:

Besides this issue is irrelevant since it doesn't reflect any bounds. #6764 is much better. I will reject it as other similar issues when you will complete #6764.

Better is just to change the title, since porting specifications is a completely different activity.

Ilja Zakharov wrote:

Generally I agree with you, but:
1) Tests have been developed for 32_7a rule of ldv-tools and almost all have specific logic to check correctness of callback sequences, so it will need huge refactoring to do that, not just replace locks by asserts. But anyway it is a work worth doing.

I suggest to develop a special test harness that should be independent on any rule specification and likely be very simple. You can just get the current rule specification for checking mutex locking but it isn't very good since it is quite hard. I guess that simple counters as you already used in some tests are well enough. To make it easily usable by all tests it will be necessary to either make it a new rule specification or include it in all tests, e.g. by using symbolic links.

6) I generated the list of sub-jobs automatically (and names too, since they all were like 'ldv_test.c') but the list is sorted by names of interface categories. I am not sure how I can rearrange them differently, since a sub-job with several modules should have a single verdict for all of them, but tests on a common interface category can have different verdicts. Also my tests check callback order (have order in names) or check a specific function model or a couple of models and I avoided to put names of functions as test names to keep them short. I think this is better to do with the rest refactoring.

You can fix the generated list of sub-jobs manually.
I agree that it is hard to include everything in test names, but sometimes it is possible and will help to understand test scopes without looking inside their code, especially if one have already analysed test results.

The test suit in its current state definitely can help me now in a development of new specifications but I agree that it has many problems. Rewriting 150 tests for 33 interface categories to meet all requirements will take a considerable amount of time, so does it make sense to do it before merge to Master and postpone the other issues?

I think that it is better to do everything well in time. Otherwise you will just spend more time in future. Besides the most of problems can be fixed quite quickly especially if #7239 will be implemented.

Note that #7239 was solved and you can fix tests faster.