Skip to content
This repository has been archived by the owner on Jun 18, 2021. It is now read-only.

Use dot for visualization of counter examples #316

Open
kderme opened this issue Jun 11, 2019 · 13 comments
Open

Use dot for visualization of counter examples #316

kderme opened this issue Jun 11, 2019 · 13 comments

Comments

@kderme
Copy link
Collaborator

kderme commented Jun 11, 2019

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 kderme mentioned this issue Jun 11, 2019
8 tasks
@kderme
Copy link
Collaborator Author

kderme commented Jun 20, 2019

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

graph

Any artistic review is welcome :)

@stevana
Copy link
Collaborator

stevana commented Jun 20, 2019

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
Copy link
Collaborator Author

kderme commented Jun 20, 2019

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
Copy link
Collaborator Author

kderme commented Jun 20, 2019

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
Copy link
Collaborator

stevana commented Jun 20, 2019

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
Copy link
Collaborator Author

kderme commented Jun 20, 2019

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
Copy link
Collaborator

stevana commented Jun 20, 2019

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
Copy link
Collaborator Author

kderme commented Jun 21, 2019

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
Copy link
Collaborator

stevana commented Jun 21, 2019

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
Copy link
Collaborator Author

kderme commented Jun 21, 2019

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
Copy link
Collaborator

stevana commented Jun 21, 2019

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
Copy link
Collaborator

stevana commented Jun 21, 2019

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
Copy link
Collaborator Author

kderme commented Jul 26, 2019

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.

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants