经形式化验证的用于科学测量的无锁软件事务内存
Formally Verified Lock-Free Software Transactional Memory for Scientific Measurement
浏览论文内容
中文总结 AI 辅助
针对科学测量中线程并发访问共享分层状态的问题，提出经形式化验证的无锁STM，实现原子子树操作，通过TLA+和TLC验证属性，接口支持Python脚本与AI自动化，已应用于多种实验。
中文摘要 AI 辅助
凝聚态实验的自动化测量需要仪器控制、数据采集和用户界面线程并发访问共享的天然分层状态。粗粒度锁会延迟采集并导致样品损失，而细粒度锁则需要在仪器间设置易发生死锁的锁排序。本文描述了一种无锁软件事务内存（STM），该STM已作为开源测量平台的核心长达16年，应用于核磁共振实验，以及近期的光探测磁共振实验。STM将该状态组织为树结构，提供原子子树更新和一致的子树快照。初始打包后，通过定制的无锁原子共享指针以O(1)时间获取未改变的子树快照。在每个有界TLA+配置内，TLC穷举检查状态空间，验证为该配置指定的安全性和活锁自由属性。原子共享指针实现的有界执行在C11弱内存模型下单独检查。相同的Snapshot和Transaction接口可暴露给Python脚本和AI辅助自动化。
英文摘要
Automated measurement of condensed-matter experiments requires instrument-control, data-acquisition, and user-interface threads to access shared, naturally hierarchical state concurrently. Coarse-grained locking can delay acquisition and cause sample loss, whereas fine-grained locking requires deadlock-prone lock ordering across instruments. Instead, we describe the lock-free software transactional memory (STM) that has been at the core of an open-source measurement platform for 16 years, in nuclear magnetic resonance experiments and, more recently, in optically detected magnetic resonance experiments. The STM organizes this state as a tree and provides atomic subtree updates and consistent subtree snapshots. After initial bundling, an unchanged subtree snapshot is acquired in $O(1)$ time through a custom lock-free atomic shared pointer. Within each bounded TLA+ configuration, TLC exhaustively checks the state space, establishing the safety and livelock-freedom properties specified for that configuration. Bounded executions of the atomic shared-pointer implementation are separately checked under the C11 weak-memory model. The same Snapshot and Transaction interfaces are exposed to Python scripting and AI-assisted automation.
