+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
