Swapping Evaluation:一种存储器可扩展的按需布线解决方案
Swapping Evaluation: A Memory-Scalable Solution for Answer-On-Demand Tabling
摘要:
基于暂停的表格评估的各种方法之间的差异之一是调度策略。两种最流行的策略是本地评估和批量评估。前者收集表列谓词的所有解,然后使其中任何一个解在表列计算之外可用。后者在计算所有答案之前逐个返回答案,原则上,如果只需要一个答案(或答案的子集),这会更好。批处理求值更接近于SLD求值,因为它在需要时会延迟计算解决方案,但它可能需要比本地求值更多的内存,这能够更快地回收内存。一些实际上可以在本地策略下执行的程序在批处理评估下很快就会耗尽内存。这导致普遍采用当地评价,而牺牲了更深入的分批战略。在本文中,我们研究的原因,高内存消耗的批量评估,并提出了一种新的调度策略,我们称之为交换评估。交换求值也会在完成表格调用之前逐个返回答案,但其内存使用量可能比批处理求值少几个数量级。在XSB系统中的实验实现表明,交换评估是一个可行的内存可扩展的策略,不需要妥协的执行速度。
英文摘要:
One of the differences among the various approaches to suspension-based tabled evaluation is the scheduling strategy. The two most popular strategies are local and batched evaluation. The former collects all the solutions to a tabled predicate before making any one of them available outside the tabled computation. The latter returns answers one by one before computing them all, which in principle is better if only one answer (or a subset of the answers) is desired. Batched evaluation is closer to SLD evaluation in that it computes solutions lazily as they are demanded, but it may need arbitrarily more memory than local evaluation, which is able to reclaim memory sooner. Some programs which in practice can be executed under the local strategy quickly run out of memory under batched evaluation. This has led to the general adoption of local evaluation at the expense of the more depth-first batched strategy. In this paper we study the reasons for the high memory consumption of batched evaluation and propose a new scheduling strategy which we have termed swapping evaluation. Swapping evaluation also returns answers one by one before completing a tabled call, but its memory usage can be orders of magnitude less than batched evaluation. An experimental implementation in the XSB system shows that swapping evaluation is a feasible memory-scalable strategy that need not compromise execution speed.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。