Kahn过程网络中基于CSP与SAT的接口协调
编程语言
2015-07-14 v4
摘要
我们提出一种基于CSP和SAT的新方法，用于协调作为闭源服务提供的分布式流连接组件的接口。Kahn过程网络（KPN）被用作形式化计算模型，并引入消息定义语言（MDL）来描述进程间通信的消息格式。MDL将节点的输入与输出接口相链接，以支持流继承与上下文化。由于接口也可通过它们之间存在的数据通道而链接，这种匹配通常不仅是部分的，而且在很大程度上是非局部的。因此KPN通信图变为一个由变量的特定实例需满足的互锁约束所构成的图。我们提出一种通过迭代近似求解CSP的算法，同时在过程中生成一个附带的布尔SAT问题。我们开发了OCaml求解器以及分析KPN顶点源代码的工具，以推导MDL项，并在CSP求解后通过将类型定义传播回顶点来自动修改代码。作为持续示例，这些技术与方法在一个实现图像处理算法的KPN上得到说明。
引用
@article{arxiv.1503.00622,
title = {Interface Reconciliation in Kahn Process Networks using CSP and SAT},
author = {Pavel Zaichenkov and Olga Tveretina and Alex Shafarenko},
journal= {arXiv preprint arXiv:1503.00622},
year = {2015}
}
备注
20 pages, 3 figures, accepted to CSPSAT 2015