Dimension Shift! 一起来学Datalog吧！

2020-10-21 本文已影响0人卷毛宿敌大小姐

Pre

相信很多阅读龙书/PPA朋友在使用C++之类的语言实现书上的程序分析算法的时候会感觉到无比头疼，甚至是在实现完成之后还是对算法稀里糊涂的。因为这些书在描述算法的时候往往是基于函数式语言来实现的！在我之前对几种常用数据流分析的实现中我也选择了Racket, 实践证明Racket在描述这些算法的过程中非常的丝滑。
不过，在工业界的实践过程中，大多数算法的实现最终都是使用C++的，因为在产品级别的代码中性能是非常重要的，特别是随着算法本身的复杂度提升，比如说过程间分析，如果使用racket去做，就显得非常的捉襟见肘了。C++的性能和程序员的技巧的关系固然是正相关但是却是不成正比的，相信只要稍微写过一点C++的人都会明白我在说什么。

那么有没有一种语言比Racket描述算法更简单，比C++(至少是90%+的程序员写的C++)更加快？
试试Datalog吧！

接下来的文章中我首先会给出Datalog的详细介绍，然后介绍如何用Datalog语言来描述PPA中定义的While Language, 并使用Datalog来实现Live Variable Analysis.

什么是Datalog

Datalog $^1$ 最早是一种在被使用在关系型数据库中的语言，他的语法非常的简单直接，只有如何描述“关系”。准确的说Datalog算不得一门真正的语言，你是没有办法找到一门语言就叫Datalog的(就像LISP)，但是有很多实现, 目前最常见，也是最快的实现是logicblox(商业)和soufflé (开源)。从我个人已知的情况来说，目前soufflé $^2$ 是logicblox的上位替换。所以在接下来的所有介绍中我会主要使用soufflé。总得来说soufflé这门语言是原本Datalog的扩展版。但是里面不是所有东西我都喜欢用，我会略去那些部分。

语法

定义关系谓词

.decl NextNumber(a: number, b: number)

Datalog是一种用来描述关系的语言，在这里面所有东西都是关系(Relation). 从常规编程语言的角度，这就比较像一个函数，这个函数有两个参数a, b，返回是Bool类型。也就是说在datalog中我们只能定义返回真假的函数。

如果relation是一种函数，那当参数取不同值的时候，我们返回到底是真还是假呢？
在datalog的语义模型中，这取决于我们的Rule和Fact.

Fact

NextNumber(1,2).
NextNumber(2,3).

这行代码就是说我们告诉Datalog求解器“1的下一个数是2”。这是一个Fact, NextNumber(1,2) = True。需要注意的是我们并不能告诉Datalog什么是False,但是可以定义Fact

NotNextNumber(2,1).

soufflé支持直接从文件中读取Fact

.input NextNumber(IO=file, delimiter=",")

Consequence Rule

Flow(a, b) :- Edge(a, b).
Flow(a, c) :- Flow(a, b), Flow(b, c). 
// if we have facts Edge(1,2) Edge(2,3), we can also infer fact Flow(1,3)

rule是逻辑规则，等价与

u ⇐ p ∧ q ∧ … ∧ t

这种逻辑表达式被称为Horn Clause.
rule可以递归定义。

输出

.output Flow

输出所有可能的Flow关系，用之前的例子就 Flow(1,2),Flow(2,3),Flow(1,3). soufflé如果这么写会直接输出结果到对应的文件。

这就是所有的datalog syntax啦！
但是要注意Datalog程序还需要满足下面的条件

所有的fact必须接地(ground),也就是说在Fact中只能出现值而不能出现变量，Edge(1,a)就是不合法的
所有在rule头部(:-之前)出现的变量必须在rule体中出现。

这两条规则直接保证了Datalog程序是有限的，一定会停机。换句话说，datalog并不是图灵完备的。

~~如果你对理论没啥兴趣下面小节请跳过~~

语义

介绍datalog的语义之前，先提一下两个概念，

外部数据库(EDB)：程序运行之前由用户提供的Facts。
内部数据库(IDB)：所有在rule在进行逻辑推理运算过程中推论出的间接产生的Facts。

逻辑语义(logic semantic)

我们可以使用经典的一阶逻辑来描述Datalog的语义。

先介绍背景知识。

Datalog rule

L0 :- L1, L2, ...., Lm

等价与一个描述为一个满足斯科伦范式(Skolem Normal Form)的一阶逻辑表达式
$\forall X_1.....\forall X_m(L_1\land .... \land L_m \implies L_0)$

Herbrand Universe(埃尔布朗空间)
对与一个斯科伦化的一阶逻辑表达式S, 他的埃尔布朗空间H可以由如下规则定义：

S中的所有常量属于H, 如果S中没有常量， H包含任意常量c
如果 $t_1\in H, ... t_n \in H$ , 那么 $f(t1, ... ,tn) \in H$

不难看出埃尔布朗空间定义了一阶逻辑中的常量和可以推出的常量。而这和Datalog的Facts直接相信大家都已经可以感觉出联系了。

可以进一步定义Herbrand Base(埃尔布朗基础)：
变量全接地的思科伦范式和他的埃尔布朗空间中的表达式。
也就是说在一个Datalog程序中，埃尔布朗基础表示了这个程序的所有Facts.定义的前半部分也叫外埃尔布朗基础(EHB), 而后半部分则叫内埃尔布朗基础(IHB).

如果S是一个Datalog程序的子句集合，cons(S) 代表所有S的逻辑推论得出的Facts.

现在我们可以来定义语义了。
Datalog程序P, 可以被描述为一个从EHB到IHB的映射关系 $M_p$ , 而所有在EHB中的外部数据库E，总有一个映射 $M_P(E) = cons(P \cup E) \cap IHB$
K和L是两个字面量(不一定接地)，如 $\theta$ 是一个变量替换， $k \theta = L$ , 我们可以说K包摄L,记做 $K ~ \triangleright ~ L$ ,也可以说L是K的一个实例(instance).
而一个Datalog查询G(查询就是比如输出所有关系Edge)可以描述为,（顺序根据包摄关系来）

$\forall E \subseteq EHB, M_{P,G}=\{H | H \in M_p(E) > H \}$

模型论语义(model theory semantic)

我们也可以从模型论的角度来描述Datalog的语义。
模型论是洛文海姆，斯科伦，歌德尔等人发展起来的一门学科, 感谢我的老师Shukai Chin在我初学的时候教了我很多这些知识。它主要是使用Interpretation来描述形式化语义。~~我真的不知道怎么翻译Interpretation，我在国内的时候理论课就没上心过。~~
Datalog的interpretation就是如何给表达式中的变量赋值，每个谓词到底表达了什么样的含义。如果一个子句C在某种interpretation中为真，那么我们称这个interpretation满足(satisfy) C。
对于一条datalog的Consequence Rule, 我们可以有如下的定义。一个Fact F,和一组子句S, 不论在什么样的interpretation下都满足S,那么可以说F follow from S，记做 $S \vDash F$ .
Datalog 这个形式系统满足一种特殊的interpretation,叫Herbrand Interpretation.这种对一阶逻辑的interpretation非常的简单，对于每一个字面常量，我们可以interpret到他本身，对于每一个谓词，我们只能赋已知的常量给其中的变量。

任意一个埃尔布朗解释都对应埃尔布朗基础中的子集t上。在这种解释中所有接地的fact都为true。用数学表达式来写就是
$t \iff p(c_1, ....,c_n)$

一条datalog rule $L0 :- L1, ..., Ln$ 为真对应的就是存在一中变量替换 $\theta$ 能把所有rule中的变量全部替换为常量。用符号表示就是 $L_1\theta \in t ~ \land ... \land L_n\theta \in t \Rightarrow L_0\theta$ .
进一步，如果一个埃尔布朗解释 I满足一组datalog语句S，那我们可以说I是S的一个埃尔布朗模型(Herbrand Model).

而cons(S)可以表达为

从定义中我们不难看出任意两个埃尔布朗模型t1,t2, $t_1 \cap t_2$ 依然是一个埃尔布朗模型，这种性质被称作model intersection property。所有基于Horn Clause的形式系统都具有这个性质。而其中cons 模型是其他所有模型的子集，所以也被称为最小埃尔布朗模型。

证明论语义Proof Theory Semantic

u1s1这部分应该是最重要的语义部分因为涉及很多求值之类的证明，但是我学得不是很好，暂时跳过。。。

Datalog 推论的不动点性质

直接放结论吧：
S 是fact和相关rule的集合， fact1是从现有fact的1步推断，则 Cons(s) 可以表示为：

这里可以看出如果我们的解释满足埃尔布朗模型，那么这个解释就是Ts的不动点，如果是Cons(s)，他是最小埃尔布朗模型，也意味着他是最小不动点。

为什么使用Datalog

其一
从上面的语义中不难看出，datalog虽然说是Prolog的一个子集，但是他们的语义却相差非常的多。Datalog必须是满足Herband Model的，这样他的表达能力其实受到了非常大的限制，但是如果我们把它用在powerset处理，不动点计算上，这个语义模型却是非常合适的。目前非常多的程序分析算法都属于这种情况，所以使用Datalog来做程序分析从语义上来说是非常非常合适的.
第二
正是因为datalog有大量的限制，所以他的求值也和prolog之类的逻辑式编程语言区别非常的大。目前从Bench mark 来看至少soufflé的速度相比其他的约束求解器是非常非常快的。 Soufflé的主要工作方式是，同过templete技巧配合非常高效的数据结构(一个trie)实现从datalog代码最终生成高效C++代码的过程。总得来说，肯定是比你自己手写worklist之类的算法的效率高很多的。

Comparison of Datalog evaluation tools for random-graphconnectivity problem.

Comparison of Datalog evaluation tools for a context-insensitive points-to analysis on the OpenJDK7 library.

我没有soufflé和logicblox的对比benchmark，但是据说logicblox的效率至少并没有比soufflé高。

Case Study: 使用fact来表示PPA中的While language

之前的介绍中应该不难发现datalog是基于一阶逻辑的一种特殊形式，既然是一阶，自然也就不能实现rule或者fact的嵌套。

while language

观察上面的程序我们不难发现，编程语言一般都是有互相嵌套与递归的结构的，这一点如果我们使用c++之类的语言可以用对象直接的组合来实现,如果是使用racket之类的函数式编程。那么利用S表达式，我们对于AST的表示是非常简单的，简直是可以直接输入代码啦23333

(define example2-11
  '((1 = x 2)
    (2 = y 4)
    (3 = x 1)
    (if (4 (> y x))
        (5 = z y)
        (6 = z (* y y)))
    (7 = x z)))

但是datalog的情况其实和c++有点像，我们没有高阶的数据类型，我们只能用类似链表的方式，每一层存放下一级的指针。datalog甚至更惨，它连指针都没有，我们只能人为的用index去代替指针(想象一下你怎么把一个c++对象放到数据库中)

// in datalog in order to discriminate different facts in relational, we need a id for expression
.decl Var(id: number, name: symbol)
.input Var(IO=file, delimiter=",")
.decl Num(id: number, val: symbol)
.input Num(IO=file, delimiter=",")
.decl Bool(id: number, val: symbol)
.input Bool(IO=file, delimiter=",")
// aexpr struture(aexpr which is only aexpr), all op-a here is just binary
// assume facts are always well-formed (`op` is op-a, left/right are aexpr)
.decl AExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input AExprStruct(IO=file, delimiter=",")
// similar to AExprStruct
.decl BExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input BExprStruct(IO=file, delimiter=",")
// relation
.decl RExprStruct(id: number, op: symbol, leftId: number, rightId: number)
.input RExprStruct(IO=file, delimiter=",")
.decl Assign(label: number, var: number, aexprId: number)
.input Assign(IO=file, delimiter=",")
.decl Skip(label: number)
.input Skip(IO=file, delimiter=",")
// if next is -1 means end
.decl Seq(id: number, prev: number, next: number)
.input Seq(IO=file, delimiter=",")
.decl If(id: number, eguardId: number, etrueId: number, efalseId: number)
.input If(IO=file, delimiter=",")
.decl While(id: number, eguardId: number, ebodyId: number)
.input While(IO=file, delimiter=",")

然后再写一堆的.facts 文件，当然实践中fact必须使用别的语言去做parse生成处理。
这也是我觉得目前datalog的弱点之一，没有结构化的fact，导致fact rule很不容易阅读。这种fact被称为"flatten facts"，大量的id让人难以搞清楚实际的类型。soufflé是有类型系统的，但是你们可以看到我只用了symbol和number因为所有别的都只是这两个alias而已.....我其实很不喜欢在datalog上用这样的类型系统，我甚至觉得不如没有类型来的清爽。因为反正flatten以后所有东西都是指针(number)类型。从数据库的角度上来说，这些只是数据库的外键之间互相连接而已。

Case Study: Live Variable Analysis in Datalog

Live variable 相信大部分看过龙书，PPA的同学都不会太陌生，是做dead code elimination中的一个步骤。主要是判断在一个给定的程序位置，某一个变量是否“存活”，即有没有重新定义。

先看PPA上使用类似一阶逻辑的集合语言的描述吧

接下来使用rakcet + chaotic interation算法可以有如下的实现

;; live variable analysis

;; For each program point, which variable may be live at the exit from the point
;; apparently, this can be used in dead code elimination

;; Yihao Sun
;; 2020 Syracuse

#lang racket

(require "tiny-lang.rkt"
         "flow.rkt")

(provide (all-defined-out))

;; left hand var will will kill a var
;; kill-LV : Blocks* → P(Var*)
(define (kill-LV b)
  (match b
    [`(,label = ,(? variable? x) ,(? aexpr? a)) (set x)]
    [`(,label ,(? bexpr? b)) (set)]
    [`(,label SKIP) (set)]))

;; gen all varible in right
;; gen-LV : Blocks* → P(Var*)
(define (gen-LV b)
  (match b
    [`(,label = ,(? variable? x) ,(? aexpr? a)) (list->set (free-vars a))]
    [`(,label ,(? bexpr? b)) (list->set (free-vars b))]
    [`(,label SKIP) (set)]))

;; entry and exit
(define (LV-chaos s*)
  (define lab* (labels s*))
  (define flow-setʳ (flowʳ s*))
  (define init-map
    (for/fold ([res (hash)])
              ([l (in-list lab*)])
      (hash-set res l (set))))
  (define (lv-exit entrym exitm l)
    (define ls-prime
      (for/fold ([res '()])
                ([edge flow-setʳ])
        (match edge
          [`(,from ,to)
           (if (equal? to l)
               (cons from res)
               res)])))
    (if (empty? ls-prime)
        (hash-set exitm l (set))
        (hash-set exitm l
                  (apply set-union
                         (map (λ (l-prime) (hash-ref entrym l-prime))
                              ls-prime)))))
  (define (lv-entry entrym exitm l)
    (define bl (find-block-by-label s* l))
    (hash-set entrym l
              (set-union (set-subtract (hash-ref exitm l)
                                       (kill-LV bl))
                         (gen-LV bl))))
  (define (iter1 entrym exitm)
    (for/fold ([res-entry entrym]
               [res-exit exitm])
              ([l (in-list lab*)])
      (values (lv-entry res-entry res-exit l)
              (lv-exit res-entry res-exit l))))
  (define (iter-to-fix entrym exitm)
    (let-values ([(next-entrym next-exitm) (iter1 entrym exitm)])
      (begin
        (cond
          [(and (equal? next-entrym entrym)
                (equal? next-exitm exitm))
           (values next-entrym next-exitm)]
          [else
           (iter-to-fix next-entrym next-exitm)]))))
  (iter-to-fix init-map init-map))

总得来说，其实kill/gen函数的部分还算是简洁直接，基本上可以直接对PPA上的描述进行直接翻译，但是后面的计算不动点的部分着实是长，而且不容易阅读，第一次做可能也不知道怎么吧Entry/Exit函数和原本的算法结合起来，不够直观。

下面是datalog的

// live variable analysis

// Yihao Sun
// 2020 Syracuse

#include "flow.dl"

// variable "x" is killed at block "l"
.decl KillLV(x: symbol, l: number)
KillLV(x, l) :- Assign(l, vid, _), Var(vid, x).

// varibale "x" is become alive at block "l"
.decl GenLV(x: symbol, l: number)
GenLV(x, l) :- Assign(l, _, a), FreeIn(x, a).
GenLV(x, l) :- BExprStruct(l, _, _, _), FreeIn(x, l).
GenLV(x, l) :- RExprStruct(l, _, _, _), FreeIn(x, l).

// variable "x" is alive when entry/exit block "l"
.decl EntryLV(x: symbol, l: number)
.output EntryLV
.decl ExitLV(x: symbol, l: number)
.output ExitLV

ExitLV(x, l) :-
   LastStmt(fl), l!=fl,
   FlowReverse(lp, l),
   EntryLV(x, lp).

EntryLV(x, l) :- GenLV(x, l).
EntryLV(x, l) :-
   ExitLV(x, l),
   !KillLV(x, l).

不得不说，确实是短

那些为空的情况都不再需要去声明了我们只需要专注于程序pattern match中的interesting case
我们不再需要去手动的计算不动点了，因为datalog的语义保证了我们的计算结果就是不动点，这一点大大简化了代码
对于很多幂集操作我们不再需要辅助函数去获取某种特定类型的信息，可以直接用relation。

总结

Datalog在写数据流分析上来说是几乎完美的，它的语义模型简直就是为了这个应用场景而生的。你需要的不动点计算和幂集操作，都已经在语义当中了。而且Soufflé的生成的C++ code, 也是足够高效，总之，真香。

完整的代码还是在我的ppa-in-code 仓库里

Ref

[1] Ceri, S., Gottlob, G., & Tanca, L. (1989). What you always wanted to know about Datalog(and never dared to ask). IEEE transactions on knowledge and data engineering, 1(1), 146-166.
[2] Jordan, H., Scholz, B., & Subotić, P. (2016, July). Soufflé: On synthesis of program analyzers. In International Conference on Computer Aided Verification (pp. 422-430). Springer, Cham.
[3] Serge Abiteboul, Richard Hull, and Victor Vianu. 1995. Foundations of Databases: The Logical Level (1st. ed.). Addison-Wesley Longman Publishing Co., Inc., USA.