Program Verification 04 - Separation Logic (unfinished)
# 前置知识
在阅读本文档前,请确保你已了解霍尔逻辑的相关概念,详见 Program Verification 知识板块中的 03 - Hoare Logic 文档。
# 基本概念
separation logic 是基于霍尔逻辑的扩展,在原始的 IMP 和操作语义的基础上追加了内存地址访问以及内存分配与回收的操作,可用于验证诸如野指针访问一类的程序错误。
# IMP 扩展
# 基本概念
# 形式化规则
扩展 IMP 追加了如下对命令的形式化规则,依次为内存的分配与回收、以及内存地址的读写:
# Command
c ::= ...
| id := alloc(e)
| free(e)
| id := [e]
| [e] := e
# 状态
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01