基于多线程并行的符号执行引擎设计与实现

周彭; 左志强

doi:10.7544/issn1000-1239.202220920

基于多线程并行的符号执行引擎设计与实现

周彭^{1, 2},
左志强^{1, 2, ,}

1.
南京大学计算机科学与技术系　南京　210023
2.
计算机软件新技术国家重点实验室（南京大学）　南京　210023

基金项目: 国家自然科学基金项目（62272217）

详细信息

作者简介:
周彭: 2000年生. 硕士研究生. 主要研究方向为系统软件，符号执行

左志强: 1986年生. 博士，副教授. CCF高级会员. 主要研究领域为系统软件、编译技术、程序分析

通讯作者:
左志强（zqzuo@nju.edu.cn）

中图分类号: TP311
计量
- 文章访问数: 445
- HTML全文浏览量: 64
- PDF下载量: 168
出版历程
- 收稿日期: 2022-11-02
- 修回日期: 2022-12-13
- 网络出版日期: 2023-02-10
- 刊出日期: 2023-01-31

Design and Implementation of a Parallel Symbolic Execution Engine Based on Multi-Threading

Zhou Peng^{1, 2},
Zuo Zhiqiang^{1, 2, ,}

1.
Department of Computer Science and Technology, Nanjing University, Nanjing 210023
2.
National Key Laboratory for Novel Software Technology (Nanjing University), Nanjing 210023

Funds: This work was supported by the National Natural Science Foundation of China (62272217).

摘要

摘要:
符号执行作为一种高效的测试生成技术，被广泛应用于软件测试、安全分析等领域. 然而，由于程序中的执行路径数量随着分支数量的增加而指数级上升，符号执行往往无法在大规模程序上进行高效执行，缺乏可扩展性. 已有的基于多进程的并行化方法具有较大的额外通信开销，并且缺乏对现有约束求解优化技术的利用. 提出了基于多线程并行处理模型的符号执行加速方法. 具体来讲，为解决并行符号执行中的不同工作节点负载不平衡问题，设计了不需要中间节点参与的工作窃取算法. 为充分利用现有约束求解优化技术，提出了让不同工作节点共享约束求解信息的加速求解方法. 基于符号执行引擎（KLEE）实现了多线程并行化符号执行方案，从而形成多线程并行化符号执行引擎（PKLEE）. 实验验证表明，在穷尽执行路径场景下，KLEE平均耗时是在给定8个线程下PKLEE的3~4倍；在同样的时间内，PKLEE执行的有效工作负载平均是KLEE的3倍.
- 符号执行 /
- 负载均衡 /
- 约束求解 /
- 并行加速 /
- 可扩展性
Abstract:
Symbolic execution, as an effective test generation technique, has been increasingly used for software testing and vulnerability discovery, etc. However, the number of execution paths in a program rises exponentially with the number of branches, and symbolic execution can hardly be performed efficiently on large-scale programs, leading to poor scalability. Considering that multi-processed parallel symbolic execution approaches not only suffer from high communication overhead, but also fail to use the existing constraint solving optimization techniqnes. To tackle the above problems, we devise a novel work-stealing algorithm that requires no centralized nodes. In addition, to exploit the existing constraint solving optimizations, we enable different worker nodes to share the constraint solving information so as to accelerate the solving process. Based on the above mechanisms, we implement our parallel engine PKLEE (parallel KLEE) on the top of KLEE and conduct the experimental evaluations on it. In the exhaustive execution path scenario, the average time consumed by KLEE is three to four times longer than that of PKLEE with 8 threads available, and the effective workload executed by PKLEE is on average three times higher than that of KLEE in the same period of time.
- symbolic execution /
- load balance /
- constraint solving /
- parallel acceleration /
- scalability

HTML全文

场景流（scene flow, SF）是定义在2个连续场景中表面点的3D运动场，是一个感知动态场景的基本工具.随着自动驾驶、人机交互等应用的大规模商业落地，感知系统需要精确感知环境中的动态运动物体^[1-2]，因此精确估计场景流成为近年来的研究热点.由LiDAR等3D传感器直接获得的点云数据可以得到场景中点的精确位置信息，因此点云数据被广泛应用于场景流估计任务中.点云数据仅包含3D点坐标，因此在稀疏点、边缘点处会出现特征信息不足的现象，在这些点上的匹配会更加困难，这些匹配困难点严重影响场景流估计的整体准确度.

近几年的方法都是关注2个连续点云间对应的匹配关系来优化场景流的估计精度，FlowNet3D^[3]在单尺度上获取匹配关系；HPLFlowNet^[4]使用双边卷积层（bilateral convolutional layer, BCL），在多个尺度上联合计算匹配关系^[5]；PointPWC-Net^[6]在多个尺度上建立用于匹配的代价体（cost volume, CV）和重投影（warping）模块.但这些方法仅考虑了点云间的匹配关系，缺少优化匹配困难点的方式. 如图1(a)所示，图片中的点为场景的一部分，其中红色代表该点的端点误差（end point error, EPE）小于0.05 m；绿色代表该点的端点误差大于等于0.05 m且小于0.3 m；蓝色代表该点的端点误差大于等于0.3 m.在图1(a)虚线框中，PointPWC-Net在一个局部邻域内（一个汽车整体）同时有匹配准确的红色点和匹配困难的蓝色点.本文提出的基于邻域一致性的点云场景流传播更新方法（neighborhood consistency propagation update method，NCPUM）方法根据点云相邻点的相关性，即属于源点云的场景流在足够小的邻域内很大程度上存在一致性，将局部邻域中的准确场景流传播到匹配困难点上.可以有效地减少匹配困难点场景流的误差，提升整体准确度.图1(b)为经过NCPUM方法优化后的效果，可以看到在虚线框内的汽车点和匹配困难的蓝色点消失，匹配较差的绿色点明显减少，匹配准确的红色点明显增多.

图 1 2种方法的可视化对比

Figure 1. Visual comparison of the two methods

下载: 全尺寸图片幻灯片

具体来说，NCPUM假设利用点云内相邻点的相关性使场景流估计具有邻域一致性，通过置信度图传播更新提升整体场景流估计的准确度.基于该假设，NCPUM设计了置信度预测模块和场景流传播模块，对骨干网络输出的初始场景流预测置信度图，经过场景流传播模块在具有一致性的邻域内将场景流从高置信度点集向低置信度点集传播，改善邻域内匹配困难点的准确度.本文的贡献有2方面：

1）根据场景流的邻域一致性设计了场景流传播优化方法NCPUM.该方法使用场景流在局部邻域内传播的方式，改善估计效果.NCPUM的评估结果优于之前的工作，证明了该方法的有效性.

2）NCPUM在Flyingthings3D和KITTI数据集上的测试结果在准确度上达到国际先进水平，并更换不同的骨干网络进行了测试，验证了NCPUM对于不同的骨干网络都能明显提升其估计准确度.

1. 相关工作

1.1 场景流估计

在Vedula等人^[7]工作中，定义和介绍了场景流的概念，之后许多工作^[8-12]在多种类型的数据集上进行场景流的估计，随着最近几年基于点云的深度学习方法^[13-15]的发展，可以在点云上直接估计场景流.其中一个使用可学习的深度网络来估计点云上的场景流的方法是FlowNet3D^[3]，它将下采样的特征进行嵌入，得到点云间的运动信息，通过上采样方法回归得到对应点的场景流.FlowNet3D只在单一尺度上进行了特征的嵌入，单一尺度的感受野无法在大尺度和小尺度运动上同时获得精确的估计结果. HPLFlowNet^[4]使用双边卷积在多个尺度上联合计算匹配度，但限于内存使用限制无法在上采样过程中细化场景流.而PointPWC-Net^[6]遵循了光流估计的“由粗到细”（coarse to fine, CTF）的范式，在多个尺度的局部范围内使用PointConv^[13]建立用于匹配的代价体和重投影的模块.FLOT^[16]通过最优传输（optimal transport），优化源点云和目标点云的匹配关系.这些关注于匹配关系的方法得到了很好的场景流估计结果.HALFlow^[17]使用注意力机制，嵌入更多的位置信息，获得更准确的场景流估计结果.

文献[3−4,6,13,16−17]都是通过匹配连续点云间的特征回归出对应源点云的场景流，在匹配困难点处没有额外的优化措施.本文方法在源点云中根据相邻点的相关性，在邻域内改善匹配困难点的场景流，获得优于匹配方法的估计准确度.

1.2 邻域一致性

之前的场景流估计工作中都会注重在邻域内提取特征，根据提取到的特征来进行连续点云间的匹配^{[3-4,6,17-19]}，回归出点云间的场景流.但这只是在提取的特征上包含了邻域信息，在邻域特征信息不足的点上会出现匹配困难的情况.在同样使用邻域信息进行匹配的任务中^[20-21]，LiteFlowNet3^[20]根据局部光流一致性，在代价体上对邻域内的点进行优化，获得了相对于匹配方法更好的光流估计精度.受该想法的启发，我们合理假设在2个连续场景中，一个合适的邻域内的点共享相同的运动模式，因此在邻域内的场景流具有一致性.NCPUM根据初始场景流显式的估计置信度，在邻域内的高置信度点向低置信度点进行传播更新.与现有方法不同的是，NCPUM的更新操作是在场景流上而非在特征上，所依赖的也不是特征上的相关或者相似，而是点云邻域内场景流的一致性.

2. 传播优化方法

NCPUM从场景流邻域一致性假设出发，构建了一种对场景流在邻域内传播更新的优化方法.具体网络框架如图2所示，分别构建置信度预测模块和场景流传播模块实现NCPUM优化方法.首先是估计初始场景流的骨干网络，在得到初始场景流以及对应特征之后，送入置信度预测模块；然后在置信度预测模块中使用编码器-解码器（encoder-decoder）的网络结构，对输入的场景流进行置信度图的预测，置信度图用来表示各个场景流估计是否准确；最后在场景流传播模块中，根据预测得到的置信度图将场景流从高置信度点集向低置信度点集传播，更新低置信度点的场景流，降低匹配困难点对准确度的影响.

图 2 网络结构图

Figure 2. Network structure

下载: 全尺寸图片幻灯片

2.1 问题定义

场景流估计任务的最终目标是估计2个连续点云之间的运动矢量，因此定义2个连续的3D点云场景：源点云 $P=\left\{{\boldsymbol{x}}_{i}\right|i=\mathrm{1,2},…,{n}_{1}\}$ ，和目标点云 $Q=\left\{{\boldsymbol{y}}_{j}\right| j= \mathrm{1,2},…,{n}_{2}\}$ ，其中 ${\boldsymbol{x}}_{i},{\boldsymbol{y}}_{i}\in {\mathbb{R}}^{3}$ ，并且 $i$ 并不必须与 $j$ 相等.源点云 $P$ 中的点运动到目标点云 $Q$ 中的对应点的运动矢量场为 ${{F}}=({\boldsymbol{f}}_1 … {\boldsymbol{f}}_{n_1})$ ，该运动矢量场即为最终估计的场景流.估计的场景流是基于源点云 $P$ 的，因此场景流与源点云中的点一一对应.

2.2. 估计初始场景流

在估计初始场景流时，使用的是PointPWC-Net作为骨干网络，该方法使用2个连续的点云作为输入，使用特征金字塔的结构，在每个分辨率尺度上都进行一次源点云 $P$ 到目标点云 $Q$ 的重投影，之后进行匹配度代价体的计算，代价体定义了逐点的匹配程度，PointPWC-Net对代价体进行回归得到逐点的场景流.

在PointPWC-Net中，构建了4个尺度的特征金字塔，在得到4个尺度的点特征后，场景流的估计会从较粗的尺度进行，遵循由粗到细的规范.估计了当前尺度的场景流后，会上采样到更精细的尺度，将上采样的场景流对源点云进行重投影，在当前尺度上对重投影后的点云和对目标点云估计一个相对于上一个尺度场景流的残差，以完成对估计场景流的精细化.将整个重投影过程进行公式化定义：

${{{P}}}_{\mathrm{w}}=\{{\boldsymbol{p}}_{\mathrm{w},i}={\boldsymbol{p}}_{i}+{\boldsymbol{f}}_{i}|{\boldsymbol{p}}_{i}\in P,{\boldsymbol{f}}_{i}\in {F}^{\mathrm{u}\mathrm{p}}{\}}_{i=1}^{{n}_{1}},$

(1)

其中 $P$ 为源点云， ${P}_{\mathrm{w}}$ 为重投影后的点云， ${F}^{\mathrm{u}\mathrm{p}}$ 为从上一个尺度上采样的场景流.

在PointPWC-Net中，对2个点云以及对应的特征进行了代价体的构建. 假设 ${\boldsymbol{g}}_{i}\in {\mathbb{R}}^{C}$ 是对应目标点云点 ${\boldsymbol{p}}_{i}\in P$ 的特征， ${\boldsymbol{h}}_{j}\in {\mathbb{R}}^{C}$ 是对应目标点云点 ${\boldsymbol{q}}_{i}\in Q$ 的特征，那么对应2个点之间的匹配度定义为：

$Cost({\boldsymbol{p}}_{i},{\boldsymbol{q}}_{j})=M\left(concat\right({\boldsymbol{g}}_{i},{\boldsymbol{h}}_{j},{\boldsymbol{q}}_{j}-{\boldsymbol{p}}_{i}\left)\right),$

(2)

使用多层感知机（multilayer perceptron） $M$ 将2点之间的潜在关系和点与点之间的距离串联后进行学习.在有了点对点的匹配度之后，将其组成当前尺度的代价体，PointPWC-Net根据源点云点到目标点云邻域点的距离对代价体加权，即对于1个源点云的点 ${\boldsymbol{p}}_{i}\in P$ ，得到它在目标点云 $Q$ 上的1个邻域 ${N}_{Q}\left({\boldsymbol{p}}_{i}\right)$ ，再根据目标点云邻域中的每个点到源点云点的距离得到权重C.

$C=\displaystyle \sum _{{\boldsymbol{q}}_{j}\in {N}_{Q}\left({\boldsymbol{p}}_{i}\right)}{W}_{Q}({\boldsymbol{q}}_{j},{\boldsymbol{p}}_{i})Cost({\boldsymbol{q}}_{j},{\boldsymbol{p}}_{i}),$

(3)

${W}_{Q}({\boldsymbol{q}}_{j},{\boldsymbol{p}}_{i})=M({\boldsymbol{q}}_{j}-{\boldsymbol{p}}_{i}).$

(4)

使用PointPWC-Net估计初始场景流时，沿用了多尺度监督损失，对应估计得到4个尺度的场景流，对场景流真实值采样到同样的尺度，在对应的尺度上做不同权重 $\alpha$ 的2范数监督.

${Loss}_{\mathrm{s}\mathrm{f}}=\displaystyle \sum _{l={l}_{0}}^{L}{\alpha }_{l}\displaystyle \sum _{\boldsymbol{p}\in P}\left|\right|{{\boldsymbol{F}}}^{l}\left({\boldsymbol{p}}\right)-{{\boldsymbol{F}}}_{\boldsymbol{GT}}^{l}\left(\boldsymbol{p}\right)|{|}_{2}.$

(5)

2.3. 场景流置信度预测模块

在骨干网络输出初始场景流后，会经过置信度预测模块对初始场景流预测置信度图.该置信度定义为初始场景流相对于真实值的误差，即预测的误差值越小，表示该点在骨干网络中估计的初始场景流越准确，置信度值越高.置信度预测模块首先使用“编码器−解码器”的构造，以初始场景流的3D矢量信息作为输入，在编码器过程中进行点的下采样，可以扩大置信度预测模块的感受野，参考更多的相邻场景流推断置信度；然后在解码器的上采样过程中使用跳跃链接，串联编码过程中对应尺度的特征信息，为上采样提供更多精细尺度的特征，获得更精细的上采样结果，并且考虑骨干网络中输出的场景流特征；最后使用sigmoid函数输出1个（0-1）分布的置信度图，并将该置信度图用于之后的场景流传播模块中.

置信度预测模块使用的是有监督的训练方式，监督信息是初始场景流与场景流真实值的2范数二值化得到的先验分布图，该分布图为初始场景流相对于真实值的先验误差分布.设定阈值 $\theta$ ，当初始场景流与真实值的2范数小于 $\theta$ 时，设定为0，否则设定为1.由此得到的分布图为场景流先验的二分类分布图，用来监督置信度预测模块的输出.

${\boldsymbol{GT}}_{{\rm{conf}}}=\left\{\begin{aligned} &0, |{\boldsymbol{F}}-{{\boldsymbol{GT}}}_{{\rm{sf}}}| <\theta ,\\ &1,|{\boldsymbol{F}}-{{\boldsymbol{GT}}}_{{\rm{sf}}}| \geqslant \theta , \end{aligned}\right.$

(6)

$\begin{aligned} {Loss}_{\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{f}}=\;&-({{\boldsymbol{GT}}}_{\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{f}}\times \mathrm{ln}\;confmap+\\ &(1-{{\boldsymbol{GT}}}_{\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{f}})\times \mathrm{ln}\left(1-confmap\right)),\end{aligned}$

(7)

其中 $confmap$ 是置信度预测模块得到的置信图. ${{\boldsymbol{GT}}}_{\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{f}}$ 是场景流先验分布图，在式（6）中由初始场景流F和真实值 ${{\boldsymbol{GT}}}_{\mathrm{sf}}$ 处理得到.估计置信度图的最后一层使用sigmoid函数将其转换为0~1之间的分布，因此就可以使用二分类交叉熵（binary cross entropy, BCE）进行监督.

2.4. 场景流传播模块

经过场景流置信度图的预测，根据场景流置信度得到源点云中的高置信度点集和低置信度点集，由高置信度点集向低置信度点集进行限制半径的传播；根据邻域一致性的假设，如果高置信度点与低置信度点的传播半径不大于传播半径阈值，可以认为两点的场景流拥有一致性，可以使用高置信度点的场景流更新低置信度点的场景流.

${\boldsymbol{p}}_{2}=KNN\left({\boldsymbol{p}}_{1}\right),\quad {\boldsymbol{p}}_{1},{\boldsymbol{p}}_{2}\in P,$

(8)

${\boldsymbol{p}}_{1}$ 和 ${\boldsymbol{p}}_{2}$ 都属于源点云 $P$ ，因为邻域一致性依赖于点云内相邻点的相关性，所以距离最近的点最有可能存在场景流的邻域一致性，式 $\left(8\right)$ 中 $KNN$ 为K最近邻（K-nearest neighbor）方法采样低置信度点 ${\boldsymbol{p}}_{1}$ 在源点云的最近点.

$f\left({\boldsymbol{p}}_{1}\right)=f\left({\boldsymbol{p}}_{2}\right), \quad {\rm{if}}({\boldsymbol{p}}_{1}-{\boldsymbol{p}}_{2}) < \beta ,$

(9)

其中 ${\boldsymbol{p}}_{1}$ 和 ${\boldsymbol{p}}_{2}$ 分别为低置信度点和高置信度点， $\beta$ 为传播半径阈值，当两点的距离不大于传播半径时传播更新低置信度点的场景流. 这里传播半径阈值非常重要，点云中的相邻点只有空间距离在一定阈值内才会具有相关性，在点密度足够的情况下，对于小邻域内的点的场景流具有一致性，这个邻域的半径阈值设置不同的数值会影响到优化结果.

NCPUM在优化初始场景流时，会将反传的梯度在初始场景流处截断，即训练置信度预测模块时不会影响到骨干网络PointPWC-Net.

3. 实验与结果分析

与之前的工作的训练过程^{[4, 6, 16]}类似，NCPUM在合成数据集Flyingthings3D^[22]上训练模型，然后在Flyingthings3D和真实场景数据集KITTI^[23]两个数据集上进行测试，将测试结果与其他方法的结果在表1中进行对比.之所以使用这样的训练策略是因为很难在真实场景中确定出来一个场景流真实值，这里使用的KITTI数据集只有142个场景，而合成数据集有更大的数据量可供训练，如Flyingthings3D数据集有19640对点云可以进行训练.在训练之前，遵循HPLFlowNet和PointPWC-Net的方式对数据进行了预处理，点云场景中没有被遮挡的点.

表 1 NCPUM与其他方法的对比

Table 1. Comparison of NCPUM and Other Methods

数据集	方法	EPE/m	Acc3DS/%	Acc3DR/%	Outlier3D/%
Flyingthings3D	FlowNet3D^[3]	0.114	41.3	77.0	60.2
	HPLFlowNet^[4]	0.080	61.4	85.5	42.9
	PointPWC-Net^[6]	0.059	73.8	92.8	34.2
	FLOT^[16]	0.052	73.2	92.7	35.7
	HALFlow^[17]	0.049	78.5	94.7	30.8
	NCPUM	0.060	76.1	93.9	30.7
KITTI	FlowNet3D^[3]	0.177	37.4	66.8	52.7
	HPLFlowNet^[4]	0.117	47.8	77.8	41.0
	PointPWC-Net^[6]	0.069	72.8	88.8	26.5
	FLOT^[16]	0.056	75.5	90.8	24.2
	HALFlow^[17]	0.062	76.5	90.3	24.9
	NCPUM	0.070	78.1	91.5	22.3
注：黑体数字表示最优结果.

下载: 导出CSV

| 显示表格

在接下来的内容中，将介绍NCPUM实现的细节，然后将测试结果与之前的方法进行对比，证明了NCPUM的有效性.并且我们认为Flyingthings3D数据集与KITTI数据集差异较大，将NCPUM在KITTI数据集前100对数据上进行微调，在后42对数据上进行了测试，更换不同骨干网络微调的测试结果在表3中展示，证明NCPUM基于邻域一致性假设的传播更新方法更适用于真实场景，并进行了消融实验，对传播半径阈值进行更多的对比实验.

表 3 在KITTI数据集上微调测试

Table 3. Fine Tuning and Testing on KITTI Dataset

骨干网络	方法	EPE/m	Acc3DS/%	Acc3DR/%	Outlier3D/%
FlowNet3D^[3]	w/o ft	0.173	27.6	60.9	64.9
	w ft	0.102	33.6	70.3	44.9
	NCPUM	0.094	38.6	74.1	37.1
PointPWC-Net^[6]	w/o ft	0.069	72.8	88.8	26.5
	w ft	0.045	82.7	95.1	25.3
	NCPUM	0.043	87.5	96.9	24.3
FLOT^[16]	w/o ft	0.056	75.5	90.8	24.2
	w ft	0.029	89.4	96.8	18.0
	NCPUM	0.028	89.9	97.0	17.5
注：黑体数字表示最优结果；w/o表示with/without；ft表示fine-funing.

下载: 导出CSV

| 显示表格

3.1 网络实现细节

NCPUM的训练设置与骨干网络PointPWC-Net相同，对输入的点云采样到8192个点，为其构建4层的特征金字塔，每一层的损失权重α设置为α₀ = 0.02，α₁ = 0.04，α₂ = 0.08，α₃ = 0.16，训练时的初始学习率设置为0.001，训练800个周期，每80个周期学习率减少一半.在对KITTI进行微调时，参数设置与NCPUM设置一致，只是将训练周期减少为400个，并且学习率每40个周期减少一半.

置信度预测模块设置了3个尺度，分别为2048，512，256个点，特征通道数都为64.在经过3次下采样的特征提取之后得到了3个尺度的场景流特征，再经过3次上采样将特征传播到原尺度.前2个尺度的上采样都同时考虑了前一尺度的特征和下采样时对应的特征；后1个尺度的上采样考虑原尺度的场景流，在上采样到原尺度之后，与骨干网络输出的场景流特征串联在一起，经过2个1D卷积，再经过sigmoid得到0～1分布的置信度.

3.2 评价标准

本文沿用了场景流估计任务一直以来的评价标准^{[3-4, 6,18]}，假设 $\boldsymbol{F}$ 代表场景流估值， ${\boldsymbol{F}}_{{\boldsymbol{GT}}}$ 代表场景流真实值，各个评价标准的定义为：

1）EPE3D. $\left|\right|{\boldsymbol{F}}-{{\boldsymbol{F}}}_{{\boldsymbol{GT}}}|{|}_{2}$ 表示点云上的逐点误差平均值.

2）Acc3DS. $EPE3D < 0.05\;\mathrm{m}$ 或者相对误差 $< 5\%$ 的点占比.

3）Acc3DR. $EPE3D < 0.1\;\mathrm{m}$ 或者相对误差 $< 10\%$ 的点占比.

4）utlier3D. $EPE3D > 0.3\;\mathrm{m}$ 或者相对误差 $> 10\%$ 的点占比.

3.3 在Flyingthings3D上的训练和测试

Flyingthings3D可用于训练的数据集共有19640对点云，可用于测试的数据集有3824对点云.与FlowNet3D、 PointPWC-Net模型方法的设置相同，本文只使用深度小于35 m的点，大部分的前景物体都能包含在这个范围内.对每个点云采样得到8192个点用于训练和测试，训练设置参数在3.1节网络实现细节中进行了介绍.

表1展示了在Flyingthings3D数据集上NCPUM在2个准确度指标和离群值占比指标上均优于骨干网络PointPWC-Net.尤其是Acc3DS指标，对比PointPWC-Net有2.3%的提升.但在EPE指标上略低于PointPWC-Net.其原因是在场景流传播模块中会使低置信度点的场景流与高置信度点的场景流相等，对于估计偏差大的点，会传播更新一个准确的场景流，对于估计误差小的低置信度点，传播更新操作反而带来了精度上的扰动.但是准确度是统计EPE3D < 0.05 m或者相对误差< 5%的点占比，所以我们的方法能够优化估计偏差大的匹配困难点，提升准确度.本文在表2中整理出更新点的统计信息(图2中 $\hat{{\boldsymbol{F}}}$ 与F的比较），其中包含更新点占全部点的比例（更新点占比）、更新点中精度提升的占比（改进点占比）、更新点中精度下降的占比（扰动点占比）、精度提升的平均值（改进均值）、精度下降的平均值（扰动均值）.可以看到，有一半以上的点其实是产生了扰动，并且产生扰动的均值大于改进的均值，因此在精度上NCPUM确实会产生一定的扰动，但是在准确度指标和离群值占比指标上有大幅提升.

表 2 Flyingthings3D数据集更新点统计信息

Table 2. Statistical Information of Update Points on Flyingthings3D Dataset

方法	更新点占比/%	改进点占比/%	扰动点占比/%	改进均值/m	扰动均值/m	EPE/m	Acc3DS/%	Acc3DR/%	Outlier3D/%
PointPWC-Net						0.059	73.8	92.8	34.2
NCPUM	9.73	46.98	53.02	0.003	0.004	0.060	76.1	93.9	30.7
注：黑体数字表示最优结果.

下载: 导出CSV

| 显示表格

3.4 在KITTI上测试和微调

KITTI Scene Flow 2015数据集包括200个训练场景和200个测试场景，遵循之前工作的方法，在具有真实值并且可用的142对点云数据集上进行测试，并且与之前的方法保持一致^[4,6]，删除了点云中高度小于0.3 m的地面点.在KITTI数据集上，先使用在Flyingthings3D数据集上训练的模型直接对KITTI数据集进行测试而不经过任何微调，以评估NCPUM的泛化能力.从表1中可以看到NCPUM在Acc3DS和Acc3DR评价指标上优于PointPWC-Net，在Acc3DS指标上有5.3%的提升，在Acc3DR指标上有2.7%的提升，提升幅度大于Flyingthings3D数据集，表现出优秀的泛化性能.不经过微调而在真实数据集上表现更加优秀的原因在于真实数据集KITTI的点云数据物体之间的距离大于Flyingthings3D数据集中物体之间的距离，NCPUM的邻域一致性假设更适用于这种数据特性，所以NCPUM在真实场景上会有更加优秀的表现.本文统计了表1中FLOT和NCPUM的场景流估计时间，FLOT在一秒钟内可以处理2.15对连续点云，而NCPUM在一秒钟内可以处理5.09对连续点云，NCPUM处理速度约是FLOT的2.37倍.在真实使用场景中，准确场景流在总体场景流中的占比比场景流的绝对平均误差值更有意义，拥有更多的准确场景流代表该方法为真实应用带来更好的稳定性.NCPUM在Acc3DS和Acc3DR准确度指标上都有可观的提升，尤其在真实数据集上的场景流Acc3DS指标超过PointPwc的Acc3DS指标7.28%，超过HALFlow的Acc3DS最佳结果2.09%，对比之前的方法，NCPUM的处理速度和准确度表现出更大的应用潜力.

因为Flyingthings3D数据集和KITTI数据集存在较大的差异，直接使用在Flyingthings3D数据集上预训练的模型在KITTI数据集上测试并不能完全展示NCPUM在KITTI数据集上的性能.所以本文将KITTI数据集拆分，使用前100对场景微调NCPUM，并在剩余的42对场景上进行测试.分别将FlowNet3D，PointPWC-Net, FLOT 3种骨干网络在KITTI数据集上进行微调，然后进行NCPUM的微调，将微调后的3种骨干网络做对比.在微调之后，3种骨干网络的NCPUM可以获得更好的效果，如表3所示，微调后的NCPUM对比微调后对应的骨干网络，在4个评价标准上都有提升，与泛化能力测试结果不同的是，NCPUM在EPE指标上也有了一定的提升，我们认为，Flyingthings3D是虚拟数据集，场景中物体间的距离较小，对某一物体边缘的低置信度点传播更新，可能采样到距离较近的其他物体上的准确点，而不是同一物体中距离较远的准确点，例如图3所示，绿色点为更新场景流的低置信度点，红色的点是传播场景流的高置信度点，黄色的连线为传播更新关系.在图3（a）和图3（b）中都出现了采样到其他物体的现象；KITTI是真实数据集，物体之间的距离较大，如图3（c）所示，不容易出现采样错误的情况，只有在如图3（d）中的远端离群点上可能出现采样不准确的情况，因此KITTI相较于Flyingthings3D数据集更容易符合邻域一致性的假设.

图 3 Flyingthings3D与KITTI替换细节对比

Figure 3. Comparison of Flyingthings3D and KITTI on replacement details

下载: 全尺寸图片幻灯片

3.5 传播半径阈值设置的影响

因为NCPUM是基于邻域一致性假设进行构建的，因此传播半径阈值设置十分重要，不同的半径阈值设置带来的效果是不一样的，甚至不合适的半径阈值会降低NCPUM优化效果.当半径阈值设置过大时，高置信度点的场景流会传播到不具有一致性的低置信度点上，出现扰动；当半径设置过小时，只会有少部分低置信度点会被更新.数据集的不同也会影响到传播半径的设置，对比虚拟数据集，真实数据集因为物体间的距离更大，更容易设置一个合适的传播半径进行传播，这也是NCPUM泛化到真实数据集表现更好的原因.表4对2个数据集上设置的不同传播半径进行对比，NCPUM在Flyingthings3D数据集上的半径设置为0.4时达到最好效果，而在KITTI数据集上的半径设置为3.0时达到最好效果.这个数据的差异表现出在真实场景上对传播的约束更加小，传播更新可以影响到更多的点，从而带来更好的改进效果.

表 4 NCPUM在不同半径阈值下的测试

Table 4. NCPUM Tested with Different Radius Threshold

数据集	半径阈值	EPE/m	Acc3DS/%	Acc3DR/%	Outlier3D/%
Flyingthings3D	1.0	0.062	75.2	93.5	31.7
	0.4	0.060	76.1	93.9	30.7
	0.2	0.060	76.0	93.8	30.7
KITTI	5.0	0.054	85.8	95.9	24.1
	3.0	0.043	87.5	96.9	24.3
	1.0	0.043	85.0	95.4	25.5
注：黑体数字表示最优结果.

下载: 导出CSV

| 显示表格

3.6 在不同骨干网络上测试

为了证明NCPUM方法的泛化性能，本文尝试在不同的骨干网络上进行优化.我们分别以FlowNet3D，PointPWC-Net，FLOT为骨干网络构建使用置信度预测模块和场景流传播模块，在KITTI数据集上进行微调和使用NCPUM优化方法改进.测试结果如表3所示，在对FlowNet3D, PointPWC-Net,FLOT方法使用NCPUM优化方法后，4个指标上都有明显的提升，展示了NCPUM优化方法对不同骨干网络的泛化性.

在图4中可视化了NCPUM的传播更新过程，绿色点为更新场景流的低置信度点，红色点是传播场景流的高置信度点，黄色的连线为传播更新关系.可以看到KITTI数据集中具有一致性的汽车表面会出现估计不准确的绿色低置信度点，这些点更多是位于距离激光雷达更远的低密度点和邻域信息单一的边缘点上，若只关注连续点云间匹配的方法容易在这些点上出现较大的误差，NCPUM对匹配困难点寻找一个匹配准确点进行更新，和相邻的准确点保持一致，从而提高整体的估计准确度；同时传播过程要限制传播半径阈值，避免引入扰动.

图 4 替换细节可视

Figure 4. Visualization of replacemental details

下载: 全尺寸图片幻灯片

4. 结　　论

本文提出了一种根据邻域一致性的传播更新方法NCPUM来优化估计场景流的精度.该方法通过置信度预测模块对骨干网络估计出的初始场景流预测置信度图来判断场景流准确度；然后通过场景流传播模块在有限制的传播半径内从匹配困难点寻找匹配准确点，将匹配准确点的场景流传播到匹配困难点上，以提高场景流的估计精度.NCPUM在不同的数据集Flyingthings3D和KITTI上都体现出了优于之前工作的性能.并且通过在真实数据集上的微调实验和不同传播半径的实验展现出NCPUM在真实场景数据有更加优秀的表现.

作者贡献声明：郑晗负责提出模型、编写代码、实施实验过程和论文撰写；王宁负责修订和完善论文；马新柱负责数据分析和数据解释；张宏负责理论和实验设计；王智慧负责理论设计；李豪杰提供论文写作指导.

图 1 SET示意图

Figure 1. Illustration of SET

下载: 全尺寸图片幻灯片

图 2 PKLEE框架

Figure 2. PKLEE architecture

下载: 全尺寸图片幻灯片

图 3 PKLEE工作线程示意图

Figure 3. Illustration of PKLEE’s worker threads

下载: 全尺寸图片幻灯片

图 4 小规模测试程序探索完整路径耗时

Figure 4. Total time taken to explore paths exhaustively under small-scale benchmark

下载: 全尺寸图片幻灯片

图 5 大规模测试程序执行指令数量

Figure 5. Total number of executed instructions under large-scale benchmark

下载: 全尺寸图片幻灯片

表 1 小规模合成测试程序列表

Table 1 List of Small-scale Benchmark

测试程序	执行指令数量	探索路径数量
multipath_1024_kle	29733	1024
multipath_65536_klee	2687035	65536
multipath_1048576_klee	51380299	1048576
knapsack	391134	1666
mergesort	92685	720
regexp	473590	1058

下载: 导出CSV

表 2 大规模真实测试程序列表

Table 2 List of Large-scale Benchmark

测试程序	代码行数
echo	276
runcon	284
uname	380
who	819
join	1108
stty	1908

下载: 导出CSV

表 3 KLEE与PKLEE执行指令数量对比

Table 3 Comparison of the Number of Executed Instructions Between KLEE and PKLEE

测试程序	KLEE/万条	单工作线程/万条	8个工作线程/万条	加速比
echo	22178	6637	67744	3.0x
runcon	58619	17218	110904	1.9x
uname	10817	9555	51911	4.8x
who	38624	31465	146016	3.7x
join	19585	10271	54681	2.8x
stty	13412	10353	39304	2.9x

下载: 导出CSV

表 4 小规模程序上工作窃取算法的时耗

Table 4 Time Consumption of Work-stealing Algorithms Under Small-scale Benchmark s

测试程序	KLEE 耗时	8个工作线程耗时	8个工作线程耗时（无工作窃取）
multipath_1024_kle	0.31	0.45	0.46
multipath_65536_klee	9.57	3.2	6.78
multipath_1048576_klee	188.39	46.21	121.42
knapsack	277.75	69.68	246.15
mergesort	18.36	6.21	12.28
regexp	29.59	11.56	23.57

下载: 导出CSV

表 5 大规模程序上工作窃取算法对指令数量影响

Table 5 Effect of Work-stealing Algorithms on the Number of Instructions Under Large-scale Benchmark

测试程序	开启工作窃取/万条	关闭工作窃取/万条
echo	67744	64510
runcon	110904	1100630
uname	51911	49430
who	146016	144290
join	54681	54598
stty	39304	37566

下载: 导出CSV

表 6 小规模程序上共享反例缓存对命中次数的影响

Table 6 Effect of Shared Cex Cache on the Number of Hits Under Small-scale Benchmark

测试程序	开启时反例缓存未命中次数	未开启时反例缓存未命中次数	减少比例/%
multipath_1024_kle	32	78	59
multipath_65536_klee	80	122	34
multipath_1048576_klee	112	156	28
knapsack	3239	3575	10
mergesort	720	783	8
regexp	1311	2134	38

下载: 导出CSV

表 7 大规模程序上共享反例缓存对命中次数的影响

Table 7 Effect of Shared Cex Cache on the Number of Hits Under Large-scale Benchmark

测试程序	开启时反例缓存未命中次数	关闭时反例缓存未命中次数	减少比例/%
echo	981	1818	46
runcon	1454	2953	51
uname	5300	6490	18
who	2975	5953	50
join	22265	29240	23
stty	17924	19260	5

下载: 导出CSV

表 8 Ranged Analysis与PKLEE的加速比对比

Table 8 Comparison of Speedup Between Ranged Analysis and PKLEE

测试程序	PKLEE加速比	Ranged Analysis加速比
tr	4.5x	1.2x
dirname	3.5x	1.1x
factor	1.3x	1.1x
dircolors	2.7x	4.2x
pr	2.5x	4.4x
cut	5.8x	4.6x
echo	2.7x	4.3x
fold	9.8x	9.7x
chgrp	2.7x	7.7x
chown	3.0x	8.8x
readlink	3.3x	9.5x

下载: 导出CSV

参考文献(25)

[1]	Baldoni R, Coppa E, D’elia D C, et al. A survey of symbolic execution techniques[J]. ACM Computing Surveys, 2018, 51(3): 1−39
[2]	Elkarablieh B, Godefroid P, Levin M Y. Precise pointer reasoning for dynamic test generation[C] //Proc of the 18th Int Symp on Software Testing and Analysis. New York: ACM, 2009: 129−140
[3]	Cadar C, Dunbar D, Engler D R. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs[C] //Proc of the 8th USENIX Conf on Operating Systems Design and Implementation. Berkeley, CA: USENIX Association, 2008, 8: 209−224
[4]	Felmetsger V, Cavedon L, Kruegel C, et al. Toward automated detection of logic vulnerabilities in web applications[C] //Proc of the 19th USENIX Security Symp. Berkeley, CA: USENIX Association, 2010: 143−160
[5]	Bucur S, Ureche V, Zamfir C, et al. Parallel symbolic execution for automated real-world software testing[C] //Proc of the 6th Conf on Computer Systems. New York: ACM, 2011: 183−198
[6]	Lattner C, Adve V. LLVM: A compilation framework for lifelong program analysis & transformation[C] //Proc of Int Symp on Code Generation and Optimization, CGO. Los Alamitos, CA: IEEE Computer Society, 2004: 75−86
[7]	Monniaux D. A survey of satisfiability modulo theory[C] //Proc of Int Workshop on Computer Algebra in Scientific Computing. Cham, Switzerland: Springer, 2016: 401−425
[8]	Moura L, Bjørner N. Z3: An efficient SMT solver[C] //Proc of Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008: 337−340
[9]	Dong Shiyu, Olivo O, Zhang Lingming, et al. Studying the influence of standard compiler optimizations on symbolic execution[C] //Proc of 2015 IEEE 26th Int Symp on Software Reliability Engineering (ISSRE). Piscataway, NJ: IEEE, 2015: 205−215
[10]	Siddiqui J H, Khurshid S. ParSym: Parallel symbolic execution[C] //Proc of the 2010 2nd Int Conf on Software Technology and Engineering. Los Alamitos, CA: IEEE Computer Society, 2010, 1: 405−409
[11]	Staats M, Pǎsǎreanu C. Parallel symbolic execution for structural test generation[C] //Proc of the 19th Int Symp on Software Testing and Analysis. New York: ACM, 2010: 183−194
[12]	King A. Distributed parallel symbolic execution[D]. Kansas: Kansas State University, 2009
[13]	Rakadjiev E, Shimosawa T, Mine H, et al. Parallel SMT solving and concurrent symbolic execution[C] //Proc of 2015 IEEE Trustcom/BigDataSE/ISPA. Piscataway, NJ: IEEE, 2015, 3: 17−26
[14]	Singh S, Khurshid S. Parallel chopped symbolic execution[C] //Proc of Int Conf on Formal Engineering Methods. Cham, Switzerland: Springer, 2020: 107−125
[15]	Karna A K, Du Jinbo, Shen Haibo, et al. Tuning parallel symbolic execution engine for better performance[J]. Frontiers of Computer Science, 2018, 12(1): 86−100 doi: 10.1007/s11704-016-5459-9
[16]	Siddiqui J H, Khurshid S. Scaling symbolic execution using ranged analysis[J]. ACM Sigplan Notices, 2012, 47(10): 523−536 doi: 10.1145/2398857.2384654
[17]	Wei Guannan, Tan Shangyin, Bračevac O, et al. LLSC: A parallel symbolic execution compiler for LLVM IR[C] //Proc of the 29th ACM Joint Meeting on European Software Engineering Conf and Symp on the Foundations of Software Engineering. New York: ACM, 2021: 1495−1499
[18]	Bugrara S, Engler D. Redundant state detection for dynamic symbolic execution[C] //Proc of the 2013 USENIX Annual Technical Conf. Berkeley, CA: USENIX Association, 2013: 199−211
[19]	Yi Qiuping, Yang Zijiang, Guo Shengjian, et al. Postconditioned symbolic execution[C] //Proc of the 2015 IEEE 8th Int Conf on Software Testing, Verification and Validation. Piscataway, NJ: IEEE, 2015: 1−10
[20]	Jaffar J, Murali V, Navas J A, et al. TRACER: A symbolic execution tool for verification[C] //Proc of the Int Conf on Computer Aided Verification. Berlin: Springer, 2012: 758−766
[21]	Krishnamoorthy S, Hsiao M S, Lingappan L. Tackling the path explosion problem in symbolic execution-driven test generation for programs[C] //Proc of the 19th IEEE Asian Test Symp. Los Alamitos, CA: IEEE Computer Society, 2010: 59−64
[22]	Li You, Su Zhendong, Wang Linzhang, et al. Steering symbolic execution to less traveled paths[J]. ACM SigPlan Notices, 2013, 48(10): 19−32 doi: 10.1145/2544173.2509553
[23]	Wang Haijun, Liu Ting, Guan Xiaohong, et al. Dependence guided symbolic execution[J]. IEEE Transactions on Software Engineering, 2016, 43(3): 252−271
[24]	Santelices R, Harrold M J. Exploiting program dependencies for scalable multiple-path symbolic execution[C] //Proc of the 19th Int Symp on Software Testing and Analysis. New York: ACM, 2010: 195−206
[25]	Liu Jingde, Chen Zhenbang, Wang Ji. Solving cost prediction based search in symbolic execution[J]. Journal of Computer Research and Development, 2016, 53(5): 1086−1094