[
https://issues.apache.org/jira/browse/CASSANDRA-18682?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=17746648#comment-17746648
]
Henrik Ingo commented on CASSANDRA-18682:
-----------------------------------------
PHP was the 5th or 6th programming language I learned, and also it was the
first time I could pick up a new programming language just by starting to code
and reading the manual as needed. They are all variations of each other, and in
2 weeks you could learn a 7th and 8th language easily...
TLA+ was... hard. I actually tried to watch the official video tutorials from
Leslie Lamport, but the problem is he teaches math and I gave up when the 3rd
video still didn't show any TLA syntax... Hillel's learntla.com was better, and
got me this far, but... It seems like a joke to think that this language is
used to prove correctness and robustness of algorithms. This is the sillyest,
most fragile, booby trapped language I've ever seen. Anyway...
The linked branch contains the beginnings of a TLA implementation as a TLA+
Spec.
Current status is that there's a key range from which a transaction will pick a
set of keys that the transaction operates on. (There is no payload and nothing
is done to the keys other than checking whether a concurrent trx might be
holding the same key.) Similarly each transaction has a t_0 and T timestamps.
A complete transaction
{{ newTrx := <<keySet, t0, T, deps, coordinator>>;}}
is passed to all nodes and back to the coordinator. However...
* Only the fast path, so the beginning of algorithm1 is implemented so far.
* Partitioning is skipped, so all nodes always hold all keys.
* deps are not actually collected, it is always the empty set
* Consequently, there isn't really any checking for conflicting transactions,
because the deps to check aren't there.
In addition:
* I chose to implement this is PlusCal, mostly because learntla/Hillel seems
to recommend it. (And Leslie recommends TLA+, which is a god reason to NOT use
it...)
* Looking at the above now, I'll probably do a second attempt where it's just
raw TLA+. PlusCal seems to make a hard language actually whimsical. For example
it introduces two new ways to assign to a variable: := and =. It depends on the
context which one to use.
* I'm considering using PlusPy as the interpreter and checker. This way I
could easily follow in python what is actually happening. I'm also tempted to
just redefine TLA+ to be less crazy, starting with using = for assignment.
Finally, in PlusPy you have the option to use python for a section instead of
TLA. For example choosing a set of numbers of varying, random size, should not
be a hard problem, but it is in TLA.
As I'm writing this it's unclear to me whether I will continue with this
tomorrow or whether I was asked to context switch to another Accord related
task.
> 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]
