StarMalloc：一个经过形式化验证的、并发的、高性能且面向安全的内存分配器
StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator
AI总结：
本文提出StarMalloc，一个经形式化验证的并发安全内存分配器，利用Steel框架高效验证，并开发可复用数据结构，经Firefox及10个分配器评估，性能具有竞争力。
摘要：
在这项工作中，我们提出了StarMalloc，一个经过验证的、面向安全的、并发内存分配器，可用作实际项目中的即插即用替代品。利用Steel分离逻辑框架，我们展示了如何规范和验证StarMalloc，依赖类型和模块化抽象使得验证高效进行。作为StarMalloc的一部分，我们还开发了几个通用数据结构和证明库，可直接用于未来的系统验证项目。最后，我们展示了StarMalloc可用于实际项目，包括Firefox浏览器，并针对10个最先进的内存分配器进行了评估，证明了其竞争力。
英文摘要：
In this work, we present StarMalloc, a verified, security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects. Using the Steel separation logic framework, we show how to specify and verify StarMalloc, relying on dependent types and modular abstractions to enable efficient verification. As part of StarMalloc, we also develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We finally show that StarMalloc can be used with real-world projects, including the Firefox browser, and evaluate it against 10 state-of-the-art memory allocators, demonstrating its competitiveness.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
