首页> 外文会议>38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages 2011 >Safe Nondeterminism in a Deterministic-by-Default Parallel Language
【24h】

Safe Nondeterminism in a Deterministic-by-Default Parallel Language

机译:默认确定性并行语言中的安全非确定性

获取原文
获取原文并翻译 | 示例

摘要

A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for non-deterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supports nondeterministic computations with a deterministic-by-default guarantee: nondeterminism must be explicitly requested via special parallel constructs (marked nd), and any deterministic construct that does not execute any nd construct has deterministic input-output behavior. Moreover, deterministic parallel constructs are always equivalent to a sequential composition of their constituent tasks, even if they enclose, or are enclosed by, nd constructs. Finally, in the execution of nd constructs, interference may occur only between pairs of accesses guarded by atomic statements, so there are no data races, either between atomic statements and unguarded accesses (strong isolation) or between pairs of unguarded accesses (stronger than strong isolation alone). We enforce the guarantees at compile time with modular checking using novel extensions to a previously described effect system. Our effect system extensions also enable the compiler to remove unnecessary transactional synchronization. We provide a static semantics, dynamic semantics, and a complete proof of soundness for the language, both with and without the barrier removal feature. An experimental evaluation shows that our language can achieve good scalability for realistic parallel algorithms, and that the barrier removal techniques provide significant performance gains.
机译:具有强安全性保证的许多确定性并行编程模型正在兴起,但是对非确定性算法(例如分支和边界搜索)的类似支持仍然是一个悬而未决的问题。我们提供一种语言以及类型和效果系统,以支持默认确定性保证的非确定性计算:必须通过特殊的并行构造(标记为nd)显式请求非确定性,并且不执行任何nd构造的任何确定性构造都必须具有确定性的输入输出行为。此外,确定性并行构造始终等同于其组成任务的顺序组成,即使它们将nd构造包围或由nd构造包围。最后,在执行nd构造时,干扰仅可能发生在由原子语句保护的访问对之间,因此在原子语句与无保护的访问之间(强隔离)或在无保护的访问对之间(强于强)都不会发生数据竞争。隔离)。我们在编译时通过模块化检查来强制执行保证,这些检查使用了对前述效果系统的新颖扩展。我们的效果系统扩展还使编译器可以删除不必要的事务同步。无论有没有障碍消除功能,我们都为该语言提供了静态语义,动态语义以及完整的语言证明。实验评估表明,对于实际的并行算法,我们的语言可以实现良好的可伸缩性,并且障碍消除技术可显着提高性能。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号