Rust 基金会公告《扩展 Rust 形式验证生态系统：欢迎 ESBMC》

Rust 基金会正式将基于 SMT 的模型检查器 ESBMC 通过 Goto-Transcoder 接入 Rust 标准库验证流水线，标志着 Rust 形式化验证生态再添利器。

1. 成果

   • ESBMC 已并入 Verify Rust std 官方工具链，CI 流程已运行。
   • 该成果在 AWS 赞助的标准库验证竞赛中胜出，获现金奖励。

2. 技术路线

   • Goto-Transcoder（博士研究项目）充当桥梁，把 Rust MIR → Goto 程序 → ESBMC，实现无缝验证。
   • 验证流程：Kani 做前端翻译 → ESBMC 做 bounded model checking → SMT 求解 → 生成反例。

3. 意义与后续

   • 为 Rust 标准库提供额外的形式化安全保障；
   • 团队正扩展 ESBMC 对更多“合约”构造的支持，并计划使其成为 Kani 的可选后端；
   • 同时探索用形式化方法验证 C → Rust 自动翻译 的正确性。

阅读：https://rustfoundation.org/media/expanding-the-rust-formal-verification-ecosystem-welcoming-esbmc/

文章《Rust 内存分析》

作者在为 Forest Filecoin 节点排查内存问题的过程中，总结了一套“实战向” Rust 内存分析工具箱，重点放在“如何快速定位大内存占用”而非理论。

1. 背景与误区

   • Filecoin 节点动辄几十 GiB，必须精确到“每一 GiB 去哪了”。
   • Rust 只能防“忘了 free”这类泄漏，防不住“无限增长的数据结构”——最常见元凶是无界缓存。

2. 前置准备

   • 新建 profiling profile：opt-level = 1 + debug = true，保留符号又不太慢。
     • 用 feature flag 切换全局分配器（System / jemalloc / mimalloc），方便不同工具需求。

3. 工具地图（按实战体验排序）

   • heaptrack
     ‑ 零成本启动：heaptrack ./bin，GUI 直观。
     ‑ 缺点：自身内存开销极大，大程序直接 OOM，作者多次“重启救机”。
   • gperftools + pprof
     ‑ 链接 tcmalloc，运行时定期 dump 1 MiB heap profile；几乎零额外内存。
     ‑ 用 Google 的 pprof -http 图形化查看，可在线分析生产进程。
     ‑ 注意：环境变量非 UTF-8 会导致崩溃，需 HEAPPROFILE_USE_PID=t。
   • dhat-rs
     ‑ 代码里插 #[global_allocator] static ALLOC: dhat::Alloc = dhat::Alloc;，即可在 CI 中写断言“峰值 ≤ 10 MiB”。
     ‑ 适合“局部代码段”或回归测试，速度慢，不宜全程序常驻。
   • Valgrind-massif
     ‑ 作者未跑通（Forest 直接卡死），给出 Makefile 模板供读者自取。
   • 其他待试
     bytehound、mimalloc 旧版、mmap 追踪脚本、Tracy、eBPF 系列。

4. 容易遗漏的“隐形内存”
   • 内存映射文件（RocksDB、MMAP 缓存）不会出现在上述 profiler，需配合 /proc/<pid>/smaps 或自写脚本查看。

5. 预防大于救火
   • 所有缓存一律用 LRU 或有界通道；用 get-size2 监控实际字节数。
   • 禁用 flume::unbounded 之类无界通道（Clippy disallowed-methods）。
   • 大对象用 Arc<Box<T>> 或链表节点减少拷贝与预留浪费。

阅读：https://rumcajs.dev/posts/memory-analysis-in-rust/

Reddit：https://www.reddit.com/r/rust/comments/1mpezl0/memory_analysis_in_rust/

Nanomp3：一个无标准、无分配、纯 Rust MP3 解码器

基于 minimp3 的 c2rust 翻译的纯 Rust MP3 解码库。

仓库：https://github.com/robbie01/nanomp3

Reddit：https://www.reddit.com/r/rust/comments/1mpjxbv/nanomp3_a_no_std_no_alloc_pure_rust_mp3_decoder/

讨论：超越 ? —— Rust 为何需要 try 来实现可组合效果

作为一名曾经不喜欢 try 关键字的程序员，我想分享我个人实现其巨大价值的经历——尤其是在处理多种效果时。

TL;DR：

• 如果异步作为一种效果由 monad（ Future ）和关键字（ async ）建模，那么我们应该给予其他两个效果，迭代和易错性相同的处理，以提高语言设计的一致性。
• 效果被组合起来并且对它们进行建模的 monad 是分层的时，手动转换它们将具有难以置信的挑战性，并且同时使用多个效果关键字来对付它们会很有帮助。

Reddit：https://www.reddit.com/r/rust/comments/1mpv0fi/beyond_why_rust_needs_try_for_composable_effects/

评论区指出 Without Boats 的文章 《The registers of Rust》（2023）

--

From 日报小组 苦瓜小仔

社区学习交流平台订阅：

• Rustcc论坛: 支持rss
• 微信公众号：Rust语言中文社区