FreeRTOS 队列的 VeriFast 形式化验证：queue 谓词与核心不变量的深度解析-平芜编程栈

FreeRTOS 队列的 VeriFast 形式化验证：queue 谓词与核心不变量的深度解析

【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS

本文基于 FreeRTOS 仓库中 FreeRTOS/Test/VeriFast/queue/README.md 展开，系统讲解 FreeRTOS 内核队列数据结构在 VeriFast 分离逻辑验证器中的形式化证明方法：从Storage / N / M / W / R / K六个核心变量约定，到queue谓词与核心队列不变量的数学表述，再到这些抽象概念与 queue/ 目录下真实内核源码证明文件的一一对应关系。读完本文，你将掌握 FreeRTOS 队列的环形缓冲区抽象模型、rotate_left/take等关键引理的语义，以及如何在本地运行、复现这些无界（unbounded）正确性证明。

为什么需要形式化验证 FreeRTOS 队列

FreeRTOS 队列是任务间通信、信号量与互斥量的底层基础结构，其环形缓冲区实现涉及指针运算、临界区、任务阻塞/唤醒等多个并发敏感环节，是内核中最容易出错、也最值得严格论证的模块之一。仓库在 FreeRTOS/Test/VeriFast/README.md 中明确说明：队列证明的目标是在任意数量任务或 ISR的前提下，证明队列实现满足三个性质：

内存安全（memory safe）：不访问无效内存；
线程安全（thread safe）：对共享状态的访问被正确同步；
功能正确（functionally correct）：行为符合队列语义。

这些性质通过 VeriFast，证明调用关系图见 FreeRTOS/Test/VeriFast/docs/callgraph.png（绿色为已证明函数，蓝色为以锁不变量建模的函数，灰色为假定桩）。

队列证明中的核心变量约定

原文档 FreeRTOS/Test/VeriFast/queue/README.md 首先定义了队列谓词与证明中统一使用的六个变量名，它们是理解整个证明体系的地基：

变量	含义	约束
`Storage`	队列的具体存储区，共`N*M`字节	`buffer`谓词将存储区视为`N`个元素的列表`contents`，每个元素`M`字节
`N`	队列长度（队列最多可存放的元素个数）	`0 < N`
`M`	每个元素的大小（字节数）	`0 < M`（队列用作互斥量时`M == 0`，见`freertos_mutex`谓词）
`W`	写指针`pcWriteTo`的逻辑索引，满足`pcWriteTo == Storage + W * M`	`0 <= W <= N-1`
`R`	读指针`pcReadFrom`的逻辑索引，满足`pcReadFrom == Storage + R * M`	`0 <= R <= N-1`
`K`	队列中当前元素个数，对应`uxMessagesWaiting`	`0 <= K <= N`

这些约束在 include/proof/queue.h 的queue谓词定义中逐条体现（0 < N &*& 0 < M &*& 0 <= W &*& W < N &*& 0 <= R &*& R < N &*& 0 <= K &*& K <= N）。QUEUE_SHAPE宏则把谓词与真实的Queue_t结构体字段（pcHead、pcWriteTo、u.xQueue.pcTail、u.xQueue.pcReadFrom、uxItemSize、uxLength、uxMessagesWaiting、cRxLock、cTxLock等）逐一对齐，保证抽象层与具体内存布局的一致性。

queue 谓词与核心队列不变量

原文档的核心是queue谓词：它把具体的队列存储区与一个抽象的K项列表abs关联起来。更精确地说，关键队列不变量为：

abs == take(K, rotate_left((R+1)%N, contents)) &*& W == (R + 1 + K) % N

其中：

(R+1)%N是队列的队首（front）位置：因为读指针pcReadFrom指向"上一次读出元素的位置"，真正的下一个待读元素在R的下一格；
W是队列的队尾（back）位置，即下一个写入位置；
rotate_left处理环形存储区的回绕（wraparound）：存储区是线性数组，但队列逻辑上是环形的，需通过左旋把以队首为起点的物理序列规整为逻辑序列；
take取出列表的前K个元素，表示队列当前实际包含的内容。

公式W == (R + 1 + K) % N则把三个整数状态量绑定在一起：队尾逻辑索引等于"队首逻辑索引 + 当前元素个数"对N取模，这正对应环形队列"队尾 = 队首 + 已占用槽位数"的直觉，同时利用取模天然覆盖了写指针绕回起点（pcWriteTo越过pcTail后回指pcHead）的情况。

abs与真实存储contents之间的桥梁是buffer谓词，其定义（include/proof/queue.h）将一个N*M字节的扁平字符数组递归地解释为N个M字节元素组成的列表：

predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) = N == 0 ? elements == nil : chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs);

queue.h 中同时提供了配套引理buffer_length、buffer_from_chars、append_buffer、split_element、join_element，分别用于：推导元素个数、把malloc后的未初始化字节转为buffer、拼接相邻缓冲、拆分出第i个元素以便对其做memcpy后重新拼接。后者是证明队列读写内存安全的关键手法——后面会看到它在prvCopyDataToQueue/prvCopyDataFromQueue中的实际应用。

围绕不变量的辅助谓词：出队特例与互斥量特例

queue_after_prvCopyDataFromQueue：出队中间态

prvCopyDataFromQueue只负责把队首元素拷贝到用户缓冲区，并不递减uxMessagesWaiting（即K）。因此拷贝完成后、调用方递减K之前的瞬间，queue谓词暂时不成立。queue.h 为此专门定义了中间谓词queue_after_prvCopyDataFromQueue，其不变量与queue仅有两处差异：

W == (R + K) % N //< 与 queue 谓词不同 abs == take(K, rotate_left(R, contents)) //< 与 queue 谓词不同

当调用方（如xQueueReceive）随后执行uxMessagesWaiting--并借助deq_lemma重新闭合谓词时，队列又恢复到标准不变量形态（读索引前进为(R+1)%N，抽象列表变为tail(abs)）。这种"谓词针对函数粒度的切分"正是分离逻辑模块化验证的典型做法。

freertos_mutex：`M == 0`的互斥量特例

当队列被用作互斥量时uxItemSize == 0，存储区不再存放数据，queue.h 中的freertos_mutex谓词用QUEUE_SHAPE(q, Storage, N, 0, K)、WPtr == Storage、RPtr == Storage、End == Storage、malloc_block(Storage, 0)等约束刻画这一退化形态。xQueueGenericReset的后置条件中即出现0 == M ? freertos_mutex(...) : queue(...)的分支，说明该谓词覆盖了队列语义与互斥量语义的切换。

并发建模：queuehandle / queuesuspend / queuelock 与幽灵锁

真实内核中队列的并发安全依赖关中断（critical section）、挂起调度器（vTaskSuspendAll）与队列锁（cRxLock/cTxLock）三层机制。VeriFast 无法建模真实中断/调度器，因此 queue.h 在Queue_t中引入了三个幽灵（ghost）互斥量字段来模拟其原子性保证：

irqMask：模拟关中断效果，其不变量irqs_masked_invariant保证持锁者能访问核心队列资源；任务可同时访问queuelists，而 ISR 仅在队列未锁定时才能访问事件列表；
schedulerSuspend：模拟调度器挂起，其不变量scheduler_suspended_invariant内部持有locked互斥量；
locked：模拟队列锁，其不变量queue_locked_invariant持有queuelists。

对应的共享谓词为：

queuehandle(q, N, M, is_isr)：任务与 ISR 均可持有的队列句柄权限（is_isr区分调用方）；
queuesuspend(q)：任务间共享的"调度器挂起"权限；
queuelock(q)：任务独占的"队列锁"权限。

setInterruptMask/clearInterruptMask（任务侧）与setInterruptMaskFromISR/clearInterruptMaskFromISR（ISR 侧）则把taskENTER_CRITICAL/portSET_INTERRUPT_MASK_FROM_ISR等宏映射为对这些幽灵互斥量的 acquire/release。这套分层建模使得xQueueGenericSend、xQueueReceive的规约（contract）可以精确表达"先进入临界区，必要时挂起调度器并加队列锁、将任务挂到事件列表"的完整控制流。

证明与实现的对应：从谓词看真实队列代码

创建与重置：create.c

xQueueGenericCreate的前置条件要求0 < uxQueueLength、0 < uxItemSize、uxQueueLength * uxItemSize <= UINT_MAX（对应源码中的乘法/加法溢出检查），后置条件给出queue(result, _, uxQueueLength, uxItemSize, 0, uxQueueLength-1, 0, false, nil)，即创建后W == 0、R == N-1、K == 0——这与xQueueGenericReset将pcWriteTo置为pcHead、将pcReadFrom置为pcHead + (uxLength-1)*uxItemSize的实现完全吻合：空队列时队首逻辑索引为(R+1)%N == 0，与写指针一致。该文件还用queue_init1、queue_init2两个局部谓词封装初始化中间状态，并在文件头注明简化假设：不验证并发环境下的初始化，假定初始化（含 reset）先于所有并发 send/receive 发生（对应VERIFAST宏下将taskENTER_CRITICAL定义为空）。

入队路径：prvCopyDataToQueue.c 与 xQueueGenericSend.c

prvCopyDataToQueue的三种拷贝位置对应三种后置条件：

queueSEND_TO_BACK（尾插）：queue(q, Storage, N, M, (W+1)%N, R, K+1, is_locked, append(abs, singleton(x)))——写索引前进，抽象列表在尾部追加新元素；
queueSEND_TO_FRONT（头插）：写索引W不变，读索引回退为R == 0 ? N-1 : R-1，抽象列表变为cons(x, abs)——与pcReadFrom -= uxItemSize、越过pcHead后回绕到pcTail - uxItemSize的实现对应；
queueOVERWRITE（覆盖，仅N == 1合法）：queue(q, Storage, N, M, W, R, 1, is_locked, singleton(x))——元素个数恒为 1，列表退化为单元素。

证明内部先以split_element把buffer拆成"前缀 + 待写槽位 + 后缀"，memcpy之后用join_element拼回，从而严格论证写入不越界；随后调用enq_lemma/front_enq_lemma维持抽象列表不变量。上层 xQueueGenericSend.c 的规约使用[1/2]queuehandle与[1/2]queuesuspend的分片权限表达"队列可被多任务/ISR 共享"，主循环不变式逐行跟踪xTicksToWait超时、队列满时vTaskPlaceOnEventList挂起、以及prvLockQueue/prvUnlockQueue加解锁的完整流程。

出队路径：prvCopyDataFromQueue.c 与 xQueueReceive.c

prvCopyDataFromQueue要求0 < K（队列非空），后置为queue_after_prvCopyDataFromQueue(...)与chars(pvBuffer, M, head(abs))——即拷贝出的正是队首元素。其内部通过split_element定位(R+1)%N槽位完成memcpy。上层 xQueueReceive.c 的规约精确刻画了两种结局：成功时chars(pvBuffer, M, _)且队列元素数减一（W == (R+1+K)%N不变量经由deq_lemma重新确立）；队列空且超时则返回errQUEUE_EMPTY且缓冲区保持原值chars(pvBuffer, M, x)。

ISR 路径：xQueueGenericSendFromISR.c

ISR 版入队以is_isr == true调用queuehandle，通过portSET_INTERRUPT_MASK_FROM_ISR/portCLEAR_INTERRUPT_MASK_FROM_ISR建模临界区，并且不阻塞：队列满时直接返回errQUEUE_FULL。值得注意的细节是，若队列被锁定（cTxLock != queueUNLOCKED），ISR 不直接操作事件列表，而是递增cTxLock计数（带configASSERT(cTxLock != queueINT8_MAX)防溢出），把唤醒工作推迟到解锁时——这正是cTxLock字段在真实内核中的语义，也被完整纳入了证明。

如何运行与复现队列证明

仓库提供了完整的验证工具链说明（FreeRTOS/Test/VeriFast/README.md）与自动化脚本（Makefile）。前提是安装 VeriFast（CI 中使用 VeriFast 19.12），并准备make与perl。

单文件命令行验证（需先cd到FreeRTOS/Test/VeriFast目录）：

$ /path/to/verifast -I include -c queue/xQueueGenericSend.c

成功时输出形如0 errors found (335 statements verified)。-I include指向公共谓词目录，-c表示编译检查模式。

需要关闭算术溢出检查的文件（加-disable_overflow_check）：queue/create.c、queue/prvCopyDataToQueue.c、queue/xQueueGenericSendFromISR.c、queue/xQueueReceiveFromISR.c。

VeriFast IDE（vfide）交互验证：

$ /path/to/vfide -I include queue/xQueueGenericSend.c

点击Verify与Verify Program（或按 F5），成功时顶部横幅变绿并显示已验证语句数。

全量回归（同时执行语句覆盖率回归，NO_COVERAGE=1可临时关闭覆盖率检查）：

$ VERIFAST=/path/to/verifast make

Makefile 中每个证明文件都锚定了预期覆盖率数值，例如xQueueGenericSend.c期望335条语句、xQueueReceive.c期望337、create.c期望315、xQueuePeek.c期望335；列表证明目录list/下uxListRemove.c期望440、vListInsert.c期望456。这使覆盖率回归成为证明内容被无意识修改时的早期告警。

标注负担统计（queue 证明约每行源码 0.3～2 行注解，list 证明最高达 7 倍）：

$ VERIFAST=/path/to/verifast ./scripts/annotation_overhead.sh

简化假设与验证边界

从 create.c 文件头注释与 queue.h 源码可以明确看到，当前证明是有意识做出简化后的结果，主要包括：

不验证并发环境下的队列初始化：假定 reset 与初始化先于所有并发收发发生（VERIFAST下taskENTER_CRITICAL定义为空）；
不验证configUSE_QUEUE_SETS配置分支：xQueueGenericSend与xQueueGenericSendFromISR中该宏下的队列集逻辑被显式标注"VeriFast: we do not verify this configuration option"；
互斥量分支不可达：prvCopyDataToQueue中uxItemSize == 0分支直接assert false，因为队列（非互斥量）场景元素大小恒大于零；
verifast环境用malloc/free替身pvPortMalloc/vPortFree，用简化结构体替换联合体（fake_union_t），并在验证版中去掉pxIndex、xListEnd等与证明无关的列表内部字段。

这些假设保证了证明的可机械检查性（机器可验证、可复现），同时也划清了结论的适用范围——它严格证明的是"在既定简化模型下，任意长度队列在任意数量任务/ISR 并发访问时内存安全、线程安全且行为符合队列语义"，而非对内核全部配置组合的穷举保证。

FreeRTOS 队列的 VeriFast 形式化验证：queue 谓词与核心不变量的深度解析