最近电脑坏了，所以上周没法写文章，抱歉。 随着AWS Automated Reasoning Group的兴起，可以感受到了编程语言在工业界的影响力的加大（这不废话吗，这么多人都被吸过去了），顺带不久前看了github semantic的ICFP Experience Report，想了想可以写一写关于这些的内容。 这方面一写paper是(缩写C)，讲coverity的程序分析框架在应用的时候的问题，<Fusing Industry and Academia at GitHub (Experience Report)>(缩写G)讲github内部的程序分析框架semantic，还有(缩写A)，讲AWS如何利用SMT solver对云上控制权限的验证。 其实ACG三篇paper都有很多共通点，我觉得与其一篇篇介绍，不如对ACG做一些总结 为什么要整X? A:没说 C:我们一开始是为了publish paper，在几百万行代码上抓了很多错误，publish了paper以后，就觉得可以搞个大的。开家公司，请几个销售员躺着数钱钱，当然这考虑完全错误 G:做一个更好的，知道语义而不是只知道unstructured text的git diff 有没有遇到什么克苏鲁问题？ A:没有 C:好多，惨惨，哭哭。有一次我们跑用户的make，结果用户用了个奇奇怪怪的make语法写path，结果在蝴蝶效应下变成了rm -rf *。用户经常会给我们奇奇怪怪，不符合C语言标准的程序，然后因为各种原因无法改C编译器，最后要我们改自己的C parser。还有一次，给用户抓出use after free error，用户说free了以后还没malloc，所以freelist没有被复写，可以继续用，气死偶嘞！（整篇paper都是各种这些克苏鲁问题） G:没有，卧槽free了后依赖于没有malloc继续用也太克苏鲁了 有没有遇到什么不克苏鲁的问题？ A: 我们遇到的最大问题是只有很小一部分用户会写SMT Query或者First Order Logic。但是，AWS有一百万用户，没有办法教这一百万个用户都写SMT。所以，我们把问题反转过来 - 对于一个输入（系统设置），我们会返回所有的信息（对于所有最终用户X跟数据Y，X能不能访问Y）。这时候，AWS用户只需要检查这些访问权限报告，就知道行不行了。 我们遇到的另一个问题是，当我们升级我们的SMT solver的时候，有的时候以前能Solve的Query会timeout，于是对一些用户来说，以前行的东东就不行了。我们的解法是，弄一个大大的portfolio，各种solver version都丢进去。 C: 我们也一样有软件升级问题。当我们升级完我们的静态分析器的时候，我们往往能抓更多错误，但这是不好的！更准确的说，我们的PM往往都想要一个这样的故事：‘我们引入了静态分析器，然后发现了X个错误，然后在过去Y个月里面，我们把这X个错误一步步消除掉！现在，我们的程序没有错误了！’，然后当他们升级软件的时候，错误越来越多，就会很气气！ 另一个问题是，用户会不停提交代码，而如果你以前报过一次错误，同样的错误就不要再报了。我们写了一个错误database，然后会把所有分析出来的错误跟这个一一对比，只报告新的。 还有一个问题是，当我们报错误的时候，用户有时候看不懂，然后就会把我们的错误看成误报。当用户认为我们误报的时候，就会更不信任我们的工具，于是下次我们报错会更可能认为是误报。于是，我们需要很好的错误信息，并且对于一些复杂的静态分析，给出好错误信息更难，如果我们给不出好错误信息，我们宁愿不要这个分析。 G: 我们的新git diff能给出很有用的summary，于是得到了更多momentum（大概是有更多资源招程序员整这个）。但是用户不想安装跟用我们的新git diff。我们只好弃掉这个project。 更具体的说，我们不做git diff了，我们用我们整的静态分析工具弄一个Code Navigator，当你指定一个函数的时候，我们用静态分析找出这个函数用在那。 总结： 我觉得这三个工作都有一个共通点：如何包装销售自己的工作(Story)很重要。这里的销售并不是’口才很好‘的意思，而是’向谁卖什么‘。对于A用户来说，他们甚至不知道什么是SMT! 这时候，这整个工具就相当于’隐形‘的，需要跟用户打交道的地方小了很多（只剩下保证版本不会regress）。C用户会不停看到Coverity的工具，于是要求也最高。G也一样有这个问题，但是他们明白Story是可以改的，于是换了一个就好了。 当然，C的方法并不一定更’不好‘ - 在一些时候，这可以抓出’关键的错误‘，而semantic则做不到这个（因为已经包装成不是抓错误工具了）。更重要的是，C引入了一个叫’话语权‘的概念。当你的工具刚刚引入的时候，大家都不知道你的工具是做什么的，也不信任你的工具，于是会e.g.把错误看成误报，不看错误，或者就e.g.不会升级，或者买静态分析服务。所以这里有一个很典型的网络效应 - 在前期要给出很多精力去一个个服务用户，但是后面工具变出名了以后就不需要了。C也说了一句‘好日子在后头’之类的话：在以前静态分析没有C的时候这么流行，于是它的前辈要做的斗争更难。可以预想的是，很多这些都是‘一次性开销’，后续工具的应用会更简单。 另外，Github：Haskell真香，ICFP是我的秘密武器！

周末看LOL比赛去了，忘了做正事了（？？？ 不过DRX真鸡儿逆天，震 撼 我 妈 一 整 年 想了想，就带逛三篇比较有意思的垃圾回收的paper凑凑数（？ 自我吐槽：喂，你就是这样对待你主方向的吗？？？ The Transactional Memory / Garbage Collection Analogy：这篇paper就如同名字上所说，把两个不太接近的概念联系起来了，大体思路就是两个东东都能提高编写体验，然后对比lock ordering，或者对比rc，都不怕cycle，但是会损失点性能。 续上，有一个更逆天的联系在How OCaml type checker works – or what polymorphism and garbage collection have in common里面。大体说，当你进行let generalization的时候，你只能generalize由你‘独占’的类型变量，而如果你独占了会‘逃逸’，或者是‘外面传来‘的类型变量，就会type unsound，而这跟你free了不该free的东东会引发dangling ptr是一样的。然后blog把解决方法联系上了region based memory management。 A theory of garbage collection：这把reference counting跟tracing based garbage collection对立起来了。更具体的说，reference counting是在求一个least fixed point of garbage，所以会从已有垃圾开始推更多垃圾，而tracing是在求greatest fixed point，于是会从live memory里面iterate。相比前两篇这个联系更’明显‘。 Improving flow analyses viaΓCFA: Abstract garbage collection and counting.：当你跑abstracting abstract machine的时候，你的allocated cell会越用越小，最后一个cell要被迫重复放值，从而需要merge，污染精度。这paper是在说，你这时候跑一跑垃圾回收就好辣！比起前面几篇，这篇的逆天之处在于提出了一个很离谱的connection，但是真的能行，还给一群人指了路，在这以后来回搬运什么Abstract Reference Counting之类的工作 Garbage collection can be faster than stack allocation - 这paper核心idea很简单：mark copy gc只动live memory不动dead memory，那我一个垃圾回收器，只要很久才回收一些内存，不就比手动内存管理（这时候需要时间去回收单独的dead memory cell）快吗？当然，现实里面没这么多内存，也就佩恩入侵木叶 - 图一乐 Ulterior Reference Counting: Fast Garbage Collection without a Long Wait：ref counting的主要问题是（不是cycle！）频繁refcount会严重降低性能，而tracing based GC的主要问题是需要不停重复遍历live set。这篇paper把两个合二为一，从而试图去掉两个的主要问题：old generation用rc，这样由于old generation动得小refcount不频繁，而young generation用gc，这时候live set只需要遍历一次（就promote了） 本来想好三篇的，但是写着写着记起来更多paper了（？

最近遇到一道很有趣的算法题： 给与数组N[0, n)跟M[0, m)，并且m <= n，其中M的元素都在[0, n)以内，换句话说可以用M索引N。这个时候，我们对每个M里面的元素m，找出N里面第m大的元素，换句话说，我们要计算出 map (\m_element -> sort n !! m_element) m 比如说，假如N是[1, 9, 3, 8, 10, 7, 2, 10, 8]，M是[7, 2, 0]，结果应该是[10, 3, 1] 但是，我们希望平均时间复杂度是O(n log m)，这怎么做？（注意，这比n log n小，而很多做法都是后者） 为了给大家一些思考时间，明天再放答案 更新：答案在https://zhuanlan.zhihu.com/p/578991429

想了想，最后还是觉得应该用这篇paper开头。 什么是Defunctionalization? 简单的来说，Defunctionalization是一个程序变换。更具体的说，Defunctionalization接受一个高阶编程语言的程序，输出一个一阶编程语言的程序。这通过一下变换完成。 创建一个代数数据类型，lam，跟创建一个函数apply: (lam * Any) -> Any（是的，naive的Defunctionalization并不类型安全） 对于所有a -> b类型作为一等公民（不是直接调用）出现的地方，把类型a -> b变换成lam。 对于所有构建闭包的地方，创建一个新的lam构造子。这个构造子的成员就是这个闭包捕获的变量。 同时，在apply函数内，给出该lam构造子的实现 - 而这实现照抄原closure的body。 对所有调用闭包f x的地方，改为apply (f, x)。 举个例子，假如我们有以下代码， (* aux : int * (int -> int) -> int *) fun aux (i, f) = f i (* main = fn : int * int list -> int list *) fun main (i, js) = let fun walk nil = nil | walk (j :: js) = (aux (i, fn i => i + j)) :: (walk js) in walk js end Defunctionalize后，会成为...

已经有很久没写文章了。 原因大概是，随着科研的进展，我看的paper，往往越来越冷门小众，也越来越‘高深’。 这时候，我对介绍这些paper动力越来越小 - 一方面，我自己都不能经常完全搞懂，那这时候我介绍效果会比原文差很多（甚至会出错！），而另一方面这些paper的受众也越来越小。 但这好像有点不对 - 如果人人都像我这样，那写文章的人岂不是都是公众号？ 所以我决定以后写一些CS里面浅显但有趣的知识，吸引读者关注各种领域，坚持一周一更 为啥要写一个公告而不是直接写捏？ 一个原因是，这样有个外部的deadline，鞭策鞭策自己 另一个原因是，尽管专栏好像不能投稿了，希望大家可以留言/私信我有趣的东东，这样我有更多写的材料 就这样。

第二节： Spore：【译】shift/reset 编程入门 (2)：应用 3 Delimited Continuation 操作符的理论基础 本节对 delimited continuation 操作符 shift/reset 的理论基础进行概述。我们使用的语言是一个从左到右求值1的 call-by-value λ 演算，并加入了多态的 let 和 shift/reset 操作符。 3.1 语法 $$\begin{alignat}{1} \text{(value)}& \quad V& \quad::=&\quad x \ | \ \lambda x. M \\ \text{(term)}& \quad M& \quad::=&\quad V \ | \ M~M \ | \ \mathsf{let}~x = M~\mathsf{in}~M \ | \ \mathcal{S}k.M \ | \ \langle M \rangle \\ \text{(pure evaluation context)}& \quad F& \quad::=&\quad [~] \ | \ F~M \ | \ V~F \ | \ \mathsf{let}~x = F~\mathsf{in}~M \\ \text{(evaluation context)}& \quad E& \quad::= &\quad [~] \ | \ E~M \ | \ V~E \ | \ \mathsf{let}~x = E~\mathsf{in}~M \ | \ \langle E \rangle \end{alignat} \\$$其中，shift (fun k -> M) 记作 $\mathcal{S}k....

0 译者前言 本文译自浅井健一先生的《shift/reset プログラミング入門（Introduction to Programming with Shift and Reset）》。找了一圈之后发现整个知乎上都没人教怎么使用 delimited continuation，遂翻译。 一些说明： 虽然文中说有任意函数式编程语言的经验即可，但例子和练习题用的是一个 Caml 变体，所以想要获得最佳阅读体验还是要了解 OCaml 或其他 ML 系编程语言的基础语法。 Rust 不算。 译文同时参考日语和英语版本，两版本如有不同则以正确/易懂一方为准。 部分译者的评论或解释用〔〕标注。原文的引用和注释则尽量还原（但由于知乎的限制只能混在一起了）。 译者翻译相关文献的经验并不丰富，如有任何错漏或可改进处请务必指出。 接下来开始正文内容。 摘要 Continuation 是在各种编程语言中都普遍存在的概念。条件语句是根据条件从两个 continuation（未来）中选择一个的操作，异常则可看作是丢弃一部分 continuation 的操作。还有，尾调用（goto 语句）就是执行 continuation 的操作。尽管 continuation 是这样一个无处不在的、十分自然的概念，目前为止，显式地使用 continuation 编程仍然一直被认为是困难的。 本教程使用 delimited continuation 操作符 shift 和 reset 来演示如何显式地使用 continuation，从零开始讲解关于 continuation 的基础知识，并在过程中指导读者实现简单的协程和非确定性搜索。本教程同时也能作为 CW 2011 演讲内容的引子。 本教程需要读者熟悉 OCaml、Standard ML、Scheme 或 Haskell 等函数式编程语言，但不需要读者在阅读本文前有任何有关 continuation 的知识。教程中穿插了各种练习问题，推荐读者随读随做。 1 引言 Continuation 就是表示「之后的计算」的概念。它可以看作是异常处理的一种推广，但远比异常处理要强力。实现复杂的计算时，实现者有时会发现需要使用在通常的程序结构中难以写出的控制结构。如果能操作 continuation，则可以在不影响程序整体可读性的前提下实现它们。 想要显式地使用 continuation，一种传统的方式是对整个程序进行 CPS1变换〔continuation passing style，指把 continuation 作为参数显式传递的编程风格〕，但这样就不能保留程序的原有结构。为了在引入 continuation 的同时保持程序的正常结构，我们就需要使用 continuation 操作符。...

第一节： Spore：【译】shift/reset 编程入门 (0)&(1)：前言和概述 2 shift/reset 编程 2.1 什么是 Continuation Continuation，简而言之就是「之后的计算」。程序的执行过程就是选出要执行的部分（称作 redex〔reducible expression，可归约表达式〕），对它求值，再使用它的结果来进行之后的计算。这里的「之后的计算」就是指 continuation。因此，continuation 是任何程序执行时都存在的基本概念。 为了展示 continuation 具体是什么，我们用 $[\,... ]$（称作 hole）来表示一段程序接下来要执行的部分。比如 $3 + 5 * 2 - 1$ 这一算式中，如果接下来要执行的部分是 $5 * 2$ 的话就可以写作 $3 + [5 * 2] - 1$，而这时的 continuation 就是 $3 + [~\cdot~] - 1$。总之，得到 $[~\cdot~]$ 的值（$5 * 2$ 的结果 $10$）之后，「给这个得到的结果加上 $3$ 减去 $1$」就是整个式子当前的 continuation。从「接受 hole 的值之后用它进行计算」这方面来看，continuation 和函数是相似的。 也可以用「抛出异常时扔掉的那部分程序」来看待 continuation。例如，把上述例子中 $[~\cdot~]$ 的部分换成 raise Abort，让它抛出异常，这时候被抛弃的部分 $3 + [~\cdot~] - 1$ 就是 continuation。...

虽然说是看看 cedille, 不过主要是因为用 cedille 写这篇內容会比较方便了。这篇主要介紹的是 MLTT 70, 又被稱為 Type : Type，只要用 dependent function type 就可以 encode higher order logic。 首先就是 well known 的 dependent function type 对应 universal qualifier。之前的 LdBeth：NuPRL 中的证明–从一到CTT 中提到的 indexed family of intersection type 也对应 universal qualifier ，不过生成的 witness 会不同。在 Cedille 中 indexed intersection 用 $\forall$ ，dependent function 用 $\Pi$ 表示。 Conjunction 可以表为如下，★ ➔ ★ ➔ ★ 是 kind， $\forall P.(A \rightarrow B \rightarrow P)\rightarrow P$ 意为对任意命題 $P$ 在有 $A \rightarrow B \rightarrow P$ 时 $A \wedge B$ 可以证明 $P$ 。...

大多数情况下，effect都是用Hoare逻辑来描述的。一个Hoare三元组$\{p\}\;S\;\{q\} $， $S$ 是一段程序， $p $ 是执行这段程序的前提条件（状态）， $q$ 是执行完这段程序后的条件（状态）。然后使用这个三元组的一些规则表示语句的一些性质： 空语句： $\frac {} {\{p\}\;skip\;\{p\}}$ 赋值语句： $\frac {} {\{p[u :=t]\}\;u:=t\;\{p\}}$ 顺序语句： $\frac {\{p\}\;S_1\;\{q\}, \{q\}\;S_2\;\{r\}} {\{p\}\;S_1;\,S_2\;\{r\}}$ 等等。这其实恰好是个幺半群——空语句是幺元，顺序语句是乘法。总之，用幺半群来描述作用（语句）是十分合适的。 于是用Monad来描述作用也是很自然的——Monad是自函子范畴上的幺半群。（这句话我就不解释了） 比如用m a表示带作用类型为m的程序，而m (m (m ... m a))表示一系列的作用，对应作用（语句）序列 $S_1, S_2, S_3, S_4 \dots S_n$ ： stms :: Monad m => m (m (m (m ... m a))) -- ^ ^ ^ ^ ^ -- | | | | ... | -- S1 S2 S3 S4... Sn stms = ....