← 返回列表
用于验证并发程序原子性违反的方法、装置及电子设备
摘要文本
本发明提供一种用于验证并发程序原子性违反的方法、装置及电子设备，其中，该方法包括：探索当前路径，生成所述当前路径对应的当前轨迹；根据所述当前轨迹，编码所述当前轨迹的等价约束，以及编码并发程序的原子性违反约束；根据所述原子性违反约束和所述当前轨迹的等价约束，使用约束求解器进行推理，验证所述当前路径是否违反原子性；其中，所述当前轨迹的等价约束包括以下一种或多种：所述当前轨迹的读写事件的数据有效性约束；所述当前轨迹的路径条件约束；所述当前轨迹的同步约束。从而可以对并发程序中各个路径的原子性是否违反都进行验证，更全面地验证并发程序中的原子性违反。 数据由马 克 数 据整理
申请人信息
- 申请人:北京邮电大学
- 申请人地址:100876 北京市海淀区西土城路10号
- 发明人: 北京邮电大学
专利详细信息
| 项目 | 内容 |
|---|---|
| 专利名称 | 用于验证并发程序原子性违反的方法、装置及电子设备 |
| 专利类型 | 发明申请 |
| 申请号 | CN202311146304.4 |
| 申请日 | 2023/9/6 |
| 公告号 | CN117370150A |
| 公开日 | 2024/1/9 |
| IPC主分类号 | G06F11/36 |
| 权利人 | 北京邮电大学 |
| 发明人 | 易秋萍; 李壮 |
| 地址 | 北京市海淀区西土城路10号 |
专利主权项内容
1.一种用于验证并发程序原子性违反的方法，其特征在于，包括：探索当前路径，生成所述当前路径对应的当前轨迹；根据所述当前轨迹，编码所述当前轨迹的等价约束，以及编码并发程序的原子性违反约束；根据所述原子性违反约束和所述当前轨迹的等价约束，使用约束求解器进行推理，验证所述当前路径是否违反原子性；其中，所述当前轨迹的等价约束包括以下一种或多种：所述当前轨迹的读写事件的数据有效性约束；所述当前轨迹的路径条件约束；所述当前轨迹的同步约束。