Quantitative Synthesis for Concurrent Programs
Quantitative Synthesis for Concurrent Programs
复制标题
并发程序的定量合成
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Rohit Singh
中科院分区：
文献类型：
--
作者：
Pavol Cerný;K. Chatterjee;T. Henzinger;Arjun Radhakrishna;Rohit Singh
我们提出了一种算法方法，用于定量，性能感知的并发程序合成。输入由一个非确定的部分程序和参数性能模型组成。非确定性允许程序员省略（如果有）在特定程序位置使用（如果有）同步结构。指定为加权自动机的性能模型可以通过为诸如锁定，上下文切换以及内存和缓存访问的操作分配不同的成本来捕获系统体系结构。定量综合问题是自动解决部分程序的非确定性，以确保正确性和性能是最佳的。作为共享记忆并发的标准，正确性是正式化的“免费规格”，尤其是种族自由或僵局自由。对于最坏情况（平均案例）性能，我们表明可以将问题简化为具有定量目标的2个玩家图形游戏（具有概率过渡）。尽管我们使用游戏理论方法表明综合问题是NEXP完整的，但我们提出了一种算法方法和一种实现，该方法可有效地适用于同时发生的程序和实际兴趣的绩效模型。我们已经实施了一个原型工具，并将其用于合成具有不同编程模式的有限状态并发程序，用于代表不同架构的几种性能模型。
We present an algorithmic method for the quantitative, performance-aware synthesis of concurrent programs. The input consists of a nondeterministic partial program and of a parametric performance model. The nondeterminism allows the programmer to omit which (if any) synchronization construct is used at a particular program location. The performance model, specified as a weighted automaton, can capture system architectures by assigning different costs to actions such as locking, context switching, and memory and cache accesses. The quantitative synthesis problem is to automatically resolve the nondeterminism of the partial program so that both correctness is guaranteed and performance is optimal. As is standard for shared memory concurrency, correctness is formalized "specification free", in particular as race freedom or deadlock freedom. For worst-case (average-case) performance, we show that the problem can be reduced to 2-player graph games (with probabilistic transitions) with quantitative objectives. While we show, using game-theoretic methods, that the synthesis problem is Nexp-complete, we present an algorithmic method and an implementation that works efficiently for concurrent programs and performance models of practical interest. We have implemented a prototype tool and used it to synthesize finite-state concurrent programs that exhibit different programming patterns, for several performance models representing different architectures.