Analysis
Represents different types of analysis sections within the Lincheck framework. These sections provide various analysis guarantees and characteristics.
The sections are ordered by the strength of the provided guarantees, from weakest to strongest: NORMAL, SILENT, SILENT_PROPAGATING, ATOMIC, IGNORED. Guarantees of each particular section are documented separately.
Section types can be split into two categories: local and propagating (see isCallStackPropagating).
Local section is only applied to the current method in the call stack. Other methods down the call stack can reside in different analysis section types, including weaker section types. Thus, it is possible to have an alternating sequence of different section types in the call stack.
Propagating sections propagate down the call stack. Other methods down the call stack can only reside in the same analysis section, or a stronger one.
Local sections are required to support methods like ConcurrentHashMap.computeIfAbsent(key, lambda). The method computeIfAbsent itself can be trusted and not analyzed by the framework in the user code by default. However, the user-provided lambda is not trusted and needs to be analyzed.
Thus, computeIfAbsent can be put into a (local, non-propagating) silent section. As such, code inside computeIfAbsent will be muted, but if this method calls the provided lambda, it still will be analyzed fully.
Local sections: NORMAL, SILENT. Propagating sections: SILENT_PROPAGATING, ATOMIC, IGNORED.
Entries
Normal section without special handling. Inside normal sections, all events are tracked. All the events occurring inside a normal section are added to the trace, unless other factors prevent it. Thread switch points can occur arbitrarily within a normal section.
Silent sections are used to mute analysis. Note that events are still tracked inside silent sections, but they are not added to the trace by default. Thread switch points can occur inside a silent section only if they are forced. For instance, because of some blocking synchronization primitive, like an attempt to acquire a monitor that is already held by another thread.
Same as the silent section, but propagates down the call stack.
Code inside an atomic section behaves like an atomic indivisible operation. Technically, the atomic section is a stronger version of the nested silent section, with an additional guarantee that thread switch points cannot occur inside an atomic section at all. TODO: "no-switch-points inside atomic section" guarantee is not checked currently.
Properties
Functions
Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
Returns an array containing the constants of this enum type, in the order they're declared.