Class LinearizabilityChecker
java.lang.Object
org.elasticsearch.cluster.coordination.LinearizabilityChecker
Basic implementation of the Wing and Gong Graph Search Algorithm, following the descriptions in
Gavin Lowe: Testing for linearizability
Concurrency and Computation: Practice and Experience 29, 4 (2017). http://dx.doi.org/10.1002/cpe.3928
Alex Horn and Daniel Kroening: Faster linearizability checking via P-compositionality
FORTE (2015). http://dx.doi.org/10.1007/978-3-319-19195-9_4
-
Nested Class Summary
Nested ClassesModifier and TypeClassDescriptionstatic final recordstatic enumstatic classSequence of invocations and responses, recording the run of a concurrent system.static interfaceSequential specification of a datatype that allows for keyed access, providing compositional checking (seeLinearizabilityChecker.SequentialSpec.partition(List)).static final classThis exception is thrown if the check could not be completed due to timeout or OOM (that could be caused by long event history)static interfaceSequential specification of a datatype. -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionstatic booleanConvenience method forisLinearizable(SequentialSpec, History, Function)that requires the history to be completestatic booleanisLinearizable(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator) Checks whether the provided history is linearizable with respect to the given sequential specificationstatic Stringvisualize(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator) Return a visual representation of the historystatic voidwriteVisualisation(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator, Writer writer) Write a visual representation of the history to the given writer
-
Constructor Details
-
LinearizabilityChecker
public LinearizabilityChecker()
-
-
Method Details
-
isLinearizable
public static boolean isLinearizable(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history) throws LinearizabilityChecker.LinearizabilityCheckAborted Convenience method forisLinearizable(SequentialSpec, History, Function)that requires the history to be complete -
isLinearizable
public static boolean isLinearizable(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator) throws LinearizabilityChecker.LinearizabilityCheckAbortedChecks whether the provided history is linearizable with respect to the given sequential specification- Parameters:
spec- the sequential specification of the datatypehistory- the history of events to check for linearizabilitymissingResponseGenerator- used to complete the history with missing responses- Returns:
- true iff the history is linearizable w.r.t. the given spec
- Throws:
LinearizabilityChecker.LinearizabilityCheckAborted
-
visualize
public static String visualize(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator) Return a visual representation of the history -
writeVisualisation
public static void writeVisualisation(LinearizabilityChecker.SequentialSpec spec, LinearizabilityChecker.History history, Function<Object, Object> missingResponseGenerator, Writer writer) Write a visual representation of the history to the given writer
-