一句话：为约束自动机编译器提出并证明两项数据约束处理优化，提升生成代码性能。
约束自动机（CA）是一种基于无限字有限自动机的协调模型，近年来被用于将协调器编译为可执行代码，从而实现构造即正确。CA 的每个迁移由数据约束标注，该约束以一阶公式描述被协调进程间的原子数据流；生成代码必须在运行时高效处理这些约束。本文面向 CA 编译器提出并证明两项数据约束优化：一是消除冗余变量的归约，二是将声明式数据约束翻译为小顺序语言中的命令式数据命令。作者给出正确性证明，并通过实验表明这些优化能正面影响生成可执行代码的性能。
Constraint automata (CA) constitute a coordination model based on finite automata on infinite words. Originally introduced for modeling of coordinators, an interesting new application of CAs is implementing coordinators (i.e., compiling CAs into executable code). Such an approach guarantees correctness-by-construction and can even yield code that outperforms hand-crafted code. The extent to which these two potential advantages materialize depends on the smartness of CA-compilers and the existence of proofs of their correctness. Every transition in a CA is labeled by a "data constraint" that specifies an atomic data-flow between coordinated processes as a first-order formula. At run-time, compiler-generated code must handle data constraints as efficiently as possible. In this paper, we present, and prove the correctness of two optimization techniques for CA-compilers related to handling of data constraints: a reduction to eliminate redundant variables and a translation from (declarative) data constraints to (imperative) data commands expressed in a small sequential language. Through experiments, we show that these optimization techniques can have a positive impact on performance of generated executable code.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{JongmansA16,
title = {Data optimizations for constraint automata},
author = {Sung-Shik T. Q. Jongmans and Farhad Arbab},
journal = {Logical Methods in Computer Science},
volume = {Volume 12, Issue 3},
year = {2017},
doi = {10.2168/lmcs-12(3:11)2016}
}