Scheduling Complexity of Interleaving Search

TL;DR

This paper investigates the scheduling complexity of interleaving search in miniKanren, introducing a semi-automatic symbolic execution method to estimate its impact on program performance.

Contribution

It presents a novel technique to analyze scheduling effects in interleaving search, addressing the challenge of reasoning about complexity in such logic programs.

Findings

Scheduling significantly affects performance in interleaving search.

The proposed method effectively estimates scheduling impact.

Analysis applies to a broad class of miniKanren programs.

Abstract

miniKanren is a lightweight embedded language for logic and relational programming. Many of its useful features come from a distinctive search strategy, called interleaving search. However, with interleaving search conventional ways of reasoning about the complexity and performance of logical programs become irrelevant. We identify an important key component -- scheduling -- which makes the reasoning for miniKanren so different, and present a semi-automatic technique to estimate the scheduling impact via symbolic execution for a reasonably wide class of programs.