线程安全的术语库
A thread-safe Term Library
摘要：
术语是计算中的基本数学概念之一。例如，每一个由上下文无关文法表征的表达式都是一个项。我们开发了一个线程安全的术语库。最大的挑战是实现超高效的多读/单写互斥，我们设计了新的繁忙禁止协议。模型检验用于证明协议和术语库的正确性。基准测试表明，与顺序版本相比，这个术语库的开销很小，并且在两个处理器上的性能已经超过了它们。在现有的状态空间生成工具中使用新的库，可以获得非常大的速度提升。
英文摘要：
Terms are one of the fundamental mathematical concepts in computing. E.g. every expression characterisable by a context free grammar is a term. We developed a thread-safe Term Library. The biggest challenge is to implement hyper-efficient multi-reader/single-writer mutual exclusion for which we designed the new busy-forbidden protocol. Model checking is used to show both the correctness of the protocol and the Term Library. Benchmarks show this Term Library has little overhead compared to sequential versions and outperforms them already on two processors. Using the new library in an existing state space generation tool, very substantial speed ups can be obtained.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
