US 2018/0121488 A1 · AUTOMATIC LINEARIZABILITY CHECKING

Abstract

A method may include executing operation types on a concurrent data structure to obtain executed operations. Each executed operation may cause a transition from a preceding state to a subsequent state. The method may further include recording each executed operation to obtain recorded operations, and assembling a concurrent history from the recorded operations. The concurrent history may include a subset of the recorded operations, and the concurrent history may impose overlapping and non-overlapping relationships on the subset of recorded operations. The method may further include checking whether the concurrent history has an equivalent linearization including a total sequential ordering of the subset of recorded operations, and reporting an error when the concurrent history has no equivalent linearization.

Claims20

Dependent claims

A method, comprising:

executing a plurality of operation types on a concurrent data structure to obtain a plurality of executed operations, wherein each executed operation of the plurality of executed operations causes a transition from a preceding state to a subsequent state;
recording each executed operation of the plurality of executed operations to obtain a plurality of recorded operations;
assembling a concurrent history from the plurality of recorded operations, wherein:
the concurrent history comprises a subset of the plurality of recorded operations, and
the concurrent history imposes overlapping and non-overlapping relationships on the subset of the plurality of recorded operations;
checking whether the concurrent history has an equivalent linearization comprising a total sequential ordering of the subset of the plurality of recorded operations;
and
reporting an error when the concurrent history has no equivalent linearization.

5 more elements

A system, comprising:

a processor;
a memory coupled to the processor;
a repository, configured to store at least a concurrent data structure and a plurality of operation types;
and
a linearizability analyzer, executing on the processor and using the memory, comprising:
an operation executor/recorder configured to:
execute the plurality of operation types on the concurrent data structure to obtain a plurality of executed operations, wherein each executed operation of the plurality of executed operations causes a transition from a preceding state to a subsequent state;
and
record each executed operation of the plurality of executed operations to obtain a plurality of recorded operations;
a concurrent history assembler configured to:
assemble a concurrent history from the plurality of recorded operations, wherein:
the concurrent history comprises a subset of the plurality of recorded operations, and
the concurrent history imposes overlapping and non-overlapping relationships on the subset of the plurality of recorded operations;
and
a linearization checker configured to:
check whether the concurrent history has an equivalent linearization comprising a total sequential ordering of the subset of the plurality of recorded operations;
and
report an error when the concurrent history has no equivalent linearization.

15 more elements

A non-transitory computer readable medium comprising instructions that, when executed by a computer processor, perform a method comprising:

executing a plurality of operation types on a concurrent data structure to obtain a plurality of executed operations, wherein each executed operation of the plurality of executed operations causes a transition from a preceding state to a subsequent state;
recording each executed operation of the plurality of executed operations to obtain a plurality of recorded operations;
assembling a concurrent history from the plurality of recorded operations, wherein:
the concurrent history comprises a subset of the plurality of recorded operations, and
the concurrent history imposes overlapping and non-overlapping relationships on the subset of the plurality of recorded operations;
checking whether the concurrent history has an equivalent linearization comprising a total sequential ordering of the subset of the plurality of recorded operations;
and
reporting an error when the concurrent history has no equivalent linearization.

5 more elements

Dependencies are inferred from the claim text.

Automatic linearizability checking

Life of this patent

Automatic linearizability checking

Life of this patent

Abstract

Claims20