线程安全的项库
分布式、并行与集群计算
2022-08-15 v2
摘要
项是计算中基本的数学概念之一。例如，可由上下文无关文法刻画的每个表达式都是一个项。我们开发了一个线程安全的项库。最大的挑战是实现高效的多读者/单写者互斥，为此我们设计了新的忙碌禁止协议。模型检测被用于证明该协议和项库的正确性。基准测试表明，与顺序版本相比，该项库几乎没有额外开销，并且在两个处理器上已经优于它们。在现有的状态空间生成工具中使用新库，可以获得非常显著的加速。
引用
@article{arxiv.2111.02706,
title = {A thread-safe Term Library},
author = {J. F. Groote and M. Laveaux and P. H. M. van Spaendonck},
journal= {arXiv preprint arXiv:2111.02706},
year = {2022}
}