Fencing off go: liveness and safety for channel-based programming
Fencing off go: liveness and safety for channel-based programming
复制标题
隔离 go：基于频道的节目的活跃度和安全性
DOI：
10.1145/3009837.3009847
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
N. Yoshida
中科院分区：
文献类型：
--
作者：
J. Lange;Nicholas Ng;Bernardo Toninho;N. Yoshida
GO是一种生产级别的静态典型编程语言，其设计具有明确的消息响起的原始图和轻量级线程，从而使（和鼓励）程序员可以开发并发系统，在这些系统中，组件通过通信与基于锁定的共享内存相关性更大的相互作用。 GO只能在运行时检测到全球僵局，但没有针对所有太常见的沟通不匹配或部分僵局提供编译时间保护。这项工作为GO计划中的有限的耐受性和安全性开发了一个静态验证框架，能够在一般一般的同时发生程序中检测通信错误和部分死锁，包括那些具有动态渠道创建和无限递归的程序。我们的方法从GO计划中反射出忠实地表示其沟通模式为行为类型。通过检查对通道使用情况的句法限制（称为围栏），我们确保程序由有限的许多不同的通信模式组成，这些模式可能会无限多次重复。这种限制使我们能够实施有限的验证程序（类似于有限的模型检查），以检查类型的livesice和安全性，而类型又近似于GO计划中的livesice和安全性。我们已经在工具链中实施了一种类型的推理，耐受性和安全检查，并针对公开可用的GO程序进行了测试。 2017年2月27日更新。请参阅评论。
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can only detect global deadlocks at runtime, but provides no compile-time protection against all too common communication mismatches or partial deadlocks. This work develops a static verification framework for bounded liveness and safety in Go programs, able to detect communication errors and partial deadlocks in a general class of realistic concurrent programs, including those with dynamic channel creation and infinite recursion. Our approach infers from a Go program a faithful representation of its communication patterns as a behavioural type. By checking a syntactic restriction on channel usage, dubbed fencing, we ensure that programs are made up of finitely many different communication patterns that may be repeated infinitely many times. This restriction allows us to implement bounded verification procedures (akin to bounded model checking) to check for liveness and safety in types which in turn approximates liveness and safety in Go programs. We have implemented a type inference and liveness and safety checks in a tool-chain and tested it against publicly available Go programs. Updated on 27th Feb 2017. See Comments.