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 <divijvaidy...@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 <wangg...@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 > > <matthew.dedetr...@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.dedetr...@aiven.io > > > On 26. Jul 2022, 16:58 +0200, 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 > > > > > > > > > -- > > -- Guozhang > > > -- > Divij Vaidya >
