TASE: Reducing latency of symbolic execution with transactional memory

TL;DR

TASE leverages transactional memory to dynamically switch between native and symbolic execution, significantly reducing latency in symbolic execution applications with small symbolic states.

Contribution

The paper introduces TASE, a novel approach using transactional memory to minimize symbolic execution latency by efficiently managing execution modes.

Findings

TASE reduces symbolic execution latency in latency-sensitive applications.

Transactional memory enables seamless switching between execution modes.

Potential for significant performance improvements in client-server verification tasks.

Abstract

We present the design and implementation of a tool called TASE that uses transactional memory to reduce the latency of symbolic-execution applications with small amounts of symbolic state. Execution paths are executed natively while operating on concrete values, and only when execution encounters symbolic values (or modeled functions) is native execution suspended and interpretation begun. Execution then returns to its native mode when symbolic values are no longer encountered. The key innovations in the design of TASE are a technique for amortizing the cost of checking whether values are symbolic over few instructions, and the use of hardware-supported transactional memory (TSX) to implement native execution that rolls back with no effect when use of a symbolic value is detected (perhaps belatedly). We show that TASE has the potential to dramatically improve some latency-sensitive applications of symbolic execution, such as methods to verify the behavior of a client in a client-server application.