← 返回列表
基于C11弱内存模型的C语言程序验证方法及装置
摘要文本
本发明提供一种基于C11弱内存模型的C语言程序验证方法及装置，该方法包括：基于C语言程序当前对应的弱内存模型中强制执行的一致性公理，确定第一操作对应的顺序一致性约束、修改顺序一致性约束以及读取一致性约束；基于第一操作对应的顺序一致性约束、修改顺序一致性约束以及读取一致性约束，验证第一操作的可执行性，并得到C语言程序的验证结果。本发明提供的基于C11弱内存模型的C语言程序验证方法及装置，通过弱内存模型中的一致性约束验证程序中每个加载操作可能读取的写操作，来探索并验证并发代码的各种可能行为，从而预测并发代码的行为和错误，提高了C语言程序检测的有效性。
申请人信息
- 申请人:北京邮电大学
- 申请人地址:100876 北京市海淀区西土城路10号
- 发明人: 北京邮电大学
专利详细信息
| 项目 | 内容 |
|---|---|
| 专利名称 | 基于C11弱内存模型的C语言程序验证方法及装置 |
| 专利类型 | 发明申请 |
| 申请号 | CN202311361548.4 |
| 申请日 | 2023/10/19 |
| 公告号 | CN117667103A |
| 公开日 | 2024/3/8 |
| IPC主分类号 | G06F8/41 |
| 权利人 | 北京邮电大学 |
| 发明人 | 易秋萍; 刘胜涵 |
| 地址 | 北京市海淀区西土城路10号 |
专利主权项内容
1.一种基于C11弱内存模型的C语言程序验证方法，其特征在于，包括：基于C语言程序当前对应的弱内存模型中强制执行的一致性公理，确定第一操作对应的顺序一致性约束、修改顺序一致性约束以及读取一致性约束；基于所述第一操作对应的顺序一致性约束、修改顺序一致性约束以及读取一致性约束，验证所述第一操作的可执行性，并得到所述C语言程序的验证结果；其中，所述第一操作包括将所述C语言程序当前任一读取操作所读取的写入操作修改为另一写入操作；所述顺序一致性约束用于约束所述C语言程序中写入操作和读取操作的程序执行顺序，所述修改顺序一致性约束用于约束所述C语言程序中同一内存位置的写入操作的内存修改顺序，所述读取一致性约束用于约束所述C语言程序中不同内存位置的写入操作的内存修改顺序。 百度搜索马 克 数 据 网