Thanks Jason and Jack! I count myself as a beginner with TLA+, but would like to take this as an opportunity to learn.
Tom On Thu, 28 Jul 2022 at 17:34, Jason Gustafson <ja...@confluent.io.invalid> wrote: > Yeah, good idea. I'm happy to submit the specs I wrote for normal kafka > replication. It will make them more accessible and I have long been looking > for help reviewing them. Hopefully it will also provide a better chance to > keep them in sync with the codebase as we update protocols. > > -Jason > > On Wed, Jul 27, 2022 at 1:50 AM Jack Vanlightly > <jvanligh...@confluent.io.invalid> wrote: > > > +1 for me too. Once the KIP-853 is agreed I will make any necessary > changes > > and submit a PR to the apache/kafka repo. > > > > Jack > > > > On Tue, Jul 26, 2022 at 10:10 PM Ismael Juma <ism...@juma.me.uk> wrote: > > > > > I'm +1 for inclusion in the main repo and I was going to suggest the > same > > > in the KIP-853 discussion. The original authors of 3 and 4 are part of > > the > > > kafka community, so we can ask them to submit PRs. > > > > > > Ismael > > > > > > On Tue, Jul 26, 2022 at 7:58 AM Tom Bentley <tbent...@redhat.com> > wrote: > > > > > > > Hi, > > > > > > > > I noticed that TLA+ has featured in the Test Plans of a couple of > > recent > > > > KIPs [1,2]. This is a good thing in my opinion. I'm aware that TLA+ > has > > > > been used in the past to prove properties of various parts of the > Kafka > > > > protocol [3,4]. > > > > > > > > The point I wanted to raise is that I think it would be beneficial to > > the > > > > community if these models could be part of the main Kafka repo. That > > way > > > > there are fewer hurdles to their discoverability and it makes it > easier > > > for > > > > people to compare the implementation with the spec. Spreading > > familiarity > > > > with TLA+ within the community is also a potential side-benefit. > > > > > > > > I notice that the specs in [4] are MIT-licensed, but according to the > > > > Apache 3rd party license policy [5] it should be OK to include. > > > > > > > > Thoughts? > > > > > > > > Kind regards, > > > > > > > > Tom > > > > > > > > [1]: > > > > > > > > > > > > > > https://cwiki.apache.org/confluence/display/KAFKA/KIP-848%3A+The+Next+Generation+of+the+Consumer+Rebalance+Protocol#KIP848:TheNextGenerationoftheConsumerRebalanceProtocol-TestPlan > > > > [2]: > > > > > > > > > > > > > > https://cwiki.apache.org/confluence/display/KAFKA/KIP-853%3A+KRaft+Voter+Changes#KIP853:KRaftVoterChanges-TestPlan > > > > [3]: https://github.com/hachikuji/kafka-specification > > > > [4]: > > > > > > > > > > > > > > https://github.com/Vanlightly/raft-tlaplus/tree/main/specifications/pull-raft > > > > [5]: https://www.apache.org/legal/resolved.html > > > > > > > > > >
