高级农民
- 积分
- 2725
- 大米
- 颗
- 鳄梨
- 个
- 水井
- 尺
- 蓝莓
- 颗
- 萝卜
- 根
- 小米
- 粒
- 学分
- 个
- 注册时间
- 2017-6-18
- 最后登录
- 1970-1-1
|
Kafka的exactly-once semantics实际上是比较常见的滥用semantics这个词的情况,其大概意思就是你按照Kafka规定的某种方式去调用它的API,那么观察到的系统的输入输出会满足一些规律/约束(也就是exactly-once)。
一般我们说某某语言满足XXX-semantics,那么XXX实际上是描述该语言的语义的某种性质的形容词,而“语义”本身首先得有个形式上(formal)的定义。比如说数据库系统的SQL语言的语义可以是扩展的relational calculus with bag-semantics,而Kafka各种讨论exactly-once semantics的文章都没有给出一个Kafka semantics的定义 —— Kafka甚至都没有设计一个语言,只是提供了一堆API加参数设定而已。
那么所谓“语义”直观上到底长什么样?这里随便找个SQL语言的例子:https://homepages.inf.ed.ac.uk/libkin/papers/pvldb17.pdf
上面这篇文章里给出的一堆公式就是定义语义的例子。当然这里只是给个直观印象,可以不去理解它到底是在说什么,下面我会写一点更简单的解释。
首先,“语义”是与“语法”成对存在的概念,语法简单来说是指由字符构造字符串的规则,而语义则是解释所构造的字符串的意义。注意这里有个套娃:我们描述语法A的语义的时候也是要用某种语言B的,B一般是数学语言(各种字母、符号与运算符等等),就好像我们用C去写Python的解释器一样,
而Semantics这个词常用的领域有几个:
(1) 语言学(linguistics),一般是研究自然语言的语义
(2) 数理逻辑(mathematical logic),考虑的是形式语言(formal language)的语义
(3) 程序设计语言理论(programming language theory),考虑的是程序设计语言的语义
其中(1)、(2)这里就不讨论了。(2)是CS理论基石,比如著名的哥德尔完备性定理(Gödel's completeness theorem,注意还有个“不完备性定理”更著名)就是说在一阶谓词演算系统中,一个在所有模型中语义为真的公式一定可以通过语法层面的证明在有限步骤内推出。
(3)的相关知识一般在Programming language concepts(国内一般叫“程序设计语言原理”或者“程序设计语言概论”)这门课上会讲,主要分为三类:
(3.a) 过程语义(procedural semantics)
(3.b) 指称语义(denotational semantics)
(3.c) 公理语义(axiomatic semantics)
这三种语义理论上分别对应三大语言范式:过程式、函数式与逻辑式。不过在实践中都是混用的,我们也可以用指称语义去描述过程式语言中一个函数的行为,或者用过程语义去描述逻辑式语言的一段代码(例如Prolog里面的cut操作)。
其中(3.a)是最常用的理解一段代码行为的方式,程序员入门时一般都是学习的过程语义。也就是想象有台虚拟机一行一行执行代码,每执行一行代码会改变这台虚拟机的状态(也就是各种变量的值),然后控制流(control flow,例如if、for loop)会决定下一行要执行的代码是什么。过程语义的缺点是太复杂琐碎,理论上难以分析,除非是超级简化的情况如老祖宗图灵机 —— 学计算理论(theory of computation)这门课的时候会让你用过程语义去证明图灵机的一些性质。
(3.b)又叫数学语义(mathematical semantics),在理论以及实践中都很实用,经验丰富的程序员也会主动用denotational semantics去理解代码、设计抽象、架构系统。上面那个讲SQL语义的论文就是denotational semantics的例子。它主要是将一段代码的输入输出描述成数学对象,然后用数学语言表达代码的行为。比如说一个sum函数,其输入就是“数组”这么一个数学对象,而语义可以表达为“数组中元素之和”(Σ)这么一个数学算子(operator),我们不用关心这个“和”的计算过程:比如说,可以从第一个元素累加到最后一个元素,也可以倒过来从最后一个元素累加到第一个元素。
Denotation semantics的一个简单的例子是整数四则运算,可以看看这个:http://homepage.divms.uiowa.edu/~slonnegr/plf/Book/Chapter9.pdf
(3.c)的话在PL领域非常常见,PL论文一大俗就是要放点公理语义在上面。直观印象就是一堆大横线描述逻辑推导过程,还是上面那本书的例子:http://homepage.divms.uiowa.edu/~slonnegr/plf/Book/Chapter11.pdf
最后回到Kafka的讨论,如果Kafka要严谨地定义exactly-once semantics,那大概至少需要这三点:
(1) 列出Kafka的完整语法(各种API)。
(2) 在语法结构上定义出语义。使用denotational semantics的话,也就是要明确a domain of mathematical objects(对于Kafka来说应该是消息流加上一些分布式状态),以及将语法(调用API的代码字符串)映射到数学对象状态的函数集合S。
(3) 定义exactly-once semantics,其本质上是描述函数集合S某些性质的一个定理。
补充内容 (2020-8-3 06:56):
有一点说错了是没有“过程语义”这个词.. 应该是“操作语义”(operational semantics) |
|