• 主题
高级搜索  >
历史搜索 清空历史
首页> 美国卫生研究院文献>Philosophical transactions. Series A Mathematical physical and engineering sciences >Compositional relaxed concurrency
【2h】

Compositional relaxed concurrency

机译：组合放松并发

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务，本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文，但由于OA文献来源多样且变更频繁，仍可能出现获取不到、文献不完整或与标题不符等情况，如果获取不到我们将提供退款服务。请知悉。
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

There is a broad design space for concurrent computer processors: they can be optimized for low power, low latency or high throughput. This freedom to tune each processor design to its niche has led to an increasing diversity of machines, from powerful pocketable devices to those responsible for complex and critical tasks, such as car guidance systems. Given this context, academic concurrency research sounds notes of both caution and optimism. Caution because recent work has uncovered flaws in the way we explain the subtle memory behaviour of concurrent systems: specifications have been shown to be incorrect, leading to bugs throughout the many layers of the system. And optimism because our tools and methods for verifying the correctness of concurrent code—although built above an idealized model of concurrency—are becoming more mature. This paper looks at the way we specify the memory behaviour of concurrent systems and suggests a new direction. Currently, there is a siloed approach, with each processor and programming language specified separately in an incomparable way. But this does not match the structure of our programs, which may use multiple processors and languages together. Instead we propose a compositional approach, where program components carry with them a description of the sort of concurrency they rely on, and there is a mechanism for composing these. This will support not only components written for the multiple varied processors found in a modern system but also those that use idealized models of concurrency, providing a sound footing for mature verification techniques.This article is part of the themed issue ‘Verified trustworthy software systems’.
机译：并发计算机处理器具有广阔的设计空间：可以针对低功耗，低延迟或高吞吐量进行优化。这种将每个处理器设计调整到合适位置的自由度导致机器的多样性不断增加，从功能强大的便携式设备到负责复杂而关键任务的设备（例如汽车导航系统）。在这种情况下，学术并发研究听起来既谨慎又乐观。小心，因为最近的工作发现了我们解释并发系统微妙的内存行为的方式中的缺陷：已经证明规范不正确，从而导致整个系统许多层中的错误。之所以要乐观，是因为尽管我们在并发的理想化模型之上构建了用于验证并发代码正确性的工具和方法，但它们变得越来越成熟。本文探讨了我们指定并发系统的内存行为的方式，并提出了一个新的方向。当前，存在一种孤立的方法，以无可比拟的方式分别指定每种处理器和编程语言。但这与我们的程序的结构不匹配，因为程序的结构可能一起使用多种处理器和语言。取而代之的是，我们提出一种组合方法，程序组件在其中附带对它们所依赖的并发类型的描述，并且有一种机制来构成这些并发。这不仅支持为现代系统中的多种处理器编写的组件，而且还支持使用理想的并发模型的组件，从而为成熟的验证技术提供了坚实的基础。本文是“验证的可信赖软件系统”主题主题的一部分。 。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
代理获取

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号