Missing support for static memory snapshot in data structures API

[dmitrii-artuhov]

Static memory snapshot is now restored only between invocations of managed strategy and after verification of the execution scenario, which is sufficient for GPMC mode. But it is not enough for data structures testing. We are missing snapshot restoring during the linearizability checking (inside verification, basically): when we are trying to find the sequence of linearizability points of the data structure operations, we need to restore static snapshot in between those tries. It is required because most of the time, sequential specification is the same class as the data structure under test, and it modifies the same static variables.

while (!canLinearize(...)):
   val linSeq = getNewLinSeq()
   checkLinearizability(linSeq)
   restoreStaticMemory(...) // it also seems that tying static snapshot solely to strategy
                            // does not seem right in case when we want to support it for data structures API

[dmitrii-artuhov]

Note:

• When sequential specification is used we need to utilize another snapshot tracker, which would record and restore static memory. For that an extra instrumentation is required