前言：这本书看的断断续续的，如果不留点笔记可能很快就忘了，所以还是要记录一下。本书作者免费发布 pdf 版本，可以在 Software Engineering at Google （一下可能简称为 SWE）免费下载。因为是个笔记，所以行文可能逻辑比较断裂。 什么是软件工程 Nothing is built on stone; all is built on sand, but we must build as if the sand were stone. —Jorge Luis Borges 第一部分主要是在讲软件工程的定义，Software Enginner （以下可能简称为 SE）与 Programming 的区别。 最核心的一个想法是，你的代码的生命周期是多久？Google 的新项目往往默认项目会存在十年——这样一来，基础组件升级、依赖变化、团队组成都可能会变化，从而最终影响决策、影响设计。 这一点上国内很多项目肉眼可见的做的不好，最典型的莫过于百度的博客。当然这不意味着个 Google 的产品做得多好，但是这个思维方式确实很有用。当你设计的时候想的是要用十年，很多设计和决策就就和短期项目完全不同了。 我猜可能有很多人会有不同意见，比如像下面这个图里的例子 我觉得也并非不可调和，业务驱动的产品，很多时候就是需要快速试错，上线一个 demo 能用就行——这种情况就是定位为 demo，定位为 programming 就好了。另一方面，这也和从业人员对 SE 了解太少，公司无法做到将 SE 融入到日常有关，如果 […]

eBPF 提问：以下哪个内核可以运行 ebpf? ZStack C74 ZStack C76 CentOS 7.7 ZStack experimental repo 中的内核 （分别对应了 3.10.0-693 3.10.0-957 3.10.0-1062 4.18.0-240） 答案：有三个内核可以支持 C74 是不支持的，C76 有有限的支持，C77 支持程度更好一点，experimental kernel 里是 4.18.0，对 ebpf 支持已经很完善（当然了，ebpf 还处于快速发展阶段，因此还是版本越高越完善） https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/7/html-single/7.6_release_notes/index#technology_previews_kernel https://access.redhat.com/documentation/en-us/red_hat_enterprise_linux/7/html/7.7_release_notes/new_features#enhancement_kernel 检查自己安装的内核： grubby –info=ALL 在 ZStack 管理的计算节点上安装来自 experimental 的 4.18 内核： yum –disablerepo=\* –enablerepo=zstack-experimental-mn install kernel-4.18.0 在 ZStack 管理节点上安装来自 experimental 的 4.18 内核： yum –disablerepo=\* –enablerepo=zstack-experimental-mn install […]

很久以前学过一些 Prolog，当时主要是为了学习人工智能和数理逻辑。TLA+ 与之有一点点像，Prolog 可以用来处理各种规划问题、一阶逻辑推理，TLA+ 可以用来设计各种分布式、异步系统，搭配 TLC（model checker） 来做验证——他们的设计目标都不是解决通用的编程问题，而是通过数理逻辑解决一些特定领域问题。 TLA+ Tools 包含很多工具，可以在这里下载，大部分人都是使用这个 Tools： http://lamport.azurewebsites.net/tla/standalone-tools.html?back-link=tools.html 在里面的链接指向的 github 地址里，有 Windows、Linux、Mac 的二进制版本，良心。 在看 TLA+ Community Meeting 2018 的时候还看到了一个形式验证语言（其实是 Python 的扩展）DistAlgo，整体思路和 Demo 看起来特别棒，就是目前各种材料和介绍还是相对少，所以我没有继续研究下去，有兴趣和时间的话，看看 DistAlgo 也挺好。 下面是笔记。 介绍 分布式系统的正确性特别难验证，所以做出了 TLA+，因为 2015 年 AWS 在 CACM 发了一篇 How Amazon Web Services Uses Formal Methods 引起了很多人注意，年底 TLA+ 作者之一的 Langworthy 和 Lamport 找微软高层推动 TLA+ […]