Efficient Linearizability Monitoring

Introduction

Concurrent Systems

Communicate

Using shared ADT

Linearizability

Extends a sequential specification to the concurrent setting. (Herlihy and Wing,TOPLAS1990)

First slide

Def continuation

Def Cont 2

Verification

We are looking at the monitoring problem; Is a given execution (consisting of a sequence of calls and returns) linearizable?

• NP-complete (in the length) for registers (Gibbons and Korach,SIAM J. Comput.1997)

Stacks

We assume the history is differentiated: each value occurs in at most one push and one pop.

Any (stack/queue) history h is linearizable if and only if there is a linearizable differentiated history h’ and some map that renames the values of h’ to the values of h. (Abdulla, Haziza, Holík, Jonsson, and Rezine,TACAS2013)

This enables us to construct polynomial-time algorithms

Tricky Problem!

can change the outcome!

Stacks

We present an algorithm that is quadratic in the length of the history.

• Compute populated and deserted segments
• Apply simplification steps
  • Extreme value removal
  • Partitioning

If we ever cannot progress, conclude unlinearizability.

First slide

Ignore threads

Slide histories/sdhk2-rw.hist.000.svg

Ignore threads

Slide histories/sdhk2-rw.hist.001.svg

Compute segments

Slide histories/sdhk2-rw.hist.002.svg

Compute segments

Slide histories/sdhk2-rw.hist.003.svg

Extreme value removal

Slide histories/sdhk2-rw.hist.004.svg

Extreme value removal

Slide histories/sdhk2-rw.hist.005.svg

Compute segments

Slide histories/sdhk2-rw.hist.006.svg

Compute segments

Slide histories/sdhk2-rw.hist.007.svg

Partitioning

Slide histories/sdhk2-rw.hist.008.svg

Compute segments

Slide histories/sdhk2-rw.hist.009.svg

Compute segments

Slide histories/sdhk2-rw.hist.010.svg

Compute segments

Slide histories/sdhk2-rw.hist.011.svg

Extreme value removal

Slide histories/sdhk2-rw.hist.012.svg

Extreme value removal

Slide histories/sdhk2-rw.hist.013.svg

Compute segments

Slide histories/sdhk2-rw.hist.014.svg

Compute segments

Slide histories/sdhk2-rw.hist.015.svg

Compute segments

Slide histories/sdhk2-rw.hist.016.svg

Extreme value removal

Slide histories/sdhk2-rw.hist.017.svg

Done!

Incomplete histories

Can be completed

Pop Empty

pop-operations that returns \(\bot\), indicating an empty stack

Slide histories/popempty.hist.000.svg

Slide histories/popempty.hist.001.svg

Slide histories/popempty.hist.002.svg

Slide histories/popempty.hist.003.svg

Complexity

First, sort values by push return. O(n log n)

• Compute deserted and populated segments. O(n)
• Finding extreme is O(n)
• Partitioning is O(n)
• Worst case, each step only removes one value, so we need \(n\) steps.
• \(O\left(\sum_{i=1}^{n} n\right) = O(n^2)\)

Queues

We achieve \(O(n~log~n)\).

Small model property; a (differentiated, completed) queue history is linearizable if and only if for no pair of values \(a\), \(b\), we have

\[enq(a) < enq(b) \wedge deq(b) < deq(a)\]

where < is the happens-before relation

Note: does not hold for stacks.

Step 1

\[enq(a) < enq(b) \wedge deq(b) < deq(a)\]

Step 2

\[\textrm{outer seg. of } b \subseteq \textrm{inner seg. of } a\]

Algorithm

We want to see if for any two values, the outer (enq.call, deq.ret) segment of one is contained in the inner (enq.ret, deq.call) segment of the other. We call a pair of such values critical.

• Construct a queue-tree
• Scan it for containment.

Tree

We construct a red-black tree, where each node contains

• A left and right subtree
• Left and right endpoints of the inner interval
• A high key, the highest right occuring in its subtrees

Example History

• Inner segments: (3, 6), (4, 11), (9, 14), (12, 26), (16, 25), (18, 20), (21, 28), (24, 30)
• Outer segments: (1, 8), (2, 13), (5, 17), (7, 29), (10, 27), (15, 23), (19, 31), (22, 32)

Slide queue_tree1.svg

• Outer segments: (1, 8), (2, 13), (5, 17), (7, 29), (10, 27), (15, 23), (19, 31), (22, 32)

Slide queue_tree2.svg

• Outer segments: (1, 8), (2, 13), (5, 17), (7, 29), (10, 27), (15, 23), (19, 31), (22, 32)

Slide queue_tree3.svg

• Outer segments: (1, 8), (2, 13), (5, 17), (7, 29), (10, 27), (15, 23), (19, 31), (22, 32)

Complexity

• Constructing the tree is O(n log n)
• Each search is O(log n)
• We do \(n\) searches.
• O(n log n)

(Multi)Sets

We present an \(O(n)\) algorithm for (multi)sets, with operations add(x) and rmv(x).

• A multiset history is linearizable \(\iff\) each single-value projection is linearizable.
• A single-valued multiset history is linearizable \(\iff\) the number of returned rmv never exceed the number of called add.

We also present a greedy linear-time algorithm for sets with membership queries.

Conclusion

We have shown monitoring algorithms

• \(O(n^2)\) for stacks
• \(O(n~log n)\) for queues
• \(O(n)\) for (multi)sets

Future Work

• Formalization in a theorem prover
• Extend to other data structures (e.g. multisets with count, snapshots)
• Extend to related correctness conditions (e.g. durable linearizability)

Thanks for listening!

References