How can an extended linearizable history G be equivalent to sequential history S?

Question

I am undertaking a module in Concurrent Programming where some of the new content this year covers linearizability, the Java Memory Model, and sequential consistency. Our class slides are companion slides to The Art Of Multiprocessor Programming.

I have been doing OK with linearizability but have become confused at this point below:

I understand that removing pending invocations gives a complete subhistory, however I cannot understand from this example how a subset G can be equivalent to set S which is larger than it - how is G obtained from S here?

As far as I am aware there is not enough information to determine if there are pending invocations from the diagram on the right and I am not sure why a --> b is removed in the subset that is G - at first I thought it's because they are overlapping but A and B both have linearization points for viewing them 'as sequential objects'.

I may be over looking something simple and have just misunderstood the slides.

Answer 1

The idea of linearizability is that the parallel events behave as if each of them happened at a single point in time, during the duration of the actual execution of the event. Given a sequence of events, if the end point of event $A$ precedes the starting point of event $B$ then in any linearization, the time point of $A$ must precede the time point of $B$. These are the constraints $\rightarrow_G$, which we can think of as a partial order. The events are linearizable if the constraints are extendable to a linear order $\rightarrow_S$ such that the semantics match — the outcome of the events is the same as if they were applied in the order underlying $\rightarrow_S$. Perhaps this is what was meant by equivalence, though as you mention, it is clearly applied to the wrong objects. What is equivalent here is the actual turn of events and the turn of events given the order $\rightarrow_S$.

Answer 2

I'm a bit late with this question, but this would be my thoughts on the slides -

There are a lot of words within the first slide which have a different meaning in this context in comparison to other scenarios.

For instance the definitions of words are :

• Legal - A history $H$ is legal, if for each object $x$ the projection $H|x$ meets the sequential specification

• Sequential History - A sequential history $H$ follows the format of an initial request, such as $A\ q:end(3)$, followed by zero or more responses and invocations - a trailing innovation is valid in this scenario.

  Note, invocations and responses of different threads may not be interleaved for a sequential history - for instance the below history is not valid, as the Thread's invocations and responses are interleaved.

  $ A\ q.enq(3) \\ B\ q.enq(4) \\ A\ q:void \\ B\ q:void $

• Equivalent - Two histories $H$ and $G$ are equivalent if their per thread projections are equal.

With this in mind

A history $H$ is linerizable if, it can be extended to $G$ by
    - Appending zero or more responses to pending invocations
    - Discarding other pending invocations

And with our definitions in mind, we can say - loosely speaking

There must exist a legal, perhaps arbitrary, sequential history S,
which follows the defined ordering within our complete history G

For instance in your slide, the following orderings (or precedences) are defined

$ \rightarrow_{G} = \{a \rightarrow c, b\rightarrow c \} $

Note that, as the ordering between $a$ and $b$ is undefined, we must check both interleavings.

Therefore given these orderings, it means to prove a history to be linearizable, we simply need to find any legal, sequential history S, which is equivalent to G and contains our defined ordering relations.

One such legal sequential to test against may be the following, ie $a \rightarrow b$

$ \rightarrow_{S} = \{a \rightarrow b, a\rightarrow c, b \rightarrow c \} $

And another possible legal sequential history may be the following, ie $b \rightarrow a$

$ \rightarrow_{S} = \{b \rightarrow a, b\rightarrow c, a \rightarrow c \} $

So, in general it should be 'easy' to prove that a History linearizable if their method innovations do not overlap. However in this scenario both $a$ and $b$ do, so we must test out both possibilities. If either yield to be true, then our history is linearizable.

Answer 3

I think the confusion comes from mixing up relations and histories.

G and S are histories. G equivalent to S means that the events happen on each process in the same order in G as in S. (Note though the ordering of events on different processes may differ between equivalent histories.)

-->G is the relation of events in G, and similarly -->S is the relation in S. -->G is a partial ordering, whereas -->S is a total ordering, since S is sequential. -->S is an extension of -->G by adding ordering between parallel events in G.

Hope it helps.