You are viewing a plain text version of this content. The canonical link for it is here.
Posted to dev@kafka.apache.org by Tom Bentley <tb...@redhat.com> on 2022/07/26 14:57:35 UTC
[DISCUSS]: Including TLA+ in the repo
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
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Tom Bentley <tb...@redhat.com>.
Hi Divij,
I don't think that really works for a couple of reasons:
1. I'm not sure every KIP author would necessarily know enough to be able
to answer that question; we don't want knowledge of TLA+ to be seen as
necessary for writing KIPs.
2. It's not just KIPs which could make breaking changes. So really this is
something we need to be aware of during PR review, rather than KIP review.
Perhaps a more fruitful line of thought is about how we can correlate bits
of a spec (such as [1]) with parts of the codebase (such as [2]). That
would make it easier for people (reviewer or otherwise) to study how the
one relates to the other. I think that gets us closer to the second point
you made in your first reply to this thread, because if it's obvious in the
code it makes it easier to know what needs to be asserted in tests of that
code. I'm not suggesting how we might enable this navigability
specifically, just that it seems like a worthwhile problem to solve
somehow. Maybe naming conventions or comments are enough, or perhaps there
are more technical/machine-readable solutions (e.g. annotations) which
could add extra benefits/assurances. Obviously this isn't a problem we have
to solve on day 1, either.
Kind regards,
Tom
[1]:
https://github.com/hachikuji/kafka-specification/blob/master/KafkaReplication.tla#L138
[2]:
https://github.com/apache/kafka/blob/b172a0a94f4ebb9fe638b064d825f0720e7d20ab/core/src/main/scala/kafka/controller/KafkaController.scala#L1066
On Wed, 10 Aug 2022 at 17:44, Divij Vaidya <di...@gmail.com> wrote:
> On keeping the proofs up to date:
>
> Shall we add a template questionnaire to the KIP template that would force
> the author to think about potential change in proofs, e.g. “Does the change
> modify the proof of semantics described at XYZ? If yes, how?”
>
> On Tue, Aug 9, 2022 at 11:54 PM Guozhang Wang <wa...@gmail.com> wrote:
>
> > +1 as well. I think adding such proofs in the repo could encourage more
> > people reviewing and challenging it, helping to improve whenever we see
> > fit. Also it helps readers better understand the design patterns.
> >
> > One thing worth noting though is how to make sure the proofs are keep up
> to
> > date with the actual designs, for large refactoring that touches on
> related
> > modules, e.g. the replication protocol etc, I think we should include the
> > proofs as part of the scope.
> >
> >
> > Guozhang
> >
> > On Thu, Jul 28, 2022 at 9:52 AM Matthew Benedict de Detrich
> > <ma...@aiven.io.invalid> wrote:
> >
> > > +1 from me as well, having the formal TLA+ proofs in the main repo is
> > > hugely beneficial not only from understanding the high level protocol
> but
> > > also in terms of awareness/making sure the proof is not outdated.
> > >
> > > --
> > > Matthew de Detrich
> > > Aiven Deutschland GmbH
> > > Immanuelkirchstraße 26, 10405 Berlin
> > > Amtsgericht Charlottenburg, HRB 209739 B
> > >
> > > Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen
> > > m: +491603708037
> > > w: aiven.io e: matthew.dedetrich@aiven.io
> > > On 26. Jul 2022, 16:58 +0200, Tom Bentley <tb...@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
> > >
> >
> >
> > --
> > -- Guozhang
> >
> --
> Divij Vaidya
>
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Divij Vaidya <di...@gmail.com>.
On keeping the proofs up to date:
Shall we add a template questionnaire to the KIP template that would force
the author to think about potential change in proofs, e.g. “Does the change
modify the proof of semantics described at XYZ? If yes, how?”
On Tue, Aug 9, 2022 at 11:54 PM Guozhang Wang <wa...@gmail.com> wrote:
> +1 as well. I think adding such proofs in the repo could encourage more
> people reviewing and challenging it, helping to improve whenever we see
> fit. Also it helps readers better understand the design patterns.
>
> One thing worth noting though is how to make sure the proofs are keep up to
> date with the actual designs, for large refactoring that touches on related
> modules, e.g. the replication protocol etc, I think we should include the
> proofs as part of the scope.
>
>
> Guozhang
>
> On Thu, Jul 28, 2022 at 9:52 AM Matthew Benedict de Detrich
> <ma...@aiven.io.invalid> wrote:
>
> > +1 from me as well, having the formal TLA+ proofs in the main repo is
> > hugely beneficial not only from understanding the high level protocol but
> > also in terms of awareness/making sure the proof is not outdated.
> >
> > --
> > Matthew de Detrich
> > Aiven Deutschland GmbH
> > Immanuelkirchstraße 26, 10405 Berlin
> > Amtsgericht Charlottenburg, HRB 209739 B
> >
> > Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen
> > m: +491603708037
> > w: aiven.io e: matthew.dedetrich@aiven.io
> > On 26. Jul 2022, 16:58 +0200, Tom Bentley <tb...@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
> >
>
>
> --
> -- Guozhang
>
--
Divij Vaidya
Re: [DISCUSS]: Including TLA+ in the repo
Posted by David Jacot <dj...@confluent.io.INVALID>.
That's a great idea. I am +1 as well.
Thanks,
David
On Tue, Aug 9, 2022 at 11:54 PM Guozhang Wang <wa...@gmail.com> wrote:
>
> +1 as well. I think adding such proofs in the repo could encourage more
> people reviewing and challenging it, helping to improve whenever we see
> fit. Also it helps readers better understand the design patterns.
>
> One thing worth noting though is how to make sure the proofs are keep up to
> date with the actual designs, for large refactoring that touches on related
> modules, e.g. the replication protocol etc, I think we should include the
> proofs as part of the scope.
>
>
> Guozhang
>
> On Thu, Jul 28, 2022 at 9:52 AM Matthew Benedict de Detrich
> <ma...@aiven.io.invalid> wrote:
>
> > +1 from me as well, having the formal TLA+ proofs in the main repo is
> > hugely beneficial not only from understanding the high level protocol but
> > also in terms of awareness/making sure the proof is not outdated.
> >
> > --
> > Matthew de Detrich
> > Aiven Deutschland GmbH
> > Immanuelkirchstraße 26, 10405 Berlin
> > Amtsgericht Charlottenburg, HRB 209739 B
> >
> > Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen
> > m: +491603708037
> > w: aiven.io e: matthew.dedetrich@aiven.io
> > On 26. Jul 2022, 16:58 +0200, Tom Bentley <tb...@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
> >
>
>
> --
> -- Guozhang
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Guozhang Wang <wa...@gmail.com>.
+1 as well. I think adding such proofs in the repo could encourage more
people reviewing and challenging it, helping to improve whenever we see
fit. Also it helps readers better understand the design patterns.
One thing worth noting though is how to make sure the proofs are keep up to
date with the actual designs, for large refactoring that touches on related
modules, e.g. the replication protocol etc, I think we should include the
proofs as part of the scope.
Guozhang
On Thu, Jul 28, 2022 at 9:52 AM Matthew Benedict de Detrich
<ma...@aiven.io.invalid> wrote:
> +1 from me as well, having the formal TLA+ proofs in the main repo is
> hugely beneficial not only from understanding the high level protocol but
> also in terms of awareness/making sure the proof is not outdated.
>
> --
> Matthew de Detrich
> Aiven Deutschland GmbH
> Immanuelkirchstraße 26, 10405 Berlin
> Amtsgericht Charlottenburg, HRB 209739 B
>
> Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen
> m: +491603708037
> w: aiven.io e: matthew.dedetrich@aiven.io
> On 26. Jul 2022, 16:58 +0200, Tom Bentley <tb...@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
>
--
-- Guozhang
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Matthew Benedict de Detrich <ma...@aiven.io.INVALID>.
+1 from me as well, having the formal TLA+ proofs in the main repo is hugely beneficial not only from understanding the high level protocol but also in terms of awareness/making sure the proof is not outdated.
--
Matthew de Detrich
Aiven Deutschland GmbH
Immanuelkirchstraße 26, 10405 Berlin
Amtsgericht Charlottenburg, HRB 209739 B
Geschäftsführer: Oskari Saarenmaa & Hannu Valtonen
m: +491603708037
w: aiven.io e: matthew.dedetrich@aiven.io
On 26. Jul 2022, 16:58 +0200, Tom Bentley <tb...@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
Re: [DISCUSS]: Including TLA+ in the repo
Posted by José Armando García Sancio <js...@confluent.io.INVALID>.
Divij Vaidya <di...@gmail.com> wrote:
> 1. As an aside, would we be open to accept other alternative forms of
> proofs such as property based testing (semi-formal methods) in future?
The Apache Kafka repository already has support for property based
testing using jqwik. So feel free to add more property based tests.
See RaftEventSimulationTest and RecordsIteratorTest for examples.
Thanks!
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Divij Vaidya <di...@gmail.com>.
I second the proposal.
1. As an aside, would we be open to accept other alternative forms of
proofs such as property based testing (semi-formal methods) in future?
2. TLA+ serves as a proof of correctness for the specification. The north
star would be to have assertions for invariants defined in TLA+ in our
integration tests so that we can also have proof of correctness for the
implementation. Do you have any thoughts on this?
--
Divij Vaidya
On Tue, Jul 26, 2022 at 5:21 PM Haruki Okada <oc...@gmail.com> wrote:
> Hi.
>
> That also sounds good to me.
>
> TLA+ spec helps us to understand the protocol from a high-level.
> Also I agree with Tim's point that the spread of familiarity with
> formal methods would be beneficial in the long term.
>
> 2022年7月26日(火) 23:58 Tom Bentley <tb...@redhat.com>:
>
> > 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
> >
>
>
> --
> ========================
> Okada Haruki
> ocadaruma@gmail.com
> ========================
>
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Haruki Okada <oc...@gmail.com>.
Hi.
That also sounds good to me.
TLA+ spec helps us to understand the protocol from a high-level.
Also I agree with Tim's point that the spread of familiarity with
formal methods would be beneficial in the long term.
2022年7月26日(火) 23:58 Tom Bentley <tb...@redhat.com>:
> 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
>
--
========================
Okada Haruki
ocadaruma@gmail.com
========================
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Tom Bentley <tb...@redhat.com>.
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
> <jv...@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 <is...@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 <tb...@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
> > > >
> > >
> >
>
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Jason Gustafson <ja...@confluent.io.INVALID>.
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
<jv...@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 <is...@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 <tb...@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
> > >
> >
>
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Jack Vanlightly <jv...@confluent.io.INVALID>.
+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 <is...@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 <tb...@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
> >
>
Re: [DISCUSS]: Including TLA+ in the repo
Posted by Ismael Juma <is...@juma.me.uk>.
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 <tb...@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
>