Do not ask for equals/hashCode on the sequential specification until necessary

[ndkoval]

Usually, the verification phase is super-fast, even with default equals and hashCode implementations. However, it might be critical to provide custom implementations when testing scenarios are large or when the data structure operations are expensive.

Let's not require equals/hashCode to be implemented if the verification phase takes excepted time -- Lincheck should neither throw an exception nor print a warning. However, when the verification process takes an unexpectedly long time, it would be helpful to print a warning with instructions on how to implement equals and hashCode.

[ndkoval]

These messages are really annoying...

To make verification faster, you can specify the state equivalence relation on your sequential specification.
At the current moment, `MultiMapTest` does not specify it, or the equivalence relation implementation is incorrect.
To fix this, please implement `equals()` and `hashCode()` functions on `MultiMapTest`; the simplest way is to extend `VerifierState`
and override the `extractState()` function, which is called at once and the result of which is used for further `equals()` and `hashCode()` invocations.

[ndkoval]

We need to make experiments to decide when equals/hashCode implementations start helping. After that, we can have heuristics that enable asking for equals/hashCode only when it seems necessary.

[ndkoval]

Let's also remove the requireStateEquivalenceImplCheck parameter: I cannot find a single usage.

[avpotapov00]

As experiments have shown, there is no explicit correlation between equals/hashcode presence and verification time and a whole test time. Equals and hashcode can significantly improve or mess up performance only if a scenario is really big. In real tasks it can be if threads count is >= 4. We measured the perfomace with and without equals/hashcode on the tests below:

• BufferedChannel
• ConcurrentHashMap
• ConcurrentLinkedDeque
• Counter
• ConcurrentSkipListMap
• LockFreeTaskQueue (QuiescentConsistency)
• ConcurrentHashMap

The graph below describes whether equals / hashcode improves or worsens verification time. The x-axis value is equal to the difference between the verification time without equals / hashcode and with equals / hashcode in milliseconds for the same experiment. The y-axis is the number of threads.

In most tests, there is not much difference, but on those where the difference is significant, the presence of equals / hashcode often worsens the results. The lack of correlation is explained as follows: although the ability to reuse states in an LTS graph reduces the graph, making its traversal faster, sometimes the comparison methods, if they are present, are not fast enough, so verification takes longer.

According to the current results of the experiments, it was decided to mark VeriferState as @Deprecated and completely remove the warning about the absence of equals / hashcode, since this option can not only improve, but also worsen the running time and also complicates the use of the framework.

[ndkoval]

These results are really surprising, thanks @avpotapov00 for the analysis!

[ndkoval]

@avpotapov00, could you please check whether it is better to use IdentityHashMap in the LTS structure then?

[avpotapov00]

Experiments have shown the following results:

[ndkoval]

It would be better to show the percentage of the time spent in the verification phase.

[avpotapov00]

Here it is.

[avpotapov00]

So I propose to keep current HashMap states holder implementation in LTS structure, to deprecate VerifierState and remove the requireStateEquivalenceImplCheck parameter. Annoying warnings about equals/hashcode will be removed as well.

[eupp]

@avpotapov00 then we can also remove checkStateEquivalenceImplementation from the Verifier interface, and make it SAM interface.

[ndkoval]

fixed in #160