自动信号布局的符号推理（扩展版）
Symbolic Reasoning for Automatic Signal Placement (Extended Version)
摘要：
线程之间的显式信号传递是并发程序中错误的一个长期原因。虽然存在若干运行时技术来在某些共享资源可用时自动通知线程，但是由于它们的运行时开销，这些技术没有被广泛采用。本文提出了一种新的解决方案，基于静态分析自动生成一个显式信号的程序，从其相应的隐式信号的实现。其关键思想是生成验证条件，使我们能够最大限度地减少所需的信号和不必要的上下文切换的数量，同时保证源程序和目标程序之间的语义等价。我们已经实现了我们的方法，在一个名为Experiment的工具，并从以前的论文和开源软件具有挑战性的基准进行评估。expresso生成的代码显著优于过去的自动信号机制（avg. 1.56倍加速），并且与手动优化的显式信号代码的性能非常接近。
英文摘要：
Explicit signaling between threads is a perennial cause of bugs in concurrent programs. While there are several run-time techniques to automatically notify threads upon the availability of some shared resource, such techniques are not widely-adopted due to their run-time overhead. This paper proposes a new solution based on static analysis for automatically generating a performant explicit-signal program from its corresponding implicit-signal implementation. The key idea is to generate verification conditions that allow us to minimize the number of required signals and unnecessary context switches, while guaranteeing semantic equivalence between the source and target programs. We have implemented our method in a tool called Expresso and evaluate it on challenging benchmarks from prior papers and open-source software. Expresso-generated code significantly outperforms past automatic signaling mechanisms (avg. 1.56x speedup) and closely matches the performance of hand-optimized explicit-signal code.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
