Persistent Queries

TL;DR

This paper introduces a formal framework for persistent queries in interactive abstract state machines, allowing late replies to be stored and used in subsequent steps, with minimal semantic modifications.

Contribution

It defines syntax and semantics for persistent queries in abstract state machines, enabling late replies to be incorporated into the computation process.

Findings

Formal syntax and semantics for persistent queries

Minimal semantic modifications needed

Framework supports late reply handling

Abstract

We propose a syntax and semantics for interactive abstract state machines to deal with the following situation. A query is issued during a certain step, but the step ends before any reply is received. Later, a reply arrives, and later yet the algorithm makes use of this reply. By a persistent query, we mean a query for which a late reply might be used. Syntactically, our proposal involves issuing, along with a persistent query, a location where a late reply is to be stored. Semantically, it involves only a minor modification of the existing theory of interactive small-step abstract state machines.