Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
Deterministic Concurrency: A Clock-Synchronised Shared Memory Approach
复制标题
确定性并发：时钟同步共享内存方法
DOI：
10.1007/978-3-319-89884-1_4
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Reinhard von Hanxleden
中科院分区：
文献类型：
--
作者：
Joaquín Aguado;Michael Mendler;Marc Pouzet;Partha S. Roop;Reinhard von Hanxleden
同步编程（SP）是一种提供确定性并发的通用计算原理。具有相同定时的相同输入序列总是导致相同的外部可观察的输出序列，即使内部行为在并发存储器访问的调度中产生不确定性。因此，SPanguages一直强烈地建立在数学语义，支持正式的程序分析。然而，迄今为止，通信一直被限制在一组原始的时钟同步共享存储器（csm）数据类型，如数据流寄存器，流和信号，限制了读和写访问，限制了模块化和行为抽象。本文提出了一个扩展的SP理论，它保留了确定性并发的优点，但是允许通信发生在比SP数据类型当前支持的更高的抽象级别上。我们的方法如下。为了避免数据竞争，每种类型都发布了一个策略接口，用于指定其访问方法的可接受性和优先级。thecsmtype的每个实例都必须是策略一致的，这意味着它必须在自己的策略下确定性地运行如果目标是构建使用这些类型的确定性系统，这是一个自然的要求。在一个策略构造的系统中，所有的访问方法都可以以符合策略的方式为所有类型进行调度，而不会出现死锁。在本文中，我们表明，一个政策建设性的程序表现出确定性的并发在这个意义上说，所有符合政策的交织产生相同的输入输出行为。政策是保守的，支持当前SPlan语言中存在的类型。从技术上讲，我们引入了一个使用任意策略驱动的smtype的kernelSPlanguage。一个大步不动点语义，我们证明了这种语言的确定性和终止的建设性计划。
Synchronous Programming (SP) is a universal computational principle that provides deterministic concurrency. The same input sequence with the same timing always results in the same externally observable output sequence, even if the internal behaviour generates uncertainty in the scheduling of concurrent memory accesses. Consequently,SPlanguages have always been strongly founded on mathematical semantics that support formal program analysis. So far, however, communication has been constrained to a set of primitive clock-synchronised shared memory (csm) data types, such as data-flow registers, streams and signals with restricted read and write accesses that limit modularity and behavioural abstractions.This paper proposes an extension to theSPtheory which retains the advantages of deterministic concurrency, but allows communication to occur at higher levels of abstraction than currently supported bySPdata types. Our approach is as follows. To avoid data races, eachcsmtype publishes apolicy interfacefor specifying the admissibility and precedence of its access methods. Each instance of thecsmtype has to be policy-coherent, meaning it must behave deterministically under its own policy—a natural requirement if the goal is to build deterministic systems that use these types. In a policy-constructive system, all access methods can be scheduled in a policy-conformant way for all the types without deadlocking. In this paper, we show that a policy-constructive program exhibits deterministic concurrency in the sense that all policy-conformant interleavings produce the same input-output behaviour. Policies are conservative and support thecsmtypes existing in currentSPlanguages. Technically, we introduce a kernelSPlanguage that uses arbitrary policy-drivencsmtypes. A big-step fixed-point semantics for this language is developed for which we prove determinism and termination of constructive programs.
登录
查看更多内容
影响因子：
1.1
作者：
J. Aguado;M. Mendler
通讯作者：
M. Mendler
C 语言的 SyncCharts：轻量级、确定性并发的提案
DOI：
--
发表时间：
2009
期刊：
International Conference on Embedded Software
影响因子：
--
作者：
R. V. Hanxleden
通讯作者：
R. V. Hanxleden
反应性对象：服务和电信通信领域的逻辑和技术
DOI：
--
发表时间：
1996
期刊：
影响因子：
--
作者：
F. Boussinot;G. Boumenic;Jean
通讯作者：
Jean
DOI：
--
发表时间：
2004
期刊：
ACM-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
D. Caromel;L. Henrio;Bernard P. Serpette
通讯作者：
Bernard P. Serpette
反应性对象
DOI：
--
发表时间：
2002
期刊：
Proceedings Fifth IEEE International Symposium on Object-Oriented Real-Time Distributed Computing. ISIRC 2002
影响因子：
--
作者：
J. Nordlander;Mark P. Jones;M. Carlsson;R. Kieburtz;A. Black
通讯作者：
A. Black