𝒦评价为：无聊。 今天听了一个关于使用大模型获得符合规则的结构化输出的工作。首先输出得是结构化的（如合法的json文本，引号括号均匹配等等），其次得符合用户指定的规范（schema）。比如必须是一列对象，其中每个对象必须有哪些键，各个键的值又分别是什么类型，诸如此类。 介绍的工作是采用先生成后筛选的思路。按下不表。 首先将所需的结构化输出转化为对应的语法树。规范一定程度上固定了树的形...

这下终于开始认真搞卡皮巴拉了。中午把设计差不多定下来了，跟一作老哥描述了一下。昨天跟ℒ开会也描述了一下，他们都说好。 就是进度赶不上了。把更新后的预期进度也给一作老哥说了一下。 如果上周没有拖着，现在能不能赶上原本的计划呢？不知道，因为冒出了额外的工作量。 不过也没必要指望自己没有拖着就是了。小拖一下是很难避免的。后面尽快搞定就是了。 在SysDW上有个三分钟的发言要准备。讲En...

拖了一周多以后今天开始相对实质性地开展了对卡皮巴拉的工作……的准备工作。 卡皮巴拉是一个做协议层连接迁移的工作。它的主要特性有 （几）微秒级超低延迟 无需感知迁移；对于应用来说连接就像没有迁移过 迁移策略设计，这个不太影响我参与的工作 卡皮巴拉这个工作本来是专门做TCP连接迁移的，在这一轮迭代中决定转向更加通用的，（基于TCP的）多层协议栈连...

距离上个检查点已经一周多了。遇到的挑战并不是像预期中的「不想动笔写」。相较之不知是更好还是更坏，实际上是「根本没想起来要写」。 大概还是应该以单位时间而不是事情告一段落作为动笔的时机。一方面固定间隔更容易记起来，另一方面，超出了时间间隔真的会记不住自己干了啥，所以不管干成啥样都必须得记下来了。 最近来到了比较需要发奋图强的一个时期。更密集地存上些检查点，吾日三省吾身。 给这个站重新写了...

风雨飘摇的一周。抑或说连绵不断的一周。早几天就想要开始动笔，总是想着把手头的事告一段落就开写，然后手头的事就有了新的情况。 把Alloy的文档看了个七七八八。对于要怎么做的想法逐渐清晰了些。就姑且称为模型检查企划吧。 跟ℒ磕磕绊绊地讨论了几个来回，逐渐接受了他的构思开始着手实施。一般来说这是很好的迹象。不过这块也不是ℒ的拿手领域。不过再不拿手也比我靠谱多了吧。 总还是觉得把顺序方面的性...

花了比预想中更多的时间研究SquirrelFS和其所基于的Soft Updates。 状态机是很多形式化验证的基础，几乎可以视作验证模型的「中间表示」。如果采取了手动对应（未验证的）实现和（验证了的）规范的手段，那么其中的一部分工作量就出自对于验证模型的状态转移的映射。 类型系统，具体到Rust类型系统，可以辅助确保其中一个重要属性：状态转移的完备性。验证模型中列出的状态转移就是全部可能...

这次的建立内容站来的很突然。从这周的This Week in Rust上读了一篇文章，然后就不由自主地被它的主题吸引了。虽然看了一下然后发现它还是做了一些定制化，不过原版也足够令我感到愉悦了，于是就像中了魅惑一样创建了这个站出来。 嘛，最近真是越发变成自己都不认识的样子了。 设立内容站这件事，对我来说一直以来最大的困扰在于出于什么目的去写。以往写了几天就不写了，因为写的东西总是挺吃灵感的...