形式化验证（Formal Verification）指一类使用数理逻辑方法来证明软件设计是正确的技术，据称是由 Edsger Dijkstra 于 1972 年最早提出，此方法一直是一种比较小众冷门的技术。形式化验证技术想要解决的核心问题是：软件总是可能存在 Bug 的，而测试始终无法涵盖所有可能性，特别是对于并发系统及分布式系统来说，就算单元测试达到了 100% 分支覆盖率，也不能肯定的说这个系统在线程安全，一致性等方面不会出问题。那如何更好的来验证我们的程序是否符合预期呢？形式化验证就旨在使用严谨的数学证明方法来证明某一算法是正确的。这样我们就可以拍着胸脯说，我的算法肯定是正确的，都证明过了:)

我们从小到大都在学习各种新东西，学的东西多了自然会对“如何学新东西”这一问题本身有一些方法论层面的思考，本文就来分享总结下自己的一些经验。

对于学习各种人为创造的东西基本都可以按相同的方法进行，不过对于学习自然科学的概念方法会有所不同，本文就不去讨论了。

学习一个新东西基本可以分为三个阶段：初步理解，即会用；深入理解，即懂原理；融会贯通。

Chia（起亚） 是最近极为火热的数字货币项目，对应的货币叫做 Chia Coin，简称 XCH。其核心算法为 PoST（Proof of Space and Time），以替代比特币中的 PoW（Proof of Work）。

使用 PoSpace 空间证明而非 PoW 工作量证明是 Chia 项目宣称的最大优点。据他们的开发者宣称，PoW 耗费太多能源了，不环保，我们来搞点更环保的东西吧，不用 PoW 了，改用 PoSpace，即谁有的硬盘空间多谁的投票权就更大。因此他们还把通常称为白皮书（White Paper）的文档改名叫做绿皮书（Green Paper）。

然而仔细想想这哪里环保了，把一堆硬盘搞来塞满毫无意义的数据比比特币矿机还要更邪恶吧……Chia 的官网上还可笑的宣称硬盘更不容易被垄断，因此个人还有小玩家可以更好的入场，简直是更荒谬的说法，哪个个人会去囤积一堆存不了有用数据的硬盘？

IPFS 好歹还可以存一些实际有用的数据，看起来还真能促进下社会发展，至于 Chia 简直是除了圈钱和泡沫看不到任何其他意义。不过抛开实际意义，由于最近也研究了下 Chia 的文档和代码，就单纯的来和大家分享下 Chia 的技术实现吧。

C++ 中的 volatile 关键字，std::atomic 变量及手动插入内存屏障指令（Memory Barrier）均是为了避免内存访问过程中出现一些不符合预期的行为。这三者的作用有些相似之处，不过显然它们并不相同，本文就将对这三者的应用场景做一总结。

今天在调试时发现了一个奇怪的core：double free or corruption (fasttop)，从堆栈看是由于 _dl_fini 函数多次重复释放了某些 STL 容器导致的，此时就算在 main 函数中只保留个简单 return 0 也会出错，因此猜想肯定和某些全局变量有关。后面经过各种修改尝试，终于发现这是由于引用的 .so 动态库和主程序中定义了同名的全局 STL 容器导致的，此时的行为简直就是一个神坑，很有必要记录一下……

在 GCC -O3 优化级别下，很多局部变量是会被优化掉的，此时只能通过人工分析反汇编代码来获取所需信息，而这么做的前提是保存下来的寄存器中的值是准确的。绝大部分情况下 coredump 是由于 segment fault 或 assert 触发的，segment fault 情况下 Kernel 保存下来的 registers 信息是准确的，GDB 中直接用 info registers 就可以看到。然而若是由 assert 触发，由于 assert 会进行多层函数调用后最终执行 raise()，错误现场的寄存器信息是不准确的，这时候就需要一些其他手段来解决此问题。下面用一个具体例子来说明此问题。

perf 是 Linux 下重要的性能分析工具，perf 可以通过采样获取很多性能指标，其中最常用的是获取 CPU Cycles，即程序各部分代码运行所需的时间，进而确定性能瓶颈在哪。不过在实际使用过程中发现，简单的使用perf record -g 获取到的调用栈是有问题的，存在大量 [Unknown] 函数，从 perf report 的结果来看这些部分对应地址大部分都是非法地址，且生成的火焰图中存在很多明显与代码矛盾的调用关系。

在旧笔记本上使用Proxmox搭建了一个OpenWRT软路由，正常使用都很稳定，然而当PC使用百度网盘，迅雷等工具进行全速率下载时偶尔会出现网络中断问题，此时Proxmox宿主机的网络会全部断掉，即PVE自己的Web管理界面也无法登录。查看终端，此时会不断打印Detected Hardware Unit Hang的错误提示。

转眼间毕业已经要一年了，今天在整理电脑文件的时候翻出了当初写的硕士毕业论文，在知网上搜搜也找得到了。想想硕士期间做过的东西也太杂了，电机控制、Android 开发、嵌入式。。。最后确定了这个毕业论文的题目后只有1年不到的时间可以做了，这期间还要复习准备找工作，不过最后做出来的东西还算是自己基本满意的，这估计也是我在学术上的顶峰了……

学习Docker时一般刚开始接触的第一个docker image就是hello-world，这个image运行起来的效果也很简单直接，仅仅是在屏幕上输出一段Docker的使用说明就结束了。这个镜像虽然简单，然而仔细分析下还是涉及不少底层机制的。