行为时序逻辑：Liveness 和 Fairness
行为时序逻辑：Liveness 和 FairnessTLA 里有两大逻辑：命题逻辑（Propositional Logic）和时序逻辑（Temporal Logic）。第七章是是《Specifying Systems》中时序逻辑的引入章，从仅仅讨论命题逻辑到开始讨论时序逻辑，命题逻辑可以规约系统的 Safety 特性，有了时序逻辑后，我们终于可以规约系统的 Liveness 特性了。本文是第七章的小结。文章不仅仅是公式笔记，也包括了少许的个人观点。
分布式系统：与时间有关的故事
分布式系统：与时间有关的故事
世界就是一个分布式系统。
时序问题在分布式系统里面是个大问题。一直以来，时序问题在很多场合有点过于理论化，所以，大部分工程领域对这个问题关心得并不多（或者说被基础组件默默地解决了），鲜有文章给出框架性的指引，我想尝试用一篇文章整理分布式系统关于时间、时钟、时序相关的经典问题和解决方法（理论、设计等），最后简单谈一谈与时序相关的一致性问题。
时序问题：从生活到分布式系统时间是生活中一个很重要的概念，我们用时间确定事件的先后关系，进一步使得许多事情得以确定。举个例子，某天，我想请我的朋友帮忙代取快件，首先要告诉朋友，朋友同意后，才有取快件这一件事发生。例子中，“告诉朋友”是一个事件，“取快件”又是另一个事件。上面事件必有严格的先后顺序。为了确定先后顺序，除了根据逻辑推理，有时候我们还会通过比较事件发生的时间。不可能出现朋友先帮我取了快件，我再向朋友发出请求这种诡异的顺序，同时事件之间也是有因果关系的。
分布式系统也是类似的。很多时候，我们希望根据事件的先后关系确定系统表现出来的行为，使得设计的分布式系统是符合预期的。在日常生活潜移默化的影响下，我们也希望用时 ...
Begin? Maybe.
Begin? Maybe.
懒狗它真会花时间写Blog吗？
作为一个不大喜欢花大块时间来写作的人（懒狗），我曾多次在心里默念：Blog啊，这辈子我都应该不会有的。然而人类的四大本质使得我似乎今天也说出了那耳熟能详的两个字：“真香”。
起因折腾一个 Blog 并不在我人生的 Roadmap 内，然而并不代表不在别人的 Roadmap 里。这不，受到某位熟人的委托，做某些产品的展示页面，我也要折腾起 Wordpress 这种这么重的东西了。再加上这段时间读了不少论文，又沉迷TLA+，信息量略大，有时候觉得总该输出一些东西。一来作为笔记总结，二来这些东西放国内来说，对于其他人，确实可能还有少许参考价值吧。既然起了个头，干脆也给自己搞一个。
结果为省去数据备份迁移运维的麻烦，也想用Markdown写作，又想对文字进行版本追踪，全静态 Github 发布基本成为了最优选择。于是就选了著名的 Hexo，配了套 CI Pipeline 进行全自动构建发布，封面选了前些天在塔公草原瞎拍的风景照，一晚上基本倒腾了个大体，细节就慢慢磨吧。
后记：纯种懒狗的 Blog 一定是空的，永远是空的。懒狗它一定不 ...