Attempt to be mentioned in TLA+ homepage

[lance6716]

Question

I'm learning TLA+ and found there's an Industrial Use of TLA+ page recording companies who use TLA+.
Since we have a TLA+ repo and posts (though in Chinese), I write a simple email to introduce us, and Lamport replied

Thanks for contacting me. That web page describes just a few of the industrial uses of TLA+. There is no attempt made to list all users of TLA+. If you posted some description of how TLA+ was used to solve some problem, I’d consider mentioning it.

Through that page there're some examples of how TLA+ was used by companies of paper, journal, post, video, and even an email

In November, 2016, Bogdan Munteanu sent me email describing TLA+ use at Dropbox. Here is an extract from that email.
[An] engineer decided to learn/experiment with [TLA+], so I provided some guidance and feedback. He wrote the formal spec for one of our two-phase commit protocols that we knew would fail in certain real-world situations. His spec found the issue ... and the engineer found the process extremely valuable. He mentioned that learning TLA+ was not at all a steep curve — it took him longer to understand the actual protocol.
About a month ago, another engineer designed a deadlock detection algorithm for one of the new distributed protocols at Dropbox. After hearing about the success of the previous TLA+ project, he decided to write a spec for this new protocol with the help of the other engineer. They found a bug in the protocol, fixed it, then confirmed the fix by re-running the model checker. In both cases the spec was written in PlusCal. Everyone was really impressed by the results, and for most came as a surprise because few have heard of formal verification before.

We have finished the most difficult part — writing the TLA+, so how about writing some description of our practice to get mentioned in this expert's website?

[lance6716]

I don't have access to edit issue assignees (was an intern in TiDB), so manually ping 😂
@siddontang @c4pt0r

[siddontang]

Great, @lance6716

I think we can write a detailed description to tell how do we use TLA+ to gain confidence when implementing our distributed transaction algorithm.

[siddontang]

Can I assign this work to you directly? @lance6716

[lance6716]

Can I assign this work to you directly? @lance6716

OK, I may interview related fellows to complete the description.

How to review the description, should I create DNM PR here or elsewhere?

[siddontang]

Maybe we can write the description here directly and discuss it at first. Then we can send a PR to lamport.

/cc @dcalvin

[lance6716]

TLA+ was firstly used by PingCAP in 2017, to verify a variant of Percolator transaction model is feasible. Different from original Percolator, TiDB optimizes its efficiency by supporting primary key and secondary keys prewriting concurrently in prewrite phase. It was a problematic idea at first glance, but with TLA+ the case was clearly identified and targeted changes were applied to enable this optimization. Another example is TLA+ verified the correctness of multi-raft region merge algorithm, which gives confidence before implementing and summarized a more clear documentation. These work was made by a 4-member group and proved a worthy investing afterwards.

PingCAP has maintained a repo in Github recording all specifications they wrote, and keeps aligning TLA+ specifications with newly implemented database optimization. There're still active PRs and disccussions to verify new feature and fix bug from high-level.

Engineers here agreed that TLA+ is necessary when proving the correctness of distributed systems, specifing the behavior to avoid patching in future, expressing the subtle details which natural languages not good at. Speech and posts were shared with infra community by PingCAP to discuss on technical reflection and experience of TLA+ application.

---

Above description aims to express "problem solved at early use; we're continuous using TLA+; we're sharing with community"
@siddontang @dcalvin

[dcalvin]

Thanks @lance6716 I will follow this up next week and provide a review before we submit.

[lance6716]

ping @dcalvin

[dcalvin]

ping @dcalvin

but with TLA+ the case was clearly identified and targeted changes were applied to enable this optimization.

What do you mean by "case was clearly identified" @

[lance6716]

I should express "...but with TLA+ the root cause was clearly identified..."

[dcalvin]

specifing the behavior to avoid patching in future, expressing the subtle details which natural languages not good at. Speech and posts were shared with infra community by PingCAP to discuss on technical reflection and experience of TLA+ application.

These few sentences don't really look well connected to me. Can you express them in Chinese?

[lance6716]

specifing the behavior to avoid patching in future, expressing the subtle details which natural languages not good at. Speech and posts were shared with infra community by PingCAP to discuss on technical reflection and experience of TLA+ application.

These few sentences don't really look well connected to me. Can you express them in Chinese?

……明确规定了（系统的）行为，避免未来用补丁修复的麻烦。表达了一些自然语言不善于描述的精微的细节。PingCAP 与网络基础设施相关的开源社区分享演讲和文章，一同探讨技术反思以及 TLA+ 使用中的经验

[dcalvin]

TLA+ was firstly used by PingCAP in 2017 to verify the feasibility of a variant of the Percolator transaction model. Different from the original Percolator, TiDB’s model has improved efficiency greatly by supporting primary key and secondary key prewriting concurrently in the prewrite phase. The implementation was problematic at first. Thanks to TLA+, the root cause was clearly identified and targeted changes were applied to enable this optimization. Another application of TLA+ at PingCAP is the correctness verification of the multi-raft region merge algorithm, which provided the necessary confidence before we implemented the feature. There were only 4 members invested in the TLA+ related work, but the rewards are far beyond that.

Engineers at PingCAP believe that TLA+ is necessary when it comes to verifying the correctness of distributed systems and specifying the right system behaviors to avoid future patching. They agree that TLA+ is better at expressing the subtle details which natural languages are not good at.

PingCAP has maintained a repo in Github that records all specifications they wrote and keeps aligning TLA+ specifications with the newly implemented database optimizations. Up to now, there're still active PRs and discussions on verifying new features and bugfixes. Speeches and posts on technical reflections and experience of TLA+ application have been shared with the infra community by PingCAP.