perfbook-c12

30/07/2021 00:00

点击量：次

perfbook

perfbook

并行编程

书籍

形式化验证

12 Formal Verification

正确性检查是有意义的，但是与原始算法一样，易于出现人工错误。而且，不能期望正确性证明找到你的需求前提、需求缺陷，对底层软件、硬件原语的误解，或者没有考虑到进行证明的地方所引起的错误。这意味着形式验证的方法不能代替测试。
拥有一个工具来找到所有竞争条件是非常有用的。一些这样的工具已经存在：

对通用目的的状态空间搜索工具Promela语言及它的编译器Spin
特殊目的的ppcmem及cppmem工具
SAT求解器

12.1 State-Space Search

12.1.1 Promela and Spin

基本原理：
用类似于C语言的Promela来重新编写算法，并进行正确性验证。然后使用Spin来将其转化为可以编译运行的C程序。最终的程序执行对你的算法进行一个全状态搜索，它要么确认通过验证，要么发现包含在Promela程序中的断言的反例。 适用范围：
在算法复杂但是小的并行程序。
可以考虑使用此工具来构造测试用例。
缺点： Promela并不理解内存模型及任何类型的乱序语义。

Spin
相关参考书籍

12.1.1.1 Promela Warm-Up: Non-Atomic Increment

测试代码atomicincrement.spin：

#define NUMPROCS 2

byte counter = 0;
byte progress[NUMPROCS];

proctype incrementer(byte me)
{
	// me是进程编号，由后面的初始化代码进行设置
	int temp;

	atomic {
		temp = counter;
		counter = temp + 1;
	}
	progress[me] = 1;
}

init {
	int i = 0;
	int sum = 0;

	atomic {
		i = 0;
		do
		:: i < NUMPROCS ->
			progress[i] = 0;
			run incrementer(i);
			i++
		:: i >= NUMPROCS -> break
		od;
	}
	atomic {
		i = 0;
		sum = 0;
		do
		:: i < NUMPROCS ->
			sum = sum + progress[i];
			i++
		:: i >= NUMPROCS -> break
		od;
		assert(sum < NUMPROCS || counter == NUMPROCS)
	}
}

测试输出结果:

pan: assertion violated ((sum<2)||(counter==2)) (at depth 20)
pan: wrote increment.spin.trail
(Spin Version 4.2.5 -- 2 April 2005)
Warning: Search not completed
+ Partial Order Reduction
Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +
State-vector 40 byte, depth reached 22, errors: 1
45 states, stored
13 states, matched
58 transitions (= stored+matched)
51 atomic steps
hash conflicts: 0 (resolved)
2.622 memory usage (Mbyte)

对输出的trail文件进行分析：

Starting :init: with pid 0
proc 0 (:init:) line 20 "increment.spin" (state 1) [i = 0]
proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
Starting incrementer with pid 1
proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
proc 0 (:init:) line 22 "increment.spin" (state 2) [((i<2))]
proc 0 (:init:) line 23 "increment.spin" (state 3) [progress[i] = 0]
Starting incrementer with pid 2
proc 0 (:init:) line 24 "increment.spin" (state 4) [(run incrementer(i))]
proc 0 (:init:) line 25 "increment.spin" (state 5) [i = (i+1)]
proc 0 (:init:) line 26 "increment.spin" (state 6) [((i>=2))]
proc 0 (:init:) line 21 "increment.spin" (state 10) [break]
proc 2 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
proc 1 (incrementer) line 10 "increment.spin" (state 1) [temp = counter]
proc 2 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
proc 2 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
proc 2 terminates
proc 1 (incrementer) line 11 "increment.spin" (state 2) [counter = (temp+1)]
proc 1 (incrementer) line 12 "increment.spin" (state 3) [progress[me] = 1]
proc 1 terminates
proc 0 (:init:) line 30 "increment.spin" (state 12) [i = 0]
proc 0 (:init:) line 31 "increment.spin" (state 13) [sum = 0]
proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
proc 0 (:init:) line 33 "increment.spin" (state 14) [((i<2))]
proc 0 (:init:) line 34 "increment.spin" (state 15) [sum = (sum+progress[i])]
proc 0 (:init:) line 35 "increment.spin" (state 16) [i = (i+1)]
proc 0 (:init:) line 36 "increment.spin" (state 17) [((i>=2))]
proc 0 (:init:) line 32 "increment.spin" (state 21) [break]
spin: line 38 "increment.spin", Error: assertion violated
spin: text of failed assertion: assert(((sum<2)||(counter==2)))
proc 0 (:init:) line 38 "increment.spin" (state 22) [assert(((sum<2)||(counter==2)))]
spin: trail ends after 21 steps
#processes: 1
counter = 1
progress[0] = 1
progress[1] = 1
proc 0 (:init:) line 40 "increment.spin" (state 24) <valid end state>
processes created

可见，初始化块的第一部分创建两个递增的进程，其中第一个进程获得计数器，然后两个进程都递增并保存它，这丢失了一个计数。随后断言被触发，然后最终状态被显示出来。

12.1.1.2 Promela Warm-Up: Atomic Increment

将12.1.1.1中的递增更换成原子操作可修复该bug，随着线程数量的增大，该工具占用内存会变多，如下所示：
这是Promela的局限所在，但在服务器端不存在这个问题。

12.1.2 How to Use Promela

spin -a qrcu.spin

给定一个源文件qrcu.spin，创建对应的c文件pan.c

cc -DSAFETY -o pan pan.c

pan．c编译生成的状态机搜索程序。-DSAFETY可提高程序运行的速度

./pan

运行状态机程序pan。

spin -t -p qrcu.spin

生成某次运行产生的跟踪文件，该运行遇到某些错误，并输出产生错误的步骤。

12.1.2.1 Promela Peculiarities

注意Promela语言和C语言的差异，作者在此提供了一些Promela编程的建议，值得参考。

12.1.2.2 Promela Coding Tricks

构造内部乱序用例:

if
:: 1 -> r1 = x;
  r2 = y
:: 1 -> r2 = y;
  r1 = x
fi

状态压缩：
如果有复杂的断言，在atomic块内赋值。
Promela不提供函数。必须使用C预处理宏来代替。

12.1.3 Promela Example: Locking

使用Promela的语言写的自旋锁如下lock.h所示：

#define spin_lock(mutex) \
    do \
    :: 1 -> atomic {\
            if \
            :: mutex == 0 -> \
                mutex = 1; \
                break \
            :: else -> skip \
            fi \
        } \
    od

#define spin_unlock(mutex) \
	mutex = 0

不需要内存屏障，因为Promela假设是强序的。正如之前提示及随后的例子将所看到的那样，弱序模型必须显式地编码。

测试该锁：

#include "lock.h"

#define N_LOCKERS 3			

bit mutex = 0;				
bit havelock[N_LOCKERS];		
int sum;				

proctype locker(byte me)		
{
	do
	:: 1 ->
		spin_lock(mutex);	
		havelock[me] = 1;	
		havelock[me] = 0;	
		spin_unlock(mutex)	
	od
}					

init {					
	int i = 0;
	int j;

end:	do 
	:: i < N_LOCKERS ->
		havelock[i] = 0;	
		run locker(i);		
		i++			
	:: i >= N_LOCKERS ->		
		sum = 0;		
		j = 0;			
		atomic {		
			do
			:: j < N_LOCKERS ->
				sum = sum + havelock[j];
				j = j + 1
			:: j >= N_LOCKERS ->
				break
			od
		}			
		assert(sum <= 1);	
		break			
	od
}					

12.1.4 Promela Example: QRCU

QRCU的作用：
QRCU是SRCU的变体，如果没有读者，优雅周期将在1μs内检测出来。与之相对的是，绝大部分其他RCU实现则有几毫秒的延迟。
使用Promela实现QRCU算法并验证。

12.1.5 Promela Parable: dynticks and Preemptible RCU

在最近的Linux内核中，可抢占RCU可能使最近的Linux内核失去了一个有价值的节能功能。
Steve编写rcu_irq_enter()和rcu_irq_exit()接口,Paul从2007年10月到2008年2月反复审查代码，每次几乎都能够找到至少一个BUG。
于是他决定使用Promela和 Spin的帮助一次性把bug都找出来。
下面描述该模块的各个接口。
12.1.5.1 Introduction to Preemptible RCU and dynticks 12.1.5.2 Task Interface 12.1.5.3 Interrupt Interface 12.1.5.4 Grace-Period Interface

12.1.6 Validating Preemptible RCU and dynticks

本节一步一步地开发一个用于dynticks和RCU之间接口的Promela模型，每一节都举例说明每一个步骤，将进程级的dynticks 进入、退出代码及优雅周期处理代码翻译为Promela。

12.1.6.1 Basic Model 12.1.6.2 Validating Safety 12.1.6.3 Validating Liveness 12.1.6.4 Interrupts 在Promela中模拟中断的方式： 12.1.6.5 Validating Interrupt Handlers 12.1.6.6 Validating Nested Interrupt Handlers 12.1.6.7 Validating NMI Handlers 12.1.6.8 Lessons (Re)Learned 从下一节开始将针对总结发现的内容，重新设计数据结构和接口。

12.1.6.9 Simplicity Avoids Formal Verification 12.1.6.10 State Variables for Simplified Dynticks Interface 12.1.6.11 Entering and Leaving Dynticks-Idle Mode 12.1.6.12 NMIs From Dynticks-Idle Mode 12.1.6.13 Interrupts From Dynticks-Idle Mode 12.1.6.14 Checking For Dynticks Quiescent States 12.1.6.15 Discussion

12.2 Special-Purpose State-Space Search

此部分的内容更详细的内容见作者在LWN中发布的文章。 PPCMEM工具，它由剑桥大学的Peter Sewell和Susmit Sarkar，INRIA 的Luc Maranget、Francesco Zappa Nardelli和Pankaj Pawan，牛津大学的Jade Alglave与IBM的Derek Williams合作完成。
这个组将Power、ARM、ARM及C/C＋＋11标准的内存模型进行了形式化，并基于Power和ARM形式设计了PPCMEM工具(ppcmem在线测试工具)。

小问题12.22：但是x86是强序的。为什么你需要将它的内存模式形式化？

实际上，学术界认为x86内存模型是弱序的，因为它允许将存储和随后的加载进行重排。从学术的观点来看，一个强序内存模型绝不允许任何重排，这样所有的线程都将对它看到的所有操作顺序达成完全一致。

12.2.1 Anatomy of a Litmus Test

这里举了个powerpc下的汇编例子。

PPC SB+lwsync-RMW-lwsync+isync-simple
""
{
0:r2=x; 0:r3=2; 0:r4=y;   0:r10=0 ; 0:r11=0; 0:r12=z ;
1:r2=y; 1:r4=x;
}
 P0                 | P1           ;
 li r1,1            | li r1,1      ;
 stw r1,0(r2)       | stw r1,0(r2) ;
 lwsync             | sync         ;
                    | lwz r3,0(r4) ;
 lwarx  r11,r10,r12 | ;
 stwcx. r11,r10,r12 | ;
 bne Fail1          | ;
 isync              | ;
 lwz r3,0(r4)       | ;
 Fail1:             | ;

exists
(0:r3=0 /\ 1:r3=0)

12.2.2 What Does This Litmus Test Mean?

其对应的c语言如下所述：

// 初始化r3
int r3 = 2;
void P0(void)
{
    int r3;
    x = 1; /* Lines 8 and 9 */
    /* int atomic_add_return (int i, atomic_t * v); 
     * 注意到以下的用法和内核中的对应接口不符。
     */
    atomic_add_return(&z, 0); /* Lines 10-15 */
    r3 = y; /* Line 16 */
}
void P1(void)
{
    int r3;

    y = 1; /* Lines 8-9 */
    smp_mb(); /* Line 10 */
    r3 = x; /* Line 11 */
}

12.2.3 Running a Test

调试界面如下图：

可以单步调试各个线程，也可以点击Auto跑全状态空间。
也可以直接搭建环境在本地服务器跑全状态空间测试，源码在此处下载。

12.2.4 PPCMEM Discussion

仍然存在以下局限性：

这些工具不构成IBM或者ARM在其CPU架构上的官方声明。
这些工具仅仅处理字长度的访问（32位），并且要访问的字必须正确对齐。而且，工具不处理ARM内存屏障的某些更弱的变种，也不处理算法。
这些工具对于复杂数据结构来说，做得不是太好

12.3 Axiomatic Approaches

使用PPCMEM做IRIW测试，大大提高了调试的效率。

但是仍然使用了14个小时。
其中，许多跟踪事件彼此之间是类似的。这表明将类似跟踪事件作为一个事件进行对待，这种方法可能提高性能。一种这样的方法是Alglave等人的公理证明方法[ATM14]，它创建一组表示内存模型的公理集，然后将Litmus测试转换为可以证明或者反驳这些公理的定理。得到的工具称为“herd”，方便的采用PPCMEM相同的Litmus测试作为输入，包括图12.28所示的IRIW Litmus测试。在PPCMEM需要14小时 CPU时间来处理IRIW的情况下，herd仅仅需要17ms。 12.3.1 Axiomatic Approaches and Locking 12.3.2 Axiomatic Approaches and RCU

12.4 SAT Solvers

任何具有有限循环和递归的有限程序，都可以被转换为逻辑表达式，这可以将程序的断言以其输入来表示。对于这样的逻辑表达式，非常有趣的是，知道任何可能的输入组合是否能够导致某个断言被触发。如果输入被表达为逻辑变量的组合，这就是SAT，也称为可满足性问题。
业界实例有cbmc。
如下图所示：

相比这下，需要对特殊用途的语言进行繁琐转换的传统工具(如Spin)，仅限于设计时验证。

12.5 Stateless Model Checkers

12.6 Summary

不管几十年来对形式验证的关注情况怎样，测试仍然属于大型并行软件的验证工作。
绝大多数形式验证技术仅仅能用于非常小的代码片断。
大量的相关BUG，也就是在生产中可能碰到的BUG，是通过测试找到的。