[
https://issues.apache.org/jira/browse/CASSANDRA-18682?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17760152#comment-17760152
]
Henrik Ingo commented on CASSANDRA-18682:
-----------------------------------------
Ok so after "sleeping on it" quite a few nights, and doing other tasks in
between, I returned to this project with some success. I removed all PlusCal
code and just did everything in TLA syntax. This greatly improves both
robustness and clarity.
What I pushed yesterday
(https://github.com/henrikingo/cassandra-accord/commit/25c43b98ed15d5762aeeab8aa1539fa0f00b9458)
is based on modeling Accord such that each "operator" (I mean function) is a
coordinator or "writer" node in a Cassandra cluster, and these steps are
connected (or separated) by message queues. This is intuitive way to think
about Accord, and luckily it seems to work. If you try to run it, just note
that TLC is less concerned about the implementation completing an end to end
trip for a given transaction, and more focused on running it through every
possible permutation of input variables.
I have also been working on an approach where the algorithm from the white
paper is pretty much 1:1 mapped into TLA+ syntax. I believe this is how TLA+ is
designed to be used. And certainly it would give more confidence in the results
of this project if the TLA+ implementation is such that it is crystal clear
that the TLA+ code definitely does the same thing as the algorithm in the paper.
In the latter approach it wasn't at first obvious how the parts that are
executed by different nodes/shards... can be modeled. But now that I've seen
more, it might be possible.
Even so, going to focus on the message queue approach first.
> Create TLA+ spec of Accord
> --------------------------
>
> Key: CASSANDRA-18682
> URL: https://issues.apache.org/jira/browse/CASSANDRA-18682
> Project: Cassandra
> Issue Type: Task
> Components: Accord
> Reporter: Henrik Ingo
> Assignee: Henrik Ingo
> Priority: Normal
> Fix For: 5.x
>
>
> Create a TLA+ Spec of Accord.
>
> For this ticket, goal is just to cover Algorithm 1. No significant
> discoveries are expected, and to really check correctness, one will have to
> implement all 4 algorithms.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]
