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.

翻译：我们展示了一个名为 TASE 的工具的设计和实施,该工具使用交易记忆来降低符号执行应用程序的延迟性,其数量小于象征性状态。执行路径在使用具体值时是本地执行的,只有在执行遇到象征性值(或模拟函数)时,才暂停当地执行,并开始解释。当不再遇到符号值时,执行将返回到原模式。TASE 设计中的关键创新是一种技术,用于摊还成本,用以检查值是否象征值高于少数指示,以及使用硬件支持的交易记忆(TSX)来实施本地执行,在检测到符号值(可能较晚)时不会产生效果。我们表明, TASE 有可能大幅改进对符号执行的某些耐久性敏感的应用,例如验证客户在客户服务器应用程序中的行为的方法。