Klever

It turned out that it is extremely difficult to find data races when having many threads even using a rather lightweight approach. Indeed there is an exponential growth of a CPU time depending on a number of threads (indeed #8581 matters). So, the verification tool does not produce anything good for rather large programs.

That's why Pavel suggested to create a single thread at the top of environment model, say, when modules are initialized/exited, and do not generate any threads below.