【置顶】Murphi手册

发表于 更新于 分类于 阅读次数：

该博文内容包括：

  • 翻译Murphi Manual

  • 并附上自己的解读和案例

  • 关于Murphi 安装，请看 Murphi入门

Murphi 手册

1. 介绍

1.1 Murphi的组成

  • 编译器：根据Murphi描述语言，生成特定目的的验证器，可以被用来检验系统的性质，比如说错误警告（error assertion），不变量和死锁。

  • 描述语言：高层次的描述性语言，用来描述有限状态的、异步的、并发系统。之所以称之为高级，是因为它具有很多我们现在称之为高级编程语言（Pascal 或 C）的特性，比如用户自定义的数据类型，程序，和带参描述。

1.2 Murphi的前世今生

  • 以前Murphi叫“Trans”，因为它的描述由一系列迁移规则组成。但是因为重名的太多了，就改名叫Murphi。

  • Murphi的一条法则：bug永远都存在于未被测试过的案例中。

  • 1990年夏，因为想要验证缓存一致协议，Ralph Melton, David L. Dill等人想出了两种方法：

    • 基于binary decision模式，用布尔公式来验证
    • 直接将协议写入c++，并用搜索程序来探索所有状态

    最终，他们决定开发一款更好的描述语言和一套验证系统，能够验证协议。

    于是，同年秋，Murphi（那时叫“Trans”）诞生了，但是还太复杂。经过改造和重新实现，次年夏天，该系统已经能够被应用于一些设计，并取得喜人成效。

    直到1992年夏，Murphi经过积累经验和实践打磨，新增了许多便利的特点，比如reasonal loops（有理循环），local variables（局部变量），recursive procedures（递归过程）。Ralph Melton又重写了一遍功能，将murphi变得更适合显式对象，使得实现变得更简洁、简单。

2. Murphi概述

2.1 Murphi描述的结构

  • 声明的常量，数据类型，全局变量，过程
  • 迁移规则集 —— 行为部分
  • 初始状态描述
  • 不变量集（invariant set）

迁移规则集是由一系列“原子的”（不能被打断，一旦开始，必须执行到结束）规则组成，每一个规则都由两部分组成：

  • 条件：当满足条件时（布尔判断），就可以执行对应的行为
  • 行为：可以是改变变量的值等操作。该操作就导致状态的迁移。

迁移规则的条件和行为都是由类Pascal语言写成的。每个行为可以很简单，也可以很复杂，可以包含循环和条件语句。但是无论多复杂，都一定保证它的原子性。

2.2 用Murphi进行验证的四个步骤

  • 写好Murphi程序，后缀为.m
  • 运行Murphi 编译器，生成对应的c
  • 用c++编译器运行c
  • 运行生成的验证器或仿真模型

2.3 Murphi执行模型

Murphi的状态，是指对所有全局变量进行赋值的描述。

所以，Murphi在执行时的描述，就是通过无限循环以下两个步骤，来生成所有可达的状态：

  • 找到所有现在的状态所能满足的规则
  • 随机选择一个可满足的，并执行，产生一个新的状态。

可以注意到，Murphi的描述是非必然性的，因为在第二步骤时，是随机选择的。而这个随机，又不是人为控制的。所以，为了保证Murphi一直正确，就必须保证在所有规则执行的情况下，都是正确的。但是一旦选择要执行某条规则，则下一步的状态就是确定的了。因为只能到达该规则所规定的行为所对应的状态。

这个执行模型可以很好的描述异步系统，这些系统通过消息传送机制可以用Murphi建模，也就是读和写缓冲区变量或数组。

某种意义上，Murphi尽管是随机选择迁移状态来执行，但是验证器会考虑到所有可能的状态，从而验证程序的正确性。通过深度搜索或广度搜索，将可达集存储于一张巨大的哈希表中，这样能够避免重复的工作，而又将可达状态记录下来。

而随着所有状态都被验证器所发掘出来，也就意味着所有可能到达的情况都被检验到了。当检验出程序有错误时，Murphi会提醒“assert”或者“error”，检验器会停下来，然后打印出诊断书，显示出完整的、从初始状态到出错状态的所经过的状态序列。

几种典型的程序错误如下：

  • run-time错误
    • run-time错误可能有很多种，最典型的就是指派越界或数组越界。
  • 不变量被违反的时候
    • 不变量也就是安全性质，是在所有可达状态时都必须满足的状态或要求。当某个时刻，安全性质被违反了，说明程序设计上出现了问题
  • 出现死锁
    • 表现为，除了该状态本身之外，没有其他的后继状态

2.4 Murphi编译器的选项

1
2
3
4
-h            help
-l            print license
-b            use bit-compacted states
-c            use hash compaction.

通常情况下，Murphi默认所有的状态都用1 byte（8bits）记录，这样会使得每个bit不一定都用到。这比每一位都用到的情况下，会多占用2-4倍的内存。但是这样能使Murphi程序运行快将近25%。空间换时间吧。

而”-c”压缩命令使用哈希压缩技术。压缩后大约占40bits，存储与一张哈希表中。详细见8.2

2.5 特殊目的检验器的使用方法

Murphi编译器根据Murphi描述，生成特定目标的检验器。以下是在命令行的一些选项：

  1. 常规
1
2
-h            help.
-l            print license.
  1. 验证策略: (默认: -v)
1
2
3
4
-s            simulate.
-v or -vbfs   verify with breadth-first search. 广度优先搜索
-vdfs         verify with depth-first search.深度优先搜索
-ndl          do not check for deadlock. 不检验死锁
  1. 其他选项: (默认: -m8, -p3, -loop1000)
1
2
3
4
5
6
7
-m<n>         amount of memory for closed hash table in Mb.
-k<n>         same, but in Kb.
-loop<n>      allow loops to be executed at most n times.
-p            make simulation or verification verbose.
-p<n>         report progress every 10^n events, n in 1..5.
-pn           print no progress reports.
-pr           print out rule information.打印规则信息
  1. 错误追踪处理: (默认: -tn)
1
2
3
4
5
6
7
8
-tv           write a violating trace (with default -td).
-td           write only state differences from the previous states.
              (in simulation mode, write only state differences in
               verbose mode.)
-tf           write full states in trace.
              (in simulation mode, write full states in verbose mode.)
-ta           write all generated states at least once.
-tn           write no trace (default).
  1. 规约技术: (default: -sym3 with -permlimit 10 and multiset
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
                          reduction)
-nosym        no symmetry reduction (multiset reduction still effective)
-nomultiset   no multiset reduction
-sym<n>       reduction by symmetry
-permlimit<n> max num of permutation checked in alg 3
              (for canonicalization, set it to zero)
              n | methods
              -----------------------------------
              1 | exhaustive canonicalize
              2 | heuristic fast canonicalization
                  (can be slower or faster than alg 3 canonicalization)
                  (use a lot of auxiliary memory for large scalarsets)
              3 | heuristic small mem canonicalization/normalization
                  (depends on -permlimit)
              4 | heuristic fast normalization (alg 3 with -permlimit 1)
  1. 哈希压缩: (默认: hash compaction with 40 bits 用40bit位进行压缩)
1
2
-b<n>         number of bits to store.
-d dir        write trace info into file dir/sci.trace.

命令选项“-s” 将生成一个仿真器，亦即随机选择规则执行。如果不选择，则默认生成的是验证器，将验证所有的规则。默认的遍历方式是广度优先搜索，如果想换成深度优先，则“-vdfs”

可达集被存储于一张大的哈希表中。它的大小由选项“-m”和“-k”来决定。默认是8Mbytes。存储于文件”mu_prolog.inc” 中的常量”gPercentActiveStates” 可以用来调整深度或广度优先搜索的队列的性能。

3 基本概念

3.1 Backus-Naur Form (BNF)

巴科斯范式，一种形式化符号来描述给定语言的语法，现用来定义编程语言的语法规则

BNF的句法如下：

1
2
3
4
5
<> denote nonterminals;   非终结符号
[] denote optional sections;   可选部分
{} denote repetition zero or more times.   重复0-n次
a | b denotes either a or b.   a或者b
() denote grouping.  组

当在语句中需要使用到这些符号时，需要在前面加上“\”加以区分

3.2 词法惯例

以下是Murphi中的保留字：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
alias           array           assert          begin           
boolean         by              case            clear
const           do              else            elsif
end             endalias        endexists       endfor
endforall       endfunction     endif           endprocedure
endrecord       endrule         endruleset      endstartstate
endswitch       endwhile        enum            error
exists          false           for             forall
function        if              in              interleaved
invariant       of              procedure       process
program         put             record          return
rule            ruleset         startstate      switch
then            to              traceuntil      true
type            var             while

有些保留字现在还没有用到，但是以后可能会用于扩展，它们是：“in, interleaved, process, program, traceuntil.”

大小写敏感： 除了保留字（ ‘Begin’ 和‘BeGiN’ 一样），其他的都是大小写敏感的。

同义词： 保留字‘end’可以替换‘endrule’和‘endfor’

标识符：标识符是由字母，下划线，数字组成的序列，其中数字前面必须有字字母。标识符以下划线开头。下文用表示。

字符串：用双引号引起来的里面的字母序列。下文用表示

整数常量：10进制。下文用表示

注释：有两种注释方式：

1
2
 -- comments1 
／* comments2 *／

3.3 程序结构

  • 程序声明
  • 规则集（包含初始状态）
  • 不变量／安全性质

Murphi程序隐式生成一个状态图。状态是指所有全局变量指派值的情况。初始状态在规则集中有声明。接下去的状态由迁移规则决定。

4 声明

4.1 常量、类型、变量声明

1
2
3
<decl> ::=	const { <constdecl> ; }
	 |	type { <typedecl> ; }
	 |	var { <vardecl> ; }

常量

常量一定要赋值，这样在编译时才会被执行。常量会被取整。

1
2
3
Const   
   I: 2;
   J: 31415 * I / 9;                 -- J will be 6981

类型

特殊的枚举类型——布尔是预先定义的，由true或false组成。整数类型没有预先定义，因为如果无限制范围的整数会造成严重消耗内存。

简单类型有：布尔、枚举、有限范围的整数。

复合类型有：简单类型组成的数组、复合类型或简单类型的记录。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Type
   val_t: 0..99;                     -- simple types.
   ind_t: 1..i;
   enum_t: enum { x, y, z };
   b: boolean;

   r_t: record f:0..1; g: 0..2; end; -- Record.
   rr_t: record r: r_t; s: r_t; end; -- Record of record.

   a_t: array [ ind_t ] of 19..29;   -- 1-dimensional array.
   aa_t: array [ ind_t ] of a_t;     -- 2-dimensional array.

   ar_t: array [ 1..2 ] of r_t;      -- Array of record.
   ra_t: record a1: a_t; foo: ind_t; end;     -- Record with array.

   ae_t: array [ enum_t ] of enum_t; -- Array with enum index and range.
   aae_t: array [ ind_t ] of ae_t;   -- 2-dim array, 2nd index is enum.
   re_t: record f: enum_t; end;      -- Record of enum.

变量

1
2
3
4
Var
   val : val_t;
   arr : ae_t;
   rec : record foo: ind_t; bar: boolean; end;

4.2 子程序和函数声明

子程序和函数必须声明在程序的最外层，即不包含于规则或执行体内部。

  • 函数，function，一定要有返回状态
  • 子程序，procedure

参数列表表示：

1
2
function add(var x,y: val_t):val_t;
procedure add(var x,y: val_t);

注意：

  • 不带参的子程序和函数，仍然需要括号括出来一个空的参数列表。

  • 从上面的代码可以发现，function的后面还带有返回值的范围，而procedure则没有

  • val_t是一个自定义类型，可以定义成一定范围的整数，比如：

1
2
type
	val_t:0..100;
  • 参数列表中，形参的值由实参传入。如果用var开头作为形参的声明，则说明其值可改，而如果不是var开头，则在子程序或函数中，实参的值不可更改。
  • 形参的声明和局部声明，将会覆盖其原本在外部的声明。比如，全局变量x本来声明为5. 在子程序内，将其赋值为3，则其在全局的值也变成3了。
例子：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
procedure Swap(var i, j: val_t); -- 子程序，执行交换i，j的值
var temp: val_t; 
begin
  temp := i;
  i := j;
  j := temp; -- 直接交换
end;

                                        --函数，执行+2操作
function plustwo(input: val_t): val_t;  -- 可以看到input没有声明成var，所以其值在函数中不可改变
const two : 2; 
begin
  return (input + two);  -- 需要返回值。 
end;

5 表达式

  • 类型的相等，是通过自定义的类型名称来决定的
  • 整数表达式是否合法，与其语句正确与否不相关
  • 布尔类型与整数类型无法相比
  • 尚未赋值的变量无法取值，这种错误会当做run-time error，运行时错误
  • 数组越界也会在运行时检查到

指代

1
<designator> :=	<ID> { . <ID> | \[ <expr> \] }

比如，student.name这种类型表示域的，或选择数组中的某个元素，都是“.” 操作。

表达式（与c语言几乎一样）：
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
| <designator>
| <integer-constant>
| <ID> \( <actuals> \)		-- a function call.
| forall <quantifier> 
  do <expr> endforall		-- universal quantification.
| exists <quantifier>
  do <expr> endexists		-- existential quantification.
| <expr> + <expr>
| <expr> - <expr>
| <expr> * <expr>		-- multiplication.
| <expr> / <expr>		-- integer division.
| <expr> % <expr>		-- remainder. “%”号两边必须是整数
| ! <expr>			-- logical negation.
| <expr> | <expr>		-- logical disjunction. 合取，即并集
| <expr> & <expr>		-- logical conjunction. 析取，即交集
| <expr> -> <expr>		-- logical implication. 逻辑蕴含
| <expr> < <expr>
| <expr> <= <expr>
| <expr> > <expr>
| <expr> >= <expr>
| <expr> = <expr>
| <expr> != <expr>
| <expr> ? <expr> : <expr>	-- C-style conditional expression.

运算符

运算优先级与c一样，不赘述

forall 和 exists 操作符

量化命题的时候会用到，类似于全称和存在命题。

6 条件语句

注：原文写的是 statement，但是因为看下面的语句都是条件语句，所以直接翻译成条件语句了

if
1
2
3
4
5
if x > 0 then
	x := x-1;
	else
	x := 0;
end;
while
1
2
3
while x > 0 do
	x := x-1;
end;
switch
1
2
3
4
5
switch x
	case 1: x:= x-1;
	else 
	x := 0;
end;

注：无限循环是一个运行时错误，但是murphi有限制，默认最多循环1000次，这个值可以用户自定义。

别名

注意看别名是用指针还是数值赋值的。通过以下例子就能理解：

1
2
3
4
5
6
7
8
9
10
-- i = 2 beforehand; arr[2] = 1. 一开始的时候，i = 2
alias
  foo : arr[i] 	-- foo gets identified with arr[2]
  bar : arr[i] + 1	-- bar gets identified with 2.
do
  arr[i] := 3;	-- now, foo = 3, but bar = 2.
  i := 1;		-- foo is still bound to a[2]. 
  foo := 4;		-- arr[2] is now 4. bar = 2.
  bar := 2;		-- Illegal. 因为arr[1]没有赋值
end
函数调用

常数形参可以由任意可比较的实参传递得到； 变量参数（以var开头的形参）只能被同类型的带值的实参传递； 类型序列作为参数的时候，只能由同种类型的、被赋值的类型序列传递得到。

清除
1
clear x；

这个操作用来清除该类型的所有组成部分，将所有值降到最低。枚举类型则还原成初始赋值。布尔类型赋值成false。

**注意**：clear这个命令常常用来清除那些不感兴趣的变量。如果不这样的话，验证的时候就会产生很多不必要的状态。但是这个方法不要乱用。
报错

就像抛出异常一样。两种写法是等同的。

1
2
assert x < 0 "error!";
if x < 0 then error "error!" end;
输出
1
put "\n";

可以输出字符串或表达式，且每一次经过该状态都会执行，所以常常在验证时会产生大量的输出（因为需要大量的重复）。所有一般用于调试，并生成文件。

函数返回

函数必须有返回值，且返回值的类型必须等于规定的返回值类型。

7 规则集，初始状态，不变量

规则

  • 迁移规则集由很多条规则组成
  • 每一条规则都由条件和动作组成
    • 如果没有规定条件，则代表该规则永远成立
  • 每一个动作代表状态的一次迁移，所以叫做迁移规则
  • 状态即所有全局变量的一次全体赋值情况

每一条规则内，可以再声明局部变量、常数和自定义类型，但都与全局变量无关，亦即，不是状态的一部分。

如果一条规则，既没有条件，也没有行为，在句法上是可行的，但是因为parse对于这样的规则常常会进行忽略处理，所以就算该规则没有条件，也要写上begin开头的动作。

1
2
3
4
5
6
7
rule		   			rule
  <condition>				  <decls>
==>					begin
  <decls>		-->		  if <condition>
begin					    <body>
  <body>				  end
end					end

这两种写法都是可以的。一种看成先有条件，条件满足才能进入规则；另一种看成可以进入规则，然后再进行条件判断，如果不满足条件，则不执行，状态也没有改变。

  • 如果程序没有规则，则程序错误。因为Murphi的程序结构是需要保证的。

初始状态

  • 初始状态可以看成特殊的规则，它只会在程序执行的一开始执行，之后就不会再执行了。
  • 初始状态一定要对所有全局变量进行赋值，否则会被检测器抓住的～
  • 如果没有初始状态，则程序错误。
1
2
3
4
startstate
	y := 5;
	x := 10;
end;

不变量／安全性质

在形式化方法中，很重要的组成部分。它的范围>=可达集的范围。指的是，在所有可达状态下，都能保证的性质；一旦不满足该性质，则程序终止。

1
2
invariant "safe"
	x = 1;

这个写法，实际上等同于一个特殊的规则：

1
2
3
4
5
rule
	x != 1;
==>
	error "Invariant violated！";
end;
  • 很多程序员认为，自己写assert 或error，比用invariant更方便。但实际上，使用invariant对于编译器而言更高效。

规则集

规则集是迁移规则的集合，可以看作是一个语法小秘方，能够对所有的量化对象（有取值范围的、可以取好多值的那种类型，类似于一个迭代器）创建一个拷贝。比如：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
Type player_t : 0..1;
Var Players : Array[ player_t ] of Record;
			       hasball, gotball: boolean;
			     End;

Ruleset p : player_t Do
  Alias ping: Players[p];
        pong: Players[ 1 - p ] Do

      Rule "Get ball"
        ping.gotball
      ==>
      Begin
        ping.hasball := true;
        ping.gotball := false;
      End;
  End;
End;

可以看到，player_t有两个取值，看成一个quantifier量词。规则集对于p，也就有两种取值，0和1。 如果不用规则集，则对于p的不同取值，需要把这些规则写两遍，但是有了规则集，对于这些不同的取值，只需要写一遍规则，即可对所有的取值情况的状态都进行遍历，并得出状态的并集，生成可达集。而这就需要别名alias来实现。因为别名经过一次指派之后，都只会遵从原来指派的那个值或表达式，不会改变，这就保证了在哈希表中，对于同样的状态，即使是不同的p的取值，也能表示相同的状态。（这个概念很复杂，是自己的理解之后写的，还有待以后加深理解之后来验证）