Program Verification 02 - Operational Semantics
# 前置知识
在阅读本文档前,请确保你已掌握布尔逻辑的基础知识,详见 Program Verification 知识板块中的 01 - Basic Logic 文档。
在阅读本文档前,请确保你已掌握 BNF 范式。详情请自学编译原理,暂无相关文档,敬请谅解。
# 前言
操作语义 (operational semantics) 是编程语言执行的数学模型,或者说是程序在抽象机器上的执行的释义。操作语义是编程语言的形式化规范,可用于精确理解编程语言中表达式的含义,或用于对编程语言进行严格的形式化验证。
- 操作语义很像是语言的解释器,不同的是,前者是基于数学定义的,后者是基于编程语言本身定义的。
结构化的操作语义 (structural operational semantics, SOS) 提供了一个能为编程语言和形式化语言提供操作语义的框架,其直观的吸引力和灵活性使其得到广泛应用,包括并发进程的语义研究、软件静态分析、编译器正确性证明等。
- SOS 可以分为 small-step 和 big-step 两种,前者描述执行中的每个步骤,后者描述执行的总体结果,详见下文。
本文将基于 IMP 介绍 SOS 的相关概念。
# IMP
# 基本概念
IMP 是一种简单的、non-procedural 的 命令式语言 (imperative language) ,它只有一个条件命令和一个 while 命令,主要用于描述基本算术表达式。
IMP 的基本语法定义如下:
整数域
布尔域
值域
变量标识符
算术表达式
布尔表达式
命令
# IMP 形式化规则
IMP 对表达式的形式化规则如下:
# Expression
e ::= a | b
# Arithmetic Expression
a ::= int
| id
| a + a | a - a | a * a | ...
# Boolean Expression
b ::= bool
| b > b | b < b | b == b | ...
| b and b | b or b | not b | ...
IMP 对命令的形式化规则如下:
# Command
c ::= skip
| id := a
| c; c
| if b then c else c
| while b do c
# IMP 状态
在 IMP 中,状态是从变量到值域的映射,即 。
我们将 非终结配置 (non-terminal configuration) 形式化为一个二元组 ,表示(算术或布尔)表达式 正在状态 下等待演算。类似地, 表示命令 正在状态 下等待执行。
# Small-Step SOS
# 基本概念
small-step SOS 又称为 transitional semantics ,它描述了执行中的每个步骤。
可以将 small-step SOS 视为一个能够 step-by-step 地执行给定代码的机器。
小步语义可以清楚地为复杂特性建模,比如并发、divergence 和运行时错误。
small-step SOS 的形式化定义包括三个部分:
configuration :对 IMP non-terminal configuration 的简记。
transition :一组等待推导的 configuration 。
rule :描述了基于 transition 推导 configuration 的规则,表示为如下形式,其中 前提 (premise) 是零至多个 transition 或 equation ,结论 (conclusion) 是一个 transition :
非形式化地讲,rule 的含义是在 premise 成立的情况下可以将 conclusion 式左的 configuration 推导到式右的 configuration 。
注意,形式化定义不是唯一的,原则上只需形式语义规范、语法合适、逻辑正确即可。本文仅提供了一种我个人最喜欢的定义,读者仅在参考资料中就能找到好几种不同的形式化定义,但本质上都是等价的。
# 表达式演算规则
在表达式演算中,transition 表现为如下两种形式之一,其中 :
我们以算术表达式的加法为例,定义 的表达式演算规则如下:
这里给出一个简单的实例来帮助理解。
设 ,则对于 有:
对于算术表达式的其它运算符,以及布尔表达式的运算,均有类似规则,不予赘述。不过,一元布尔运算符稍有不同:
事实上,我们可以将所有二元(算术或布尔)运算符的 和 规则结合为更简洁的一条规则:
其中 定义为:
E[] ::= [] + e | int + []
| [] - e | int - []
| ...
对于更复杂的表达式(例如多元的、复合的),可以递归或归约地进行演算,并构造出对应的 派生树 (derivation tree) 。
# 命令执行规则
在命令执行中,transition 表现为如下两种形式之一:
注意 和 。与表达式的演算不同,命令的执行可能会改变状态。
对于状态 ,定义 如下:
定义 skip 命令的执行规则如下:
定义赋值命令的执行规则如下:
定义多条命令展开的执行规则如下:
定义 if 命令的执行规则如下:
定义 while 命令的执行规则稍微有些特别。如果我们简单地仿照 if 命令进行形式化,将无法处理 的情况:
事实上,我们应当在每次循环中对 while 命令执行 transition rule ,而不是在第一次 transition 时就将 替换掉。
我们可以将循环展开:
也可以借助 if 命令,这仅需一条规则就能完成形式化:
# 多步执行
定义 为 的自反传递闭包,有如下归约表示:
亦可用 -step 的方式表示:
# 有关 transition 的性质
对于表达式 ,不存在无限长的推导序列 ,最终必然会归约到 。
而对于命令 ,可能存在无限长的推导序列,例如无限循环 。
# 扩展规则
在上述基本规则的基础上,我们追加定义三种新的规则。
# Abort
如果语言归约得到 ,则不能再继续归约,这可能在除零或非法数据访问等情况下出现:
其中 。
同时要为命令追加定义,这里省略了类似的 while 命令:
注意 abort 的含义是 go wrong 而非 get stuck 。
- 若 ,则称命令 gets stuck 。
# Local Variable Declaration
在 IMP 中追加规则:
c ::= ...
| newvar id := e in c
变量声明的形式化定义并不那么容易,例如下面的规则就是一个不完备的例子,因为局部变量 的值可能在 执行时暴露给外部观察者,这会在并发环境下成为问题:
一种正确定义的规则如下(from Eugene Fink):
注:第一条我还未能完全理解,先放着。
# Dynamic Memory Allocation
对 IMP 基本语法进行扩展:
- 可用的内存地址范围
- 值域
对 IMP 状态进行扩展,重新定义 ,其中:
,即原先的 IMP 状态。
,这是一个 partial mapping ,描述了从内存地址到值域的映射。
在 IMP 中追加规则,其中 [x]
表示从地址 中取值:
c ::= ...
| x := alloc(e) | free(x)
| y := [x] | [x] := e
记 configuration 为 。
定义 alloc / free 命令的执行规则如下:
定义 lookup / mutation 命令的执行规则如下:
# Small-Step Contextual SOS
small-step contextual SOS 又称为 reduction semantics ,是另一种形式的 small-step SOS 。
small-step contextual SOS 的形式化定义包括三个部分:
redex :可以通过一步原子步骤进行归约的句法表达式或命令,记为 。
evaluation context, or reduction context :“挖了洞”的表达式或命令,记为 。
local reduction rule :基于 构建的局部归约规则,指示了如何为每个 redex 执行归约。
global reduction rule :基于 和 构建的全局归约规则,指示了下一步要演算的 redex 。
# Redex
r ::= x
| int + int | int - int | ...
| x := int
| skip; c
| if true then c else c | if false then c else c
| while b do c
| ...
# Evaluation Context
ε ::= []
| ε + e | ε - e | ...
| int + ε | int - ε | ...
| x := ε
| ε; c
| if ε then c else c
| ...
small-step contextual SOS 的核心 idea 是:
将当前项(表达式或指令)分解为 redex 和 evaluation context(事实上是原项中除 redex 外的部分);
根据局部归约规则将 redex 归约为更简单的形式;
将简化后的项放回到 evaluation context 中。
这可以形式化为如下的 small-step 规则,称为全局归约规则:
evaluation context 有且仅有一个“洞”,“洞”的位置唯一标识了下一步要演算的 redex 。我们用 表示将 中的洞替换为 redex 所得的表达式。
- 例如对于 有 。
small-step contextual SOS 以 递归分解 (recursive decomposition) 的形式进行演算,每一步演算的 solution 都是唯一的。其分解定理可描述为:
若表达式 还未转换为 ,则存在唯一的 和 ,使得 。
若命令 还未转换为 ,则存在唯一的 和 ,使得 。
下面给出几个分解的示例:
对于 及其分解 :
若 还未转换为 ,则 ;
若 而 还未转换为 ,则 ;
若 且 ,则 。
对于 及其分解 :
若 还未转换为 ,则 ;
若 ,则 。
# Big-Step SOS
# 基本概念
big-step SOS 又称为 natural semantics 或 relational semantics ,它描述了执行的总体结果。
可以将 big-step SOS 视为一个递归解释器,能对于给定的代码和状态给出演算结果。
在某些情况下,小步语义的细致性是不必要的,大步语义将小步语义中那些指定求值顺序的“枯燥”规则折叠起来,使规则变得更少、证明变得更快。
然而在大步语义中,所有没有 final configuration 的程序(例如无限循环、get stuck 等)看起来都一样,因此我们有时无法用大步语义证明与此相关的内容。
big-step SOS 的形式化定义同样由 configuration 、transition 和 rule 三个部分组成。
不同的是,大步语义的一步 transition 直接描述了演算的结果,而不考虑演算过程的中间状态:
# 表达式演算规则
我们以算术表达式的加法为例,定义 的表达式演算规则如下:
# 命令执行规则
定义 skip 命令的执行规则如下:
定义赋值命令的执行规则如下:
定义多条命令展开的执行规则如下:
定义 if 命令的执行规则如下:
定义 while 命令的执行规则如下:
# 有关 transition 的性质
small-step 语义和 big-step 语义的等价性:
# 更多
# 大步语义推导
我们用记号 表示大步语义的推导结果:若 ,则 。
# 伪状态
伪状态 (pseudo-state) 指的是不能成功终止的程序状态,用 表示,并且有 。
若 ,则称从状态 出发执行程序片段 导致 发散 (diverge) ,其中 是表示程序因始终运行而不能终止(例如死循环)的伪状态。
若 ,则称从状态 出发执行程序片段 时出现 运行时错误 (runtime error) ,其中 是表示程序因出现错误而无法正常终止的伪状态。
# 操作语义的运用
Sample 1 :
IIT-CS536 Samples. TBD.
# 参考资料
Univ of Parma - SOS-intro-1.pdf (opens new window)
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01