We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures.

翻译：我们提出可行性逻辑与实现逻辑两种程序逻辑，共同解决语义引导综合中的解搜索问题。其新颖之处在于采用急切处理方式，不仅分析单个候选程序，而是对整个程序集合进行推理。可行性逻辑以前向方式计算候选程序集合的语义信息，实现逻辑则利用这些信息通过后向方式识别合适的候选程序。通过引入追踪综合替代方案的新型断言，可行性逻辑能够分析程序集合。随后，实现逻辑通过选择替代方案构造最终程序，我们保证该过程无需回溯。本文展示了如何利用验证条件实现这两种程序逻辑，并在无锁数据结构的安全内存回收原型系统中进行了实验验证。