机器学习模型依赖于批处理(Batching)来提高推断吞吐量，尤其是对于ResNet和DenseNet等较小的计算机视觉模型。GPT以及其他大型语言模型(Large Language Model, LLM)是当今最热门的模型。批处理对于GPT和大语言模型仍然适用吗？让我们一探究竟。

上交了连照片名字都没有的临时工牌，上星期五我为期13周的谷歌实习告一段落。我给谷歌写了7500行C++代码，再加上还没有合并的1000行，我觉得我对自己贡献代码的数量和质量还是比较满意的。这次谷歌实习是我第一次在工业界的经历，感觉收获很多。

每当我的程序崩溃的时候，我都会用核心转储 (core dump) 文件来找出来崩溃发生的具体位置。（关于怎么产生和使用核心转储可以看我之前的文章。）一直以来我调程序的时候都是很开心的……直到我遇到了这个新的 bug。当我把它的核心转储文件载入到 GDB 之后，我很失望地发现所有的堆栈追踪 (stack trace) 都是关于系统库的，没有一行是关于我的代码的。

太长不看：那就看看这个补丁就好了。

让我们踏上探索未知的旅程吧。

我第一次听说 Coq 是在本科的时候。从那以后我就一直很想学 Coq，但是并不知道怎么开始。大部分的 Coq 教程都是在讲逻辑，我觉得并不是很有趣。

上个学期我选了 UW CSE505 这门课。Prof. Zach Tatlock 和 TA Talia Ringer 设计了一系列非常棒的作业来帮我们学习 Coq。在这个课里面，我们证明了一些更加实际的东西，包括一个简单的编程语言的解释器还有一个简单的正则表达式引擎。事实上，我发现我对在 Coq 里面写证明还蛮在行的（但是写规范就完全是另外一回事了），至少在做作业的时候我是这么觉得的。

如果你在自学 Coq，我推荐以下资源：

• UW CSE505 的作业
• Formal Reasoning About Programs 这本书是我们上课的教材。这本书很短，边距很大，空白很多，每一章附带了详细的 Coq 代码。这本书还自带了一个很好用的 Coq 库 frap。
• Software Foundations 如果你真的对形式化验证很感兴趣的话。

我非常高兴我终于能把 Coq 从我的愿望单里面划掉了。不过我并不是形式化验证的狂热粉丝，我觉得我之后也不用用到 Coq。我决定趁我还没完全忘记 Coq，赶紧把我做作业时学会的 Coq 技巧写下来，万一以后哪天我又用到 Coq 了呢，希望也对读者有所帮助。

这算是开了 CS140e 的坑了吧。在淘宝上买树莓派的时候发现了出了3B+版本，而课程用的是3B版本。新的性能要强得多，肯定要买新的呀。但是，3B的CPU是BCM2837，3B+的是BCM2837B0，买的时候有点担心能不能正常地运行 CS140e 的程序。

收了货试了下，果然不行。ACT灯先慢闪4下再快闪4下，循环往复。搜索 raspberry pi act led，找到了这么一个wiki，上面说闪4下是 start.elf 无法载入。

我猜测这个 start.elf 可能不是课程专用的，于是搜索 start.elf raspberry pi 3 “b+”，找到了这个帖子，发现了官方的固件，用里面的 start.elf 替换就能成功启动了！