Use dot for visualization of counter examples

[kderme]

As @stevana mentioned

Regarding visualisation: perhaps it's easier to use/read graphviz (dot) instead of ASCII?

Examples:

Jepsen: https://github.com/jepsen-io/knossos/blob/master/README.md#visualization-of-faults
Molly: https://gist.github.com/cstorey/38d2ba04f661a7ed727d76cd47d6b40e#file-lamport-svg

we can use dot for visualizing counter examples.

[kderme]

So I used graphviz and dot and these kind of graphs are generated

Any artistic review is welcome :)

[stevana]

Looks nice!

How do you handle overlapping/concurrent actions? Currently it looks like Write and Increment both start and finish exactly at the same time, this shouldn't happen. Because as we execute parallel commands we write a History containing Invocation (start) and Response (finish) events to a channel, and so one command's Invocation should always happen before the other's.

[kderme]

If I'm not mistaken the channel can only serialise the order in which the threads wrote to the channel. It is possible that this order is different from the execution order. So I only take care of the order within the same pid and I think this is the only we can be sure about, by looking the history alone.

[kderme]

What I mean is that Write from Pid 1 may have finished before Increment from Pid 2, but Pid 2 may have written to the channel before Pid 1.

[stevana]

It is possible that this order is different from the execution order.

Yeah, that's possible.

Can you think of a way to improve this situation? Because linearisability relies there being an order of invocation and response events (and of course that they match the actual execution). And it is this order together with the overlaps that we want to visualise, I think.

[kderme]

Indeed, I've been thinking about this question for some time: is it possible to retrieve the real execution order? I think the answer in general is we can't. Say for example we have two parallel writes (I meant increments) : We can't find the order they happen by the result, we can only check that they can be linearized.

I think all possibilities form a tree, which is a subtree of the whole tree that linearization creates. Maybe we could visualise something like that.

[stevana]

We can't find the order they happen by the result

Why do you want to find the order by (from?) the result?

We know when semantics of a command was invoked and when it give us back a response. That's all we care about from a black box perspective? I'm not sure if using timestamps would be any better than using a channel. I've wondered if one could use Lamport clocks somehow, I guess it would be more important if we actually use different computers for executing the different parallel commands (rather than just different threads).

[kderme]

We know when semantics of a command was invoked and when it give us back a response. That's all we care about from a black box perspective?

That's not enough though to find the order, since these times give us only a interval in which an action was commited. These intervals give a partial order for all actions - we can compare only some of them, but not all of them.

The result can give us additional information about the order. By result I mean for example the result of a Read. However even with the resuts we can't be sure about the total order of every action. The more results we have the more we can narrow down to the real order.

[stevana]

That's not enough though to find the order, since these times give us only a interval in which an action was commited.

My understanding of the linearisability paper is that the intervals are enough information. We don't know the exact order, and that doesn't matter. The main result says: if we can find points on the intervals for each action, where if the actions were performed atomically at those points, and we can show that this sequential execution (if we pick points on the intervals there will be no overlapping/concurrent actions) is correct (with regard to post-conditions) then the original concurrent execution is correct.

(Here's a drawing I made that tries to show what I mean by picking points on the interval.)

[kderme]

We don't know the exact order, and that doesn't matter.

We seem to agree that the exact order is unknown.

My understanding of the linearisability paper is that the intervals are enough information.

You mean enough information about what?

[stevana]

We seem to agree that the exact order is unknown.

Yeah, good. :-)

You mean enough information about what?

About the execution, to find out if it is correct or to visualise a counterexample it if its not.

I guess maybe the misunderstand is in that I thought that you meant that the order we write to the channel might not be the same order as semantics for a command is invoked and responds? I.e. the intervals from the channel doesn't reflect the real execution intervals.

[stevana]

I can see what you mean about being able to visualise a possibly better counterexample if you inspect the results (and hence possibly learn a bit more about the order). Not sure if this is worth the effort though? Usually it's quite clear what the problem is once you see the overlapping/concurrent actions.

[kderme]

The dot graph can be indeed improved in the following way: If a Response of a command, is before the Invocation of another and the commands are executed from different pids, then the first command should be as a whole higher than the second command and they should not appear to overlap. I found some examples where this does not work as expected.